NYLL
Module

ModPTailExactness.lean

Nyll.ProCGroups.ProP.Fox.ModPTailExactness
5 declarations indexed from sourceView source ↗

Module documentation

Tail exactness of the mod-p Fox boundary

The completed mod-p Fox boundary has closed range. Density of the algebraic group algebra, together with the presentation fundamental formula, identifies that range with the canonical augmentation ideal.

Imports2
Imported by2

Declarations

theorem

isClosed_range_presentationModPFoxBoundary

L39 ↗
ClassFieldTower.ProP.isClosed_range_presentationModPFoxBoundary
Documentation

The range of the completed mod-p Fox boundary is closed.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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_range_presentationModPFoxBoundary
    (P : FiniteProPPresentation p d r sourceData G) :
    IsClosed (Set.range (presentationModPFoxBoundary P))
theorem

presentationModPFoxBoundary_mem_augmentationIdeal

L52 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_mem_augmentationIdeal
Documentation

The completed Fox boundary lands in the canonical augmentation ideal.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationModPFoxBoundary_mem_augmentationIdeal
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) :
    presentationModPFoxBoundary P v ∈ modPAugmentationIdeal p G
theorem

groupLikeDifference_mem_presentationModPFoxBoundary_range

L62 ↗
ClassFieldTower.ProP.groupLikeDifference_mem_presentationModPFoxBoundary_range
Documentation

Every standard completed augmentation generator is in the boundary range.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 groupLikeDifference_mem_presentationModPFoxBoundary_range
    (P : FiniteProPPresentation p d r sourceData G) (g : G) :
    groupLikeDifference p G g ∈ LinearMap.range (presentationModPFoxBoundary P)
theorem

toCompletedGroupAlgebraInClass_mem_presentationModPFoxBoundary_range

L70 ↗
ClassFieldTower.ProP.toCompletedGroupAlgebraInClass_mem_presentationModPFoxBoundary_range
Documentation

The dense algebraic augmentation ideal maps into the completed boundary range.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 toCompletedGroupAlgebraInClass_mem_presentationModPFoxBoundary_range
    (P : FiniteProPPresentation p d r sourceData G)
    (a : MonoidAlgebra (ZMod p) G)
    (ha : a ∈ groupAlgebraAugmentationIdeal (ZMod p) G) :
    toCompletedGroupAlgebraInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G a ∈
      LinearMap.range (presentationModPFoxBoundary P)
theorem

presentationModPFoxBoundary_range_eq_augmentationIdeal

L111 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_range_eq_augmentationIdeal
Documentation

The completed mod-p Fox boundary has range equal to the canonical augmentation ideal.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationModPFoxBoundary_range_eq_augmentationIdeal
    (P : FiniteProPPresentation p d r sourceData G) :
    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.