Yamaguchi Lean 4 Library
ProCGroups.NormalSubgroups.PointedSumsAndSimpleQuotients
ProCGroups/NormalSubgroups/PointedSumsAndSimpleQuotients

ProCGroups.NormalSubgroups.PointedSumsAndSimpleQuotients

1 Structure

This module studies pointed sums and simple quotients for pro cgroups. Input data recording a closed normal closure that is free of the expected stabilized rank.

Open this file on GitHub
import
Imported by

Declarations

Structure ProCGroups.NormalSubgroups.NormalClosureFreeInputData GitHub 
structure NormalClosureFreeInputData
    (C : ProCGroups.FiniteGroupClass.{u})
    (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (S : Set F) (m : Cardinal) : Type (u + 1) where
  normalClosure : Subgroup F
  isClosedNormalClosure : IsClosedNormalClosure S normalClosure
  isFree : ProCGroups.FreeProC.IsFreeProCGroupOfClassRank C normalClosure (m ⊔ ℵ₀)

Input data recording a closed normal closure that is free of the expected stabilized rank.