ProCGroups.FreeProC.FiniteBasis

6 Theorems | 3 Definitions

This module develops the finite-basis interface for ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData. Its canonical finite index is ULift (Fin n), which lies in the carrier universe required by the generated-target lifting property. Concrete Fin n displays can be obtained by reindexing with ULift.up.

import

ProCGroups.FreeProC.Basic

Imported by

Definition CrowellExactSequence.freeProCChosenBasisEquivOfBasisCard

def freeProCChosenBasisEquivOfBasisCard
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
    sourceData.basis ≃ Fin n :=
  Classical.choice ((Cardinal.mk_eq_nat_iff).1 hbasis)

Choose an equivalence from a finite epimorphically free pro-\(C\) basis to \(\operatorname{Fin} n\).

Definition CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard

def freeProCChosenULiftFamilyOfBasisCard
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
    ULift.{u} (Fin n) → sourceData.carrier :=
  fun i =>
    sourceData.inclusion
      ((freeProCChosenBasisEquivOfBasisCard (C := C) sourceData hbasis).symm i.down)

The canonical chosen finite family. The universe lift keeps its generator type in the same universe as the pro-\(C\) carrier.

Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

theorem freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
    ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) (ULift.{u} (Fin n)) sourceData.carrier
      (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)

Reindexing preserves the epimorphically free pro-\(C\) converging-basis property.

Show Lean proof

Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_generates

theorem freeProCChosenULiftFamilyOfBasisCard_generates
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
    ProCGroups.Generation.TopologicallyGenerates
      (G := sourceData.carrier)
      (Set.range (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis))

The canonical chosen family topologically generates the epimorphically free pro-\(C\) source.

Show Lean proof

Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

theorem freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
    {H : Type u} [Group H] [TopologicalSpace H]
    (ψ : sourceData.carrier →* H) :
    ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
      (G := H)
      (fun i : ULift.{u} (Fin n) =>
        ψ (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))

The image of the finite lifted basis under any target homomorphism satisfies the open-subgroup convergence condition used by the epimorphically free pro-\(C\) formulation.

Show Lean proof

Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

theorem freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
    ProCGroups.Generation.TopologicallyGenerates
      (G := H)
      (Set.range
        (fun i : ULift.{u} (Fin n) =>
          psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)))

A surjective continuous homomorphism carries the lifted chosen finite basis to a topological generating family of the target.

Show Lean proof

Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective

theorem freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
    (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
    (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree
      (C := C) sourceData hbasis).liftHom hH
        (fun i : ULift.{u} (Fin n) =>
          psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))
        (freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
          (C := C) sourceData hbasis psi.toMonoidHom)
        (freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
          (C := C) sourceData hbasis psi hpsi) =
      psi

For the lifted finite basis, the generated-target lift of a surjective target map is the target map itself. This is the concrete bridge needed when Fox constructions produce a right component from the epimorphic lifting property.

Show Lean proof

Theorem CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective

theorem freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective
    {C : ProCGroups.FiniteGroupClass.{u}}
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (V : OpenNormalSubgroupInClass C sourceData.carrier) :
    Function.Surjective
      ((QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)).comp
        (FreeGroup.lift
          (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)))

The chosen lifted finite free basis surjects onto every finite open-normal quotient of the free pro-\(C\) source.

Show Lean proof

Definition CrowellExactSequence.finULiftEquiv

def finULiftEquiv (r : Nat) : Fin r ≃ ULift.{u} (Fin r) where
  toFun i := ULift.up i
  invFun i := i.down
  left_inv := by
    intro i
    rfl
  right_inv := by
    intro i
    cases i
    rfl

The finite-index lift comparison is an equivalence, with inverse given by the reverse comparison map.

ProCGroups.FreeProC.FiniteBasis

Declarations