NYLL
Module

FiniteDimensions.lean

Nyll.ProCGroups.GolodShafarevich.FiniteDimensions
10 declarations indexed from sourceView source ↗

Module documentation

Finite augmentation-dimension sequences

For a finite target group, the dimensions of the augmentation truncations form a bounded monotone sequence and hence eventually stabilize. The degree-zero truncation is the one-dimensional augmentation quotient.

Imports2
Imported by3

Declarations

def

modPCanonicalAugmentationAlgHom

L34 ↗
ClassFieldTower.ProP.modPCanonicalAugmentationAlgHom
Documentation

The canonical mod-p augmentation as an algebra homomorphism over its coefficient field.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · full declaration
def modPCanonicalAugmentationAlgHom :
    ModPCompletedGroupAlgebra p G →ₐ[ZMod p] ZMod p where
  toRingHom := completedGroupAlgebraCanonicalAugmentationInClass
    (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
  commutes' :=
    completedGroupAlgebraCanonicalAugmentationInClass_algebraMap
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
def

modPCanonicalAugmentationLinearMap

L45 ↗
ClassFieldTower.ProP.modPCanonicalAugmentationLinearMap
Documentation

The canonical mod-p augmentation, regarded as a linear map over its coefficient field.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
def modPCanonicalAugmentationLinearMap :
    ModPCompletedGroupAlgebra p G →ₗ[ZMod p] ZMod p
theorem

modPCanonicalAugmentationLinearMap_apply

L50 ↗
ClassFieldTower.ProP.modPCanonicalAugmentationLinearMap_apply
Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem modPCanonicalAugmentationLinearMap_apply
    (x : ModPCompletedGroupAlgebra p G) :
    modPCanonicalAugmentationLinearMap (p := p) (G := G) x =
      completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p) x
theorem

isClosed_modPAugmentationIdeal

L59 ↗
ClassFieldTower.ProP.isClosed_modPAugmentationIdeal
Documentation

The canonical mod-p augmentation ideal is closed.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem isClosed_modPAugmentationIdeal :
    IsClosed
      ((modPAugmentationIdeal p G :
        Ideal (ModPCompletedGroupAlgebra p G)) :
          Set (ModPCompletedGroupAlgebra p G))
theorem

closedAugmentationPower_one_eq_modPAugmentationIdeal

L73 ↗
ClassFieldTower.ProP.closedAugmentationPower_one_eq_modPAugmentationIdeal
Documentation

The first closed augmentation power is the augmentation ideal itself.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem closedAugmentationPower_one_eq_modPAugmentationIdeal :
    closedAugmentationPower p G 1 = modPAugmentationIdeal p G
theorem

truncatedAugmentationDimension_zero

L88 ↗
ClassFieldTower.ProP.truncatedAugmentationDimension_zero
Documentation

The degree-zero truncation is the augmentation quotient and has dimension one over ZMod p.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem truncatedAugmentationDimension_zero :
    truncatedAugmentationDimension (p := p) (G := G) 0 = 1
theorem

truncatedAugmentationDimension_monotone

L121 ↗
ClassFieldTower.ProP.truncatedAugmentationDimension_monotone
Documentation

For a finite group, augmentation-truncation dimensions increase with the cutoff.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem truncatedAugmentationDimension_monotone [Finite G] :
    Monotone (truncatedAugmentationDimension (p := p) (G := G))
theorem

truncatedAugmentationDimension_le

L146 ↗
ClassFieldTower.ProP.truncatedAugmentationDimension_le
Documentation

For a finite group, every truncation dimension is bounded by the dimension of the completed group algebra.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem truncatedAugmentationDimension_le [Finite G] (N : ℕ) :
    truncatedAugmentationDimension (p := p) (G := G) N ≤
      Module.finrank (ZMod p) (ModPCompletedGroupAlgebra p G)
theorem

truncatedAugmentationDimension_bounded

L161 ↗
ClassFieldTower.ProP.truncatedAugmentationDimension_bounded
Documentation

The finite-group truncation dimensions admit a uniform natural-number bound.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem truncatedAugmentationDimension_bounded [Finite G] :
    ∃ C, ∀ N, truncatedAugmentationDimension (p := p) (G := G) N ≤ C
theorem

truncatedAugmentationDimension_eventuallyConstant

L169 ↗
ClassFieldTower.ProP.truncatedAugmentationDimension_eventuallyConstant
Documentation

A finite group's bounded monotone truncation-dimension sequence is eventually constant.

Source context 9 commands

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

namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem truncatedAugmentationDimension_eventuallyConstant [Finite G] :
    ∃ M, ∀ N, M ≤ N →
      truncatedAugmentationDimension (p := p) (G := G) N =
        truncatedAugmentationDimension (p := p) (G := G) M

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