Classical Groups
Results named in Tau Ceti's TauCeti.RepresentationTheory.ClassicalGroups modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremBrauer duality on the tensor square#
Over a field K with 2 ≠ 0 that has a point
(c, s) of the unit circle with c ≠ 0 and s ≠ 0, the image of the Brauer algebra B₂(n) in
the endomorphisms of (Kⁿ)^{⊗2} is the commutant of the diagonal action of the orthogonal group:
an operator commuting with every g ⊗ g is a combination of the identity, the flip of the two
tensor factors and the cup-cap generator.
TauCeti.range_brauerActionOrth_two_eq_centralizer_of_sq_add_sq_eq_one.{u_1} (K : Type u_1) [Field K]
(n : ℕ) (h2 : 2 ≠ 0) {c s : K} (hcs : c ^ 2 + s ^ 2 = 1) (hc : c ≠ 0) (hs : s ≠ 0) :
(TauCeti.brauerActionOrth K n 2).range =
Subalgebra.centralizer K (Set.range ⇑((TauCeti.stdOrthogonalRep K n).tensorPower 2))
Lean
Formalized in Tau Ceti as TauCeti.range_brauerActionOrth_two_eq_centralizer_of_sq_add_sq_eq_one.
Other forms
Brauer duality for the orthogonal group on two strands. Formalized in Tau Ceti as TauCeti.range_brauerActionOrth_two_eq_centralizer_of_noZeroDivisors.
TauCeti.range_brauerActionOrth_two_eq_centralizer_of_noZeroDivisors.{u} (R : Type u) [CommRing R]
(n : ℕ) [NoZeroDivisors R] (h2 : 2 ≠ 0) (hrot : ∃ c s, c ^ 2 + s ^ 2 = 1 ∧ c * s ≠ 0) :
(TauCeti.brauerActionOrth R n 2).range =
Subalgebra.centralizer R (Set.range ⇑((TauCeti.stdOrthogonalRep R n).tensorPower 2))
Brauer duality for the symplectic group on two strands. Formalized in Tau Ceti as TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer.
TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer.{u_1} {K : Type u_1} [CommRing K]
{n : ℕ} [IsDomain K] (ht : ∃ t, ∀ (m : ℕ), 0 < m → m ≤ 4 → t ^ m ≠ 1) :
K[TauCeti.symplecticCrossing K n, TauCeti.symplecticCupCap K n] =
Subalgebra.centralizer K (Set.range ⇑((TauCeti.stdSymplecticRep K n).tensorPower 2))
Brauer duality for the symplectic group on two strands in characteristic zero, for instance over ℂ. Formalized in Tau Ceti as TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer_of_charZero.
TauCeti.adjoin_symplecticCrossing_symplecticCupCap_eq_centralizer_of_charZero.{u_1} {K : Type u_1}
[Field K] [CharZero K] {n : ℕ} :
K[TauCeti.symplecticCrossing K n, TauCeti.symplecticCupCap K n] =
Subalgebra.centralizer K (Set.range ⇑((TauCeti.stdSymplecticRep K n).tensorPower 2))
Brauer duality on the tensor square in characteristic zero. Formalized in Tau Ceti as TauCeti.range_brauerActionOrth_two_eq_centralizer.
TauCeti.range_brauerActionOrth_two_eq_centralizer.{u_1} (K : Type u_1) [Field K] [CharZero K]
(n : ℕ) :
(TauCeti.brauerActionOrth K n 2).range =
Subalgebra.centralizer K (Set.range ⇑((TauCeti.stdOrthogonalRep K n).tensorPower 2))
Sources
TheoremThe Gelfand–Tsetlin decomposition#
The rational Weyl module V_λ of GL n ℂ is the
internal direct sum of the Gelfand–Tsetlin lines of the patterns with top weight λ.
TauCeti.isInternal_gtLine {n : ℕ} (l : TauCeti.DominantWeight n) :
DirectSum.IsInternal (TauCeti.gtLine l)
TheoremThe Gelfand-Tsetlin dimension formula#
The Gelfand-Tsetlin patterns with top row a
weakly decreasing sequence λ are counted by the Weyl dimension formula
∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i).
Both sides are candidates for the dimension of the irreducible rational representation of GL n
with highest weight λ, but that representation and the Gelfand-Tsetlin basis are not built here
and do not enter the proof: what is proved is the identity of a lattice-point count with a product
formula, obtained by checking that both satisfy the branching recursion of GL (n + 1) ↓ GL n.
This is deliberately not a simp lemma: {P : GTPattern n // P.topRow = l} carries a Fintype
instance, so Nat.card_eq_fintype_card rewrites the left-hand side first and the simpNF linter
rejects the tag. The DominantWeight-indexed
TauCeti.GTPattern.card_topWeight_eq_weylDimension below, whose subtype has no such instance, is
the simp form.
TauCeti.GTPattern.card_topRow_eq_weylDimension {n : ℕ} (l : TauCeti.DominantWeight n) :
Nat.card { P // P.topRow = ↑l } = TauCeti.weylDimension l
Lean
Formalized in Tau Ceti as TauCeti.GTPattern.card_topRow_eq_weylDimension.
Other forms
The Gelfand-Tsetlin dimension formula, indexed by a dominant weight. Formalized in Tau Ceti as TauCeti.GTPattern.card_topWeight_eq_weylDimension.
TauCeti.GTPattern.card_topWeight_eq_weylDimension {n : ℕ} (l : TauCeti.DominantWeight n) :
Nat.card { P // P.topWeight = l } = TauCeti.weylDimension l
Sources
Used by 1
TheoremThe Schur-Weyl decomposition of the character of a tensor power#
For every g ∈ GL n k,
the character of (kⁿ)^{⊗d} at g is the sum over the partitions μ of d of the characters of
the Weyl modules 𝕊^μ(kⁿ) at g, each weighted by the dimension f^μ of the Specht module
S^μ.
TauCeti.sum_finrank_spechtModule_mul_char_weylRepOfShape_ofPartition.{u} {k : Type u} [Field k]
[CharZero k] {n : ℕ} (d : ℕ) (g : GL (Fin n) k) :
∑ μ,
↑(Module.finrank ℚ ↑(TauCeti.spechtModule μ).V) *
(TauCeti.weylRepOfShape k n (YoungDiagram.ofPartition μ)).character g =
(TauCeti.tensorPowerRep k n d).character g
Lean
Formalized in Tau Ceti as TauCeti.sum_finrank_spechtModule_mul_char_weylRepOfShape_ofPartition.
Other forms
The Schur-Weyl decomposition of the character of the bundled tensor power. Formalized in Tau Ceti as TauCeti.sum_finrank_spechtModule_mul_char_weylFDRepOfShape_ofPartition.
TauCeti.sum_finrank_spechtModule_mul_char_weylFDRepOfShape_ofPartition.{u} {k : Type u} [Field k]
[CharZero k] {n : ℕ} (d : ℕ) (g : GL (Fin n) k) :
∑ μ,
↑(Module.finrank ℚ ↑(TauCeti.spechtModule μ).V) *
(TauCeti.weylFDRepOfShape k n (YoungDiagram.ofPartition μ)).character g =
(TauCeti.tensorPowerFDRep k n d).character g
Sources
Uses 1
TheoremThe Weyl dimension formula for GL n#
over a field of characteristic zero, the rational
Weyl module of a dominant weight λ has dimension ∏_{i < j} (λᵢ - λⱼ + j - i) / (j - i), the
Weyl dimension of λ.
TauCeti.finrank_rationalWeylFDRep.{u} (k : Type u) [Field k] [CharZero k] (n : ℕ)
(l : TauCeti.DominantWeight n) :
Module.finrank k ↑(TauCeti.rationalWeylFDRep k n l).V = TauCeti.weylDimension l
Lean
Formalized in Tau Ceti as TauCeti.finrank_rationalWeylFDRep.
Other forms
The Weyl dimension formula for SO (2n + 1) in its product form. Formalized in Tau Ceti as TauCeti.oddOrthogonalWeylDimension_eq_prod_prod_div.
TauCeti.oddOrthogonalWeylDimension_eq_prod_prod_div (n : ℕ) (μ : YoungDiagram) :
↑(TauCeti.oddOrthogonalWeylDimension n μ) =
∏ i ∈ Finset.range n,
(↑(μ.rowLen i) + ↑n - ↑i - 1 / 2) / (↑n - ↑i - 1 / 2) *
∏ j ∈ Finset.Ico (i + 1) n,
((↑(μ.rowLen i) + ↑n - ↑i - 1 / 2) ^ 2 - (↑(μ.rowLen j) + ↑n - ↑j - 1 / 2) ^ 2) /
((↑n - ↑i - 1 / 2) ^ 2 - (↑n - ↑j - 1 / 2) ^ 2)
The Weyl dimension formula for SO (2n) in its product form. Formalized in Tau Ceti as TauCeti.evenOrthogonalWeylDimension_eq_prod_prod_div.
TauCeti.evenOrthogonalWeylDimension_eq_prod_prod_div (n : ℕ) (μ : YoungDiagram) :
↑(TauCeti.evenOrthogonalWeylDimension n μ) =
∏ i ∈ Finset.range n,
∏ j ∈ Finset.Ico (i + 1) n,
((↑(μ.rowLen i) + ↑n - 1 - ↑i) ^ 2 - (↑(μ.rowLen j) + ↑n - 1 - ↑j) ^ 2) /
((↑n - 1 - ↑i) ^ 2 - (↑n - 1 - ↑j) ^ 2)
The Weyl dimension formula for Sp 2n in its product form. Formalized in Tau Ceti as TauCeti.symplecticWeylDimension_eq_prod_prod_div.
TauCeti.symplecticWeylDimension_eq_prod_prod_div (n : ℕ) (μ : YoungDiagram) :
↑(TauCeti.symplecticWeylDimension n μ) =
∏ i ∈ Finset.range n,
↑(TauCeti.symplecticRhoShift n μ i) / (↑n - ↑i) *
∏ j ∈ Finset.Ico (i + 1) n,
(↑(TauCeti.symplecticRhoShift n μ i) ^ 2 - ↑(TauCeti.symplecticRhoShift n μ j) ^ 2) /
((↑n - ↑i) ^ 2 - (↑n - ↑j) ^ 2)
The Weyl dimension formula in its quotient form. Formalized in Tau Ceti as TauCeti.weylDimension_eq_prod_prod_div.
TauCeti.weylDimension_eq_prod_prod_div {n : ℕ} (l : TauCeti.DominantWeight n) :
↑(TauCeti.weylDimension l) = ∏ i, ∏ j > i, (↑(↑l i) - ↑(↑l j) + (↑↑j - ↑↑i)) / (↑↑j - ↑↑i)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.