Commit 2025-04-30 15:39 6a8f7910

View on Github →

feat: generalise nondegeneracy of root pairing forms to allow coefficients in subring (#23329) This PR adds generalized versions of existing results, where the original base ring is no longer necessarily linearly ordered, but is an algebra over a LinearOrderedCommRing.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

deleted theorem RootPairing.IsValuedIn.trans

deleted theorem RootPairing.algebraMap_coxeterWeightIn

deleted theorem RootPairing.algebraMap_pairingIn

deleted theorem RootPairing.coroot'_apply_apply_mem_of_mem_span

deleted theorem RootPairing.corootSpan_dualAnnihilator_map_eq

deleted theorem RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'

deleted theorem RootPairing.corootSpan_map_toDualRight

deleted theorem RootPairing.corootSpan_mem_invtSubmodule_coreflection

deleted theorem RootPairing.corootSpan_ne_bot

deleted def RootPairing.coxeterWeightIn

deleted theorem RootPairing.iInf_ker_coroot'_eq

deleted theorem RootPairing.iInf_ker_root'_eq

deleted theorem RootPairing.isValuedIn_iff_mem_range

deleted def RootPairing.pairingIn

deleted theorem RootPairing.pairingIn_reflection_perm_self_left

deleted theorem RootPairing.pairingIn_reflection_perm_self_right

deleted theorem RootPairing.pairingIn_same

deleted theorem RootPairing.root'_apply_apply_mem_of_mem_span

deleted theorem RootPairing.rootSpan_dualAnnihilator_map_eq

deleted theorem RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'

deleted theorem RootPairing.rootSpan_map_toDualLeft

deleted theorem RootPairing.rootSpan_mem_invtSubmodule_reflection

deleted theorem RootPairing.rootSpan_ne_bot

deleted theorem RootPairing.span_coroot'_eq_top

deleted theorem RootPairing.span_root'_eq_top

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

added def RootPairing.CoPolarizationIn

added theorem RootPairing.CoPolarizationIn_apply

added theorem RootPairing.CoPolarizationIn_eq

added def RootPairing.PolarizationIn

added theorem RootPairing.PolarizationIn_apply

added theorem RootPairing.PolarizationIn_eq

added def RootPairing.RootFormIn

added theorem RootPairing.algebraMap_posRootForm_posForm

added theorem RootPairing.algebraMap_rootFormIn

modified theorem RootPairing.exists_ge_zero_eq_rootForm

modified def RootPairing.posRootForm

added theorem RootPairing.posRootForm_eq

added theorem RootPairing.posRootForm_posForm_apply_apply

added theorem RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn

added theorem RootPairing.range_polarizationIn

added theorem RootPairing.range_polarizationIn_le_span_coroot

added theorem RootPairing.rootFormIn_self_smul_coroot

added theorem RootPairing.toPerfectPairing_apply_PolarizationIn

added theorem RootPairing.zero_le_posForm

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

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

added theorem RootPairing.exists_coroot_ne

added theorem RootPairing.finrank_corootSpan_eq'

modified theorem RootPairing.finrank_corootSpan_eq

added theorem RootPairing.finrank_range_polarization_eq_finrank_span_coroot

added theorem RootPairing.polarizationIn_Injective

added theorem RootPairing.posRootForm_posForm_anisotropic

added theorem RootPairing.posRootForm_posForm_nondegenerate

added theorem RootPairing.posRootForm_posForm_pos_of_ne_zero

modified theorem RootPairing.rootForm_pos_of_ne_zero

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

Created Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

added theorem RootPairing.IsValuedIn.trans

added theorem RootPairing.algebraMap_coroot'In_apply

added theorem RootPairing.algebraMap_coxeterWeightIn

added theorem RootPairing.algebraMap_pairingIn

added theorem RootPairing.algebraMap_root'In_apply

added def RootPairing.coroot'In

added theorem RootPairing.coroot'In_rootSpanMem_eq_pairingIn

added theorem RootPairing.coroot'_apply_apply_mem_of_mem_span

added theorem RootPairing.corootSpan_dualAnnihilator_map_eq

added theorem RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'

added theorem RootPairing.corootSpan_map_toDualRight

added theorem RootPairing.corootSpan_mem_invtSubmodule_coreflection

added theorem RootPairing.corootSpan_ne_bot

added def RootPairing.coxeterWeightIn

added theorem RootPairing.iInf_ker_coroot'_eq

added theorem RootPairing.iInf_ker_root'_eq

added theorem RootPairing.isValuedIn_iff_mem_range

added def RootPairing.pairingIn

added theorem RootPairing.pairingIn_reflection_perm

added theorem RootPairing.pairingIn_reflection_perm_self_left

added theorem RootPairing.pairingIn_reflection_perm_self_right

added theorem RootPairing.pairingIn_same

added def RootPairing.root'In

added theorem RootPairing.root'In_corootSpanMem_eq_pairingIn

added theorem RootPairing.root'_apply_apply_mem_of_mem_span

added theorem RootPairing.rootSpan_dualAnnihilator_map_eq

added theorem RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'

added theorem RootPairing.rootSpan_map_toDualLeft

added theorem RootPairing.rootSpan_mem_invtSubmodule_reflection

added theorem RootPairing.rootSpan_ne_bot

added theorem RootPairing.span_coroot'_eq_top

added theorem RootPairing.span_root'_eq_top

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean