Scaffolding shared by the pinned simply connected root data

The pinned simply connected root data are integral root data, one per valid Dynkin type, each on the lattices Fin n → ℤ with the dot product as pairing, and each carrying a base whose support is the image of an injective simple index map e naming the simple roots in Bourbaki order. This file holds the part of that construction which carries no information about the type: only the per-type files, such as TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.A and ...SimplyConnectedRootDatum.D.Basic, supply the mathematics of their own root system.

Main definitions

• TauCeti.simpleSupport: the support of a pinned base, the image of a simple index map.

Main results

• TauCeti.hasCartanType_of_pairing_eq: a base supported on a simple index map has Cartan type t as soon as the pairings of the simple roots are the entries of the standard Cartan matrix of t.
• TauCeti.corootSpan_eq_top_of_coroot_eq_single: the coroots span the cocharacter lattice as soon as the simple coroots are the standard basis. This is the simply connected lattice condition.

The membership axioms of RootPairing.Base are met by the pinned data through TauCeti.sum_smul_mem_or_neg_mem_closure in TauCeti/Algebra/Group/Submonoid/Closure.lean, or, for data written in a coordinate potential, through TauCeti.sub_mem_closure_of_le in TauCeti/Algebra/Group/Submonoid/Telescoping.lean. Every pinned datum pairs its two lattices by the dot product, which is a perfect pairing by TauCeti.dotProductBilin_isPerfPair in TauCeti/LinearAlgebra/Matrix/Dual.lean. The symmetry and reflection preservation of the quadratic form carried by the Cartan matrix are supplied by TauCeti.vecMul_dotProduct_comm and TauCeti.reflect_vecMul_dotProduct_self in TauCeti/LinearAlgebra/Matrix/Gram.lean.

The support of a pinned base

def TauCeti.simpleSupport {ι : Type u_1} {κ : Type u_2} [Fintype κ] {e : κ → ι} (he : Function.Injective e) : Finset ι

The support of a pinned base: the image of the simple index map e, which names the simple roots among all root indices.

Equations

• TauCeti.simpleSupport he = Finset.map { toFun := e, inj' := he } Finset.univ

@[simp]

theorem TauCeti.mem_simpleSupport {ι : Type u_1} {κ : Type u_2} [Fintype κ] {e : κ → ι} (he : Function.Injective e) {k : ι} : k ∈ simpleSupport he ↔ ∃ (i : κ), e i = k

@[simp]

theorem TauCeti.coe_simpleSupport {ι : Type u_1} {κ : Type u_2} [Fintype κ] {e : κ → ι} (he : Function.Injective e) : ↑(simpleSupport he) = Set.range e

theorem TauCeti.image_simpleSupport {ι : Type u_1} {κ : Type u_2} [Fintype κ] {e : κ → ι} (he : Function.Injective e) {M : Type u_3} (f : ι → M) : f '' ↑(simpleSupport he) = Set.range (f ∘ e)

The image of a pinned support under a family indexed by the root indices is the range of the family's restriction to the simple indices.

theorem TauCeti.linearIndepOn_simpleSupport {ι : Type u_1} {κ : Type u_2} [Fintype κ] {e : κ → ι} (he : Function.Injective e) {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : ι → M) (h : LinearIndependent R (f ∘ e)) : LinearIndepOn R f ↑(simpleSupport he)

Linear independence of the simple members of a family is linear independence on the pinned support, the form in which RootPairing.Base asks for it.

theorem TauCeti.mem_simpleSupport_iff_lt {n N : ℕ} {e : Fin n → Fin N} (he : Function.Injective e) (h : ∀ (i : Fin n), ↑(e i) = ↑i) {k : Fin N} : k ∈ simpleSupport he ↔ ↑k < n

A pinned support numbered in order is an initial segment. When the simple index map sends i to the root index i, membership in the support is the bound k < n on the index.

Recognizing the pinned data

theorem TauCeti.hasCartanType_of_pairing_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [FaithfulSMul ℤ R] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} {t : DynkinType} {e : Fin t.rank → ι} (he : Function.Injective e) (hb : b.support = simpleSupport he) (h : ∀ (i j : Fin t.rank), P.pairing (e i) (e j) = (algebraMap ℤ R) (t.cartanMatrix i j)) : HasCartanType P b t

A pinned base has the Cartan type its simple pairings display. The Cartan matrix of a base supported on a simple index map is read off the pairings of the simple roots, so a base whose simple pairings are the entries of the standard Cartan matrix of t has Cartan type t.

theorem TauCeti.corootSpan_eq_top_of_coroot_eq_single {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {κ : Type u_5} [Finite κ] [DecidableEq κ] {P : RootPairing ι R M (κ → R)} {e : κ → ι} (h : ∀ (i : κ), P.coroot (e i) = Pi.single i 1) : P.corootSpan R = ⊤

The coroots span the cocharacter lattice when the simple coroots are the standard basis. For a root datum on the lattice κ → ℤ this is the simply connected lattice condition.