Induction

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

TheoremAn induction theorem for a family of subgroups makes restriction to that family detect the virtual characters#

For a class function on G, membership in the virtual-character lattice is equivalent to membership of all its restrictions to the family.

The forward direction TauCeti.comp_subtype_mem_virtualCharacters needs no hypothesis on the family; the hypothesis is used only for the converse.

TauCeti.mem_virtualCharacters_iff_forall_comp_subtype.{u, v} {k : Type u} {G : Type v} [Field k]
  [Group G] [Finite G] {P : Subgroup G → Prop}
  (hP : TauCeti.ClassFunction.indVirtualCharacters k G P = TauCeti.virtualCharacters k G)
  {f : G → k} (hf : f ∈ TauCeti.ClassFunction k G) :
  f ∈ TauCeti.virtualCharacters k G ↔
    ∀ (S : Subgroup G), P S → (fun s => f ↑s) ∈ TauCeti.virtualCharacters k ↥S
Lean

Formalized in Tau Ceti as TauCeti.mem_virtualCharacters_iff_forall_comp_subtype.

Sources
LeanTauCeti.mem_virtualCharacters_iff_forall_comp_subtype
Uses 1
Proof usesAn induction theorem is a single membership

TheoremAn induction theorem is a single membership#

The virtual characters induced from a family of subgroups exhaust R(G) exactly when the constant function 1, the character of the trivial representation, is one of them.

Brauer's induction theorem is this statement for the elementary subgroups, and its whole content is therefore the membership 1 ∈ V_G.

TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff.{u, v} {k : Type u} {G : Type v}
  [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} :
  TauCeti.ClassFunction.indVirtualCharacters k G P = TauCeti.virtualCharacters k G ↔
    1 ∈ TauCeti.ClassFunction.indVirtualCharacters k G P
Lean

Formalized in Tau Ceti as TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff.

Sources
LeanTauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff
Used by 2
Used byAn induction theorem for a family of subgroups makes restriction to that family detect the virtual characters · An induction theorem, one prime at a time and with coefficients in a subring

TheoremAn induction theorem, one prime at a time and with coefficients in a subring#

Let A be a subring of k admitting an additive map t : A → ℤ with t 1 = 1; for example ℤ[ζ] for a root of unity ζ in characteristic zero (PowerBasis.exists_linearMap_apply_one). The virtual characters induced from a family of subgroups exhaust R(G) exactly when, for every prime p, some multiple m • 1 with p ∤ m is an A-linear combination of them.

This reduces an induction theorem to a separate statement for each prime p. In Serre's proof of Brauer's induction theorem, that statement is supplied, for the elementary subgroups, by the p-elementary subgroups with coefficients in ℤ[ζ], ζ a primitive |G|-th root of unity; this declaration does not prove it.

TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff_forall_prime.{u, v} {k : Type u}
  {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} [IsAlgClosed k]
  [Invertible ↑(Nat.card G)] (A : Subring k) (t : ↥A →+ ℤ) (ht : t 1 = 1) :
  TauCeti.ClassFunction.indVirtualCharacters k G P = TauCeti.virtualCharacters k G ↔
    ∀ (p : ℕ),
      Nat.Prime p →
        ∃ m, ¬p ∣ m ∧ m • 1 ∈ Submodule.span ↥A ↑(TauCeti.ClassFunction.indVirtualCharacters k G P)
Lean

Formalized in Tau Ceti as TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff_forall_prime.

Sources
LeanTauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff_forall_prime
Uses 1 · Used by 1
Proof usesAn induction theorem is a single membership
Used byBrauer's induction theorem

TheoremArtin's induction theorem with its induced-character-span target#

Over a algebraically closed field in which |G| is invertible (in particular, in characteristic zero), |G| • f belongs to the additive subgroup generated by characters induced from irreducible characters of cyclic subgroups.

TauCeti.ClassFunction.natCard_nsmul_mem_indCharacterSpanInt_isCyclic.{u, v} {k : Type u}
  {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {f : G → k}
  (hf : f ∈ TauCeti.virtualCharacters k G) :
  Nat.card G • f ∈ TauCeti.ClassFunction.indCharacterSpanInt k G fun C => IsCyclic ↥C
Lean

Formalized in Tau Ceti as TauCeti.ClassFunction.natCard_nsmul_mem_indCharacterSpanInt_isCyclic.

Other forms

Artin's induction theorem, sharp form, through the canonical API. Formalized in Tau Ceti as TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isCyclic.

TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isCyclic.{u, v} {k : Type u}
  {G : Type v} [Field k] [Group G] [Finite G] {f : G → k} (hf : f ∈ TauCeti.virtualCharacters k G) :
  Nat.card G • f ∈ TauCeti.ClassFunction.indVirtualCharacters k G fun C => IsCyclic ↥C
Sources
LeanTauCeti.ClassFunction.natCard_nsmul_mem_indCharacterSpanInt_isCyclic · TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isCyclic
Used by 1
Used byArtin's sharp induction theorem, read for the elementary subgroups

TheoremArtin's sharp induction theorem, read for the elementary subgroups#

Every cyclic subgroup is elementary, so the sharp cyclic theorem gives the explicit multiplier |G| here too.

When Nat.card G vanishes in k, the multiple is zero; the intended nonvacuous content is the characteristic-zero specialization.

This is weaker than Brauer's induction theorem, which asserts the same with multiplier 1. By TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff, Brauer's theorem is equivalent to 1 being induced from the elementary subgroups, which is not proved here.

TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isElementary.{u, v} {k : Type u}
  {G : Type v} [Field k] [Group G] [Finite G] {f : G → k} (hf : f ∈ TauCeti.virtualCharacters k G) :
  Nat.card G • f ∈ TauCeti.ClassFunction.indVirtualCharacters k G fun E => TauCeti.IsElementary ↥E
Lean

Formalized in Tau Ceti as TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isElementary.

Sources
LeanTauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isElementary
Uses 1
Proof usesArtin's induction theorem with its induced-character-span target

TheoremBrauer's induction theorem#

Over an algebraically closed field of characteristic zero, every virtual character of a finite group is an integral combination of virtual characters induced from elementary subgroups.

TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_isElementary.{u, v} {k : Type u}
  {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] [IsAlgClosed k] :
  (TauCeti.ClassFunction.indVirtualCharacters k G fun E => TauCeti.IsElementary ↥E) =
    TauCeti.virtualCharacters k G
Lean

Formalized in Tau Ceti as TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_isElementary.

Other forms

Brauer's induction theorem, character form. Formalized in Tau Ceti as TauCeti.ClassFunction.character_mem_indCharacterSpanInt_isElementary.

TauCeti.ClassFunction.character_mem_indCharacterSpanInt_isElementary.{u, v} {k : Type u}
  {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] [IsAlgClosed k] (V : FDRep k G) :
  V.character ∈ TauCeti.ClassFunction.indCharacterSpanInt k G fun E => TauCeti.IsElementary ↥E
Sources
LeanTauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_isElementary · TauCeti.ClassFunction.character_mem_indCharacterSpanInt_isElementary
Uses 2
Proof usesAn induction theorem, one prime at a time and with coefficients in a subring · Brauer's local lemma

TheoremBrauer's local lemma#

For every prime p there is a function ψ : G → ℕ, none of whose values is divisible by p, whose cast to k is an A-combination of virtual characters induced from p-elementary subgroups, for every subring A of k containing the |G|-th roots of unity. It is the sum, over the conjugacy classes of p-regular elements s, of orderOf s times the induced p-section indicator of s: at y only the class of the p-free part of y contributes, and its contribution is prime to p.

TauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd.{u, v} (k : Type u) {G : Type v}
  [Group G] [Field k] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (p : ℕ)
  [Fact (Nat.Prime p)] :
  ∃ ψ,
    (∀ (y : G), ¬p ∣ ψ y) ∧
      ∀ (A : Subring k),
        (∀ (x : k), x ^ Nat.card G = 1 → x ∈ A) →
          (fun y => ↑(ψ y)) ∈
            Submodule.span ↥A
              ↑(TauCeti.ClassFunction.indVirtualCharacters k G fun S => TauCeti.IsPElementary p ↥S)
Lean

Formalized in Tau Ceti as TauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd.

Sources
LeanTauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd
Used by 1
Used byBrauer's induction theorem

TheoremBurnside's lemma for two permutation characters#

The unnormalized sum ∑ g, χ_X(g) · χ_Y(g⁻¹) is the number of orbits of G on X × Y times the order of G.

This form carries no division, so it holds over any field.

TauCeti.sum_character_ofMulAction_mul_character_ofMulAction_eq_card_orbits_mul_card_group.{u, v, w,
    z}
  (k : Type u) {G : Type v} [Field k] [Group G] [Fintype G] (X : Type w) (Y : Type z)
  [MulAction G X] [MulAction G Y] [Finite X] [Finite Y] :
  ∑ g,
      (Representation.ofMulAction k G X).character g *
        (Representation.ofMulAction k G Y).character g⁻¹ =
    ↑(Nat.card (MulAction.orbitRel.Quotient G (X × Y))) * ↑(Nat.card G)
Lean

Formalized in Tau Ceti as TauCeti.sum_character_ofMulAction_mul_character_ofMulAction_eq_card_orbits_mul_card_group.

Sources
LeanTauCeti.sum_character_ofMulAction_mul_character_ofMulAction_eq_card_orbits_mul_card_group
Uses 1
Proof usesBurnside's lemma on a product

TheoremClifford's theorem, dimension form#

The dimension of an irreducible representation of G is the common multiplicity e of the constituents of its restriction to N, times the number [G : inertia V] of those constituents, times the dimension of one of them.

The decomposition Res_N W ≅ V.cliffordSum e that FDRep.clifford_restrict_iso supplies is returned alongside the identity, so that V is exhibited as a constituent of the restriction and not merely named by it.

In particular the index of the inertia group of a constituent divides the dimension of W; that is the arithmetic that FDRep.clifford_restrict_dvd_finrank reads off and that FDRep.clifford_restrict_inertia_eq_top_of_coprime exploits.

FDRep.clifford_restrict_finrank.{u, v} {k : Type u} {G : Type v} [Field k] [Group G]
  {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] :
  ∃ V,
    ∃ (_ : CategoryTheory.Simple V) (hfinite : Finite (G ⧸ TauCeti.inertia V)),
      have x := hfinite;
      ∃ e,
        e ≠ 0 ∧
          Nonempty (N.resFDRep W ≅ V.cliffordSum e) ∧
            Module.finrank k ↑W.V = e * (TauCeti.inertia V).index * Module.finrank k ↑V.V
Lean

Formalized in Tau Ceti as FDRep.clifford_restrict_finrank.

Other forms

Clifford's theorem for a specified constituent. Formalized in Tau Ceti as FDRep.clifford_restrict_iso_of_isAtom.

FDRep.clifford_restrict_iso_of_isAtom.{u, v} {k : Type u} {G : Type v} [Field k] [Group G]
  {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W]
  (σ : Subrepresentation (W.ρ.comp N.subtype)) (hσ : IsAtom σ) :
  ∃ (hfinite : Finite (G ⧸ TauCeti.inertia (FDRep.of σ.toRepresentation))),
    have x := hfinite;
    ∃ e, e ≠ 0 ∧ Nonempty (N.resFDRep W ≅ (FDRep.of σ.toRepresentation).cliffordSum e)

Clifford's theorem, character form. Formalized in Tau Ceti as TauCeti.clifford_restrict_character.

TauCeti.clifford_restrict_character.{u, v} {k : Type u} {G : Type v} [Field k] [Group G]
  {N : Subgroup G} [N.Normal] [Finite G] [IsAlgClosed k] (hG : IsUnit ↑(Nat.card G)) (W : FDRep k G)
  [CategoryTheory.Simple W] :
  ∃ V,
    ∃ (_ : CategoryTheory.Simple V),
      ∃ e reps,
        e ≠ 0 ∧
          (∀ (g : G), ∃! r, r ∈ reps ∧ g⁻¹ * r ∈ TauCeti.inertia V) ∧
            ∀ (n : ↥N), W.character ↑n = ↑e * ∑ g ∈ reps, (TauCeti.conjNormalFDRep g V).character n

Clifford's theorem, multiplicity form. Formalized in Tau Ceti as Representation.finrank_linearMap_eq_of_isAtom.

Representation.finrank_linearMap_eq_of_isAtom.{u_1, u_2, u_3} {k : Type u_1} {G : Type u_2}
  {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [_root_.Module k V] {N : Subgroup G}
  [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible]
  {σ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ)
  (T : Submodule (MonoidAlgebra k ↥N) (Representation.asModule (MonoidHom.comp ρ N.subtype)))
  [IsSimpleModule (MonoidAlgebra k ↥N) ↥T] :
  Module.finrank k
      (↥T →ₗ[MonoidAlgebra k ↥N] Representation.asModule (MonoidHom.comp ρ N.subtype)) =
    Module.finrank k
      (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] Representation.asModule (MonoidHom.comp ρ N.subtype))

Clifford's theorem, multiplicity form, for two minimal subspaces. Formalized in Tau Ceti as Representation.finrank_linearMap_eq_of_isAtom_of_isAtom.

Representation.finrank_linearMap_eq_of_isAtom_of_isAtom.{u_1, u_2, u_3} {k : Type u_1}
  {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [_root_.Module k V]
  {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible]
  {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ) (hτ : IsAtom τ) :
  Module.finrank k
      (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N] Representation.asModule (MonoidHom.comp ρ N.subtype)) =
    Module.finrank k
      (↥τ.asSubmodule →ₗ[MonoidAlgebra k ↥N] Representation.asModule (MonoidHom.comp ρ N.subtype))

Clifford's theorem, representation form. Formalized in Tau Ceti as FDRep.clifford_restrict_iso.

FDRep.clifford_restrict_iso.{u, v} {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G}
  [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] :
  ∃ V,
    ∃ (_ : CategoryTheory.Simple V) (hfinite : Finite (G ⧸ TauCeti.inertia V)),
      have x := hfinite;
      ∃ e, e ≠ 0 ∧ Nonempty (N.resFDRep W ≅ V.cliffordSum e)

Clifford's theorem, single-orbit form. Formalized in Tau Ceti as TauCeti.Representation.exists_nonempty_linearEquiv_conjSubrep.

TauCeti.Representation.exists_nonempty_linearEquiv_conjSubrep.{u_1, u_2, u_3} {k : Type u_1}
  {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [_root_.Module k V]
  {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible]
  {σ τ : Subrepresentation (MonoidHom.comp ρ N.subtype)} (hσ : IsAtom σ) (hτ : IsAtom τ) :
  ∃ g,
    Nonempty
      (↥τ.asSubmodule ≃ₗ[MonoidAlgebra k ↥N] ↥(TauCeti.Representation.conjSubrep ρ g σ).asSubmodule)

Clifford's theorem, single-orbit form, packaged. Formalized in Tau Ceti as TauCeti.Representation.exists_isAtom_forall_nonempty_linearEquiv_conjSubrep.

TauCeti.Representation.exists_isAtom_forall_nonempty_linearEquiv_conjSubrep.{u_1, u_2, u_3}
  {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V]
  [_root_.Module k V] {N : Subgroup G} [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible]
  [FiniteDimensional k V] :
  ∃ σ,
    IsAtom σ ∧
      ∀ (τ : Subrepresentation (MonoidHom.comp ρ N.subtype)),
        IsAtom τ →
          ∃ g,
            Nonempty
              (↥τ.asSubmodule ≃ₗ[MonoidAlgebra k ↥N]
                ↥(TauCeti.Representation.conjSubrep ρ g σ).asSubmodule)

Clifford's theorem, the common multiplicity. Formalized in Tau Ceti as Representation.exists_forall_finrank_linearMap_eq.

Representation.exists_forall_finrank_linearMap_eq.{u_1, u_2, u_3} {k : Type u_1} {G : Type u_2}
  {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [_root_.Module k V] {N : Subgroup G}
  [N.Normal] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] :
  ∃ e,
    0 < e ∧
      ∀ (σ : Subrepresentation (MonoidHom.comp ρ N.subtype)),
        IsAtom σ →
          Module.finrank k
              (↥σ.asSubmodule →ₗ[MonoidAlgebra k ↥N]
                Representation.asModule (MonoidHom.comp ρ N.subtype)) =
            e
Sources
LeanFDRep.clifford_restrict_finrank · FDRep.clifford_restrict_iso_of_isAtom · TauCeti.clifford_restrict_character · Representation.finrank_linearMap_eq_of_isAtom · Representation.finrank_linearMap_eq_of_isAtom_of_isAtom · FDRep.clifford_restrict_iso · TauCeti.Representation.exists_nonempty_linearEquiv_conjSubrep · TauCeti.Representation.exists_isAtom_forall_nonempty_linearEquiv_conjSubrep · Representation.exists_forall_finrank_linearMap_eq
Uses 1 · Used by 1
Proof usesThe multiplicity theorem
Used byThe divisibilities in Clifford's theorem

TheoremThe divisibilities in Clifford's theorem#

For an irreducible constituent V of the restriction of an irreducible W to a normal subgroup, both the index of the inertia group of V and the dimension of V divide the dimension of W; the index divides [G : N], and it divides the quotient dim W / (e * dim V) that the dimension identity leaves.

The decomposition Res_N W ≅ V.cliffordSum e is carried along from FDRep.clifford_restrict_finrank, so that V is exhibited as a constituent of the restriction and the divisibilities are read as statements about that constituent rather than about some unrelated irreducible representation of N.

This is the form in which the dimension identity of FDRep.clifford_restrict_finrank is used. The number of distinct conjugates occurring in the restriction is [G : inertia V], and it is constrained from two sides at once: by the degree of W, through the dimension identity, and by the index of N, through TauCeti.le_inertia. Neither constraint mentions the multiplicity e, which the last divisibility divides out instead: dim W / (e * dim V) counts the distinct conjugates.

FDRep.clifford_restrict_dvd_finrank.{u, v} {k : Type u} {G : Type v} [Field k] [Group G]
  {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] :
  ∃ V,
    ∃ (_ : CategoryTheory.Simple V) (hfinite : Finite (G ⧸ TauCeti.inertia V)),
      have x := hfinite;
      ∃ e,
        e ≠ 0 ∧
          Nonempty (N.resFDRep W ≅ V.cliffordSum e) ∧
            (TauCeti.inertia V).index ∣ Module.finrank k ↑W.V ∧
              Module.finrank k ↑V.V ∣ Module.finrank k ↑W.V ∧
                (TauCeti.inertia V).index ∣ N.index ∧
                  (TauCeti.inertia V).index ∣ Module.finrank k ↑W.V / (e * Module.finrank k ↑V.V)
Lean

Formalized in Tau Ceti as FDRep.clifford_restrict_dvd_finrank.

Sources
LeanFDRep.clifford_restrict_dvd_finrank
Uses 1
Proof usesClifford's theorem, dimension form

TheoremFrobenius reciprocity for class functions#

The normalized pairing over G of an induced class function with a class function of G is the normalized pairing over S of the original class function with the restricted one.

Both sides are written as explicit normalized sums, so the statement does not depend on the name of any particular pairing; TauCeti.characterPairing_ind is the same identity phrased against TauCeti.ClassFunction.characterPairing. Specialized to two characters this is TauCeti.frobenius_reciprocity, but no representation is involved here: the identity is a double count over G × G and holds for arbitrary class functions.

TauCeti.frobenius_reciprocity_classFunction.{u, v} {k : Type u} {G : Type v} [Group G]
  {S : Subgroup G} [Semifield k] [Fintype G] (hG : IsUnit ↑(Nat.card G))
  (f : ↥(TauCeti.ClassFunction k ↥S)) (h : ↥(TauCeti.ClassFunction k G)) :
  (↑(Nat.card G))⁻¹ * ∑ g, S.indClassFun (↑f) g * ↑h g⁻¹ =
    (↑(Nat.card ↥S))⁻¹ * ∑ s, ↑f s * ↑h (↑s)⁻¹
Lean

Formalized in Tau Ceti as TauCeti.frobenius_reciprocity_classFunction.

Other forms

Frobenius reciprocity as a character identity. Formalized in Tau Ceti as TauCeti.frobenius_reciprocity.

TauCeti.frobenius_reciprocity.{u, v} {k : Type u} {G : Type v} [Field k] [Group G] {S : Subgroup G}
  [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) (B : FDRep k G) :
  (↑(Nat.card G))⁻¹ * ∑ g, (TauCeti.indFDRep A).character g * B.character g⁻¹ =
    (↑(Nat.card ↥S))⁻¹ * ∑ s, A.character s * B.character (↑s)⁻¹

Frobenius reciprocity in the other direction. Formalized in Tau Ceti as TauCeti.frobenius_reciprocity_resFDRep.

TauCeti.frobenius_reciprocity_resFDRep.{u, v} {k : Type u} {G : Type v} [Field k] [Group G]
  {S : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) (B : FDRep k G) :
  (↑(Nat.card ↥S))⁻¹ * ∑ s, B.character ↑s * A.character s⁻¹ =
    (↑(Nat.card G))⁻¹ * ∑ g, B.character g * (TauCeti.indFDRep A).character g⁻¹
Sources
LeanTauCeti.frobenius_reciprocity_classFunction · TauCeti.frobenius_reciprocity · TauCeti.frobenius_reciprocity_resFDRep
Used by 2
Used byFrobenius's theorem returns the normal complement it was handed · Frobenius's theorem: the Frobenius kernel is normal

TheoremThe Mackey criterion for a linear character of an inverted subgroup of index two#

the induced representation is irreducible exactly when some value of χ is not a square root of 1. Conjugation by any element outside N inverts it, by TauCeti.conj_eq_inv_of_notMem_of_index_two, so {}^s χ = χ⁻¹ for every such s and the criterion becomes the single condition χ ≠ χ⁻¹. The inversion hypothesis is asked of the one outside element s only.

TauCeti.simple_indFDRep_ofLinearCharacter_iff_of_conj_eq_inv.{u} {k G : Type u} [Field k] [Group G]
  {N : Subgroup G} [Finite G] [IsAlgClosed k] [CharZero k] (hindex : N.index = 2) {s : G}
  (hs : s ∉ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) (χ : ↥N →* kˣ) :
  CategoryTheory.Simple (TauCeti.indFDRep (FDRep.ofLinearCharacter χ)) ↔ ∃ x, χ x ^ 2 ≠ 1
Lean

Formalized in Tau Ceti as TauCeti.simple_indFDRep_ofLinearCharacter_iff_of_conj_eq_inv.

Sources
LeanTauCeti.simple_indFDRep_ofLinearCharacter_iff_of_conj_eq_inv
Uses 1
Proof usesThe Mackey irreducibility criterion

TheoremThe Mackey decomposition formula, character form#

For a finite-dimensional representation A of a finite-index subgroup H and an element x of a subgroup K, the character of Res_K (Ind_H^G A) at x is the sum, over the double cosets K \ G / H, of the characters of the Mackey summands.

The character of Ind_H^G A at x : K, read on G, is the same number: FDRep.character_actionRes is a simp lemma rewriting the left-hand side into it.

TauCeti.character_resFDRep_indFDRep_mackey.{u} {k G : Type u} [Field k] [Group G] {H K : Subgroup G}
  [H.FiniteIndex] (A : FDRep k ↥H) (x : ↥K) :
  (K.resFDRep (TauCeti.indFDRep A)).character x =
    ∑ D, (TauCeti.mackeySummand (Quotient.out D) A).character x
Lean

Formalized in Tau Ceti as TauCeti.character_resFDRep_indFDRep_mackey.

Other forms

The Mackey decomposition formula for class functions. Formalized in Tau Ceti as Subgroup.indClassFun_mackey.

Subgroup.indClassFun_mackey.{u_1, u_2} {k : Type u_1} [Semiring k] {G : Type u_2} [Group G]
  (H : Subgroup G) {K : Subgroup G} [H.FiniteIndex] {f : ↥H → k}
  (hf : f ∈ TauCeti.ClassFunction k ↥H) (x : ↥K) :
  H.indClassFun f ↑x =
    ∑ D,
      ((TauCeti.mackeySubgroup (Quotient.out D) H K).subgroupOf K).indClassFun
        (TauCeti.mackeyClassFun (Quotient.out D) H K f) x
Sources
LeanTauCeti.character_resFDRep_indFDRep_mackey · Subgroup.indClassFun_mackey
Used by 1
Used byThe Mackey decomposition of a restricted induced class function

TheoremThe Mackey decomposition of a restricted induced class function#

Restricting to K a class function induced from H gives the sum, over the double cosets K \ G / H, of the class functions induced to K from the Mackey subgroups.

This is Subgroup.indClassFun_mackey rewritten as an identity of bundled class functions, which is the form the character pairing consumes.

Subgroup.comap_subtype_indClassFunction_mackey.{u_1, u_2} {k : Type u_1} [Semiring k] {G : Type u_2}
  [Group G] (K : Subgroup G) {H : Subgroup G} [H.FiniteIndex] (f : ↥(TauCeti.ClassFunction k ↥H)) :
  (TauCeti.ClassFunction.comap K.subtype) (H.indClassFunction f) =
    ∑ D,
      ((TauCeti.mackeySubgroup (Quotient.out D) H K).subgroupOf K).indClassFunction
        (TauCeti.mackeyClassFunction (Quotient.out D) H K f)
Lean

Formalized in Tau Ceti as Subgroup.comap_subtype_indClassFunction_mackey.

Sources
LeanSubgroup.comap_subtype_indClassFunction_mackey
Uses 1
Proof usesThe Mackey decomposition formula, character form

TheoremThe Mackey irreducibility criterion#

The representation induced from A is irreducible exactly when A is irreducible and every double coset HsH other than H itself, read at its chosen representative, is Mackey disjoint. Algebraic closure supplies scalar Schur.

TauCeti.simple_indFDRep_iff_doubleCoset.{u} {k G : Type u} [Field k] [Group G] [Finite G]
  [IsAlgClosed k] [NeZero ↑(Nat.card G)] {H : Subgroup G} (A : FDRep k ↥H) :
  CategoryTheory.Simple (TauCeti.indFDRep A) ↔
    CategoryTheory.Simple A ∧
      ∀ (D : DoubleCoset.Quotient ↑H ↑H),
        D ≠ DoubleCoset.mk H H 1 → TauCeti.MackeyDisjoint A (Quotient.out D)
Lean

Formalized in Tau Ceti as TauCeti.simple_indFDRep_iff_doubleCoset.

Other forms

The Mackey irreducibility criterion for a normal subgroup. Formalized in Tau Ceti as TauCeti.simple_indFDRep_iff_of_normal.

TauCeti.simple_indFDRep_iff_of_normal.{u} {k G : Type u} [Field k] [Group G] [Finite G]
  [IsAlgClosed k] [NeZero ↑(Nat.card G)] {H : Subgroup G} [H.Normal] (A : FDRep k ↥H) :
  CategoryTheory.Simple (TauCeti.indFDRep A) ↔
    CategoryTheory.Simple A ∧ ∀ s ∉ H, IsEmpty (TauCeti.conjNormalFDRep s A ≅ A)

The Mackey irreducibility criterion for an induced linear character. Formalized in Tau Ceti as TauCeti.simple_indFDRep_ofLinearCharacter_iff.

TauCeti.simple_indFDRep_ofLinearCharacter_iff.{u} {k G : Type u} [Field k] [Group G]
  {N : Subgroup G} [N.Normal] [Finite G] [IsAlgClosed k] [CharZero k] (χ : ↥N →* kˣ) :
  CategoryTheory.Simple (TauCeti.indFDRep (FDRep.ofLinearCharacter χ)) ↔
    ∀ s ∉ N, ∃ x, χ ((MulAut.conjNormal s) x) ≠ χ x

The Mackey irreducibility criterion, elementwise. Formalized in Tau Ceti as TauCeti.simple_indFDRep_iff.

TauCeti.simple_indFDRep_iff.{u} {k G : Type u} [Field k] [Group G] [Finite G] [IsAlgClosed k]
  [NeZero ↑(Nat.card G)] {H : Subgroup G} (A : FDRep k ↥H) :
  CategoryTheory.Simple (TauCeti.indFDRep A) ↔
    CategoryTheory.Simple A ∧ ∀ s ∉ H, TauCeti.MackeyDisjoint A s
Sources
LeanTauCeti.simple_indFDRep_iff_doubleCoset · TauCeti.simple_indFDRep_iff_of_normal · TauCeti.simple_indFDRep_ofLinearCharacter_iff · TauCeti.simple_indFDRep_iff
Used by 1
Used byThe Mackey criterion for a linear character of an inverted subgroup of index two

TheoremThe modular Artin induction theorem (NSW (7.3.4), Milne ADT I Lemma 2.10)#

In characteristic p, every class in G₀(k[G]) has a positive multiple in TauCeti.indCyclicCoprimeK0, the subgroup generated by the classes induced from cyclic subgroups of order prime to p; the multiplier |G| works for every class.

TauCeti.modularArtin_exists_nsmul_mem_indCyclicCoprimeK0.{u} {k G : Type u} [Field k] [Group G]
  [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p]
  (x : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure (MonoidAlgebra k G))) :
  ∃ N, 0 < N ∧ N • x ∈ TauCeti.indCyclicCoprimeK0 k G p
Lean

Formalized in Tau Ceti as TauCeti.modularArtin_exists_nsmul_mem_indCyclicCoprimeK0.

Sources
LeanTauCeti.modularArtin_exists_nsmul_mem_indCyclicCoprimeK0
Uses 3
Proof usesThe dual Noether isomorphism · The modular Artin theorem with multiplier |G| · The Noether isomorphism for exact categories

TheoremThe modular Artin theorem with multiplier |G|#

In characteristic p, the group-order multiple of every class in G₀(k[G]) lies in TauCeti.indCyclicCoprimeK0, the subgroup generated by the classes induced from cyclic subgroups of order prime to p; for the prime p, order prime to p is non-divisibility of the order by p (Nat.Prime.coprime_iff_not_dvd).

TauCeti.modularArtin_natCard_nsmul_mem_indCyclicCoprimeK0.{u} {k G : Type u} [Field k] [Group G]
  [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p]
  (x : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure (MonoidAlgebra k G))) :
  Nat.card G • x ∈ TauCeti.indCyclicCoprimeK0 k G p
Lean

Formalized in Tau Ceti as TauCeti.modularArtin_natCard_nsmul_mem_indCyclicCoprimeK0.

Sources
LeanTauCeti.modularArtin_natCard_nsmul_mem_indCyclicCoprimeK0
Uses 4 · Used by 1
Proof usesArtin's induction identity for every virtual class over every field · The dual Noether isomorphism · Kolchin's common fixed vector theorem · The Noether isomorphism for exact categories
Used byThe modular Artin induction theorem (NSW (7.3.4), Milne ADT I Lemma 2.10)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.