Commit 2025-01-24 19:43 395adf24

View on Github →

feat: define the Cartan matrix of a root pairing relative to a base (#20999) Also adding RootPairing.IsValuedIn (together with some API) since this enables us to define an integer-valued Cartan matrix for crystallographic pairings. More importantly, RootPairing.IsValuedIn is also the missing piece to generalise (and unify) some results which currently require ordered scalars such as RootPairing.coxeterWeight_mem_set_of_isCrystallographic but this work is left for a future PR (mostly to simplify review).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

Modified Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Created Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

added def RootPairing.Base.cartanMatrixIn

added theorem RootPairing.Base.cartanMatrixIn_apply_same

added theorem RootPairing.Base.cartanMatrixIn_def

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

deleted theorem RootPairing.IsCrystallographic.mem_range_algebraMap

added theorem RootPairing.IsValuedIn.trans

added theorem RootPairing.algebraMap_coxeterWeightIn

added theorem RootPairing.algebraMap_pairingIn

added def RootPairing.coxeterWeightIn

deleted theorem RootPairing.exists_int_eq_coxeterWeight

deleted theorem RootPairing.isCrystallographic_iff

added theorem RootPairing.isValuedIn_iff_mem_range

added def RootPairing.pairingIn

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean