Commit 2024-09-09 08:37 eac55c09

View on Github →

feat (LinearAlgebra/RootPairing): define RootPairingCat (#16295) This PR defines a category of root pairings, roughly following the treatment of morphisms of root data in SGA3 Exp.21 Sec.6.

Estimated changes

Modified Mathlib.lean

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

deleted theorem LieAlgebra.IsKilling.rootSystem_toLin_apply

added theorem LieAlgebra.IsKilling.rootSystem_toPerfectPairing_apply

Modified Mathlib/LinearAlgebra/PerfectPairing.lean

added theorem PerfectPairing.flip_apply_apply

modified theorem PerfectPairing.flip_flip

added theorem PerfectPairing.toLin_apply

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

modified def RootPairing.pairing

added theorem RootPairing.reflection_perm_involutive

added theorem RootPairing.reflection_perm_self

added theorem RootPairing.reflection_perm_symm

modified theorem RootPairing.root_coroot_eq_pairing

added theorem RootPairing.toLin_toPerfectPairing

Created Mathlib/LinearAlgebra/RootSystem/Hom.lean

added def RootPairing.Hom.comp

added theorem RootPairing.Hom.comp_assoc

added theorem RootPairing.Hom.comp_id

added def RootPairing.Hom.id

added theorem RootPairing.Hom.id_comp

added def RootPairing.Hom.reflection

added structure RootPairing.Hom

Created Mathlib/LinearAlgebra/RootSystem/RootPairingCat.lean

added structure RootPairingCat