Symmetric
Results named in Tau Ceti's TauCeti.RepresentationTheory.Symmetric modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremFrobenius's formula#
the power-sum product of a partition ρ of n expands in the Schur
polynomials as p_ρ = ∑_{λ ⊢ n} χ^λ(ρ) s_λ, the coefficients being the column of ρ in the
character table of Sₙ. This holds in every finite alphabet and over every commutative ring; the
Schur polynomials of the partitions with more parts than the alphabet has letters vanish.
TauCeti.psumPart_eq_sum_spechtCharValue_smul_schurPoly.{u_1, u_2} {n : ℕ} {σ : Type u_1} [Fintype σ]
(R : Type u_2) [CommRing R] (ρ : n.Partition) :
MvPolynomial.psumPart σ R ρ = ∑ l, TauCeti.spechtCharValue l ρ • TauCeti.schurPoly σ R l
Lean
Formalized in Tau Ceti as TauCeti.psumPart_eq_sum_spechtCharValue_smul_schurPoly.
Sources
Uses 3
TheoremThe inverse of Frobenius's formula#
weighting the power-sum products over the cycle types by
a Specht character recovers the Schur polynomial, ∑_{π ∈ Sₙ} χ^μ(π) p_{ρ(π)} = n! s_μ. Over a
ℚ-algebra this says that (1 / n!) ∑_π χ^μ(π) p_{ρ(π)} is s_μ.
TauCeti.sum_spechtChar_smul_psumPart.{u_1, u_2} {n : ℕ} {σ : Type u_1} [Fintype σ] (R : Type u_2)
[CommRing R] (μ : n.Partition) :
∑ π, TauCeti.spechtChar μ π • MvPolynomial.psumPart σ R π.partition =
n.factorial • TauCeti.schurPoly σ R μ
Uses 3 · Used by 2
TheoremJames's dominance lemma#
If the column antisymmetrizer of a lam-tableau t does not
annihilate the μ-tabloid q, then the shape of t dominates μ.
This is the statement the classification of the Specht modules consumes: a homomorphism
M^{lam} → M^μ that does not kill the polytabloid b_t · {t} carries it to a combination of the
vectors b_t · q, so one of those is nonzero and the shape of t dominates μ.
TauCeti.dominates_of_asAlgebraHom_columnAntisymmetrizer_ne_zero {lam : YoungDiagram}
(t : TauCeti.YoungTableau lam) (μ : lam.card.Partition)
(q : Equiv.Perm (Fin lam.card) ⧸ TauCeti.youngSubgroup μ)
(h :
((TauCeti.permutationModule μ).ρ.asAlgebraHom t.columnAntisymmetrizer)
(MonoidAlgebra.single q 1) ≠
0) :
(TauCeti.shapePartition lam).Dominates μ
Lean
Formalized in Tau Ceti as TauCeti.dominates_of_asAlgebraHom_columnAntisymmetrizer_ne_zero.
Other forms
James's dominance lemma for an arbitrary vector. Formalized in Tau Ceti as TauCeti.YoungTableau.dominates_of_asAlgebraHom_columnAntisymmetrizer_apply_ne_zero.
TauCeti.YoungTableau.dominates_of_asAlgebraHom_columnAntisymmetrizer_apply_ne_zero
{lam : YoungDiagram} (t : TauCeti.YoungTableau lam) (μ : lam.card.Partition)
{x : ↑(TauCeti.permutationModule μ)}
(hx : ((TauCeti.permutationModule μ).ρ.asAlgebraHom t.columnAntisymmetrizer) x ≠ 0) :
(TauCeti.shapePartition lam).Dominates μ
Sources
Used by 2
TheoremJames's submodule theorem#
A subrepresentation U of the Young permutation module M^μ
either contains the Specht module S^μ or is orthogonal to it for the tabloid form.
The dichotomy is whether some column antisymmetrizer b_t fails to annihilate some vector of U.
If it does fail, the value is a nonzero multiple of the polytabloid e_t and lies in U, so U
contains the orbit of e_t, which spans S^μ. If every b_t annihilates every vector of U,
then self-adjointness of b_t moves it off each polytabloid e_t = b_t · {t} and onto the vector
of U, where it vanishes.
TauCeti.spechtSubrepresentation_le_or_le_orthogonal (μ : YoungDiagram)
(U : Subrepresentation (TauCeti.permutationModule (TauCeti.shapePartition μ)).ρ) :
TauCeti.spechtSubrepresentation μ ≤ U ∨
U ≤ TauCeti.orthogonalSubrepresentation (TauCeti.spechtSubrepresentation μ)
Lean
Formalized in Tau Ceti as TauCeti.spechtSubrepresentation_le_or_le_orthogonal.
Sources
TheoremSchur-Weyl duality: the commutant of the image of k[S_d] is the image of k[GLₙ]#
TauCeti.centralizer_range_permTensorActionAlgHom_eq_range_tensorPowerRep_asAlgebraHom.{u_1}
{k : Type u_1} {n d : ℕ} [Field k] [Infinite k] [NeZero ↑d.factorial] :
Subalgebra.centralizer k (Set.range ⇑(TauCeti.permTensorActionAlgHom k n d)) =
(TauCeti.tensorPowerRep k n d).asAlgebraHom.range
Lean
Formalized in Tau Ceti as TauCeti.centralizer_range_permTensorActionAlgHom_eq_range_tensorPowerRep_asAlgebraHom.
Other forms
Schur-Weyl duality. Formalized in Tau Ceti as TauCeti.centralizer_span_range_map_const_eq_range_permTensorActionAlgHom.
TauCeti.centralizer_span_range_map_const_eq_range_permTensorActionAlgHom.{u_1} {k : Type u_1}
{n d : ℕ} [Field k] [NeZero ↑d.factorial] :
Subalgebra.centralizer k ↑(Submodule.span k (Set.range fun f => PiTensorProduct.map fun x => f)) =
(TauCeti.permTensorActionAlgHom k n d).range
Schur-Weyl duality for the group ranges. Formalized in Tau Ceti as TauCeti.centralizer_range_permTensorAction_eq_range_tensorPowerRep_asAlgebraHom.
TauCeti.centralizer_range_permTensorAction_eq_range_tensorPowerRep_asAlgebraHom.{u_1} {k : Type u_1}
{n d : ℕ} [Field k] [Infinite k] [NeZero ↑d.factorial] :
Subalgebra.centralizer k (Set.range ⇑(TauCeti.permTensorAction k n d)) =
(TauCeti.tensorPowerRep k n d).asAlgebraHom.range
Schur-Weyl duality for the group ranges. Formalized in Tau Ceti as TauCeti.centralizer_range_tensorPowerRep_eq_range_permTensorActionAlgHom.
TauCeti.centralizer_range_tensorPowerRep_eq_range_permTensorActionAlgHom.{u_1} {k : Type u_1}
{n d : ℕ} [Field k] [Infinite k] [NeZero ↑d.factorial] :
Subalgebra.centralizer k (Set.range ⇑(TauCeti.tensorPowerRep k n d)) =
(TauCeti.permTensorActionAlgHom k n d).range
Schur-Weyl duality, as a membership criterion. Formalized in Tau Ceti as TauCeti.mem_range_permTensorActionAlgHom_iff_forall_commute.
TauCeti.mem_range_permTensorActionAlgHom_iff_forall_commute.{u_1} {k : Type u_1} {n d : ℕ} [Field k]
[NeZero ↑d.factorial] (x : Module.End k (PiTensorProduct k fun x => Fin n → k)) :
x ∈ (TauCeti.permTensorActionAlgHom k n d).range ↔
∀ (f : (Fin n → k) →ₗ[k] Fin n → k), Commute x (PiTensorProduct.map fun x => f)
Schur-Weyl duality, as a membership criterion. Formalized in Tau Ceti as TauCeti.mem_range_permTensorActionAlgHom_iff_forall_commute_tensorPowerRep.
TauCeti.mem_range_permTensorActionAlgHom_iff_forall_commute_tensorPowerRep.{u_1} {k : Type u_1}
{n d : ℕ} [Field k] [Infinite k] [NeZero ↑d.factorial]
(x : Module.End k (PiTensorProduct k fun x => Fin n → k)) :
x ∈ (TauCeti.permTensorActionAlgHom k n d).range ↔
∀ (g : GL (Fin n) k), Commute x ((TauCeti.tensorPowerRep k n d) g)
Schur-Weyl duality, as a membership criterion. Formalized in Tau Ceti as TauCeti.mem_range_tensorPowerRep_asAlgebraHom_iff_forall_commute_permTensorAction.
TauCeti.mem_range_tensorPowerRep_asAlgebraHom_iff_forall_commute_permTensorAction.{u_1}
{k : Type u_1} {n d : ℕ} [Field k] [Infinite k] [NeZero ↑d.factorial]
(x : Module.End k (PiTensorProduct k fun x => Fin n → k)) :
x ∈ (TauCeti.tensorPowerRep k n d).asAlgebraHom.range ↔
∀ (σ : Equiv.Perm (Fin d)), Commute x ((TauCeti.permTensorAction k n d) σ)
Schur-Weyl duality: the commutant of the image of k[GLₙ] is the image of k[S_d]. Formalized in Tau Ceti as TauCeti.centralizer_range_tensorPowerRep_asAlgebraHom_eq_range_permTensorActionAlgHom.
TauCeti.centralizer_range_tensorPowerRep_asAlgebraHom_eq_range_permTensorActionAlgHom.{u_1}
{k : Type u_1} {n d : ℕ} [Field k] [Infinite k] [NeZero ↑d.factorial] :
Subalgebra.centralizer k (Set.range ⇑(TauCeti.tensorPowerRep k n d).asAlgebraHom) =
(TauCeti.permTensorActionAlgHom k n d).range
Sources
Uses 1 · Used by 1
DefinitionThe standard basis theorem#
The polytabloids of the standard μ-tableaux are a basis of
the Specht module S^μ: they are linearly independent by
TauCeti.linearIndependent_polytabloid and they span by
TauCeti.spechtSubrepresentation_eq_span_standard.
TauCeti.standardPolytabloidBasis (μ : YoungDiagram) :
Module.Basis (TauCeti.StandardYoungTableau μ) ℚ ↥(TauCeti.spechtSubrepresentation μ).toSubmodule
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.