Compute the charpoly of compounds of triangular matrices - #409
Closed
PerAlexandersson wants to merge 2 commits into
Closed
Compute the charpoly of compounds of triangular matrices#409PerAlexandersson wants to merge 2 commits into
PerAlexandersson wants to merge 2 commits into
Conversation
The triangular half of the compound eigenvalue theorem (issue #405 item 3): - `BlockTriangular.det_of_injective`, `BlockTriangular.charpoly_of_injective`: a block triangular matrix with an injective block map has determinant and characteristic polynomial given by its diagonal (generalizes `Matrix.det_of_upperTriangular` to indices without a linear order); - `compound_apply_eq_zero_of_blockTriangular`: minors of an upper triangular matrix vanish unless the row selection is pointwise dominated by the column selection (permutation expansion plus a pigeonhole step); - `powersetCode`: the binary encoding of a selection, injective via Mathlib's colex `Finset.geomSum_injective`, monotone for pointwise domination; - `blockTriangular_compound`, `compound_apply_self_of_blockTriangular`, `charpoly_compound_of_blockTriangular`: the compound of a triangular matrix is triangular for the binary encoding, with diagonal the selected products, so its charpoly is `∏_s (X - C ∏_{i ∈ s} T i i)`; - `compound_one`, `charpoly_compound_conj`: the compound charpoly is invariant under conjugation, by multiplicativity. What remains for the full eigenvalue statement is matrix-level triangularization over an algebraically closed field, which Mathlib lacks. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 21, 2026
PerAlexandersson
commented
Aug 22, 2026
OwnerAuthor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The triangular half of #405 item 3, stacked on #408.
BlockTriangular.det_of_injective/charpoly_of_injective: a blocktriangular matrix with an injective block map has determinant and charpoly
given by its diagonal —
Matrix.det_of_upperTriangularwithout a linearorder on the index type (upstreamable to
Mathlib.LinearAlgebra.Matrix.Block/
Charpoly.Basic);compound_apply_eq_zero_of_blockTriangular: minors of an upper triangularmatrix vanish unless the row selection is pointwise dominated by the column
selection (permutation expansion + pigeonhole);
powersetCode: binary encoding of a selection; injective via Mathlib's colexFinset.geomSum_injective, monotone for pointwise domination;charpoly_compound_of_blockTriangular:(compound q T).charpoly = ∏_s (X - C (∏_{i ∈ s} T i i))for triangularT;compound_one,charpoly_compound_conj: conjugation invariance of thecompound charpoly, by multiplicativity.
With these, #405 item 3 reduces to matrix-level triangularization over an
algebraically closed field (conjugate any
Ato an upper triangular matrix),which Mathlib currently lacks — that is the remaining piece, planned as a
separate
RealRooted/Mathlib/file.Sorry-free.
🤖 Generated with Claude Code