Other results

Results named in the rest of Tau Ceti's TauCeti.RepresentationTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBurnside density theorem#

The monoid algebra of a finite-dimensional irreducible representation over an algebraically closed field exhausts the full endomorphism algebra.

Jacobson density gives all endomorphisms linear over the representation's commuting endomorphism ring. Schur's lemma identifies that ring with the base field, so these are exactly the k-linear endomorphisms.

Representation.asAlgebraHom_surjective_of_isIrreducible.{u_1, u_2, u_3} {k : Type u_1}
  {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [_root_.Module k V]
  [IsAlgClosed k] [FiniteDimensional k V] (ρ : Representation k G V) (hρ : ρ.IsIrreducible) :
  Function.Surjective ⇑ρ.asAlgebraHom

Lean

Formalized in Tau Ceti as Representation.asAlgebraHom_surjective_of_isIrreducible.

Sources

• Tau Ceti documentation: Representation.asAlgebraHom_surjective_of_isIrreducible
• Source of Representation.asAlgebraHom_surjective_of_isIrreducible in TauCeti/RepresentationTheory/Irreducible.lean

LeanRepresentation.asAlgebraHom_surjective_of_isIrreducible

Uses 1 · Used by 1

Proof usesSchur's lemma, vanishing form

Used byKolchin's common fixed vector theorem

TheoremFrobenius reciprocity for coind₁, uniqueness#

Two intertwining maps into a coinduced representation that agree after evaluation at 1 are equal.

ContIntertwiningMap.coind₁_ext.{u_1, u_2, u_3, u_4} {R : Type u_1} {G : Type u_2} {V : Type u_3}
  {W : Type u_4} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [AddCommGroup V] [_root_.Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V]
  [AddCommGroup W] [_root_.Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W]
  [ContinuousSMul R W] {π : ContRepresentation R G V} {σ : ContRepresentation R G W}
  {f g : ContIntertwiningMap π σ.coind₁} (h : ∀ (v : V), (f v) 1 = (g v) 1) : f = g

Lean

Formalized in Tau Ceti as ContIntertwiningMap.coind₁_ext.

Sources

• Tau Ceti documentation: ContIntertwiningMap.coind₁_ext
• Source of ContIntertwiningMap.coind₁_ext in TauCeti/RepresentationTheory/Continuous/Coinduced.lean

LeanContIntertwiningMap.coind₁_ext

Used by 2

Used byTauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass · TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal

TheoremFrobenius's theorem returns the normal complement it was handed#

If G = N ⋊ H with N normal and H a trivial-intersection subgroup, then the subgroup that the exceptional-character argument above constructs -- out of the irreducible characters of H, with no reference to N -- is N itself.

This is what makes the abstract construction checkable on a concrete Frobenius group, which comes presented as such a decomposition with H acting on N without nonidentity fixed points (TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree).

TauCeti.frobeniusKernelSubgroup_eq_of_isComplement'.{u} {G : Type u} [Group G] [Finite G]
  {H N : Subgroup G} [N.Normal] (hH : TauCeti.IsTISubgroup H) (hNH : N.IsComplement' H) :
  TauCeti.frobeniusKernelSubgroup hH = N

Lean

Formalized in Tau Ceti as TauCeti.frobeniusKernelSubgroup_eq_of_isComplement'.

Sources

• Tau Ceti documentation: TauCeti.frobeniusKernelSubgroup_eq_of_isComplement'
• Source of TauCeti.frobeniusKernelSubgroup_eq_of_isComplement' in TauCeti/RepresentationTheory/FrobeniusGroup/Basic.lean

LeanTauCeti.frobeniusKernelSubgroup_eq_of_isComplement'

Uses 1

Proof usesFrobenius reciprocity for class functions

TheoremFrobenius's theorem: the Frobenius kernel is normal#

TauCeti.frobeniusKernelSubgroup_normal.{u} {G : Type u} [Group G] [Finite G] {H : Subgroup G}
  (hH : TauCeti.IsTISubgroup H) : (TauCeti.frobeniusKernelSubgroup hH).Normal

Lean

Formalized in Tau Ceti as TauCeti.frobeniusKernelSubgroup_normal.

Sources

• Tau Ceti documentation: TauCeti.frobeniusKernelSubgroup_normal
• Source of TauCeti.frobeniusKernelSubgroup_normal in TauCeti/RepresentationTheory/FrobeniusGroup/Basic.lean

LeanTauCeti.frobeniusKernelSubgroup_normal

Uses 1

Proof usesFrobenius reciprocity for class functions

TheoremMaschke's theorem for intertwining maps#

Over a field in which the order of the finite group G is invertible, an injective intertwining map f : ρ → σ has an intertwining left inverse p : σ → ρ, that is, p ∘ f = id.

Representation.IntertwiningMap.exists_leftInverse_of_injective.{u_1, u_2, u_3, u_4} {k : Type u_1}
  {G : Type u_2} {V : Type u_3} {W : Type u_4} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)]
  [AddCommGroup V] [_root_.Module k V] [AddCommGroup W] [_root_.Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ)
  (hf : Function.Injective ⇑f) : ∃ p, p.comp f = Representation.IntertwiningMap.id ρ

Lean

Formalized in Tau Ceti as Representation.IntertwiningMap.exists_leftInverse_of_injective.

Sources

• Tau Ceti documentation: Representation.IntertwiningMap.exists_leftInverse_of_injective
• Source of Representation.IntertwiningMap.exists_leftInverse_of_injective in TauCeti/RepresentationTheory/Maschke.lean

LeanRepresentation.IntertwiningMap.exists_leftInverse_of_injective

TheoremSchur's lemma for contravariant forms#

Over an algebraically closed field, a contravariant form on a finite-dimensional irreducible representation is a scalar multiple of any separating contravariant form.

Representation.exists_forall_apply_eq_mul_apply.{u_1, u_2, u_4} {𝕜 : Type u_1} {V : Type u_2}
  [Field 𝕜] [StarRing 𝕜] [AddCommGroup V] [_root_.Module 𝕜 V] {G : Type u_4} [Monoid G] [StarMul G]
  (ρ : Representation 𝕜 G V) [IsAlgClosed 𝕜] [FiniteDimensional 𝕜 V] [ρ.IsIrreducible]
  {B : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜} (hB : B.SeparatingRight)
  (hρ : ∀ (g : G) (x y : V), (B ((ρ g) x)) y = (B x) ((ρ (star g)) y)) {S : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜}
  (hS : ∀ (g : G) (x y : V), (S ((ρ g) x)) y = (S x) ((ρ (star g)) y)) :
  ∃ c, ∀ (x y : V), (S x) y = c * (B x) y

Lean

Formalized in Tau Ceti as Representation.exists_forall_apply_eq_mul_apply.

Other forms

Schur's lemma for pairings of nonisomorphic representations. Formalized in Tau Ceti as Representation.eq_zero_of_isEmpty_equiv.

Representation.eq_zero_of_isEmpty_equiv.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {V : Type u_2}
  {W : Type u_3} [Field 𝕜] [StarRing 𝕜] [AddCommGroup V] [_root_.Module 𝕜 V] [AddCommGroup W]
  [_root_.Module 𝕜 W] {G : Type u_4} [Monoid G] [StarMul G] (ρ : Representation 𝕜 G V)
  (σ : Representation 𝕜 G W) [FiniteDimensional 𝕜 V] [ρ.IsIrreducible] [σ.IsIrreducible]
  {B : V →ₗ⋆[𝕜] V →ₗ[𝕜] 𝕜} (hB : B.SeparatingRight)
  (hρ : ∀ (g : G) (x y : V), (B ((ρ g) x)) y = (B x) ((ρ (star g)) y)) {S : V →ₗ⋆[𝕜] W →ₗ[𝕜] 𝕜}
  (hS : ∀ (g : G) (x : V) (y : W), (S ((ρ g) x)) y = (S x) ((σ (star g)) y))
  (hne : IsEmpty (σ.Equiv ρ)) : S = 0

Sources

• Tau Ceti documentation: Representation.exists_forall_apply_eq_mul_apply
• Source of Representation.exists_forall_apply_eq_mul_apply in TauCeti/RepresentationTheory/ContravariantForm.lean

LeanRepresentation.exists_forall_apply_eq_mul_apply · Representation.eq_zero_of_isEmpty_equiv

TheoremSchur's lemma, scalar form#

Over an algebraically closed field, a linear endomorphism of a finite-dimensional irreducible representation commuting with the action is multiplication by a scalar. This is Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed read pointwise on an unbundled endomorphism.

Representation.IsIrreducible.exists_forall_apply_eq_smul.{u_1, u_2, u_3} {k : Type u_1}
  {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [_root_.Module k V]
  [IsAlgClosed k] [FiniteDimensional k V] {ρ : Representation k G V} [ρ.IsIrreducible]
  (f : V →ₗ[k] V) (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (ρ g) (f v)) : ∃ c, ∀ (v : V), f v = c • v

Lean

Formalized in Tau Ceti as Representation.IsIrreducible.exists_forall_apply_eq_smul.

Sources

• Tau Ceti documentation: Representation.IsIrreducible.exists_forall_apply_eq_smul
• Source of Representation.IsIrreducible.exists_forall_apply_eq_smul in TauCeti/RepresentationTheory/Irreducible.lean

LeanRepresentation.IsIrreducible.exists_forall_apply_eq_smul

TheoremSchur's lemma, scalar half#

Every continuous self-intertwiner of an irreducible finite-dimensional representation over an algebraically closed field is a scalar multiple of the identity.

ContRepresentation.exists_eq_smul_one_of_isIrreducible.{u_1, u_2, u_3} {𝕜 : Type u_1} {G : Type u_2}
  {V : Type u_3} [Field 𝕜] [IsAlgClosed 𝕜] [Monoid G] [AddCommGroup V] [_root_.Module 𝕜 V]
  [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousConstSMul 𝕜 V] [FiniteDimensional 𝕜 V]
  (π : ContRepresentation 𝕜 G V)
  (hirr : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible)
  (f : ContIntertwiningMap π π) : ∃ c, f = c • 1

Lean

Formalized in Tau Ceti as ContRepresentation.exists_eq_smul_one_of_isIrreducible.

Other forms

Schur's lemma, vanishing half. Formalized in Tau Ceti as ContRepresentation.eq_zero_of_isEmpty_equiv.

ContRepresentation.eq_zero_of_isEmpty_equiv.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {G : Type u_2}
  {V : Type u_3} {W : Type u_4} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G]
  [AddCommGroup V] [_root_.Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V]
  [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] [AddCommGroup W] [_root_.Module 𝕜 W]
  [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] [T2Space W]
  {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W}
  (hπ : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible)
  (hρ : (ContRepresentation.toRepresentation 𝕜 G W ρ).IsIrreducible) (hne : IsEmpty (π.Equiv ρ))
  (f : ContIntertwiningMap π ρ) : f = 0

Sources

• Tau Ceti documentation: ContRepresentation.exists_eq_smul_one_of_isIrreducible
• Source of ContRepresentation.exists_eq_smul_one_of_isIrreducible in TauCeti/RepresentationTheory/Continuous/Schur.lean

LeanContRepresentation.exists_eq_smul_one_of_isIrreducible · ContRepresentation.eq_zero_of_isEmpty_equiv

Used by 2

Used byThe Peter-Weyl theorem · The Peter-Weyl theorem, unconditionally

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.