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:

• RootPairing.IsValuedIn: Given a commutative ring S and an S-algebra R, a root pairing over R is valued in S if all root-coroot pairings lie in the image of algebraMap S R.
• RootPairing.IsCrystallographic: A root pairing is said to be crystallographic if the pairing between a root and coroot is always an integer.
• RootPairing.pairingIn: The S-valued pairing between roots and coroots.
• RootPairing.coxeterWeightIn: The product of pairingIn i j and pairingIn j i.

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] : Prop

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.

• exists_value (i j : ι) : ∃ (s : S), (algebraMap S R) s = P.pairing i j

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) : Prop

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

Equations

• P.IsCrystallographic = P.IsValuedIn ℤ

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) : P.IsValuedIn R

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] : P.flip.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

• P.pairingIn S i j = ⋯.choose

@[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_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.reflection_perm i) k) = P.pairingIn S ((P.reflection_perm i) j) k

@[simp]

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.reflection_perm i) i) j = -P.pairingIn S i j

@[simp]

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.reflection_perm j) j) = -P.pairingIn S i j

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] : P.IsValuedIn S

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 : ι) : (P.root' i) x ∈ LinearMap.range (Algebra.linearMap S R)

@[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] : Submodule S M

The S-span of roots.

Equations

• P.rootSpan S = Submodule.span S (Set.range ⇑P.root)

@[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] : Submodule S N

The S-span of coroots.

Equations

• P.corootSpan S = Submodule.span S (Set.range ⇑P.coroot)

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 ι] : Module.Finite S ↥(P.rootSpan S)

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 ι] : Module.Finite S ↥(P.corootSpan S)

@[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

• P.rootSpanMem S i = ⟨P.root i, ⋯⟩

@[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

• P.corootSpanMem S i = ⟨P.coroot i, ⋯⟩

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 : ι) : P.rootSpanMem S ((P.reflection_perm i) i) = -P.rootSpanMem S i

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 : ι) : P.corootSpanMem S ((P.reflection_perm i) i) = -P.corootSpanMem S i

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 : ι) : Module.Dual S ↥(P.corootSpan S)

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

Equations

• P.root'In S i = (P.corootSpan S).subtype.restrictScalarsRange (Algebra.linearMap S R) ⋯ (P.root' i) ⋯

@[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 : ι) : Module.Dual S ↥(P.rootSpan S)

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

Equations

• P.coroot'In S i = P.flip.root'In S i

@[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] : P.rootSpan S ≠ ⊥

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] : P.corootSpan S ≠ ⊥

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 : ι) : P.rootSpan R ∈ Module.End.invtSubmodule ↑(P.reflection 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 : ι) : P.corootSpan R ∈ Module.End.invtSubmodule ↑(P.coreflection i)

theorem RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root' {ι : 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) : Submodule.map P.toDualRight.symm (P.rootSpan R).dualAnnihilator = ⨅ (i : ι), LinearMap.ker (P.root' i)

theorem RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot' {ι : 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) : Submodule.map P.toDualLeft.symm (P.corootSpan R).dualAnnihilator = ⨅ (i : ι), LinearMap.ker (P.coroot' i)

theorem RootPairing.rootSpan_dualAnnihilator_map_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) : Submodule.map P.toDualRight.symm (P.rootSpan R).dualAnnihilator = (Submodule.span R (Set.range P.root')).dualCoannihilator

theorem RootPairing.corootSpan_dualAnnihilator_map_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) : Submodule.map P.toDualLeft.symm (P.corootSpan R).dualAnnihilator = (Submodule.span R (Set.range P.coroot')).dualCoannihilator

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) : ⨅ (i : ι), LinearMap.ker (P.root' i) = (Submodule.span R (Set.range P.root')).dualCoannihilator

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) : ⨅ (i : ι), LinearMap.ker (P.coroot' i) = (Submodule.span R (Set.range P.coroot')).dualCoannihilator

@[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) : Submodule.map P.toDualLeft (P.rootSpan R) = Submodule.span R (Set.range P.root')

@[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) : Submodule.map P.toDualRight (P.corootSpan R) = Submodule.span R (Set.range P.coroot')

@[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) : Submodule.span R (Set.range P.root') = ⊤

@[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) : Submodule.span R (Set.range P.coroot') = ⊤

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

• P.coxeterWeightIn S i j = P.pairingIn S i j * P.pairingIn S j i

@[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 : ι) : (algebraMap S R) (P.coxeterWeightIn S i j) = P.coxeterWeight i j