NYLL
Module

TruncatedFoxMaps.lean

Nyll.ProCGroups.GolodShafarevich.TruncatedFoxMaps
25 declarations indexed from sourceView source ↗

Module documentation

Truncated mod-p Fox maps

This file descends the completed relation matrix, Fox boundary, and canonical augmentation to the shifted closed-augmentation quotients used in the truncated Golod--Shafarevich sequence.

Imports4
Imported by2

Declarations

abbrev

PresentationModPTruncatedRelationSource

L38 ↗
ClassFieldTower.ProP.PresentationModPTruncatedRelationSource
Documentation

The relation source after passing coordinatewise to shifted truncations.

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
abbrev PresentationModPTruncatedRelationSource (ν : Fin r → ℕ) (N : ℕ)
abbrev

PresentationModPTruncatedFoxCoordinates

L43 ↗
ClassFieldTower.ProP.PresentationModPTruncatedFoxCoordinates
Documentation

The Fox-coordinate module after truncation, with the boundary shift.

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
abbrev PresentationModPTruncatedFoxCoordinates (N : ℕ)
def

presentationModPFoxCoordinateFinEquiv

L47 ↗
ClassFieldTower.ProP.presentationModPFoxCoordinateFinEquiv
Documentation

Reindex the universe-lifted presentation coordinates by Fin d.

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 · full declaration
def presentationModPFoxCoordinateFinEquiv :
    (Fin d → ModPCompletedGroupAlgebra p G) ≃ₗ[ModPCompletedGroupAlgebra p G]
      PresentationModPFoxCoordinates (p := p) (d := d) (G := G) where
  toFun v i := v i.down
  invFun v i := v (ULift.up i)
  left_inv v := rfl
  right_inv v := by
    funext i
    cases i
    rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
abbrev

relationTruncationFamily

L60 ↗
ClassFieldTower.ProP.relationTruncationFamily
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
abbrev relationTruncationFamily (ν : Fin r → ℕ) (N : ℕ)
    (j : Fin r) : Submodule (ZMod p) (ModPCompletedGroupAlgebra p G)
abbrev

foxTruncationFamily

L64 ↗
ClassFieldTower.ProP.foxTruncationFamily
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
abbrev foxTruncationFamily (N : ℕ) (_i : Fin d) :
    Submodule (ZMod p) (ModPCompletedGroupAlgebra p G)
abbrev

relationPiFiltration

L68 ↗
ClassFieldTower.ProP.relationPiFiltration
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
abbrev relationPiFiltration (ν : Fin r → ℕ) (N : ℕ) :
    Submodule (ZMod p) (Fin r → ModPCompletedGroupAlgebra p G)
abbrev

foxPiFiltration

L72 ↗
ClassFieldTower.ProP.foxPiFiltration
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
abbrev foxPiFiltration (N : ℕ) :
    Submodule (ZMod p) (Fin d → ModPCompletedGroupAlgebra p G)
def

presentationModPRelationMatrixFin

L76 ↗
ClassFieldTower.ProP.presentationModPRelationMatrixFin
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
def presentationModPRelationMatrixFin
    (P : FiniteProPPresentation p d r sourceData G) :
    (Fin r → ModPCompletedGroupAlgebra p G) →ₗ[ZMod p]
      (Fin d → ModPCompletedGroupAlgebra p G)
def

presentationModPFoxBoundaryFin

L83 ↗
ClassFieldTower.ProP.presentationModPFoxBoundaryFin
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
def presentationModPFoxBoundaryFin
    (P : FiniteProPPresentation p d r sourceData G) :
    (Fin d → ModPCompletedGroupAlgebra p G) →ₗ[ZMod p]
      ModPCompletedGroupAlgebra p G
theorem

relationMatrixFin_mem_foxPiFiltration

L91 ↗
ClassFieldTower.ProP.relationMatrixFin_mem_foxPiFiltration
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 relationMatrixFin_mem_foxPiFiltration
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) :
    relationPiFiltration (p := p) (G := G) ν N ≤
      (foxPiFiltration (p := p) (G := G) (d := d) N).comap
        (presentationModPRelationMatrixFin P)
theorem

foxBoundaryFin_mem_truncation

L112 ↗
ClassFieldTower.ProP.foxBoundaryFin_mem_truncation
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 foxBoundaryFin_mem_truncation
    (P : FiniteProPPresentation p d r sourceData G)
    (N : ℕ) :
    foxPiFiltration (p := p) (G := G) (d := d) N ≤
      (shiftedClosedAugmentationSubmodule (p := p) (G := G) N 0).comap
        (presentationModPFoxBoundaryFin P)
def

presentationModPTruncatedRelationMap

L137 ↗
ClassFieldTower.ProP.presentationModPTruncatedRelationMap
Documentation

The relation matrix induced on the shifted truncation quotients.

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
def presentationModPTruncatedRelationMap
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) :
    PresentationModPTruncatedRelationSource (p := p) (G := G) ν N →ₗ[ZMod p]
      PresentationModPTruncatedFoxCoordinates (p := p) (d := d) (G := G) N
def

presentationModPTruncatedFoxBoundary

L154 ↗
ClassFieldTower.ProP.presentationModPTruncatedFoxBoundary
Documentation

The Fox boundary induced on the shifted truncation quotients.

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
def presentationModPTruncatedFoxBoundary
    (P : FiniteProPPresentation p d r sourceData G) (N : ℕ) :
    PresentationModPTruncatedFoxCoordinates (p := p) (d := d) (G := G) N →ₗ[ZMod p]
      ShiftedAugmentationTruncation (p := p) (G := G) N 0
theorem

presentationModPTruncatedRelationMap_mk

L165 ↗
ClassFieldTower.ProP.presentationModPTruncatedRelationMap_mk
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 · full declaration
theorem presentationModPTruncatedRelationMap_mk
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) (a : Fin r → ModPCompletedGroupAlgebra p G) :
    presentationModPTruncatedRelationMap P ν hν N
        (fun j ↦ Submodule.Quotient.mk (a j)) =
      fun i ↦ Submodule.Quotient.mk
        ((presentationModPRelationMatrix P a) (ULift.up i)) := by
  let ps := relationTruncationFamily (p := p) (G := G) ν N
  have hs :
      (Submodule.quotientPi ps).symm.toLinearMap
          (fun j ↦ Submodule.Quotient.mk (a j)) =
        Submodule.Quotient.mk a := by
    change (Submodule.quotientPi ps).symm
        (fun j ↦ Submodule.Quotient.mk (a j)) = _
    rw [show (fun j ↦ Submodule.Quotient.mk (a j)) =
        (Submodule.quotientPi ps) (Submodule.Quotient.mk a) by rfl]
    exact (Submodule.quotientPi ps).symm_apply_apply _
  rw [presentationModPTruncatedRelationMap]
  simp only [LinearMap.comp_apply]
  rw [hs]
  rfl
theorem

presentationModPTruncatedFoxBoundary_mk

L189 ↗
ClassFieldTower.ProP.presentationModPTruncatedFoxBoundary_mk
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 · full declaration
theorem presentationModPTruncatedFoxBoundary_mk
    (P : FiniteProPPresentation p d r sourceData G)
    (N : ℕ) (v : Fin d → ModPCompletedGroupAlgebra p G) :
    presentationModPTruncatedFoxBoundary P N
        (fun i ↦ Submodule.Quotient.mk (v i)) =
      Submodule.Quotient.mk
        (presentationModPFoxBoundary P
          ((presentationModPFoxCoordinateFinEquiv
            (p := p) (d := d) (G := G)) v)) := by
  let pt := foxTruncationFamily (p := p) (G := G) (d := d) N
  have ht :
      (Submodule.quotientPi pt).symm.toLinearMap
          (fun i ↦ Submodule.Quotient.mk (v i)) =
        Submodule.Quotient.mk v := by
    change (Submodule.quotientPi pt).symm
        (fun i ↦ Submodule.Quotient.mk (v i)) = _
    rw [show (fun i ↦ Submodule.Quotient.mk (v i)) =
        (Submodule.quotientPi pt) (Submodule.Quotient.mk v) by rfl]
    exact (Submodule.quotientPi pt).symm_apply_apply _
  rw [presentationModPTruncatedFoxBoundary]
  simp only [LinearMap.comp_apply]
  rw [ht]
  rfl
instance

(anonymous instance)

L215 ↗
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
instance : AddCommGroup (ZMod p)
instance

(anonymous instance)

L218 ↗
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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance : Module (ZMod p) (ZMod p)
def

presentationModPAugmentationLinearMap

L220 ↗
ClassFieldTower.ProP.presentationModPAugmentationLinearMap
Source context 12 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · full declaration
def presentationModPAugmentationLinearMap :
    ModPCompletedGroupAlgebra p G →ₗ[ZMod p] ZMod p where
  toFun := completedGroupAlgebraCanonicalAugmentationInClass
    (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
  map_add' x y := by simp
  map_smul' c x := by
    change completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p) (c • x) =
      c • completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p) x
    simp [Algebra.smul_def]
theorem

shiftedTruncation_le_augmentation_ker

L233 ↗
ClassFieldTower.ProP.shiftedTruncation_le_augmentation_ker
Source context 13 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem shiftedTruncation_le_augmentation_ker (N : ℕ) :
    shiftedClosedAugmentationSubmodule (p := p) (G := G) N 0 ≤
      (presentationModPAugmentationLinearMap (p := p) (G := G)).ker
def

presentationModPTruncatedAugmentation

L264 ↗
ClassFieldTower.ProP.presentationModPTruncatedAugmentation
Documentation

The canonical augmentation induced on the unshifted truncation.

Source context 12 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
def presentationModPTruncatedAugmentation (N : ℕ) :
    ShiftedAugmentationTruncation (p := p) (G := G) N 0 →ₗ[ZMod p] ZMod p
theorem

presentationModPTruncatedAugmentation_mk

L271 ↗
ClassFieldTower.ProP.presentationModPTruncatedAugmentation_mk
Source context 13 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem presentationModPTruncatedAugmentation_mk
    (N : ℕ) (x : ModPCompletedGroupAlgebra p G) :
    presentationModPTruncatedAugmentation (p := p) (G := G) N
        (Submodule.Quotient.mk x) =
      completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p) x
theorem

presentationModPTruncatedRelationSource_mk_surjective

L280 ↗
ClassFieldTower.ProP.presentationModPTruncatedRelationSource_mk_surjective
Source context 13 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · full declaration
theorem presentationModPTruncatedRelationSource_mk_surjective
    (ν : Fin r → ℕ) (N : ℕ) :
    Function.Surjective
      (fun a : Fin r → ModPCompletedGroupAlgebra p G ↦
        (fun j ↦ Submodule.Quotient.mk (a j) :
          PresentationModPTruncatedRelationSource (p := p) (G := G) ν N)) := by
  classical
  intro x
  choose a ha using fun j ↦
    (shiftedClosedAugmentationSubmodule
      (p := p) (G := G) N (ν j)).mkQ_surjective (x j)
  refine ⟨a, ?_⟩
  funext j
  exact ha j
theorem

presentationModPTruncatedFoxCoordinates_mk_surjective

L296 ↗
ClassFieldTower.ProP.presentationModPTruncatedFoxCoordinates_mk_surjective
Source context 13 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · full declaration
theorem presentationModPTruncatedFoxCoordinates_mk_surjective (N : ℕ) :
    Function.Surjective
      (fun v : Fin d → ModPCompletedGroupAlgebra p G ↦
        (fun i ↦ Submodule.Quotient.mk (v i) :
          PresentationModPTruncatedFoxCoordinates
            (p := p) (d := d) (G := G) N)) := by
  classical
  intro x
  choose v hv using fun i ↦
    (shiftedClosedAugmentationSubmodule
      (p := p) (G := G) N 1).mkQ_surjective (x i)
  refine ⟨v, ?_⟩
  funext i
  exact hv i
theorem

presentationModPTruncatedFoxBoundary_comp_relationMap

L312 ↗
ClassFieldTower.ProP.presentationModPTruncatedFoxBoundary_comp_relationMap
Documentation

The induced relation map is killed by the induced Fox boundary.

Source context 12 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
theorem presentationModPTruncatedFoxBoundary_comp_relationMap
    (P : FiniteProPPresentation p d r sourceData G)
    (ν : Fin r → ℕ)
    (hν : ∀ j, P.RelatorZassenhausDepthAtLeast (ν j) j)
    (N : ℕ) :
    (presentationModPTruncatedFoxBoundary P N).comp
        (presentationModPTruncatedRelationMap P ν hν N) = 0
theorem

presentationModPTruncatedAugmentation_comp_foxBoundary

L341 ↗
ClassFieldTower.ProP.presentationModPTruncatedAugmentation_comp_foxBoundary
Documentation

The induced augmentation kills the induced Fox boundary.

Source context 12 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]
local instance : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
theorem presentationModPTruncatedAugmentation_comp_foxBoundary
    (P : FiniteProPPresentation p d r sourceData G) (N : ℕ) :
    (presentationModPTruncatedAugmentation (p := p) (G := G) N).comp
        (presentationModPTruncatedFoxBoundary P N) = 0

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