Documentation

Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Root pairings taking values in a subring #

This file lays out the basic theory of root pairings over a commutative ring R, where R is an S-algebra, and the the pairing between roots and coroots takes values in S. The main application of this theory is the theory of crystallographic root systems, where S = ℤ.

Main definitions: #

class RootPairing.IsValuedIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] :

If R is an S-algebra, a root pairing over R is said to be valued in S if the pairing between a root and coroot always belongs to S.

Of particular interest is the case S = ℤ. See RootPairing.IsCrystallographic.

Instances
    theorem RootPairing.isValuedIn_iff {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] :
    P.IsValuedIn S ∀ (i j : ι), ∃ (s : S), (algebraMap S R) s = P.pairing i j
    theorem RootPairing.exists_value {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} {inst✝ : CommRing R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {P : RootPairing ι R M N} {S : Type u_6} {inst✝⁵ : CommRing S} {inst✝⁶ : Algebra S R} [self : P.IsValuedIn S] (i j : ι) :
    ∃ (s : S), (algebraMap S R) s = P.pairing i j

    Alias of RootPairing.IsValuedIn.exists_value.

    @[reducible, inline]
    abbrev RootPairing.IsCrystallographic {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :

    A root pairing is said to be crystallographic if the pairing between a root and coroot is always an integer.

    Equations
    instance RootPairing.instIsValuedIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :
    theorem RootPairing.isValuedIn_iff_mem_range {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) {S : Type u_6} [CommRing S] [Algebra S R] :
    P.IsValuedIn S ∀ (i j : ι), P.pairing i j Set.range (algebraMap S R)
    instance RootPairing.instIsValuedInFlip {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [P.IsValuedIn S] :
    def RootPairing.pairingIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [P.IsValuedIn S] (i j : ι) :
    S

    A variant of RootPairing.pairing for root pairings which are valued in a smaller set of coefficients.

    Note that it is uniquely-defined only when the map S → R is injective, i.e., when we have [FaithfulSMul S R].

    Equations
    @[simp]
    theorem RootPairing.algebraMap_pairingIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [P.IsValuedIn S] (i j : ι) :
    (algebraMap S R) (P.pairingIn S i j) = P.pairing i j
    @[simp]
    theorem RootPairing.pairingIn_same {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) :
    P.pairingIn S i i = 2
    theorem RootPairing.pairingIn_reflectionPerm {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i j k : ι) :
    P.pairingIn S j ((P.reflectionPerm i) k) = P.pairingIn S ((P.reflectionPerm i) j) k
    @[deprecated RootPairing.pairingIn_reflectionPerm (since := "2025-05-28")]
    theorem RootPairing.pairingIn_reflection_perm {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i j k : ι) :
    P.pairingIn S j ((P.reflectionPerm i) k) = P.pairingIn S ((P.reflectionPerm i) j) k

    Alias of RootPairing.pairingIn_reflectionPerm.

    @[simp]
    theorem RootPairing.pairingIn_reflectionPerm_self_left {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S ((P.reflectionPerm i) i) j = -P.pairingIn S i j
    @[deprecated RootPairing.pairingIn_reflectionPerm_self_left (since := "2025-05-28")]
    theorem RootPairing.pairingIn_reflection_perm_self_left {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S ((P.reflectionPerm i) i) j = -P.pairingIn S i j

    Alias of RootPairing.pairingIn_reflectionPerm_self_left.

    @[simp]
    theorem RootPairing.pairingIn_reflectionPerm_self_right {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S i ((P.reflectionPerm j) j) = -P.pairingIn S i j
    @[deprecated RootPairing.pairingIn_reflectionPerm_self_right (since := "2025-05-28")]
    theorem RootPairing.pairingIn_reflection_perm_self_right {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (i j : ι) :
    P.pairingIn S i ((P.reflectionPerm j) j) = -P.pairingIn S i j

    Alias of RootPairing.pairingIn_reflectionPerm_self_right.

    theorem RootPairing.IsValuedIn.trans {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] (T : Type u_7) [CommRing T] [Algebra T S] [Algebra T R] [IsScalarTower T S R] [P.IsValuedIn T] :
    theorem RootPairing.coroot'_apply_apply_mem_of_mem_span {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] {x : M} (hx : x Submodule.span S (Set.range P.root)) (i : ι) :
    (P.coroot' i) x Set.range (algebraMap S R)
    theorem RootPairing.root'_apply_apply_mem_of_mem_span {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] {x : N} (hx : x Submodule.span S (Set.range P.coroot)) (i : ι) :
    @[reducible, inline]
    abbrev RootPairing.rootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S M] :

    The S-span of roots.

    Equations
    @[reducible, inline]
    abbrev RootPairing.corootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S N] :

    The S-span of coroots.

    Equations
    instance RootPairing.instFiniteSubtypeMemSubmoduleRootSpanOfFinite {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S M] [Finite ι] :
    instance RootPairing.instFiniteSubtypeMemSubmoduleCorootSpanOfFinite {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S N] [Finite ι] :
    @[reducible, inline]
    abbrev RootPairing.rootSpanMem {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S M] (i : ι) :
    (P.rootSpan S)

    A root, seen as an element of the span of roots.

    Equations
    @[reducible, inline]
    abbrev RootPairing.corootSpanMem {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S N] (i : ι) :
    (P.corootSpan S)

    A coroot, seen as an element of the span of coroots.

    Equations
    theorem RootPairing.rootSpanMem_reflectionPerm_self {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S M] (i : ι) :
    @[deprecated RootPairing.rootSpanMem_reflectionPerm_self (since := "2025-05-28")]
    theorem RootPairing.rootSpanMem_reflection_perm_self {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S M] (i : ι) :

    Alias of RootPairing.rootSpanMem_reflectionPerm_self.

    theorem RootPairing.corootSpanMem_reflectionPerm_self {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S N] (i : ι) :
    @[deprecated RootPairing.corootSpanMem_reflectionPerm_self (since := "2025-05-28")]
    theorem RootPairing.corootSpanMem_reflection_perm_self {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S N] (i : ι) :

    Alias of RootPairing.corootSpanMem_reflectionPerm_self.

    def RootPairing.root'In {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S N] [IsScalarTower S R N] [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) :

    The S-linear map on the span of coroots given by evaluating at a root.

    Equations
    @[simp]
    theorem RootPairing.algebraMap_root'In_apply {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S N] [IsScalarTower S R N] [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) (x : (P.corootSpan S)) :
    (algebraMap S R) ((P.root'In S i) x) = (P.root' i) x
    @[simp]
    theorem RootPairing.root'In_corootSpanMem_eq_pairingIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i j : ι) (S : Type u_6) [CommRing S] [Algebra S R] [Module S N] [IsScalarTower S R N] [FaithfulSMul S R] [P.IsValuedIn S] :
    (P.root'In S i) (P.corootSpanMem S j) = P.pairingIn S i j
    def RootPairing.coroot'In {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) :

    The S-linear map on the span of roots given by evaluating at a coroot.

    Equations
    @[simp]
    theorem RootPairing.algebraMap_coroot'In_apply {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) (x : (P.rootSpan S)) :
    (algebraMap S R) ((P.coroot'In S i) x) = (P.coroot' i) x
    @[simp]
    theorem RootPairing.coroot'In_rootSpanMem_eq_pairingIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i j : ι) (S : Type u_6) [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] [FaithfulSMul S R] [P.IsValuedIn S] :
    (P.coroot'In S i) (P.rootSpanMem S j) = P.pairingIn S j i
    theorem RootPairing.rootSpan_ne_bot {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S M] [Nonempty ι] [NeZero 2] :
    theorem RootPairing.corootSpan_ne_bot {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Module S N] [Nonempty ι] [NeZero 2] :
    theorem RootPairing.rootSpan_mem_invtSubmodule_reflection {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) :
    theorem RootPairing.corootSpan_mem_invtSubmodule_coreflection {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) :
    theorem RootPairing.iInf_ker_root'_eq {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :
    theorem RootPairing.iInf_ker_coroot'_eq {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :
    @[simp]
    theorem RootPairing.rootSpan_map_toDualLeft {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :
    @[simp]
    theorem RootPairing.corootSpan_map_toDualRight {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) :
    @[simp]
    theorem RootPairing.span_root'_eq_top {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootSystem ι R M N) :
    @[simp]
    theorem RootPairing.span_coroot'_eq_top {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootSystem ι R M N) :
    theorem RootPairing.pairingIn_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) {S : Type u_7} [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] [NoZeroSMulDivisors R M] [NeZero 2] {i j : ι} :
    P.pairingIn S i j = 0 P.pairingIn S j i = 0
    def RootPairing.coxeterWeightIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_7) [CommRing S] [Algebra S R] [P.IsValuedIn S] (i j : ι) :
    S

    A variant of RootPairing.coxeterWeight for root pairings which are valued in a smaller set of coefficients.

    Note that it is uniquely-defined only when the map S → R is injective, i.e., when we have [FaithfulSMul S R].

    Equations
    @[simp]
    theorem RootPairing.algebraMap_coxeterWeightIn {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_7) [CommRing S] [Algebra S R] [P.IsValuedIn S] (i j : ι) :