NYLL
Module

ModPFilteredExactness.lean

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

Module documentation

Filtered packaging for the mod-p Fox complex

The coordinate module is filtered coordinatewise by closed augmentation powers. A displayed relator of Zassenhaus depth at least ν j gives a row of depth at least ν j - 1; this makes the relation matrix filtered when its source is given the corresponding shifted filtration. The Fox boundary raises coordinate depth by one.

The final theorem packages these filtration bounds with the underlying unfiltered exactness and the identification of the boundary range. It does not assert strictness of either filtered map.

Imports3
Imported by2

Declarations

def

presentationModPFoxCoordinateFiltration

L44 ↗
ClassFieldTower.ProP.presentationModPFoxCoordinateFiltration
Documentation

The coordinatewise closed-augmentation filtration on mod-p Fox vectors.

Source context 10 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]
Lean source · full declaration
def presentationModPFoxCoordinateFiltration (n : ℕ) :
    Submodule (ModPCompletedGroupAlgebra p G)
      (PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) where
  carrier := {v | ∀ i, v i ∈ closedAugmentationPower p G n}
  zero_mem' i := (closedAugmentationPower p G n).zero_mem
  add_mem' {v w} hv hw i :=
    (closedAugmentationPower p G n).add_mem (hv i) (hw i)
  smul_mem' a v hv i := by
    change a * v i ∈ closedAugmentationPower p G n
    exact (closedAugmentationPower p G n).mul_mem_left a (hv i)
theorem

mem_presentationModPFoxCoordinateFiltration_iff

L57 ↗
ClassFieldTower.ProP.mem_presentationModPFoxCoordinateFiltration_iff
Documentation

Membership in the coordinate filtration is coordinatewise membership.

Source context 10 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]
Lean source · statement
theorem mem_presentationModPFoxCoordinateFiltration_iff
    (n : ℕ)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) :
    v ∈ presentationModPFoxCoordinateFiltration (p := p) (d := d) (G := G) n ↔
      ∀ i, v i ∈ closedAugmentationPower p G n
def

presentationModPWeightedRelationSourceFiltration

L66 ↗
ClassFieldTower.ProP.presentationModPWeightedRelationSourceFiltration
Documentation

The source filtration shifted by the prescribed Zassenhaus depth ν of each displayed relator.

Source context 10 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]
Lean source · full declaration
def presentationModPWeightedRelationSourceFiltration
    (ν : Fin r → ℕ) (N : ℕ) :
    Submodule (ModPCompletedGroupAlgebra p G)
      (Fin r → ModPCompletedGroupAlgebra p G) where
  carrier := {a | ∀ j, a j ∈ closedAugmentationPower p G (N + 1 - ν j)}
  zero_mem' j := (closedAugmentationPower p G (N + 1 - ν j)).zero_mem
  add_mem' {a b} ha hb j :=
    (closedAugmentationPower p G (N + 1 - ν j)).add_mem (ha j) (hb j)
  smul_mem' c a ha j := by
    change c * a j ∈ closedAugmentationPower p G (N + 1 - ν j)
    exact (closedAugmentationPower p G (N + 1 - ν j)).mul_mem_left c (ha j)
theorem

mem_presentationModPWeightedRelationSourceFiltration_iff

L81 ↗
ClassFieldTower.ProP.mem_presentationModPWeightedRelationSourceFiltration_iff
Documentation

Membership in the weighted source filtration is the stated shifted coordinatewise condition.

Source context 10 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]
Lean source · statement
theorem mem_presentationModPWeightedRelationSourceFiltration_iff
    (ν : Fin r → ℕ) (N : ℕ)
    (a : Fin r → ModPCompletedGroupAlgebra p G) :
    a ∈ presentationModPWeightedRelationSourceFiltration
        (p := p) (G := G) ν N ↔
      ∀ j, a j ∈ closedAugmentationPower p G (N + 1 - ν j)
theorem

presentationModPFoxBoundary_mem_closedAugmentationPower_succ

L93 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_mem_closedAugmentationPower_succ
Documentation

The mod-p Fox boundary sends coordinate depth n to augmentation depth n + 1.

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_mem_closedAugmentationPower_succ
    (P : FiniteProPPresentation p d r sourceData G) (n : ℕ)
    {v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)}
    (hv : v ∈ presentationModPFoxCoordinateFiltration
      (p := p) (d := d) (G := G) n) :
    presentationModPFoxBoundary P v ∈ closedAugmentationPower p G (n + 1)
theorem

presentationModPRelationMatrix_mem_coordinateFiltration

L110 ↗
ClassFieldTower.ProP.presentationModPRelationMatrix_mem_coordinateFiltration
Documentation

With the source shifted by the displayed-relator depths, the relation matrix preserves every target filtration depth.

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_mem_coordinateFiltration
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) {a : Fin r → ModPCompletedGroupAlgebra p G}
    (ha : a ∈ presentationModPWeightedRelationSourceFiltration
      (p := p) (G := G) ν N) :
    presentationModPRelationMatrix P a ∈
      presentationModPFoxCoordinateFiltration
        (p := p) (d := d) (G := G) N
theorem

presentationModP_filteredRelationBoundary_package

L147 ↗
ClassFieldTower.ProP.presentationModP_filteredRelationBoundary_package
Documentation

The filtered bounds together with the underlying exactness and the augmentation-ideal description of the boundary range. This package makes no strict filtered-lifting claim.

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_filteredRelationBoundary_package
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j) :
    Function.Exact (presentationModPRelationMatrix P)
        (presentationModPFoxBoundary P) ∧
      LinearMap.range (presentationModPFoxBoundary P) =
        (modPAugmentationIdeal p G :
          Submodule (ModPCompletedGroupAlgebra p G)
            (ModPCompletedGroupAlgebra p G)) ∧
      (∀ (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)) ∧
      ∀ (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

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