Realisations of Cartan Matrices

Let R be an integral domain of characteristic zero, and let M and N be R-modules in perfect pairing. Then, given vectors r₁, r₂, …, rₗ in M and c₁, c₂, …, cₗ in N, the following two propositions are equivalent:

1. The vectors rᵢ, cᵢ are the simple roots and coroots of a finite, reduced, crystrallographic root pairing (i.e., a reduced root datum except we do not require R = ℤ).
2. The matrix Aᵢⱼ = ⟨cⱼ, rᵢ⟩ is a finite-type Cartan matrix.

The definition RootPairing formalises item 1 above. Here we introduce CartanMatrix.Realisation to formalise item 2.

Main definitions / results:

• CartanMatrix.Realisation: the definition of a realisation of a Cartan matrix.
• CartanMatrix.Realisation.toRootPairing: the root pairing defined by a realisation of a Cartan matrix.
• Matrix.IsFiniteCartan.toRealisation: a realisation associated to an invertible Cartan matrix.
• Matrix.IsFiniteCartan.toRootPairing: a reduced, irreducible, crystallographic root system assocated to a Cartan matrix, with coefficients in any field of characteristic zero.

structure CartanMatrix.Realisation (n : Type u_1) (R : Type u_2) (M : Type u_3) (N : Type u_4) [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Type (max (max (max u_1 u_2) u_3) u_4)

A realisation of a Cartan matrix indexed by n is a family of vectors v and covectors f, both indexed by n, such that ⟨fⱼ, vᵢ⟩ = Aᵢⱼ for all i j.

• sRoot : n → M

  The simple roots.

• sCoroot : n → N

  The simple coroots.

• matrix : Matrix n n ℤ

  The Cartan matrix.

• isCartan : self.matrix.IsFiniteCartan
• pairing : M →ₗ[R] N →ₗ[R] R

  The perfect pairing.

• isPerfPair : self.pairing.IsPerfPair
• pairingMatrix (i j : n) : (self.pairing (self.sRoot i)) (self.sCoroot j) = ↑(self.matrix i j)

instance CartanMatrix.Realisation.instIsPerfPairPairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.pairing.IsPerfPair

def CartanMatrix.Realisation.flip {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : Realisation n R N M

The realisation obtained by interchanging the roles of M and N.

Equations

• rl.flip = { sRoot := rl.sCoroot, sCoroot := rl.sRoot, matrix := rl.matrix.transpose, isCartan := ⋯, pairing := rl.pairing.flip, isPerfPair := ⋯, pairingMatrix := ⋯ }

theorem CartanMatrix.Realisation.lin_ind_sRoot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : LinearIndependent R rl.sRoot

theorem CartanMatrix.Realisation.lin_ind_sCoroot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : LinearIndependent R rl.sCoroot

theorem CartanMatrix.Realisation.injective_sRoot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : Function.Injective rl.sRoot

theorem CartanMatrix.Realisation.injective_sCoroot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : Function.Injective rl.sCoroot

theorem CartanMatrix.Realisation.pairing_sRoot_sCoroot_self {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : (rl.pairing (rl.sRoot i)) (rl.sCoroot i) = 2

theorem CartanMatrix.Realisation.exist_int_eq_pairing_of_mem_span_int {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {x : M} (hx : x ∈ Submodule.span ℤ (Set.range rl.sRoot)) {y : N} (hy : y ∈ Submodule.span ℤ (Set.range rl.sCoroot)) : ∃ (z : ℤ), (rl.pairing x) y = ↑z

def CartanMatrix.Realisation.reflection {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : M ≃ₗ[R] M

The reflection associated to a simple root.

Equations

• rl.reflection i = Module.reflection ⋯

def CartanMatrix.Realisation.coreflection {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : N ≃ₗ[R] N

The reflection associated to a simple coroot.

Equations

• rl.coreflection i = rl.flip.reflection i

theorem CartanMatrix.Realisation.reflection_apply {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) (x : M) : (rl.reflection i) x = x - (rl.pairing x) (rl.sCoroot i) • rl.sRoot i

theorem CartanMatrix.Realisation.coreflection_apply {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) (y : N) : (rl.coreflection i) y = y - (rl.pairing (rl.sRoot i)) y • rl.sCoroot i

@[simp]

theorem CartanMatrix.Realisation.reflection_same {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) (x : M) : (rl.reflection i) ((rl.reflection i) x) = x

@[simp]

theorem CartanMatrix.Realisation.coreflection_same {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) (y : N) : (rl.coreflection i) ((rl.coreflection i) y) = y

@[simp]

theorem CartanMatrix.Realisation.flip_pairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.flip.pairing = rl.pairing.flip

@[simp]

theorem CartanMatrix.Realisation.flip_sRoot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.flip.sRoot = rl.sCoroot

@[simp]

theorem CartanMatrix.Realisation.flip_sCoroot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.flip.sCoroot = rl.sRoot

@[simp]

theorem CartanMatrix.Realisation.flip_reflection {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : rl.flip.reflection i = rl.coreflection i

@[simp]

theorem CartanMatrix.Realisation.flip_coreflection {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : rl.flip.coreflection i = rl.reflection i

theorem CartanMatrix.Realisation.eq_iff_forall_pairing_sRoot_eq {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] {y₁ y₂ : N} (hy : y₁ - y₂ ∈ Submodule.span R (Set.range rl.sCoroot)) : y₁ = y₂ ↔ ∀ (i : n), (rl.pairing (rl.sRoot i)) y₁ = (rl.pairing (rl.sRoot i)) y₂

theorem CartanMatrix.Realisation.pairing_reflection_left {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) (x : M) (y : N) : (rl.pairing ((rl.reflection i) x)) y = (rl.pairing x) ((rl.coreflection i) y)

theorem CartanMatrix.Realisation.pairing_reflection_coreflection {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) (x : M) (y : N) : (rl.pairing ((rl.reflection i) x)) ((rl.coreflection i) y) = (rl.pairing x) y

def CartanMatrix.Realisation.weylGroup {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : Subgroup ((M ≃ₗ[R] M) × N ≃ₗ[R] N)

The Weyl group of a realisation.

Equations

• rl.weylGroup = Subgroup.closure (Set.range (Function.prod rl.reflection rl.coreflection))

theorem CartanMatrix.Realisation.mem_weyl {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : (rl.reflection i, rl.coreflection i) ∈ rl.weylGroup

@[instance_reducible]

instance CartanMatrix.Realisation.instSMulSubtypeProdLinearEquivIdMemSubgroupWeylGroup {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : SMul (↥rl.weylGroup) (M × N)

Equations

• rl.instSMulSubtypeProdLinearEquivIdMemSubgroupWeylGroup = { smul := fun (w : ↥rl.weylGroup) (p : M × N) => ((↑w).1 p.1, (↑w).2 p.2) }

theorem CartanMatrix.Realisation.weylGroup_smul_def {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (w : ↥rl.weylGroup) (p : M × N) : w • p = ((↑w).1 p.1, (↑w).2 p.2)

@[instance_reducible]

instance CartanMatrix.Realisation.instDistribMulActionSubtypeProdLinearEquivIdMemSubgroupWeylGroup {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : DistribMulAction (↥rl.weylGroup) (M × N)

Equations

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

theorem CartanMatrix.Realisation.flip_weyl {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.flip.weylGroup = Subgroup.map MulEquiv.prodComm.toMonoidHom rl.weylGroup

@[simp]

theorem CartanMatrix.Realisation.mem_flip_weyl {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {w : (N ≃ₗ[R] N) × M ≃ₗ[R] M} : w ∈ rl.flip.weylGroup ↔ (w.2, w.1) ∈ rl.weylGroup

@[simp]

theorem CartanMatrix.Realisation.reflection_inv {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : (rl.reflection i)⁻¹ = rl.reflection i

@[simp]

theorem CartanMatrix.Realisation.coreflection_inv {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : (rl.coreflection i)⁻¹ = rl.coreflection i

theorem CartanMatrix.Realisation.weylGroup.induction {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {pred : (g : (M ≃ₗ[R] M) × N ≃ₗ[R] N) → g ∈ rl.weylGroup → Prop} (mem : ∀ (i : n), pred (rl.reflection i, rl.coreflection i) ⋯) (one : pred 1 ⋯) (mul : ∀ (x y : (M ≃ₗ[R] M) × N ≃ₗ[R] N) (hx : x ∈ rl.weylGroup) (hy : y ∈ rl.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯) {w : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw : w ∈ rl.weylGroup) : pred w hw

theorem CartanMatrix.Realisation.pairing_apply_apply_of_mem_weyl {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {w : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw : w ∈ rl.weylGroup) (x : M) (y : N) : (rl.pairing (w.1 x)) (w.2 y) = (rl.pairing x) y

theorem CartanMatrix.Realisation.mapsTo_span_int_range_sRoot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {w : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw : w ∈ rl.weylGroup) : Set.MapsTo ⇑w.1 ↑(Submodule.span ℤ (Set.range rl.sRoot)) ↑(Submodule.span ℤ (Set.range rl.sRoot))

theorem CartanMatrix.Realisation.exists_zsum_eq_of_mem_weylGroup {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {d : n → ℤ} (hd : (rl.matrix * Matrix.diagonal d).IsSymm) {w : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw : w ∈ rl.weylGroup) (c : n → ℤ) : ∃ (c' : n → ℤ), w.1 (∑ j : n, c j • rl.sRoot j) = ∑ j : n, c' j • rl.sRoot j ∧ c' ⬝ᵥ (rl.matrix * Matrix.diagonal d).mulVec c' = c ⬝ᵥ (rl.matrix * Matrix.diagonal d).mulVec c

theorem CartanMatrix.Realisation.finite_setOf_mem_weylGroup_apply_sRoot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : {x : M | ∃ w ∈ rl.weylGroup, ∃ (i : n), w.1 (rl.sRoot i) = x}.Finite

theorem CartanMatrix.Realisation.eq_of_mem_weylGroup_of_forall_apply_sRoot_eq {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] {w₁ w₂ : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw₁ : w₁ ∈ rl.weylGroup) (hw₂ : w₂ ∈ rl.weylGroup) (h : ∀ (i : n), w₁.1 (rl.sRoot i) = w₂.1 (rl.sRoot i)) : w₁ = w₂

instance CartanMatrix.Realisation.instFiniteSubtypeProdLinearEquivIdMemSubgroupWeylGroupOfCharZeroOfIsDomain {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : Finite ↥rl.weylGroup

def CartanMatrix.Realisation.idx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : Set (M × N)

Taking the Weyl-group orbits of all (simple root, simple coroot) pairs, yields a natural indexing set for the roots and coroots for the root pairing corresponding to a realisation.

Equations

• rl.idx = {x : M × N | ∃ w ∈ rl.weylGroup, ∃ (i : n), (w.1 (rl.sRoot i), w.2 (rl.sCoroot i)) = x}

theorem CartanMatrix.Realisation.idx_eq_smul {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.idx = Set.univ • Set.range (Function.prod rl.sRoot rl.sCoroot)

theorem CartanMatrix.Realisation.mk_mem_idx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {w : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw : w ∈ rl.weylGroup) (i : n) : (w.1 (rl.sRoot i), w.2 (rl.sCoroot i)) ∈ rl.idx

theorem CartanMatrix.Realisation.sPair_mem_idx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) (i : n) : (rl.sRoot i, rl.sCoroot i) ∈ rl.idx

theorem CartanMatrix.Realisation.apply_mem_idx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {w : (M ≃ₗ[R] M) × N ≃ₗ[R] N} (hw : w ∈ rl.weylGroup) {p : M × N} (hp : p ∈ rl.idx) : (w.1 p.1, w.2 p.2) ∈ rl.idx

@[simp]

theorem CartanMatrix.Realisation.flip_idx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.flip.idx = Prod.swap '' rl.idx

theorem CartanMatrix.Realisation.pairing_fst_snd {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {p : M × N} (hp : p ∈ rl.idx) : (rl.pairing p.1) p.2 = 2

theorem CartanMatrix.Realisation.idx_subset_span_int_sprod_span_int {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : rl.idx ⊆ ↑(Submodule.span ℤ (Set.range rl.sRoot)) ×ˢ ↑(Submodule.span ℤ (Set.range rl.sCoroot))

instance CartanMatrix.Realisation.instFiniteElemProdIdx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) : Finite ↑rl.idx

def CartanMatrix.Realisation.reflectionPair {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {p : M × N} (hp : p ∈ rl.idx) : (M ≃ₗ[R] M) × N ≃ₗ[R] N

The (co)reflection determined by a root / coroot pair.

Equations

• rl.reflectionPair hp = (Module.reflection ⋯, Module.reflection ⋯)

theorem CartanMatrix.Realisation.reflectionPair_mem {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) {p : M × N} (hp : p ∈ rl.idx) : rl.reflectionPair hp ∈ rl.weylGroup

theorem CartanMatrix.Realisation.injOn_fst {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : Set.InjOn Prod.fst rl.idx

theorem CartanMatrix.Realisation.injOn_snd {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : Set.InjOn Prod.snd rl.idx

noncomputable def CartanMatrix.Realisation.toRootPairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : RootPairing (↑rl.idx) R M N

The root pairing associated to a realisation of a Cartan matrix.

Equations

• rl.toRootPairing = RootPairing.mk' rl.pairing { toFun := fun (p : ↑rl.idx) => (↑p).1, inj' := ⋯ } { toFun := fun (p : ↑rl.idx) => (↑p).2, inj' := ⋯ } ⋯ ⋯ ⋯

@[simp]

theorem CartanMatrix.Realisation.toRootPairing_root {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] (i : ↑rl.idx) : rl.toRootPairing.root i = (↑i).1

@[simp]

theorem CartanMatrix.Realisation.toRootPairing_coroot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] (i : ↑rl.idx) : rl.toRootPairing.coroot i = (↑i).2

@[simp]

theorem CartanMatrix.Realisation.toRootPairing_toLinearMap {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : rl.toRootPairing.toLinearMap = rl.pairing

theorem CartanMatrix.Realisation.toRootPairing_pairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] (i j : ↑rl.idx) : rl.toRootPairing.pairing i j = (rl.pairing (↑i).1) (↑j).2

instance CartanMatrix.Realisation.instIsCrystallographicElemProdIdxToRootPairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : rl.toRootPairing.IsCrystallographic

theorem CartanMatrix.Realisation.eq_one_or_neg_one_of_eq_zsmul_sRoot {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] {p : M × N} (hp : p ∈ rl.idx) {z : ℤ} {j : n} (h : p.1 = z • rl.sRoot j) : z = 1 ∨ z = -1

instance CartanMatrix.Realisation.instIsReducedElemProdIdxToRootPairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : rl.toRootPairing.IsReduced

theorem CartanMatrix.Realisation.isRootSystem_toRootPairing {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] (hr : Submodule.span R (Set.range rl.sRoot) = ⊤) (hc : Submodule.span R (Set.range rl.sCoroot) = ⊤) : rl.toRootPairing.IsRootSystem

theorem CartanMatrix.Realisation.isIrreducible_toRootPairing {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {k : Type u_5} {V : Type u_6} {W : Type u_7} [Field k] [CharZero k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (rl : Realisation n k V W) (hr : Submodule.span k (Set.range rl.sRoot) = ⊤) (hA' : rl.matrix.IsIndecomposable) : rl.toRootPairing.IsIrreducible

def CartanMatrix.Realisation.baseIdx {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : n ↪ ↑rl.idx

The simple (co)roots are naturally parameterised by the index type of the Cartan matrix.

Equations

• rl.baseIdx = { toFun := fun (i : n) => ⟨(rl.sRoot i, rl.sCoroot i), ⋯⟩, inj' := ⋯ }

@[simp]

theorem CartanMatrix.Realisation.baseIdx_apply {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] (i : n) : rl.baseIdx i = ⟨(rl.sRoot i, rl.sCoroot i), ⋯⟩

noncomputable def CartanMatrix.Realisation.rootPairingBase {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : rl.toRootPairing.Base

The base carried by the root pairing associated to a realisation of a Cartan matrix.

Equations

• rl.rootPairingBase = RootPairing.Base.mkOfPairwiseLEZero rl.toRootPairing ⋯ ⋯ ⋯ ⋯

noncomputable def CartanMatrix.Realisation.rootPairingBaseEquiv {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : n ≃ ↥rl.rootPairingBase.support

The indexing type of a Cartan matrix realisation bijects to the support of the base carried by the corresponding root pairing.

Equations

• rl.rootPairingBaseEquiv = (Equiv.ofInjective ⇑rl.baseIdx ⋯).trans (Equiv.subtypeEquivRight ⋯)

@[simp]

theorem CartanMatrix.Realisation.val_rootPairingBaseEquiv_apply {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] (i : n) : ↑(rl.rootPairingBaseEquiv i) = ⟨(rl.sRoot i, rl.sCoroot i), ⋯⟩

@[simp]

theorem CartanMatrix.Realisation.rootPairingBase_cartanMatrix_eq {n : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rl : Realisation n R M N) [CharZero R] [IsDomain R] : rl.rootPairingBase.cartanMatrix.submatrix ⇑rl.rootPairingBaseEquiv ⇑rl.rootPairingBaseEquiv = rl.matrix

noncomputable def Matrix.IsFiniteCartan.toRealisation {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (hAI : Invertible (A.map Int.cast)) : CartanMatrix.Realisation n R (n → R) (n → R)

If a Cartan matrix is invertible in R then it has a canonical realisation.

Equations

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

noncomputable def Matrix.IsFiniteCartan.toRootPairing {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : RootPairing (↑(hA.toRealisation ⋯.invertible).idx) k (n → k) (n → k)

Given a field k of chacteristic zero and Cartan matrix A, this is a reduced crystrallographic root system over k. It carries a natural base with Cartan matrix A.

Equations

• hA.toRootPairing k = (hA.toRealisation ⋯.invertible).toRootPairing

instance Matrix.IsFiniteCartan.instIsReducedElemProdForallIdxToRealisationInvertibleToRootPairing {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : (hA.toRootPairing k).IsReduced

instance Matrix.IsFiniteCartan.instIsCrystallographicElemProdForallIdxToRealisationInvertibleToRootPairing {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : (hA.toRootPairing k).IsCrystallographic

instance Matrix.IsFiniteCartan.instIsRootSystemElemProdForallIdxToRealisationInvertibleToRootPairing {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : (hA.toRootPairing k).IsRootSystem

theorem Matrix.IsFiniteCartan.isIrreducible_toRootPairing {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] [Nonempty n] (hA' : A.IsIndecomposable) : (hA.toRootPairing k).IsIrreducible

noncomputable def Matrix.IsFiniteCartan.rootPairingBase {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : (hA.toRootPairing k).Base

The base of the root system defined by a Cartan matrix.

Equations

• hA.rootPairingBase k = (hA.toRealisation ⋯.invertible).rootPairingBase

noncomputable def Matrix.IsFiniteCartan.rootPairingBaseEquiv {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : n ≃ ↥(hA.rootPairingBase k).support

The Cartan matrix indexing type indexes the elements of the support of the base.

Equations

• hA.rootPairingBaseEquiv k = (hA.toRealisation ⋯.invertible).rootPairingBaseEquiv

@[simp]

theorem Matrix.IsFiniteCartan.rootPairingBase_cartanMatrix_eq {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℤ} (hA : A.IsFiniteCartan) (k : Type u_5) [Field k] [CharZero k] : (hA.rootPairingBase k).cartanMatrix.submatrix ⇑(hA.rootPairingBaseEquiv k) ⇑(hA.rootPairingBaseEquiv k) = A