Module

TruncatedFoxSequence.lean

Nyll.ProCGroups.GolodShafarevich.TruncatedFoxSequence

4 declarations indexed from sourceView source ↗

Module documentation

Right exactness of the truncated mod-p Fox sequence

Strict lifting for the filtered Fox complex and the augmentation-ideal description of the boundary range give a concrete right-exact sequence on shifted finite truncations.

Imports1

Nyll.ProCGroups.GolodShafarevich.TruncatedFoxMaps

Imported by2

theorem

presentationModPTruncatedRelationBoundary_exact

L35 ↗

ClassFieldTower.ProP.presentationModPTruncatedRelationBoundary_exact

Documentation

Strict filtered lifting makes the induced relation--boundary pair exact.

Source context 10 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open FoxDifferential
open ProCGroups
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem presentationModPTruncatedRelationBoundary_exact
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) :
    Function.Exact (presentationModPTruncatedRelationMap P ν hν N)
      (presentationModPTruncatedFoxBoundary P N)

theorem

presentationModPTruncatedBoundaryAugmentation_exact

L82 ↗

ClassFieldTower.ProP.presentationModPTruncatedBoundaryAugmentation_exact

Documentation

Tail equality identifies the induced boundary kernel with its range.

Source context 10 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open FoxDifferential
open ProCGroups
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem presentationModPTruncatedBoundaryAugmentation_exact
    (P : FiniteProPPresentation p d r sourceData G) (N : ℕ) :
    Function.Exact (presentationModPTruncatedFoxBoundary P N)
      (presentationModPTruncatedAugmentation (p := p) (G := G) N)

theorem

presentationModPTruncatedAugmentation_surjective

L120 ↗

ClassFieldTower.ProP.presentationModPTruncatedAugmentation_surjective

Documentation

The induced augmentation is surjective.

Source context 11 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open FoxDifferential
open ProCGroups
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem presentationModPTruncatedAugmentation_surjective (N : ℕ) :
    Function.Surjective
      (presentationModPTruncatedAugmentation (p := p) (G := G) N)

theorem

presentationModP_truncatedFoxSequence_rightExact

L131 ↗

ClassFieldTower.ProP.presentationModP_truncatedFoxSequence_rightExact

Documentation

Concrete right-exact data for the truncated mod-p Fox sequence.

Source context 10 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open FoxDifferential
open ProCGroups
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem presentationModP_truncatedFoxSequence_rightExact
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) :
    Function.Exact (presentationModPTruncatedRelationMap P ν hν N)
        (presentationModPTruncatedFoxBoundary P N) ∧
      Function.Exact (presentationModPTruncatedFoxBoundary P N)
        (presentationModPTruncatedAugmentation (p := p) (G := G) N) ∧
      Function.Surjective
        (presentationModPTruncatedAugmentation (p := p) (G := G) N)

Module documentation

Right exactness of the truncated mod-p Fox sequence

Declarations

presentationModPTruncatedRelationBoundary_exact

presentationModPTruncatedBoundaryAugmentation_exact

presentationModPTruncatedAugmentation_surjective

presentationModP_truncatedFoxSequence_rightExact