Base change of a root pairing carried by the standard lattices

An integral root datum carries its roots and coroots on the standard lattices κ → ℤ, paired by the dot product. The constructions which build a Lie algebra out of a root system — Serre's presentation, and Geck's construction — instead want a root system over a field of characteristic zero. This file moves such a pairing along an injective algebra map, expressed by [FaithfulSMul R S], applying the structure map entrywise to every root and coroot and keeping the same reflection permutation.

Only the target pairing is chosen here: it is again the dot product, which is perfect on κ → S for every commutative ring S by TauCeti.dotProductBilin_isPerfPair. So the construction asks the source pairing to be the dot product too, and every axiom of RootPairing then transports along Pi.algebraMap, entrywise application of algebraMap R S.

The properties a downstream Lie-theoretic consumer needs are transported separately, each under its own hypotheses: being crystallographic, being reduced, spanning, carrying a base with a prescribed Cartan matrix, and the root-string coefficients. Irreducibility is deliberately absent, because it is false over ℤ: the sublattice 2 • (κ → ℤ) is invariant under every reflection. It has to be proved over the new base ring rather than transported.

Main definitions

• TauCeti.rootPairingBaseChange: the base change of a dot-product root pairing along an injective algebra map R → S, expressed by [FaithfulSMul R S].
• TauCeti.rootPairingBaseChangeBase: the base of the base change attached to a base of the original pairing, supported on the same indices.

Main results

• TauCeti.isCrystallographic_rootPairingBaseChange: base change preserves being crystallographic.
• TauCeti.isReduced_rootPairingBaseChange: base change preserves being reduced.
• TauCeti.span_range_root_rootPairingBaseChange_eq_top and TauCeti.span_range_coroot_rootPairingBaseChange_eq_top: a spanning family of roots or coroots stays spanning.
• TauCeti.pairingIn_rootPairingBaseChange: the integral pairings, hence the Cartan matrix of a base, are unchanged.
• TauCeti.chainTopCoeff_rootPairingBaseChange and TauCeti.chainBotCoeff_rootPairingBaseChange: the root-string coefficients are unchanged.

References

The construction is the standard passage from a root datum over ℤ to the root system over ℚ that it determines; see N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.

Entrywise base change of the standard lattice

theorem TauCeti.piAlgebraMap_apply {κ : Type u_1} {R : Type u_2} (S : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] (x : κ → R) (j : κ) : (Pi.algebraMap κ R S) x j = (algebraMap R S) (x j)

Entrywise base change of the standard lattice reads off entrywise.

theorem TauCeti.piAlgebraMap_injective {κ : Type u_1} {R : Type u_2} (S : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [FaithfulSMul R S] : Function.Injective ⇑(Pi.algebraMap κ R S)

Entrywise base change along an injective algebra map is injective.

theorem TauCeti.mem_closure_image_piAlgebraMap {κ : Type u_1} {R : Type u_2} (S : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] {ι : Type u_4} {g : ι → κ → R} {s : Set ι} {x : κ → R} (hx : x ∈ AddSubmonoid.closure (g '' s)) : (Pi.algebraMap κ R S) x ∈ AddSubmonoid.closure ((fun (i : ι) => (Pi.algebraMap κ R S) (g i)) '' s)

Entrywise base change carries the additive closure of a family into the additive closure of the base-changed family.

theorem TauCeti.span_range_piAlgebraMap_eq_top {κ : Type u_1} {R : Type u_2} (S : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Finite κ] {ι : Type u_4} {v : ι → κ → R} (hv : Submodule.span R (Set.range v) = ⊤) : Submodule.span S (Set.range fun (i : ι) => (Pi.algebraMap κ R S) (v i)) = ⊤

A family of vectors spanning the standard lattice still spans after entrywise base change.

The base-changed pairing

def TauCeti.rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] : RootPairing ι S (κ → S) (κ → S)

Base change of a root pairing on the standard lattices. The roots and coroots of P : RootPairing ι R (κ → R) (κ → R), whose pairing is the dot product, are pushed entrywise along the injective map algebraMap R S, with injectivity supplied by [FaithfulSMul R S], and paired again by the dot product on κ → S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.root_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (i : ι) : (rootPairingBaseChange S P hP).root i = (Pi.algebraMap κ R S) (P.root i)

@[simp]

theorem TauCeti.coroot_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (i : ι) : (rootPairingBaseChange S P hP).coroot i = (Pi.algebraMap κ R S) (P.coroot i)

@[simp]

theorem TauCeti.reflectionPerm_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] : (rootPairingBaseChange S P hP).reflectionPerm = P.reflectionPerm

@[simp]

theorem TauCeti.toLinearMap_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (x y : κ → S) : ((rootPairingBaseChange S P hP).toLinearMap x) y = x ⬝ᵥ y

@[simp]

theorem TauCeti.pairing_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (i j : ι) : (rootPairingBaseChange S P hP).pairing i j = (algebraMap R S) (P.pairing i j)

theorem TauCeti.piAlgebraMap_mem_range_root_rootPairingBaseChange_iff {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (x : κ → R) : (Pi.algebraMap κ R S) x ∈ Set.range ⇑(rootPairingBaseChange S P hP).root ↔ x ∈ Set.range ⇑P.root

An entrywise base-changed vector is a root of the base change exactly when the vector is a root of the original pairing.

theorem TauCeti.linearIndependent_pair_root_rootPairingBaseChange_iff {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] (i j : ι) : LinearIndependent S ![(rootPairingBaseChange S P hP).root i, (rootPairingBaseChange S P hP).root j] ↔ LinearIndependent R ![P.root i, P.root j]

Two roots of the base change into a domain are linearly independent exactly when the corresponding roots of the original pairing are.

Transport of the axioms a Lie-theoretic consumer needs

instance TauCeti.isCrystallographic_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [P.IsCrystallographic] : (rootPairingBaseChange S P hP).IsCrystallographic

Base change preserves being crystallographic: a pairing which was an integer stays that same integer in the new base ring.

@[simp]

theorem TauCeti.pairingIn_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [CharZero S] [P.IsCrystallographic] (i j : ι) : (rootPairingBaseChange S P hP).pairingIn ℤ i j = P.pairingIn ℤ i j

The integral pairing of a crystallographic root pairing is unchanged by base change into a ring of characteristic zero. Hence so is the Cartan matrix of any base.

theorem TauCeti.isReduced_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] [P.IsReduced] : (rootPairingBaseChange S P hP).IsReduced

Base change along an injective map into a domain preserves being reduced.

theorem TauCeti.span_range_root_rootPairingBaseChange_eq_top {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (h : Submodule.span R (Set.range ⇑P.root) = ⊤) : Submodule.span S (Set.range ⇑(rootPairingBaseChange S P hP).root) = ⊤

Base change preserves spanning by the roots.

theorem TauCeti.span_range_coroot_rootPairingBaseChange_eq_top {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] (h : Submodule.span R (Set.range ⇑P.coroot) = ⊤) : Submodule.span S (Set.range ⇑(rootPairingBaseChange S P hP).coroot) = ⊤

Base change preserves spanning by the coroots.

Bases

def TauCeti.rootPairingBaseChangeBase {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] (b : P.Base) : (rootPairingBaseChange S P hP).Base

The base change of a base. A base of P is a base of the base-changed pairing, supported on the same indices.

Equations

• TauCeti.rootPairingBaseChangeBase S P hP b = { support := b.support, linearIndepOn_root := ⋯, linearIndepOn_coroot := ⋯, root_mem_or_neg_mem := ⋯, coroot_mem_or_neg_mem := ⋯ }

@[simp]

theorem TauCeti.support_rootPairingBaseChangeBase {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] (b : P.Base) : (rootPairingBaseChangeBase S P hP b).support = b.support

def TauCeti.supportEquivRootPairingBaseChangeBase {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] (b : P.Base) : ↥(rootPairingBaseChangeBase S P hP b).support ≃ ↥b.support

The supports of a base and of its base change name the same indices.

Equations

• TauCeti.supportEquivRootPairingBaseChangeBase S P hP b = Equiv.subtypeEquivRight ⋯

@[simp]

theorem TauCeti.coe_supportEquivRootPairingBaseChangeBase {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] (b : P.Base) (i : ↥(rootPairingBaseChangeBase S P hP b).support) : ↑((supportEquivRootPairingBaseChangeBase S P hP b) i) = ↑i

@[simp]

theorem TauCeti.cartanMatrix_rootPairingBaseChangeBase {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [FaithfulSMul R S] [IsDomain S] (b : P.Base) [CharZero S] [P.IsCrystallographic] (i j : ↥(rootPairingBaseChangeBase S P hP b).support) : (rootPairingBaseChangeBase S P hP b).cartanMatrix i j = b.cartanMatrix ((supportEquivRootPairingBaseChangeBase S P hP b) i) ((supportEquivRootPairingBaseChangeBase S P hP b) j)

Base change does not change the Cartan matrix of a base.

Root strings

@[simp]

theorem TauCeti.chainTopCoeff_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Finite ι] [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [CharZero R] [IsDomain S] [CharZero S] [FaithfulSMul R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [P.IsCrystallographic] (i j : ι) : RootPairing.chainTopCoeff i j = RootPairing.chainTopCoeff i j

Base change preserves the upper root-string coefficient.

@[simp]

theorem TauCeti.chainBotCoeff_rootPairingBaseChange {ι : Type u_1} {κ : Type u_2} {R : Type u_3} (S : Type u_4) [Finite ι] [Fintype κ] [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [CharZero R] [IsDomain S] [CharZero S] [FaithfulSMul R S] (P : RootPairing ι R (κ → R) (κ → R)) (hP : ∀ (x y : κ → R), (P.toLinearMap x) y = x ⬝ᵥ y) [P.IsCrystallographic] (i j : ι) : RootPairing.chainBotCoeff i j = RootPairing.chainBotCoeff i j

Base change preserves the lower root-string coefficient.