NYLL
Module

FreeExactness.lean

Nyll.ProCGroups.CrowellExactSequence.Profinite.FreeExactness
6 declarations indexed from sourceView source ↗

Module documentation

Free pro-C Crowell exactness

For a free pro-\(C\) source, this file combines continuous Magnus injectivity, the completed boundary calculation, and bifiltered finite-stage exactness. The resulting theorems assemble the presented and separated Crowell exact sequences under a surjective presentation map.

Imports3
Imported by2

Declarations

theorem

freeProC_presentedCrowellGroupAlgebraExactProCInteger_of_psi_surjective

L37 ↗
CrowellExactSequence.freeProC_presentedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
Documentation

For surjective \(\psi\), the presented Crowell group-algebra sequence over the pro-\(C\) integers is exact.

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
theorem freeProC_presentedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
    (hForm : ProCGroups.FiniteGroupClass.Formation 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) :
    Function.Exact
      (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
        (G := sourceData.carrier) (H := H) C psi)
      (zcCompletedGroupAlgebraAugmentation C H)
theorem

freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective

L64 ↗
CrowellExactSequence.freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
Documentation

For surjective \(\psi\), the separated presented Crowell group-algebra sequence over the pro-\(C\) integers is exact.

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
theorem freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
    (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) :
    Function.Exact
      (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
        (G := sourceData.carrier) (H := H) C
        hC.hereditary psi)
      (zcCompletedGroupAlgebraAugmentation C H)
theorem

freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus

L93 ↗
CrowellExactSequence.freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
Documentation

The continuous Magnus hypothesis makes the separated pro-\(C\) kernel-abelianization boundary injective.

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
theorem freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
    [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))] :
    Function.Injective
      (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
        (G := sourceData.carrier) (H := H) C psi)
theorem

freeProC_completedBoundaryKillsTopCommZC_of_closedGen_and_psi_surj

L141 ↗
CrowellExactSequence.freeProC_completedBoundaryKillsTopCommZC_of_closedGen_and_psi_surj
Documentation

Under closed generation and surjectivity of \(\psi\), the completed boundary kills the topological commutator subgroup.

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 · full declaration
theorem freeProC_completedBoundaryKillsTopCommZC_of_closedGen_and_psi_surj
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hForm : ProCGroups.FiniteGroupClass.Formation 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)
    (htarget :
      HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C)
          (fun i : ULift.{u} (Fin r) =>
            psi (freeProCChosenULiftFamilyOfBasisCard
              (C := C) sourceData hbasis i)) : Subgroup
            (ZCCompletedFoxSemidirect
              C (ULift.{u} (Fin r)) H)))
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := sourceData.carrier) (H := H) C psi
        (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger
      (G := sourceData.carrier) (H := H) C psi := by
  let family : ULift.{u} (Fin r) → sourceData.carrier :=
    freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
  let hfree :=
    freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
  let hφconv :=
    freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
      (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
  have hH : HasOpenNormalBasisInClass C H :=
    HasOpenNormalBasisInClass.of_surjective
      hForm
      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
  have hleft_graph_eq :
      ∀ g : sourceData.carrier,
        freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
            (C := C) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
            htarget hφconv g =
          presentedCompletedDifferentialFamilyCoordinatesProCInteger
            (G := sourceData.carrier) (H := H) C psi family hbasis_A
            (zcUniversalDifferential C psi.toMonoidHom g) := by
    exact
      freeProCZCCompletedFoxDerivativeVectorViaClosedGen_eq_presentedCoordinates_zcUnivDiff
        (G := sourceData.carrier) (H := H) C psi family hbasis_A hfree hH htarget hφconv
        hφHconv hφHgen
  exact
    completedBoundaryKillsTopCommZC_of_closedGen_leftGraph
      (G := sourceData.carrier) (H := H) C psi family hbasis_A hfree htarget hφconv
      hleft_graph_eq
theorem

freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages

L207 ↗
CrowellExactSequence.freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
Documentation

Continuous Magnus injectivity together with the bifiltered finite-quotient calculations gives exactness at the separated middle term for a finite-rank free pro-\(C\) presentation.

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
theorem freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
    [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))] :
    Function.Exact
      (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
        (G := sourceData.carrier) (H := H) C psi)
      (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
        (G := sourceData.carrier) (H := H) C
        hC.hereditary psi)
theorem

freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj

L359 ↗
CrowellExactSequence.freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
Documentation

The all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the separated Crowell exact sequence over \(\mathbb{Z}_C\).

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
theorem freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
    [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) :
    Function.Injective
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := sourceData.carrier) (H := H) C psi) ∧
      Function.Exact
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := sourceData.carrier) (H := H) C psi)
        (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
          (G := sourceData.carrier) (H := H) C
          hC.hereditary psi) ∧
        Function.Exact
          (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
            (G := sourceData.carrier) (H := H) C
            hC.hereditary psi)
          (zcCompletedGroupAlgebraAugmentation C H) ∧
          Function.Surjective
            (zcCompletedGroupAlgebraAugmentation C H)

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