NYLL
Module

LimitPresentation.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
10 declarations indexed from sourceView source ↗

Module documentation

Presenting pro-\(C\) groups as inverse limits

The canonical map to the inverse limit of all finite open-normal quotients is identified stage by stage and shown to be a multiplicative equivalence. An exact quotient-basis condition then yields the Hausdorff, totally disconnected, and pro-\(C\) structures.

Compatibility with mathlib's finite-quotient presentation

Imports5
Imported by6

Declarations

theorem

toFiniteQuotientFunctor_map_apply_openNormalSubgroupInClass

L34 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.toFiniteQuotientFunctor_map_apply_openNormalSubgroupInClass
Documentation

On open normal subgroups whose quotient lies in \(C\), mathlib's finite-quotient functor uses the same transition maps as openNormalSubgroupInClassSystem.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · full declaration
theorem toFiniteQuotientFunctor_map_apply_openNormalSubgroupInClass
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {U V : OpenNormalSubgroupInClass C G}
    (hUV : U.1 ≤ V.1) (x : G ⧸ (U.1 : Subgroup G)) :
    (ProfiniteGrp.toFiniteQuotientFunctor (ProfiniteGrp.of G)).map
        (CategoryTheory.homOfLE hUV) x =
      OpenNormalSubgroupInClass.map (C := C) (G := G) (U := V) (V := U)
        (show (U.1 : Subgroup G) ≤ (V.1 : Subgroup G) from hUV) x := by
  rfl
theorem

toLimit_val_openNormalSubgroupInClass

L49 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.toLimit_val_openNormalSubgroupInClass
Documentation

The coordinate of mathlib's canonical ProfiniteGrp.toLimit map at an in-class open normal subgroup is the quotient projection used by openNormalSubgroupInClassSystem.

We state this through the explicit .val coordinate of ProfiniteGrp.limit; this avoids choosing a second, potentially non-definitionally-equal HasLimit instance merely to name the projection.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · statement
theorem toLimit_val_openNormalSubgroupInClass
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (U : OpenNormalSubgroupInClass C G) (g : G) :
    (ProfiniteGrp.toLimit (ProfiniteGrp.of G) g).val U.1 =
      openNormalSubgroupInClassProj (C := C) (G := G) (OrderDual.toDual U) g
def

openNormalSubgroupInClassMulEquivInverseLimit

L60 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.openNormalSubgroupInClassMulEquivInverseLimit
Documentation

A pro-\(C\) group is canonically the inverse limit of its quotients by open normal subgroups whose quotients lie in \(C\).

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · statement
def openNormalSubgroupInClassMulEquivInverseLimit
    [CompactSpace G] [T2Space G]
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    G ≃ₜ* (openNormalSubgroupInClassSystem C G).inverseLimit
theorem

openNormalSubgroupInClassMulEquivInverseLimit_projection

L139 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.openNormalSubgroupInClassMulEquivInverseLimit_projection
Documentation

Under the canonical equivalence from a pro-\(C\) group to the inverse limit of its open-normal \(C\)-quotients, the \(U\)-coordinate of an element is its quotient class modulo \(U\).

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · statement
theorem openNormalSubgroupInClassMulEquivInverseLimit_projection
    [CompactSpace G] [T2Space G]
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
    (U : OrderDual (OpenNormalSubgroupInClass C G)) (g : G) :
    (openNormalSubgroupInClassSystem C G).projection U
        (openNormalSubgroupInClassMulEquivInverseLimit
          (C := C) (G := G) hForm hG g) =
      openNormalSubgroupInClassProj (C := C) (G := G) U g
theorem

openNormalSubgroupInClassMulEquivInverseLimit_projection_eq_toLimit_val

L156 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.openNormalSubgroupInClassMulEquivInverseLimit_projection_eq_toLimit_val
Documentation

The concrete pro-\(C\) presentation and mathlib's finite-quotient presentation have identical canonical coordinates. The generic concrete/categorical-limit comparison is InverseSystems.InverseSystem.profiniteGrpConeIsLimit.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · statement
theorem openNormalSubgroupInClassMulEquivInverseLimit_projection_eq_toLimit_val
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
    (U : OpenNormalSubgroupInClass C G) (g : G) :
    (openNormalSubgroupInClassSystem C G).projection (OrderDual.toDual U)
        (openNormalSubgroupInClassMulEquivInverseLimit
          (C := C) (G := G) hForm hG g) =
      (ProfiniteGrp.toLimit (ProfiniteGrp.of G) g).val U.1
theorem

isomorphic_to_inverseLimit_finiteGroupsInClass

L172 ↗
ProCGroups.ProC.HasOpenNormalBasisInClass.isomorphic_to_inverseLimit_finiteGroupsInClass
Documentation

A pro-\(C\) group is topologically isomorphic to an inverse limit of finite groups in \(C\), realized using the quotient system indexed by the open normal subgroups whose quotients lie in \(C\).

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace HasOpenNormalBasisInClass
Lean source · full declaration
theorem isomorphic_to_inverseLimit_finiteGroupsInClass
    [CompactSpace G] [T2Space G]
    (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    let S := openNormalSubgroupInClassSystem C G
    (∀ U : OrderDual (OpenNormalSubgroupInClass C G), C (S.X U) ∧ Finite (S.X U)) ∧
      Nonempty (G ≃ₜ* S.inverseLimit) := by
  let S := openNormalSubgroupInClassSystem C G
  refine ⟨?_, ⟨openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG⟩⟩
  intro U
  dsimp [S, openNormalSubgroupInClassSystem]
  refine ⟨(OrderDual.ofDual U).2, ?_⟩
  exact C.finite (OrderDual.ofDual U).2
def

HasExactOpenNormalQuotientBasisInClass

L191 ↗
ProCGroups.ProC.HasExactOpenNormalQuotientBasisInClass
Documentation

Existence of an open-normal subgroup basis whose quotients lie in \(C\) and whose quotient presentations are exact.

Source context 4 commands

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

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

t2Space_of_exactOpenNormalQuotientBasisInClass

L201 ↗
ProCGroups.ProC.t2Space_of_exactOpenNormalQuotientBasisInClass
Documentation

An open-normal family with trivial intersection makes the group Hausdorff.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem t2Space_of_exactOpenNormalQuotientBasisInClass
    (hC : HasExactOpenNormalQuotientBasisInClass C G) : T2Space G
theorem

totallyDisconnectedSpace_of_exactOpenNormalQuotientBasisInClass

L247 ↗
ProCGroups.ProC.totallyDisconnectedSpace_of_exactOpenNormalQuotientBasisInClass
Documentation

An open-normal family yields a clopen basis and total disconnectedness.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem totallyDisconnectedSpace_of_exactOpenNormalQuotientBasisInClass
    (hC : HasExactOpenNormalQuotientBasisInClass C G) : TotallyDisconnectedSpace G
theorem

hasOpenNormalBasisInClass_of_hasExactOpenNormalQuotientBasisInClass

L282 ↗
ProCGroups.ProC.hasOpenNormalBasisInClass_of_hasExactOpenNormalQuotientBasisInClass
Documentation

An exact open-normal quotient basis in \(C\) implies HasOpenNormalBasisInClass C G. This direction needs no formation closure because the chosen basis already supplies the required open-normal quotients in \(C\).

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem hasOpenNormalBasisInClass_of_hasExactOpenNormalQuotientBasisInClass
    (hC : HasExactOpenNormalQuotientBasisInClass C G) : HasOpenNormalBasisInClass C G

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