Module

FiniteBasis.lean

Nyll.ProCGroups.FreeProC.FiniteBasis

9 declarations indexed from sourceView source ↗

Module documentation

Free pro-C finite-basis utilities

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.

Imports1

Nyll.ProCGroups.FreeProC.Basic

Imported by11

def

freeProCChosenBasisEquivOfBasisCard

L32 ↗

CrowellExactSequence.freeProCChosenBasisEquivOfBasisCard

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · statement

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

def

freeProCChosenULiftFamilyOfBasisCard

L42 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · statement

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

theorem

freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

L53 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · statement

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)

theorem

freeProCChosenULiftFamilyOfBasisCard_generates

L94 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_generates

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · statement

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))

theorem

freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

L108 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

Documentation

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.

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · full declaration

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)) := by
  exact ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain
    (G := H)
    (fun i : ULift.{u} (Fin n) =>
      ψ (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))

theorem

freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

L126 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · full declaration

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))) := by
  let family : ULift.{u} (Fin n) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  have hsourceGen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := sourceData.carrier) (Set.range family) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_generates (C := C) sourceData hbasis
  have himage :=
    ProCGroups.Generation.topologicallyGenerates_image_of_continuousMonoidHom_surjective
      (G := sourceData.carrier) (H := H) psi hpsi hsourceGen
  have hrange :
      psi '' Set.range family = Set.range (fun i => psi (family i)) := by
    ext h
    constructor
    · rintro ⟨g, ⟨i, rfl⟩, rfl⟩
      exact ⟨i, rfl⟩
    · rintro ⟨i, rfl⟩
      exact ⟨family i, ⟨i, rfl⟩, rfl⟩
  simpa [family, hrange] using himage

theorem

freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective

L161 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective

Documentation

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.

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · full declaration

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 := by
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let liftedFamily : ULift.{u} (Fin n) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  let φ : ULift.{u} (Fin n) → H := fun i => psi (liftedFamily i)
  let hconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ :=
    by
      simpa [φ, liftedFamily] using
        freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
          (C := C) sourceData hbasis psi.toMonoidHom
  let hgen :
      ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
    simpa [φ, liftedFamily] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  ext g
  have hmon :
      psi.toMonoidHom = hfree.lift hH φ hconv hgen :=
    hfree.lift_unique hH φ hconv hgen psi.continuous_toFun (by
      intro i
      rfl)
  exact (congrArg (fun f : sourceData.carrier →* H => f g) hmon).symm

theorem

freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective

L207 ↗

CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · statement

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)))

def

finULiftEquiv

L266 ↗

CrowellExactSequence.finULiftEquiv

Documentation

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

Source context 6 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.ProC
open ProCGroups.ProC.HasOpenNormalBasisInClass
universe u

Lean source · full declaration

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

Module documentation

Free pro-C finite-basis utilities

Declarations