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: #

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

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

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

P.IsCrystallographic = P.IsValuedIn ℤ

Instances For

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

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

Instances For

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

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

The S-span of roots.

Equations

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

Instances For

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

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

Instances For

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, ⋯⟩

Instances For

@[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, ⋯⟩

Instances For

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) ⋯

Instances For

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

Instances For

@[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') = ⊤

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

Instances For

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