NYLL
Module

ModPFilteredLifting.lean

Nyll.ProCGroups.ProP.Fox.ModPFilteredLifting
3 declarations indexed from sourceView source ↗

Module documentation

Strict filtered lifting for the mod-p Fox boundary

The completed Fox boundary is strict for the closed augmentation filtration: every element of filtration depth n + 1 has a coordinate preimage of depth n. The proof first shows that the boundary image of the coordinate layer is closed, using compactness of the completed group algebra. The raw power of the augmentation ideal lies in this image by algebraic multiplication and the unfiltered boundary-range theorem, so taking closures gives the strict lift.

Combining this result with unfiltered relation--boundary exactness gives the source-level lifting statement needed for exactness after passing to the shifted filtration quotients.

Imports1
Imported by2

Declarations

theorem

presentationModPFoxBoundary_coordinateFiltration_surjective

L45 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_coordinateFiltration_surjective
Documentation

Every element of closed augmentation depth n + 1 is the boundary of a Fox coordinate vector of depth n.

Source context 11 commands

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

open scoped Topology
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 presentationModPFoxBoundary_coordinateFiltration_surjective
    (P : FiniteProPPresentation p d r sourceData G) (n : ℕ)
    {x : ModPCompletedGroupAlgebra p G}
    (hx : x ∈ closedAugmentationPower p G (n + 1)) :
    ∃ v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G),
      v ∈ presentationModPFoxCoordinateFiltration
          (p := p) (d := d) (G := G) n ∧
        presentationModPFoxBoundary P v = x
theorem

presentationModPRelationMatrix_lift_mod_coordinateFiltration

L115 ↗
ClassFieldTower.ProP.presentationModPRelationMatrix_lift_mod_coordinateFiltration
Documentation

If a coordinate vector has boundary of depth n + 1, it differs from a relation-matrix image by a coordinate vector of depth n.

Source context 11 commands

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

open scoped Topology
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 presentationModPRelationMatrix_lift_mod_coordinateFiltration
    (P : FiniteProPPresentation p d r sourceData G) (n : ℕ)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    (hv : presentationModPFoxBoundary P v ∈
      closedAugmentationPower p G (n + 1)) :
    ∃ a : Fin r → ModPCompletedGroupAlgebra p G,
      v - presentationModPRelationMatrix P a ∈
        presentationModPFoxCoordinateFiltration
          (p := p) (d := d) (G := G) n
theorem

presentationModP_filteredRightExact

L142 ↗
ClassFieldTower.ProP.presentationModP_filteredRightExact
Documentation

The completed mod-p Fox--Crowell complex is filtered right-exact: the relation matrix and boundary respect their shifted filtrations, the underlying middle complex is exact, and every filtered boundary cycle admits a relation lift modulo the target filtration.

Source context 11 commands

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

open scoped Topology
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_filteredRightExact
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j) :
    (∀ (N : ℕ) {a : Fin r → ModPCompletedGroupAlgebra p G},
        a ∈ presentationModPWeightedRelationSourceFiltration
            (p := p) (G := G) ν N →
          presentationModPRelationMatrix P a ∈
            presentationModPFoxCoordinateFiltration
              (p := p) (d := d) (G := G) N) ∧
      (∀ (n : ℕ)
          {v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)},
        v ∈ presentationModPFoxCoordinateFiltration
            (p := p) (d := d) (G := G) n →
          presentationModPFoxBoundary P v ∈
            closedAugmentationPower p G (n + 1)) ∧
      Function.Exact (presentationModPRelationMatrix P)
        (presentationModPFoxBoundary P) ∧
      (∀ (n : ℕ)
          (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)),
        presentationModPFoxBoundary P v ∈
            closedAugmentationPower p G (n + 1) →
          ∃ a : Fin r → ModPCompletedGroupAlgebra p G,
            v - presentationModPRelationMatrix P a ∈
              presentationModPFoxCoordinateFiltration
                (p := p) (d := d) (G := G) n) ∧
      LinearMap.range (presentationModPFoxBoundary P) =
        (modPAugmentationIdeal p G :
          Submodule (ModPCompletedGroupAlgebra p G)
            (ModPCompletedGroupAlgebra p G))

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