Classes of finite groups

A class of finite groups in the sense of profinite group theory is a collection C of finite groups that is closed under isomorphism, subgroups, quotients and extensions, and contains the trivial group. Finite p-groups, finite solvable groups and all finite groups are the examples of record. Such a class is exactly the data needed to speak of a pro-C group and of the universal pro-C quotient of a topological group, so it is bundled here as a structure rather than left as a loose predicate.

Closure under finite products is a consequence of the four closure properties, through the extension 1 → H → H × K → K → 1, and so is a theorem here rather than a field.

The membership predicate of a class carries the typeclass assumptions [Group H] [Finite H], which is awkward for a group that is not yet known to be finite. FiniteGroupClass.MemFinite packages the two together: C.MemFinite H says that H is finite and belongs to C. All the closure properties below are stated in that form, because the groups they are applied to — quotients of a topological group by open normal subgroups — are finite for a reason that is not visible in the statement.

The raw membership predicate speaks about groups in one universe. For a finite group in any other universe, FiniteGroupClass.MemFinite transports its group structure through Shrink; thus all derived constructions are universe-independent.

Main definitions

• TauCeti.FiniteGroupClass: a class of finite groups, as the data of its membership predicate together with its closure properties.
• TauCeti.FiniteGroupClass.MemFinite: membership of a group that is not yet known to be finite.
• TauCeti.finiteGroupClassP: the class of finite p-groups.
• TauCeti.finiteGroupClassTrivial: the class of finite trivial groups.
• TauCeti.finiteGroupClassSolvable: the class of finite solvable groups.
• TauCeti.finiteGroupClassAll: the class of all finite groups.

Main results

• TauCeti.FiniteGroupClass.MemFinite.prod: a class of finite groups is closed under binary products.
• TauCeti.FiniteGroupClass.MemFinite.quotient_inf: the normal subgroups with quotient in the class are closed under binary intersection.
• TauCeti.FiniteGroupClass.MemFinite.quotient_comap: they are preserved by preimage along a group homomorphism.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.1.

structure TauCeti.FiniteGroupClass : Type (w + 1)

A class of finite groups: a collection of finite groups containing the trivial group and closed under isomorphism, subgroups, quotients and extensions. This is the data a pro-C completion is built from.

• mem (H : Type w) [Group H] [Finite H] : Prop

  Membership of a finite group in the class.

• mem_congr {H K : Type w} [Group H] [Finite H] [Group K] [Finite K] : ∀ (a : H ≃* K), self.mem H ↔ self.mem K

  Membership depends only on the isomorphism class.

• mem_trivial : self.mem PUnit.{w + 1}

  The trivial group is in the class.

• mem_subgroup {H : Type w} [Group H] [Finite H] : self.mem H → ∀ (K : Subgroup H), self.mem ↥K

  The class is closed under subgroups.

• mem_quotient {H : Type w} [Group H] [Finite H] : self.mem H → ∀ (N : Subgroup H) [inst : N.Normal], self.mem (H ⧸ N)

  The class is closed under quotients.

• mem_extension {H : Type w} [Group H] [Finite H] (N : Subgroup H) [N.Normal] : self.mem ↥N → self.mem (H ⧸ N) → self.mem H

  The class is closed under extensions.

theorem TauCeti.FiniteGroupClass.ext {x y : FiniteGroupClass} (mem : x.mem = y.mem) : x = y

theorem TauCeti.FiniteGroupClass.ext_iff {x y : FiniteGroupClass} : x = y ↔ x.mem = y.mem

theorem TauCeti.FiniteGroupClass.shrinkFinite {H : Type v} [Finite H] : Finite (Shrink.{w, v} H)

def TauCeti.FiniteGroupClass.MemFinite (C : FiniteGroupClass) (H : Type v) [Group H] : Prop

C.MemFinite H says that the group H is finite and lies in the class C. The group is transported through Shrink before applying the raw membership predicate, so H may live in any universe. This is the form used for groups whose finiteness is not part of the ambient context, such as quotients by open normal subgroups.

Equations

• C.MemFinite H = ∃ (x : Finite H), C.mem (Shrink.{?u.1, ?u.2} H)

theorem TauCeti.FiniteGroupClass.MemFinite.finite {C : FiniteGroupClass} {H : Type v} [Group H] (h : C.MemFinite H) : Finite H

A group that lies in a class of finite groups is finite.

@[simp]

theorem TauCeti.FiniteGroupClass.memFinite_iff_shrink {C : FiniteGroupClass} {H : Type v} [Group H] [Finite H] : C.MemFinite H ↔ C.mem (Shrink.{w, v} H)

For a group already known to be finite, MemFinite is membership of its shrink.

theorem TauCeti.FiniteGroupClass.memFinite_iff {C : FiniteGroupClass} {H : Type w} [Group H] [Finite H] : C.MemFinite H ↔ C.mem H

In the defining universe, membership through Shrink agrees with raw membership.

theorem TauCeti.FiniteGroupClass.memFinite_of_subsingleton {C : FiniteGroupClass} {H : Type v} [Group H] [Subsingleton H] : C.MemFinite H

A class of finite groups contains every trivial group.

theorem TauCeti.FiniteGroupClass.MemFinite.of_surjective {C : FiniteGroupClass} {H : Type v} [Group H] {K : Type u} [Group K] (hH : C.MemFinite H) (f : H →* K) (hf : Function.Surjective ⇑f) : C.MemFinite K

A class of finite groups is closed under surjective images: a quotient of a member is a member.

theorem TauCeti.FiniteGroupClass.MemFinite.of_injective {C : FiniteGroupClass} {H : Type v} [Group H] {K : Type u} [Group K] (hK : C.MemFinite K) (f : H →* K) (hf : Function.Injective ⇑f) : C.MemFinite H

A class of finite groups is closed under subobjects: a group that embeds in a member is a member.

theorem TauCeti.FiniteGroupClass.memFinite_congr {C : FiniteGroupClass} {H : Type v} [Group H] {K : Type u} [Group K] (e : H ≃* K) : C.MemFinite H ↔ C.MemFinite K

Membership in a class of finite groups is invariant under isomorphism.

theorem TauCeti.FiniteGroupClass.memFinite_shrink {C : FiniteGroupClass} {H : Type v} [Group H] [Finite H] : C.MemFinite (Shrink.{u, v} H) ↔ C.MemFinite H

Membership in a class of finite groups is preserved when a finite group is moved to any other universe through Shrink.

theorem TauCeti.FiniteGroupClass.MemFinite.extension {C : FiniteGroupClass} {H : Type v} [Group H] {N : Subgroup H} [N.Normal] (hN : C.MemFinite ↥N) (hQ : C.MemFinite (H ⧸ N)) : C.MemFinite H

A class of finite groups is closed under extensions.

theorem TauCeti.FiniteGroupClass.MemFinite.prod {C : FiniteGroupClass} {H : Type v} [Group H] {K : Type u} [Group K] (hH : C.MemFinite H) (hK : C.MemFinite K) : C.MemFinite (H × K)

A class of finite groups is closed under binary products. This is the closure property that is not a field of the structure: it follows from closure under extensions, applied to 1 → H → H × K → K → 1.

theorem TauCeti.FiniteGroupClass.MemFinite.quotient_inf {C : FiniteGroupClass} {G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (hM : C.MemFinite (G ⧸ M)) (hN : C.MemFinite (G ⧸ N)) : C.MemFinite (G ⧸ M ⊓ N)

The normal subgroups with quotient in C are closed under binary intersection, because G ⧸ (M ⊓ N) embeds in (G ⧸ M) × (G ⧸ N). This is what makes that family downward directed.

theorem TauCeti.FiniteGroupClass.MemFinite.quotient_comap {C : FiniteGroupClass} {G : Type u} {H : Type v} [Group G] [Group H] {N : Subgroup H} [N.Normal] (hN : C.MemFinite (H ⧸ N)) (f : G →* H) : C.MemFinite (G ⧸ Subgroup.comap f N)

The normal subgroups with quotient in C are preserved by preimage, because G ⧸ N.comap f embeds in H ⧸ N.

The examples of record

def TauCeti.finiteGroupClassP (p : ℕ) : FiniteGroupClass

The class of finite p-groups, the class that pro-p theory is about.

Equations

• TauCeti.finiteGroupClassP p = { mem := fun (H : Type ?u.1) [Group H] [Finite H] => IsPGroup p H, mem_congr := ⋯, mem_trivial := ⋯, mem_subgroup := ⋯, mem_quotient := ⋯, mem_extension := ⋯ }

@[simp]

theorem TauCeti.finiteGroupClassP_mem_iff (p : ℕ) (H : Type w) [Group H] [Finite H] : (finiteGroupClassP p).mem H ↔ IsPGroup p H

Membership in finiteGroupClassP p is being a p-group.

@[simp]

theorem TauCeti.finiteGroupClassP_memFinite_iff (p : ℕ) (H : Type v) [Group H] : (finiteGroupClassP p).MemFinite H ↔ Finite H ∧ IsPGroup p H

A group belongs to finiteGroupClassP p exactly when it is finite and a p-group.

def TauCeti.finiteGroupClassTrivial : FiniteGroupClass

The class of finite trivial groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.finiteGroupClassTrivial_mem_iff (H : Type w) [Group H] [Finite H] : finiteGroupClassTrivial.mem H ↔ Subsingleton H

Membership in finiteGroupClassTrivial is being a trivial group.

@[simp]

theorem TauCeti.finiteGroupClassTrivial_memFinite_iff (H : Type v) [Group H] : finiteGroupClassTrivial.MemFinite H ↔ Subsingleton H

A group belongs to finiteGroupClassTrivial exactly when it is trivial.

def TauCeti.finiteGroupClassSolvable : FiniteGroupClass

The class of finite solvable groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.finiteGroupClassSolvable_mem_iff (H : Type w) [Group H] [Finite H] : finiteGroupClassSolvable.mem H ↔ Group.IsSolvable H

Membership in finiteGroupClassSolvable is solvability.

@[simp]

theorem TauCeti.finiteGroupClassSolvable_memFinite_iff (H : Type v) [Group H] : finiteGroupClassSolvable.MemFinite H ↔ Finite H ∧ Group.IsSolvable H

A group belongs to finiteGroupClassSolvable exactly when it is finite and solvable.

def TauCeti.finiteGroupClassAll : FiniteGroupClass

The class of all finite groups. Its C-kernel intersects the open normal subgroups whose quotient is finite; for a profinite group these are all the open normal subgroups, so the kernel is trivial.

Equations

• TauCeti.finiteGroupClassAll = { mem := fun (x : Type ?u.1) [Group x] [Finite x] => True, mem_congr := ⋯, mem_trivial := trivial, mem_subgroup := ⋯, mem_quotient := ⋯, mem_extension := ⋯ }

@[simp]

theorem TauCeti.finiteGroupClassAll_mem (H : Type w) [Group H] [Finite H] : finiteGroupClassAll.mem H

Every finite group is a member of finiteGroupClassAll.

@[simp]

theorem TauCeti.finiteGroupClassAll_memFinite_iff (H : Type v) [Group H] : finiteGroupClassAll.MemFinite H ↔ Finite H

A group belongs to finiteGroupClassAll exactly when it is finite.