NYLL
Module

MainTheorem.lean

Nyll.ProCGroups.CrowellExactSequence.Profinite.MainTheorem
8 declarations indexed from sourceView source ↗

Module documentation

Crowell Exact Sequence / Profinite / Main Theorem

This module packages the separated completed Crowell and Blanchfield--Lyndon sequences as FourTermLinearSequence values and states their exactness theorems under the required formation hypotheses.

Imports1
Imported by1

Declarations

def

profiniteSeparatedCrowellLinearSequence

L33 ↗
CrowellExactSequence.profiniteSeparatedCrowellLinearSequence
Documentation

The separated completed Crowell sequence over pro-C integer coefficients. The additive head map and the completed augmentation are viewed canonically as ℤ-linear maps.

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 profiniteSeparatedCrowellLinearSequence
    [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) :
    FourTermLinearSequence ℤ
      (ProfiniteKernelAbelianizationAdd psi)
      (ZCSeparatedCompletedDifferentialModule
        C psi.toMonoidHom)
      (ZCCompletedGroupAlgebra C H)
      (ZCCoeff C)
theorem

profiniteSeparatedCrowellLinearSequence_isExact

L75 ↗
CrowellExactSequence.profiniteSeparatedCrowellLinearSequence_isExact
Documentation

The separated completed Crowell exact sequence over pro-\(C\) integer coefficients, packaged as the full four-term exact sequence \(N^{\mathrm{ab}}(C)\) \(\to\) \(A_{\psi}(C)\) \(\to\) \(\mathbb{Z}_C\llbracket H\rrbracket\) \(\to\) \(\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 profiniteSeparatedCrowellLinearSequence_isExact
    [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) :
    (profiniteSeparatedCrowellLinearSequence
      (H := H) (C := C) hC sourceData hbasis psi hpsi).IsExact
def

profiniteSeparatedBlanchfieldLyndonBoundaryLinear

L89 ↗
CrowellExactSequence.profiniteSeparatedBlanchfieldLyndonBoundaryLinear
Documentation

The separated Blanchfield--Lyndon head map in the universe-lifted coordinates, bundled as an integer-linear map.

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 profiniteSeparatedBlanchfieldLyndonBoundaryLinear
    [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) :
    ProfiniteKernelAbelianizationAdd psi →ₗ[ℤ]
      ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H)
def

profiniteSeparatedBlanchfieldLyndonLinearSequence

L107 ↗
CrowellExactSequence.profiniteSeparatedBlanchfieldLyndonLinearSequence
Documentation

The canonical separated Blanchfield--Lyndon sequence in the universe-lifted coordinate 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 profiniteSeparatedBlanchfieldLyndonLinearSequence
    [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) :
    FourTermLinearSequence ℤ
      (ProfiniteKernelAbelianizationAdd psi)
      (ZCFreeFoxCoordinates C
        (X := ULift.{u} (Fin r)) (H := H))
      (ZCCompletedGroupAlgebra C H)
      (ZCCoeff C)
theorem

profiniteSeparatedBlanchfieldLyndonLinearSequence_isExact

L170 ↗
CrowellExactSequence.profiniteSeparatedBlanchfieldLyndonLinearSequence_isExact
Documentation

The separated completed Blanchfield--Lyndon exact sequence in the universe-lifted finite coordinate basis, packaged as the full four-term exact sequence.

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 profiniteSeparatedBlanchfieldLyndonLinearSequence_isExact
    [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) :
    (profiniteSeparatedBlanchfieldLyndonLinearSequence
      (H := H) (C := C) hC sourceData hbasis psi hpsi).IsExact
def

finULiftCompletedGroupAlgebraCoordinateLinearEquiv

L184 ↗
CrowellExactSequence.finULiftCompletedGroupAlgebraCoordinateLinearEquiv
Documentation

The integer-linear coordinate equivalence from concrete Fin r coordinates to the universe-lifted coordinates used by the epimorphic generated-target lifting property.

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 finULiftCompletedGroupAlgebraCoordinateLinearEquiv (r : Nat) :
    (Fin r → ZCCompletedGroupAlgebra C H) ≃ₗ[ℤ]
      (ULift.{u} (Fin r) → ZCCompletedGroupAlgebra C H)
def

profiniteSeparatedBlanchfieldLyndonFinLinearSequence

L193 ↗
CrowellExactSequence.profiniteSeparatedBlanchfieldLyndonFinLinearSequence
Documentation

The canonical concrete-coordinate BL sequence, obtained by reindexing the bundled universe-lifted sequence once at sequence level.

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 profiniteSeparatedBlanchfieldLyndonFinLinearSequence
    [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) :
    FourTermLinearSequence ℤ
      (ProfiniteKernelAbelianizationAdd psi)
      (Fin r → ZCCompletedGroupAlgebra C H)
      (ZCCompletedGroupAlgebra C H)
      (ZCCoeff C)
theorem

profiniteSeparatedBlanchfieldLyndonFinLinearSequence_isExact

L215 ↗
CrowellExactSequence.profiniteSeparatedBlanchfieldLyndonFinLinearSequence_isExact
Documentation

The separated completed Blanchfield--Lyndon exact sequence in the concrete \(\operatorname{Fin} r\) coordinate basis, packaged as the full four-term exact sequence.

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 profiniteSeparatedBlanchfieldLyndonFinLinearSequence_isExact
    [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) :
    (profiniteSeparatedBlanchfieldLyndonFinLinearSequence
      (H := H) (C := C) hC sourceData hbasis psi hpsi).IsExact

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