Module

AllFinite.lean

Nyll.ProCGroups.FiniteGroups.AllFinite

10 declarations indexed from sourceView source ↗

Module documentation

The class of all finite groups

This module defines FiniteGroupClass.allFinite and proves its standard closure properties: formation, subgroup, normal-subgroup, quotient, finite-subdirect-product, extension, and hereditary closure. It also supplies the trivial-quotient instance used by pro-\(C\) constructions when no restriction beyond finiteness is intended.

Imports2

Mathlib.GroupTheory.QuotientGroup.Finite
Nyll.ProCGroups.FiniteGroups.Classes

Imported by4

def

allFinite

L26 ↗

ProCGroups.FiniteGroupClass.allFinite

Documentation

The class of all finite groups.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · full declaration

def allFinite : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G
  finite_of_mem := fun hG => hG
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG
    exact Finite.of_equiv G e.toEquiv

theorem

allFinite_formation

L35 ↗

ProCGroups.FiniteGroupClass.allFinite_formation

Documentation

The class of all finite groups is an extension-closed formation.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_formation : Formation allFinite

instance

allFinite_containsTrivialQuotients

L45 ↗

ProCGroups.FiniteGroupClass.allFinite_containsTrivialQuotients

Documentation

The class of all finite groups contains the trivial quotients.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

instance allFinite_containsTrivialQuotients :
    ContainsTrivialQuotients (allFinite : FiniteGroupClass.{u})

theorem

allFinite_isomClosed

L50 ↗

ProCGroups.FiniteGroupClass.allFinite_isomClosed

Documentation

The class of all finite groups is closed under isomorphism.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_isomClosed : IsomClosed allFinite

theorem

allFinite_subgroupClosed

L54 ↗

ProCGroups.FiniteGroupClass.allFinite_subgroupClosed

Documentation

The class of all finite groups is closed under subgroups.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_subgroupClosed : SubgroupClosed allFinite

theorem

allFinite_normalSubgroupClosed

L60 ↗

ProCGroups.FiniteGroupClass.allFinite_normalSubgroupClosed

Documentation

The class of all finite groups is closed under normal subgroups.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_normalSubgroupClosed : NormalSubgroupClosed allFinite

theorem

allFinite_quotientClosed

L65 ↗

ProCGroups.FiniteGroupClass.allFinite_quotientClosed

Documentation

The class of all finite groups is closed under quotients.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_quotientClosed : QuotientClosed allFinite

theorem

allFinite_finiteSubdirectProductClosed

L69 ↗

ProCGroups.FiniteGroupClass.allFinite_finiteSubdirectProductClosed

Documentation

The class of all finite groups is closed under finite subdirect products.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_finiteSubdirectProductClosed : FiniteSubdirectProductClosed allFinite

theorem

allFinite_extensionClosed

L73 ↗

ProCGroups.FiniteGroupClass.allFinite_extensionClosed

Documentation

The class of all finite groups is extension closed.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_extensionClosed : ExtensionClosed allFinite

theorem

allFinite_hereditary

L80 ↗

ProCGroups.FiniteGroupClass.allFinite_hereditary

Documentation

The class of all finite groups is hereditary.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
namespace FiniteGroupClass

Lean source · statement

theorem allFinite_hereditary : Hereditary allFinite

Module documentation

The class of all finite groups

Declarations