Cartan matrices for root systems #
This file contains definitions and basic results about Cartan matrices of root pairings / systems.
Main definitions: #
RootPairing.Base.cartanMatrix: the Cartan matrix of a crystallographic root pairing, with respect to a baseb.RootPairing.Base.cartanMatrix_nondegenerate: the Cartan matrix is non-degenerate.RootPairing.Base.induction_on_cartanMatrix: an induction principle expressing the connectedness of the Dynkin diagram of an irreducible root pairing.RootPairing.Base.equivOfCartanMatrixEq: a root system is determined by its Cartan matrix.
def
RootPairing.Base.cartanMatrixIn
{ι : 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]
(S : Type u_5)
[CommRing S]
[Algebra S R]
{P : RootPairing ι R M N}
[P.IsValuedIn S]
(b : P.Base)
:
The Cartan matrix of a root pairing, taking values in S, with respect to a base b.
See also RootPairing.Base.cartanMatrix.
Equations
Instances For
theorem
RootPairing.Base.cartanMatrixIn_def
{ι : 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]
(S : Type u_5)
[CommRing S]
[Algebra S R]
{P : RootPairing ι R M N}
[P.IsValuedIn S]
(b : P.Base)
(i j : { x : ι // x ∈ b.support })
:
@[simp]
theorem
RootPairing.Base.algebraMap_cartanMatrixIn_apply
{ι : 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]
(S : Type u_5)
[CommRing S]
[Algebra S R]
{P : RootPairing ι R M N}
[P.IsValuedIn S]
(b : P.Base)
(i j : { x : ι // x ∈ b.support })
:
@[simp]
theorem
RootPairing.Base.cartanMatrixIn_apply_same
{ι : 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]
(S : Type u_5)
[CommRing S]
[Algebra S R]
{P : RootPairing ι R M N}
[P.IsValuedIn S]
(b : P.Base)
[FaithfulSMul S R]
(i : { x : ι // x ∈ b.support })
:
theorem
RootPairing.Base.cartanMatrixIn_mul_diagonal_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]
(S : Type u_5)
[CommRing S]
[Algebra S R]
{P : RootSystem ι R M N}
[P.IsValuedIn S]
(B : P.InvariantForm)
(b : P.Base)
[DecidableEq ι]
:
((cartanMatrixIn S b).map ⇑(algebraMap S R) * Matrix.diagonal fun (i : { x : ι // x ∈ b.support }) => (B.form (P.root ↑i)) (P.root ↑i)) = 2 • (BilinForm.toMatrix b.toWeightBasis) B.form
theorem
RootPairing.Base.cartanMatrixIn_nondegenerate
{ι : 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]
(S : Type u_5)
[CommRing S]
[Algebra S R]
[IsDomain R]
[NeZero 2]
[FaithfulSMul S R]
[IsDomain S]
{P : RootSystem ι R M N}
[P.IsValuedIn S]
[Fintype ι]
[P.IsAnisotropic]
(b : P.Base)
:
(cartanMatrixIn S b).Nondegenerate
@[reducible, inline]
abbrev
RootPairing.Base.cartanMatrix
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
:
The Cartan matrix of a crystallographic root pairing, with respect to a base b.
Equations
Instances For
theorem
RootPairing.Base.cartanMatrix_apply_same
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
(i : { x : ι // x ∈ b.support })
:
theorem
RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
{i j : { x : ι // x ∈ b.support }}
:
theorem
RootPairing.Base.cartanMatrix_apply_eq_zero_iff_symm
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
{i j : { x : ι // x ∈ b.support }}
:
theorem
RootPairing.Base.cartanMatrix_le_zero_of_ne
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
(i j : { x : ι // x ∈ b.support })
(h : i ≠ j)
:
theorem
RootPairing.Base.cartanMatrix_mem_of_ne
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
{i j : { x : ι // x ∈ b.support }}
(hij : i ≠ j)
:
theorem
RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
{i j : { x : ι // x ∈ b.support }}
(hij : i ≠ j)
:
theorem
RootPairing.Base.cartanMatrix_apply_eq_zero_iff
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
{i j : { x : ι // x ∈ b.support }}
(hij : i ≠ j)
:
theorem
RootPairing.Base.abs_cartanMatrix_apply
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
[DecidableEq ι]
{i j : { x : ι // x ∈ b.support }}
:
@[simp]
theorem
RootPairing.Base.cartanMatrix_map_abs
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
[DecidableEq ι]
:
theorem
RootPairing.Base.cartanMatrix_nondegenerate
{ι : 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]
[CharZero R]
[IsDomain R]
[Finite ι]
{P : RootSystem ι R M N}
[P.IsCrystallographic]
(b : P.Base)
:
theorem
RootPairing.Base.induction_on_cartanMatrix
{ι : 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]
{P : RootPairing ι R M N}
(b : P.Base)
[P.IsCrystallographic]
[CharZero R]
[IsDomain R]
[Finite ι]
[P.IsReduced]
[P.IsIrreducible]
(p : { x : ι // x ∈ b.support } → Prop)
{i j : { x : ι // x ∈ b.support }}
(hi : p i)
(hp : ∀ (i j : { x : ι // x ∈ b.support }), p i → b.cartanMatrix j i ≠ 0 → p j)
:
p j
A characterisation of the connectedness of the Dynkin diagram for irreducible root pairings.
theorem
RootPairing.Base.injective_pairingIn
{ι : 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]
[CharZero R]
[IsDomain R]
[Finite ι]
{P : RootSystem ι R M N}
[P.IsCrystallographic]
(b : P.Base)
:
theorem
RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne
{ι : Type u_1}
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[AddCommGroup N]
[Finite ι]
{K : Type u_6}
[Field K]
[CharZero K]
[Module K M]
[Module K N]
{P : RootSystem ι K M N}
[P.IsCrystallographic]
(b : P.Base)
:
theorem
RootPairing.Base.apply_mem_range_root_of_cartanMatrixEq
{ι : 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]
[CharZero R]
[IsDomain R]
[Finite ι]
{ι₂ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_8}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootSystem ι R M N}
[P.IsCrystallographic]
[P.IsReduced]
(b : P.Base)
{P₂ : RootSystem ι₂ R M₂ N₂}
[P₂.IsCrystallographic]
(b₂ : P₂.Base)
(e : { x : ι // x ∈ b.support } ≃ { x : ι₂ // x ∈ b₂.support })
(f : M ≃ₗ[R] M₂)
(hf : ∀ (i : { x : ι // x ∈ b.support }), f (P.root ↑i) = P₂.root ↑(e i))
(m : M)
(hm : m ∈ Set.range ⇑P.root)
(he : ∀ (i j : { x : ι // x ∈ b.support }), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j)
:
def
RootPairing.Base.equivOfCartanMatrixEq
{ι : 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]
[CharZero R]
[IsDomain R]
[Finite ι]
{ι₂ : Type u_6}
{M₂ : Type u_7}
{N₂ : Type u_8}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup N₂]
[Module R N₂]
{P : RootSystem ι R M N}
[P.IsCrystallographic]
[P.IsReduced]
(b : P.Base)
{P₂ : RootSystem ι₂ R M₂ N₂}
[P₂.IsCrystallographic]
(b₂ : P₂.Base)
(e : { x : ι // x ∈ b.support } ≃ { x : ι₂ // x ∈ b₂.support })
[Finite ι₂]
[P₂.IsReduced]
(he : ∀ (i j : { x : ι // x ∈ b.support }), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j)
:
P.Equiv P₂.toRootPairing
A root system is determined by its Cartan matrix.
Equations
- One or more equations did not get rendered due to their size.