Group Action

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

TheoremBurnside's lemma on a product#

For a finite group G acting on two finite sets X and Y, the sum over g : G of the product of the two fixed-point counts is the number of orbits of G on X × Y, times the order of G.

TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group.{u_1, u_2, u_3}
  {G : Type u_1} (X : Type u_2) (Y : Type u_3) [Group G] [MulAction G X] [MulAction G Y] [Fintype G]
  [Finite X] [Finite Y] :
  ∑ g, Nat.card ↑(MulAction.fixedBy X g) * Nat.card ↑(MulAction.fixedBy Y g) =
    Nat.card (MulAction.orbitRel.Quotient G (X × Y)) * Nat.card G

Lean

Formalized in Tau Ceti as TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group.

Sources

• Tau Ceti documentation: TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group
• Source of TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group in TauCeti/GroupTheory/GroupAction/Burnside.lean

LeanTauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group

Used by 1

Used byBurnside's lemma for two permutation characters

TheoremIwasawa's criterion for a quotient#

Let a perfect group G have an Iwasawa structure on a quasiprimitive action. If a proper normal subgroup N contains every element acting trivially, then G ⧸ N is simple.

MulAction.IwasawaStructure.isSimpleGroup_quotient.{u_1, u_2} {G : Type u_1} {α : Type u_2} [Group G]
  [MulAction G α] [MulAction.IsQuasiPreprimitive G α] (IwaS : MulAction.IwasawaStructure G α)
  [Group.IsPerfect G] {N : Subgroup G} [N.Normal] (hN : N ≠ ⊤)
  (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ N) : IsSimpleGroup (G ⧸ N)

Lean

Formalized in Tau Ceti as MulAction.IwasawaStructure.isSimpleGroup_quotient.

Other forms

Iwasawa's criterion for the central quotient. Formalized in Tau Ceti as MulAction.IwasawaStructure.isSimpleGroup_quotient_center.

MulAction.IwasawaStructure.isSimpleGroup_quotient_center.{u_1, u_2} {G : Type u_1} {α : Type u_2}
  [Group G] [MulAction G α] [MulAction.IsQuasiPreprimitive G α]
  (IwaS : MulAction.IwasawaStructure G α) [Group.IsPerfect G] [Nontrivial G]
  (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ Subgroup.center G) :
  IsSimpleGroup (G ⧸ Subgroup.center G)

Iwasawa's criterion for the derived central quotient. Formalized in Tau Ceti as MulAction.IwasawaStructure.isSimpleGroup_derivedCentralQuotient.

MulAction.IwasawaStructure.isSimpleGroup_derivedCentralQuotient.{u_1, u_2} {G : Type u_1}
  {α : Type u_2} [Group G] [MulAction G α] [MulAction.IsQuasiPreprimitive G α]
  (IwaS : MulAction.IwasawaStructure G α) [Group.IsPerfect G] [Nontrivial G]
  (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ Subgroup.center G) :
  IsSimpleGroup (TauCeti.DerivedCentralQuotient G)

Sources

• Tau Ceti documentation: MulAction.IwasawaStructure.isSimpleGroup_quotient
• Source of MulAction.IwasawaStructure.isSimpleGroup_quotient in TauCeti/GroupTheory/GroupAction/Iwasawa.lean

LeanMulAction.IwasawaStructure.isSimpleGroup_quotient · MulAction.IwasawaStructure.isSimpleGroup_quotient_center · MulAction.IwasawaStructure.isSimpleGroup_derivedCentralQuotient

Uses 1 · Used by 1

Proof usesIwasawa's normal-subgroup theorem for a perfect group

Used byIwasawa's theorem for the projective symplectic group

TheoremIwasawa's normal-subgroup theorem for a perfect group#

If a perfect group has an Iwasawa structure on a quasiprimitive action, each of its normal subgroups either fixes every point or is the whole group.

MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top.{u_1, u_2} {G : Type u_1} {α : Type u_2}
  [Group G] [MulAction G α] [MulAction.IsQuasiPreprimitive G α]
  (IwaS : MulAction.IwasawaStructure G α) [Group.IsPerfect G] (N : Subgroup G) [N.Normal] :
  MulAction.fixedPoints (↥N) α = Set.univ ∨ N = ⊤

Lean

Formalized in Tau Ceti as MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top.

Sources

• Tau Ceti documentation: MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top
• Source of MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top in TauCeti/GroupTheory/GroupAction/Iwasawa.lean

LeanMulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top

Used by 1

Used byIwasawa's criterion for a quotient

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.