NYLL
Module

ModPDensityExactness.lean

Nyll.ProCGroups.ProP.Fox.ModPDensityExactness
7 declarations indexed from sourceView source ↗

Module documentation

Completed mod-p Fox density and relation exactness

Finite reflected Fox exactness supplies a matching presentation word at every finite p-group quotient. The corresponding matching subsets of the compact free pro-p source are nonempty, closed, and directed under refinement. Compactness therefore produces one source element matching all completed coefficient coordinates and all target quotients. Separation identifies it as an actual presentation-kernel element whose mod-p Fox derivative is the given boundary cycle.

Combining this density result with the displayed-row span theorem proves unfiltered exactness of the completed relation matrix followed by the Fox boundary.

Imports2
Imported by2

Declarations

theorem

presentationModPFiniteStageRightMap_presentationWord

L49 ↗
ClassFieldTower.ProP.presentationModPFiniteStageRightMap_presentationWord
Documentation

The reflected right projection sends a presentation word to its finite quotient class.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageRightMap_presentationWord
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (w : FreeGroup (ULift.{u} (Fin d))) :
    presentationModPFiniteStageRightMap P U hU
        (P.quotient (FreeGroup.lift (presentationChosenGenerator P) w)) =
      QuotientGroup.mk' (presentationModPFiniteStageKernel P U hU) w
def

presentationModPFiniteStageMatchSet

L67 ↗
ClassFieldTower.ProP.presentationModPFiniteStageMatchSet
Documentation

Raw finite-stage equality conditions on a possible lift of a completed boundary cycle.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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
def presentationModPFiniteStageMatchSet
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    (j : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p)) :
    Set sourceData.carrier
theorem

presentationModPFiniteStageMatchSet_nonempty

L85 ↗
ClassFieldTower.ProP.presentationModPFiniteStageMatchSet_nonempty
Documentation

Finite-stage exactness produces a presentation word matching a completed boundary cycle at every raw coefficient and target quotient coordinate.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageMatchSet_nonempty
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    (hv : presentationModPFoxBoundary P v = 0)
    (j : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p)) :
    (presentationModPFiniteStageMatchSet P v j).Nonempty
theorem

isClosed_presentationModPFiniteStageMatchSet

L141 ↗
ClassFieldTower.ProP.isClosed_presentationModPFiniteStageMatchSet
Documentation

Each raw finite-stage matching condition is closed in the compact free pro-p source.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 isClosed_presentationModPFiniteStageMatchSet
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    (j : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p)) :
    IsClosed (presentationModPFiniteStageMatchSet P v j)
theorem

presentationModPFiniteStageMatchSet_anti

L201 ↗
ClassFieldTower.ProP.presentationModPFiniteStageMatchSet_anti
Documentation

Matching at a finer raw quotient stage implies matching at every coarser stage.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageMatchSet_anti
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    {j k : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p)} (hjk : j ≤ k) :
    presentationModPFiniteStageMatchSet P v k ⊆
      presentationModPFiniteStageMatchSet P v j
theorem

exists_presentationKernel_of_presentationModPFoxBoundary_eq_zero

L248 ↗
ClassFieldTower.ProP.exists_presentationKernel_of_presentationModPFoxBoundary_eq_zero
Documentation

Every completed mod-p boundary cycle is the Fox derivative of an actual presentation-kernel element.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 exists_presentationKernel_of_presentationModPFoxBoundary_eq_zero
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    (hv : presentationModPFoxBoundary P v = 0) :
    ∃ f : sourceData.carrier,
      P.quotient f = 1 ∧ presentationModPFoxDerivative P f = v
theorem

presentationModPRelationMatrix_boundary_exact

L294 ↗
ClassFieldTower.ProP.presentationModPRelationMatrix_boundary_exact
Documentation

Unfiltered exactness of the completed relation matrix followed by the mod-p Fox boundary.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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_boundary_exact
    (P : FiniteProPPresentation p d r sourceData G) :
    Function.Exact (presentationModPRelationMatrix P)
      (presentationModPFoxBoundary P)

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