NYLL
Module

ProCGroup.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
51 declarations indexed from sourceView source ↗

Module documentation

Open-normal quotient bases in a finite-group class

HasOpenNormalBasisInClass C G says exactly that the identity neighborhoods of G have a basis of open normal subgroups whose quotients lie in C. It does not assert compactness, Hausdorffness, total disconnectedness, or even the topological-group laws.

For an ambient ProfiniteGrp, this is precisely the additional property used to define the bundled category ProCGrp C.

The module also packages the class-indexed open normal subgroups, their quotient projections and transition maps, and the separation consequences of a Hausdorff open-normal basis.

Imports4
Imported by17

Declarations

def

HasOpenNormalBasisInClass

L39 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass
Documentation

The identity-neighborhood basis property for open normal subgroups with quotient in \(C\).

This predicate deliberately carries no profiniteness assumptions. A bundled pro-\(C\) object is an ambient ProfiniteGrp satisfying this additional property, as expressed by ProCGrp C.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def HasOpenNormalBasisInClass (C : FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] : Prop
def

HasOpenNormalBasisInClassAcrossUniverses

L47 ↗
ProCGroups.ProC.HasOpenNormalBasisInClassAcrossUniverses
Documentation

Universe-independent open-normal basis membership. Quotients are tested up to multiplicative equivalence with a finite group represented in the carrier universe of C.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def HasOpenNormalBasisInClassAcrossUniverses (C : FiniteGroupClass.{u})
    (G : Type v) [Group G] [TopologicalSpace G] : Prop
theorem

hasOpenNormalBasisInClassAcrossUniverses_iff

L54 ↗
ProCGroups.ProC.hasOpenNormalBasisInClassAcrossUniverses_iff
Documentation

In the native universe of C, the universe-independent and original basis predicates agree.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem hasOpenNormalBasisInClassAcrossUniverses_iff
    {C : FiniteGroupClass.{u}} {G : Type u} [Group G] [TopologicalSpace G] :
    HasOpenNormalBasisInClassAcrossUniverses C G ↔ HasOpenNormalBasisInClass C G
theorem

mono

L71 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.mono
Documentation

The existence of an open-normal basis in a class is monotone under enlarging the finite-group class.

Source context 6 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace HasOpenNormalBasisInClass
Lean source · statement
theorem mono {C D : FiniteGroupClass.{u}} {G : Type u} [Group G] [TopologicalSpace G]
    (hbasis : HasOpenNormalBasisInClass C G)
    (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q) :
    HasOpenNormalBasisInClass D G
abbrev

OpenNormalSubgroupInClass

L86 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass
Documentation

Open normal subgroups whose quotient lies in the chosen class \(C\). This packages the specified family as an actual type so later inverse-limit and basis constructions can quantify over it directly.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
abbrev OpenNormalSubgroupInClass (C : FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G]
def

ofOpenNormal

L98 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.ofOpenNormal
Documentation

Repackage an open normal subgroup together with a certificate that its quotient lies in \(C\).

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def ofOpenNormal (U : OpenNormalSubgroup G) (hU : C (G ⧸ (U : Subgroup G))) :
    OpenNormalSubgroupInClass C G
theorem

quotient_mem

L103 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.quotient_mem
Documentation

The quotient attached to a normal subgroup in the finite-quotient index family lies in \(C\).

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotient_mem (U : OpenNormalSubgroupInClass C G) :
    C (G ⧸ (U.1 : Subgroup G))
def

of_mono

L108 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.of_mono
Documentation

Move an open-normal-in-class subgroup along an inclusion of finite-group classes.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def of_mono {D : FiniteGroupClass.{u}}
    (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q)
    (U : OpenNormalSubgroupInClass C G) :
    OpenNormalSubgroupInClass D G
def

top

L115 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.top
Documentation

The top subgroup belongs to any finite-group class containing trivial quotients.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def top [FiniteGroupClass.ContainsTrivialQuotients C] :
    OpenNormalSubgroupInClass C G
theorem

nonempty_of_containsTrivialQuotients

L127 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.nonempty_of_containsTrivialQuotients
Documentation

There is an open-normal-in-class subgroup whenever the class contains trivial quotients.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem nonempty_of_containsTrivialQuotients [FiniteGroupClass.ContainsTrivialQuotients C] :
    Nonempty (OpenNormalSubgroupInClass C G)
def

of_allFinite

L132 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.of_allFinite
Documentation

Every open normal quotient of a compact group lies in the all-finite class.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def of_allFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
    OpenNormalSubgroupInClass FiniteGroupClass.allFinite G
def

comap

L140 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.comap
Documentation

Pull back an open-normal-in-class subgroup along a continuous homomorphism, when the class is hereditary.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def comap {H : Type u} [Group H] [TopologicalSpace H]
    (hHer : FiniteGroupClass.Hereditary C) (f : G →ₜ* H)
    (U : OpenNormalSubgroupInClass C H) : OpenNormalSubgroupInClass C G
def

mapOpenNormal

L171 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.mapOpenNormal
Documentation

An open surjective continuous homomorphism sends an open-normal-in-class subgroup to an open normal subgroup when target quotient membership is supplied explicitly. This is the lightweight bridge; stronger automatic versions can be derived from class closure hypotheses as needed.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def mapOpenNormal {H : Type u} [Group H] [TopologicalSpace H]
    (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
    (U : OpenNormalSubgroupInClass C G)
    (hC : C (H ⧸ ((OpenNormalSubgroup.map f hfopen hfsurj U.1 : OpenNormalSubgroup H) :
      Subgroup H))) :
    OpenNormalSubgroupInClass C H
def

mapOpenNormal_of_formation

L183 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.mapOpenNormal_of_formation
Documentation

An open surjective continuous homomorphism sends an in-class open normal subgroup to an in-class open normal subgroup. Formation closure supplies the target quotient membership.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def mapOpenNormal_of_formation {H : Type u} [Group H] [TopologicalSpace H]
    (hForm : FiniteGroupClass.Formation C)
    (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
    (U : OpenNormalSubgroupInClass C G) :
    OpenNormalSubgroupInClass C H
def

inf

L214 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.inf
Documentation

Finite intersections stay in class for a formation.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def inf (hForm : FiniteGroupClass.Formation C)
    (U V : OpenNormalSubgroupInClass C G) : OpenNormalSubgroupInClass C G
def

quotientProj

L221 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj
Documentation

The quotient projection attached to an open-normal-in-class subgroup.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def quotientProj (U : OpenNormalSubgroupInClass C G) :
    G →ₜ* G ⧸ (U.1 : Subgroup G)
theorem

quotientProj_apply

L227 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj_apply
Documentation

The quotient projection evaluates to the quotient class of the element.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientProj_apply (U : OpenNormalSubgroupInClass C G) (x : G) :
    quotientProj (C := C) U x = QuotientGroup.mk' (U.1 : Subgroup G) x
theorem

quotientProj_surjective

L233 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj_surjective
Documentation

The quotient projection attached to an open-normal-in-class subgroup is surjective.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientProj_surjective (U : OpenNormalSubgroupInClass C G) :
    Function.Surjective (quotientProj (C := C) U)
theorem

quotientProj_eq_one_iff

L239 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj_eq_one_iff
Documentation

The kernel predicate of the quotient projection is membership in the subgroup.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientProj_eq_one_iff {U : OpenNormalSubgroupInClass C G} {x : G} :
    quotientProj (C := C) U x = 1 ↔ x ∈ (U.1 : Subgroup G)
theorem

quotientProj_eq_quotientProj_iff

L244 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj_eq_quotientProj_iff
Documentation

Equality in the quotient attached to an open-normal-in-class subgroup.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroupInClass C G} {x y : G} :
    quotientProj (C := C) U x = quotientProj (C := C) U y ↔
      x / y ∈ (U.1 : Subgroup G)
theorem

mem_ker_quotientProj

L251 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.mem_ker_quotientProj
Documentation

Kernel membership for the quotient projection attached to an open-normal-in-class subgroup.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroupInClass C G} {x : G} :
    x ∈ OpenNormalSubgroup.ker (quotientProj (C := C) U) ↔
      x ∈ (U.1 : Subgroup G)
theorem

ker_quotientProj

L258 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.ker_quotientProj
Documentation

The open-normal kernel of the quotient projection is the original subgroup.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroupInClass C G) :
    ((OpenNormalSubgroup.ker (quotientProj (C := C) U) : OpenNormalSubgroup G) :
      Subgroup G) = (U.1 : Subgroup G)
def

map

L267 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.map
Documentation

The canonical transition map between quotients attached to nested open normal subgroups in the class-indexing family.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def map {U V : OpenNormalSubgroupInClass C G}
    (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
    G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G)
theorem

map_surjective

L273 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.map_surjective
Documentation

These transition maps are the natural quotient epimorphisms.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem map_surjective {U V : OpenNormalSubgroupInClass C G}
    (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
    Function.Surjective (map (C := C) (G := G) hUV)
theorem

map_id

L281 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.map_id
Documentation

The identity transition map is the identity monoid homomorphism.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem map_id (U : OpenNormalSubgroupInClass C G) :
    map (C := C) (G := G) (le_rfl : (U.1 : Subgroup G) ≤ (U.1 : Subgroup G)) = MonoidHom.id _
theorem

map_comp

L286 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.map_comp
Documentation

Maps induced on topological abelianizations compose as expected.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem map_comp {U V W : OpenNormalSubgroupInClass C G}
    (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G))
    (hVW : (W.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
    (map (C := C) (G := G) hUV).comp (map (C := C) (G := G) hVW) =
      map (C := C) (G := G) (hVW.trans hUV)
def

transition

L299 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.transition
Documentation

The continuous transition map between quotients attached to nested open-normal-in-class subgroups.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def transition {U V : OpenNormalSubgroupInClass C G}
    (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
    G ⧸ (U.1 : Subgroup G) →ₜ* G ⧸ (V.1 : Subgroup G)
theorem

transition_mk

L306 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.transition_mk
Documentation

Transition maps send quotient classes to the corresponding quotient classes.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem transition_mk {U V : OpenNormalSubgroupInClass C G}
    (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) (x : G) :
    transition (C := C) (G := G) hUV (QuotientGroup.mk' (U.1 : Subgroup G) x) =
      QuotientGroup.mk' (V.1 : Subgroup G) x
theorem

transition_comp_quotientProj

L317 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.transition_comp_quotientProj
Documentation

Composing the transition map with the smaller quotient projection gives the larger quotient projection.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem transition_comp_quotientProj {U V : OpenNormalSubgroupInClass C G}
    (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
    (transition (C := C) (G := G) hUV).comp (quotientProj (C := C) U) =
      quotientProj (C := C) V
theorem

transition_surjective

L324 ↗
ProCGroups.ProC.OpenNormalSubgroupInClass.transition_surjective
Documentation

Transition maps between quotients by nested open-normal-in-class subgroups are surjective.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroupInClass
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem transition_surjective {U V : OpenNormalSubgroupInClass C G}
    (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
    Function.Surjective (transition (C := C) (G := G) hUV)
def

openNormalSubgroupInClassSystem

L340 ↗
ProCGroups.ProC.openNormalSubgroupInClassSystem
Documentation

The inverse system of quotient groups indexed by open normal subgroups whose quotients lie in \(C\), ordered by reverse inclusion.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def openNormalSubgroupInClassSystem (C : FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    InverseSystems.InverseSystem (I := OrderDual (OpenNormalSubgroupInClass C G)) where
  X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
  topologicalSpace := fun _ => inferInstance
  map := fun {U V} hUV =>
    OpenNormalSubgroupInClass.map (C := C) (G := G)
      (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV
  continuous_map := by
    intro U V hUV
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (OpenNormalSubgroupInClass.map_id
          (C := C) (G := G) (U := OrderDual.ofDual U))) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    rcases QuotientGroup.mk'_surjective
        ((((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
    rfl
instance

instGroupOpenNormalSubgroupInClassSystemX

L366 ↗
ProCGroups.ProC.instGroupOpenNormalSubgroupInClassSystemX
Documentation

Every coordinate of the open-normal-in-class inverse system is a quotient group.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instGroupOpenNormalSubgroupInClassSystemX
    (U : OrderDual (OpenNormalSubgroupInClass C G)) :
    Group ((openNormalSubgroupInClassSystem C G).X U)
def

openNormalSubgroupInClassProj

L376 ↗
ProCGroups.ProC.openNormalSubgroupInClassProj
Documentation

The canonical quotient homomorphisms from \(G\) into the open-normal-subgroup inverse system whose quotients lie in \(C\).

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def openNormalSubgroupInClassProj
    (U : OrderDual (OpenNormalSubgroupInClass C G)) :
    G →* G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
theorem

openNormalSubgroupInClassProj_compatible

L382 ↗
ProCGroups.ProC.openNormalSubgroupInClassProj_compatible
Documentation

The canonical quotient homomorphisms are compatible with the transition maps.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
theorem openNormalSubgroupInClassProj_compatible :
    (openNormalSubgroupInClassSystem C G).CompatibleMaps
      (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
        openNormalSubgroupInClassProj (C := C) (G := G) U) := by
  intro U V hUV
  funext g
  rfl
instance

instIsGroupSystemOpenNormalSubgroupInClassSystem

L391 ↗
ProCGroups.ProC.instIsGroupSystemOpenNormalSubgroupInClassSystem
Documentation

The quotient system attached to open normal subgroups in \(C\) is group-valued.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instIsGroupSystemOpenNormalSubgroupInClassSystem :
    InverseSystems.IsGroupSystem (openNormalSubgroupInClassSystem C G) where
  map_one := by
    intro i j hij
    change
      OpenNormalSubgroupInClass.map
        (C := C) (G := G)
        (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij 1 = 1
    exact
      (OpenNormalSubgroupInClass.map
        (C := C) (G := G)
        (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_one
  map_mul := by
    intro i j hij x y
    change
      OpenNormalSubgroupInClass.map
        (C := C) (G := G)
        (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij (x * y) =
          OpenNormalSubgroupInClass.map
            (C := C) (G := G)
            (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x *
          OpenNormalSubgroupInClass.map
            (C := C) (G := G)
            (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij y
    exact
      (OpenNormalSubgroupInClass.map
        (C := C) (G := G)
        (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_mul x y
  map_inv := by
    intro i j hij x
    change
      OpenNormalSubgroupInClass.map
        (C := C) (G := G)
        (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x⁻¹ =
          (OpenNormalSubgroupInClass.map
            (C := C) (G := G)
            (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x)⁻¹
    exact
      (OpenNormalSubgroupInClass.map
        (C := C) (G := G)
        (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_inv x
theorem

openNormalSubgroupInClassProj_surjective

L435 ↗
ProCGroups.ProC.openNormalSubgroupInClassProj_surjective
Documentation

Each projection from \(G\) to an open-normal-in-class quotient is surjective.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem openNormalSubgroupInClassProj_surjective
    (U : OrderDual (OpenNormalSubgroupInClass C G)) :
    Function.Surjective (openNormalSubgroupInClassProj (C := C) (G := G) U)
theorem

directed_openNormalSubgroupInClass

L442 ↗
ProCGroups.ProC.directed_openNormalSubgroupInClass
Documentation

The open-normal-in-class index family is directed under reverse inclusion.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · full declaration
theorem directed_openNormalSubgroupInClass
    (hForm : FiniteGroupClass.Formation C) :
    Directed (α := OrderDual (OpenNormalSubgroupInClass C G)) (· ≤ ·) fun U => U := by
  intro U V
  let W : OpenNormalSubgroupInClass C G :=
    ⟨U.1 ⊓ V.1,
      FiniteGroupClass.Formation.quotient_inf_mem
        (C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩
  refine ⟨OrderDual.toDual W, ?_, ?_⟩
  · change ((W.1 : Subgroup G) ≤ (U.1 : Subgroup G))
    exact inf_le_left
  · change ((W.1 : Subgroup G) ≤ (V.1 : Subgroup G))
    exact inf_le_right
theorem

ofContinuousMulEquiv

L468 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.ofContinuousMulEquiv
Documentation

The open-normal quotient-basis property is preserved by continuous multiplicative equivalences.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem ofContinuousMulEquiv
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (hG : HasOpenNormalBasisInClass C G) (e : G ≃ₜ* H) :
    HasOpenNormalBasisInClass C H
theorem

hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed

L492 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
Documentation

With isomorphism and quotient closure, the basis property implies that every open-normal quotient lies in the class.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (hG : HasOpenNormalBasisInClass C G) :
    ∀ U : OpenNormalSubgroup G, C (G ⧸ (U : Subgroup G))
theorem

quotient_mem

L512 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.quotient_mem
Documentation

For a group with an open-normal \(C\)-basis, every open-normal quotient lies in C when C is a formation.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem quotient_mem (hForm : FiniteGroupClass.Formation C)
    (hG : HasOpenNormalBasisInClass C G) (U : OpenNormalSubgroup G) :
    C (G ⧸ (U : Subgroup G))
theorem

exists_openNormalSubgroupInClass_sub_open_nhds_of_one

L521 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.exists_openNormalSubgroupInClass_sub_open_nhds_of_one
Documentation

Every open neighborhood of 1 contains an indexed open normal subgroup whose quotient lies in C.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem exists_openNormalSubgroupInClass_sub_open_nhds_of_one (hG : HasOpenNormalBasisInClass C G)
    {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
    ∃ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G)) ⊆ W
theorem

exists_openNormalSubgroupInClass_eq_on_right_coset_of_continuous_discrete

L532 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.exists_openNormalSubgroupInClass_eq_on_right_coset_of_continuous_discrete
Documentation

A continuous map to a discrete target is locally fixed on a sufficiently small right coset, with the small subgroup chosen from the open normal subgroups whose quotients lie in C.

Source context 10 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section DiscreteCoset
omit [IsTopologicalGroup G] in
Lean source · statement
theorem exists_openNormalSubgroupInClass_eq_on_right_coset_of_continuous_discrete
    (hG : HasOpenNormalBasisInClass C G)
    [ContinuousMul G]
    {A : Type v} [TopologicalSpace A] [DiscreteTopology A]
    (f : G → A) (hf : Continuous f) (g₀ : G) :
    ∃ U : OpenNormalSubgroupInClass C G,
      ∀ g : G, g * g₀⁻¹ ∈ (U.1 : Subgroup G) → f g = f g₀
theorem

iInf_openNormalSubgroupInClass_eq_bot

L562 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.iInf_openNormalSubgroupInClass_eq_bot
Documentation

In a Hausdorff group with an open-normal \(C\)-basis, the open normal subgroups whose quotients lie in C have trivial total intersection.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · full declaration
theorem iInf_openNormalSubgroupInClass_eq_bot (hG : HasOpenNormalBasisInClass C G) :
    iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) = (⊥ : Subgroup G) := by
  apply le_antisymm
  · intro x hx
    change x = 1
    by_contra hxne
    let W : Set G := ({x} : Set G)ᶜ
    have hW : IsOpen W := by
      simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
    have h1W : (1 : G) ∈ W := by
      have hx1 : (1 : G) ≠ x := by
        intro h1x
        exact hxne h1x.symm
      simpa [W] using hx1
    rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
    have hxall : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G) := by
      simpa [Subgroup.mem_iInf] using hx
    have hxU : x ∈ (U.1 : Subgroup G) := hxall U
    have hxW : x ∈ W := hUW hxU
    exact hxW (by simp only [Set.mem_singleton_iff])
  · exact bot_le
theorem

iInter_openNormalSubgroupInClass_eq_singleton

L586 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.iInter_openNormalSubgroupInClass_eq_singleton
Documentation

Set-theoretic form of the trivial-intersection statement.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem iInter_openNormalSubgroupInClass_eq_singleton (hG : HasOpenNormalBasisInClass C G) :
    (⋂ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G))) = ({1} : Set G)
theorem

exists_openNormalBasisInClassFamily

L601 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.exists_openNormalBasisInClassFamily
Documentation

Explicit family form of the open-normal basis and trivial-intersection package.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · full declaration
theorem exists_openNormalBasisInClassFamily (hG : HasOpenNormalBasisInClass C G) :
    ∃ ι : Type u, ∃ U : ι → OpenNormalSubgroup G,
      (∀ i, C (G ⧸ (U i : Subgroup G))) ∧
      (∀ W : Set G, IsOpen W → (1 : G) ∈ W →
        ∃ i, (((U i : Subgroup G) : Set G)) ⊆ W) ∧
      iInf (fun i => (U i : Subgroup G)) = (⊥ : Subgroup G) := by
  refine ⟨OpenNormalSubgroupInClass C G, fun i => i.1, ?_, ?_, ?_⟩
  · intro i
    exact i.2
  · intro W hW h1W
    rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
    exact ⟨U, hUW⟩
  · simpa using hG.iInf_openNormalSubgroupInClass_eq_bot
theorem

eq_one_of_mem_all_openNormalSubgroupInClass

L617 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.eq_one_of_mem_all_openNormalSubgroupInClass
Documentation

Membership in every open-normal-in-class subgroup forces an element to be trivial.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem eq_one_of_mem_all_openNormalSubgroupInClass (hG : HasOpenNormalBasisInClass C G) {x : G}
    (hx : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G)) :
    x = 1
theorem

exists_openNormalSubgroupInClass_not_mem

L628 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.exists_openNormalSubgroupInClass_not_mem
Documentation

If x ≠ 1, then some open normal subgroup in the class-family omits x.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem exists_openNormalSubgroupInClass_not_mem (hG : HasOpenNormalBasisInClass C G) {x : G}
    (hx : x ≠ 1) :
    ∃ U : OpenNormalSubgroupInClass C G, x ∉ (U.1 : Subgroup G)
theorem

eq_of_forall_openNormalSubgroupInClass_quotient_eq

L641 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.eq_of_forall_openNormalSubgroupInClass_quotient_eq
Documentation

In a Hausdorff group with an open-normal \(C\)-basis, two elements are equal once they agree in every quotient by an open normal subgroup whose quotient lies in C.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem eq_of_forall_openNormalSubgroupInClass_quotient_eq (hG : HasOpenNormalBasisInClass C G)
    {x y : G}
    (hxy : ∀ U : OpenNormalSubgroupInClass C G,
      QuotientGroup.mk' (U.1 : Subgroup G) x = QuotientGroup.mk' (U.1 : Subgroup G) y) :
    x = y
theorem

eq_of_forall_openNormalSubgroupInClassProj_eq

L658 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.eq_of_forall_openNormalSubgroupInClassProj_eq
Documentation

In a Hausdorff group with an open-normal \(C\)-basis, coordinatewise equality in the canonical inverse-system projections forces equality in the ambient group.

Source context 11 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
section Hausdorff
variable [T2Space G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem eq_of_forall_openNormalSubgroupInClassProj_eq (hG : HasOpenNormalBasisInClass C G) {x y : G}
    (hxy : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),
      openNormalSubgroupInClassProj (C := C) (G := G) U x =
        openNormalSubgroupInClassProj (C := C) (G := G) U y) :
    x = y
theorem

of_allOpenNormalQuotients

L675 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.of_allOpenNormalQuotients
Documentation

For a profinite group, the stronger all-open-normal-quotient condition supplies an open-normal \(C\)-basis.

Source context 8 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · statement
theorem of_allOpenNormalQuotients [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hquot : ∀ U : OpenNormalSubgroup G, C (G ⧸ (U : Subgroup G))) :
    HasOpenNormalBasisInClass C G
theorem

openNormalSubgroupInClass_nonempty

L685 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.openNormalSubgroupInClass_nonempty
Documentation

An open-normal \(C\)-basis contains at least one subgroup.

Source context 9 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
omit [IsTopologicalGroup G] in
Lean source · statement
theorem openNormalSubgroupInClass_nonempty (hG : HasOpenNormalBasisInClass C G) :
    Nonempty (OpenNormalSubgroupInClass C G)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.