Commit 2025-08-20 19:33 9bac7175

View on Github →

feat: the Geck construction yields (finite-dimensional) semisimple Lie algebras (#27237) Modulo the proof that 4 is not an eigenvalue of the Cartan matrix. This will be proved later.

Estimated changes

Modified Mathlib/Algebra/Lie/Semisimple/Defs.lean

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

added theorem RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

added theorem RootPairing.GeckConstruction.apply_inr_eq_zero_of_mem_span_range_u

added theorem RootPairing.GeckConstruction.apply_sum_inl_eq_zero_of_mem_span_h

added def RootPairing.GeckConstruction.cartanSubalgebra'

added theorem RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan

modified theorem RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra

added theorem RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff

added theorem RootPairing.GeckConstruction.e_lie_u

added theorem RootPairing.GeckConstruction.e_lie_v_ne

added theorem RootPairing.GeckConstruction.e_mem_lieAlgebra

added theorem RootPairing.GeckConstruction.f_lie_v_ne

added theorem RootPairing.GeckConstruction.f_lie_v_same

added theorem RootPairing.GeckConstruction.f_mem_lieAlgebra

added def RootPairing.GeckConstruction.h'

added theorem RootPairing.GeckConstruction.h_mem_cartanSubalgebra'

added theorem RootPairing.GeckConstruction.h_mem_cartanSubalgebra

added theorem RootPairing.GeckConstruction.h_mem_lieAlgebra

added theorem RootPairing.GeckConstruction.lie_e_lie_f_apply

added theorem RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff

added theorem RootPairing.GeckConstruction.span_range_h'_eq_top

added theorem RootPairing.GeckConstruction.span_range_h_le_range_diagonal

added def RootPairing.GeckConstruction.ωConj

added def RootPairing.GeckConstruction.ωConjLieSubmodule

added theorem RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff

added theorem RootPairing.GeckConstruction.ωConj_mem_of_mem

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean

added theorem RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u