NYLL
Module

Coordinates.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Coordinates
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — coordinates

The principal declarations in this module are:

  • freeProCChosenULift_closedGeneratedCoordinateMap

The coordinate map determined by the chosen \(U\)-lifts has the specified closed generated image.

  • freeProCChosenULift_sepFamilyMap

The separated finite-family map sends lifted chosen-basis coordinates to the separated completed differential module.

  • freeProCChosenULift_sepFamilyMap_single

The separated family map sends the standard vector at a chosen lifted basis element to its separated universal differential.

  • freeProCChosenULift_sepCoordinateMap_universal

The separated coordinate map sends the separated universal differential to the closed-generated Fox derivative vector.

Imports3
Imported by2

Declarations

def

freeProCChosenULift_closedGeneratedCoordinateMap

L47 ↗
CrowellExactSequence.freeProCChosenULift_closedGeneratedCoordinateMap
Documentation

The coordinate map determined by the chosen \(U\)-lifts has the specified closed generated image.

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
def freeProCChosenULift_closedGeneratedCoordinateMap
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi) :
    ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[
      ZCCompletedGroupAlgebra C H]
      ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H)
def

freeProCChosenULift_sepFamilyMap

L92 ↗
CrowellExactSequence.freeProCChosenULift_sepFamilyMap
Documentation

The separated finite-family map sends lifted chosen-basis coordinates to the separated completed differential module.

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
def freeProCChosenULift_sepFamilyMap
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H) :
    ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H) →ₗ[
      ZCCompletedGroupAlgebra C H]
      ZCSeparatedCompletedDifferentialModule
        C psi.toMonoidHom
theorem

freeProCChosenULift_sepFamilyMap_single

L111 ↗
CrowellExactSequence.freeProCChosenULift_sepFamilyMap_single
Documentation

The separated family map sends the standard vector at a chosen lifted basis element to its separated universal differential.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
omit [C.ContainsTrivialQuotients] in
Lean source · statement
theorem freeProCChosenULift_sepFamilyMap_single
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ULift.{u} (Fin r)) :
    freeProCChosenULift_sepFamilyMap
        (H := H) (C := C) sourceData hbasis psi
        (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
      zcSeparatedUniversalDifferential
        C psi.toMonoidHom
        (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)
def

freeProCChosenULift_sepCoordinateMap

L128 ↗
CrowellExactSequence.freeProCChosenULift_sepCoordinateMap
Documentation

The separated closed-generated coordinate map for the chosen finite free pro-\(C\) basis.

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
def freeProCChosenULift_sepCoordinateMap
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    [T1Space
      (ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H))] :
    ZCSeparatedCompletedDifferentialModule
        C psi.toMonoidHom →ₗ[
      ZCCompletedGroupAlgebra C H]
      ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H)
theorem

freeProCChosenULift_sepCoordinateMap_universal

L199 ↗
CrowellExactSequence.freeProCChosenULift_sepCoordinateMap_universal
Documentation

The separated coordinate map sends the separated universal differential to the closed-generated Fox derivative vector.

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · full declaration
theorem freeProCChosenULift_sepCoordinateMap_universal
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    [T1Space
      (ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H))]
    (g : sourceData.carrier) :
    freeProCChosenULift_sepCoordinateMap
        (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
        (zcSeparatedUniversalDifferential
          C psi.toMonoidHom g) =
      freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C)
        (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
        (fun i : ULift.{u} (Fin r) =>
          psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))
        (freeProCClosedGeneratedTarget_proC_of_surjective
          (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
        (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)))
        g := by
  let :
      Nonempty
        (ZCCompletedDifferentialModuleIndex
          C psi.toMonoidHom) :=
    ⟨zcCompletedDifferentialModuleComapIndex
      (C := C) (G := sourceData.carrier) (H := H)
      hC.hereditary psi
      ((ProCGroups.Completion.ProCIntegerIndex.terminal
          (C := C) inferInstance),
        zcCompletedGroupAlgebraTopIndex C H)⟩
  have hdir :
      Directed (· ≤ ·)
        (id :
          ZCCompletedDifferentialModuleIndex
              C psi.toMonoidHom →
            ZCCompletedDifferentialModuleIndex
              C psi.toMonoidHom) :=
    directed_zcCompletedDifferentialModuleIndex
      (C := C) (G := sourceData.carrier) (H := H)
      (hC.melnikovFormation.formation)
      hC.hereditary psi
  let family : ULift.{u} (Fin r) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let htarget :=
    freeProCClosedGeneratedTarget_proC_of_surjective
      (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
  let hφconv :=
    freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
      (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
  have hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H) :=
    HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
      sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
  have hφHconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
        (C := C) sourceData hbasis psi.toMonoidHom
  have hφHgen :
      ProCGroups.Generation.TopologicallyGenerates
        (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
    simpa [family] using
      freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
        (C := C) sourceData hbasis psi hpsi
  simpa [freeProCChosenULift_sepCoordinateMap, family, hfree, htarget, hφconv] using
    separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
      (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
      hdir sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen g
def

freeProCChosenULift_sepCoordinateEquiv

L278 ↗
CrowellExactSequence.freeProCChosenULift_sepCoordinateEquiv
Documentation

The separated coordinate equivalence for the chosen finite free pro-\(C\) basis.

Source context 8 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
universe u
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
Lean source · statement
def freeProCChosenULift_sepCoordinateEquiv
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hC : ProCGroups.FiniteGroupClass.FullFormation C)
    (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    [T1Space
      (ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H))] :
    ZCSeparatedCompletedDifferentialModule
        C psi.toMonoidHom ≃ₗ[
      ZCCompletedGroupAlgebra C H]
      ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H)

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