Commit 2026-08-13 09:59 6fe686bd

feat(LinearAlgebra/Matrix): add the generalized E-type Cartan matrix family (#42157) This PR adds a generalized family CartanMatrix.E n, obtained by continuing the Dynkin-diagram pattern of the exceptional matrices E₆, E₇, and E₈. For n ≥ 3, it proves the uniform determinant formula:

theorem E_det {n : ℕ} (hn : 3 ≤ n) : (E n).det = 9 - n

Public API

• CartanMatrix.E (n : ℕ) is the generalized E-type Cartan matrix.
• CartanMatrix.E_det gives its determinant for n ≥ 3.
• CartanMatrix.E_diag, CartanMatrix.E_off_diag_nonpos, CartanMatrix.E_transpose, CartanMatrix.E_isSymm, and CartanMatrix.isSimplyLaced_E hold uniformly for all n.
• CartanMatrix.E_six_eq, CartanMatrix.E_seven_eq, and CartanMatrix.E_eight_eq identify E 6, E 7, and E 8 with the usual explicit matrices.
• The fixed-size lemmas E₆_diag, E₆_off_diag_nonpos, E₆_transpose, E₆_isSymm, isSimplyLaced_E₆ and their E₇/E₈ counterparts are deprecated in favor of the uniform statements above. The generalized family is the canonical definition. The former constants CartanMatrix.E₆, CartanMatrix.E₇, and CartanMatrix.E₈ are retained as deprecated abbreviations for E 6, E 7, and E 8, and the fixed-size theorem names as deprecated aliases of the uniform statements, to preserve compatibility. The downstream definitions LieAlgebra.e₆, LieAlgebra.e₇, and LieAlgebra.e₈ in SerreConstruction.lean now use CartanMatrix.E 6, CartanMatrix.E 7, and CartanMatrix.E 8. The fixed-size determinant theorems E₆_det, E₇_det, and E₈_det are retained (they are also instances of E_det); following #42119, their proofs use norm_det after rewriting with the corresponding explicit-matrix equality lemmas.

Proof outline

Passing from E n to E (n + 1) amounts to appending a leaf to the end of the path: extendPath places the new node at Fin.last, joined by a -1 edge to the previous final node, and E_succ : E (n + 1) = extendPath (E n) holds for n ≥ 4. Row expansion along the new row (Matrix.det_succ_row) gives the recurrence

dₙ₊₂ = 2dₙ₊₁ - dₙ.

The initial values are d₃ = 6, d₄ = 5, and d₅ = 4. A two-step induction gives dₙ = 9 - n for every n ≥ 4, while n = 3 is handled by a direct computation. The auxiliary definitions describing the path extension are private, while the recurrence det_E_add_two is public.

Review changes

The definition of E uses Matrix.of, consistently with the other infinite Cartan matrix families in this file. Following review, reverseE was dropped: extendPath now appends the new node at the end of the path (via Fin.lastCases), so E_succ works directly on E, and the determinant recurrence follows from Matrix.det_succ_row. The separate definitions of E₆, E₇, and E₈ are replaced by deprecated abbreviations for E 6, E 7, and E 8. The lemmas E_six_eq, E_seven_eq, and E_eight_eq identify these canonical matrices with their usual explicit forms. Following review, the fixed-size diagonal, off-diagonal, transpose, symmetry, and simply-laced lemmas are generalized to statements uniform in n (E_diag, E_off_diag_nonpos, E_transpose, E_isSymm, isSimplyLaced_E), with the old fixed-size names kept as deprecated aliases. The branch was also merged with current master (including the Wanted mechanism of #42284 and the toolchain bump), so that CI builds against the latest mathlib.

AI usage

Codex with GPT 5.6-Sol xhigh was used to assist implementing the Lean changes, which are then meticulously reviewed and adjusted by the author to align with mathlib4 styles before pushing.