ModuleGradedPieces.lean
Nyll.ProCGroups.GolodShafarevich.GradedPieces
8 declarations indexed from sourceView source ↗ Module documentation
Truncated augmentation dimensions
This file packages the finite-dimensional quotients of a mod-p completed group algebra used by the truncated Golod--Shafarevich inequality. The shifted definition uses truncated subtraction, so shifts beyond the cutoff give the zero quotient without side conditions in downstream statements.
Declarations
ClassFieldTower.ProP.finite_modPCompletedGroupAlgebra
DocumentationFor a finite profinite group, its mod-p completed group algebra is a finite type. This is kept as a theorem so no noncanonical global instance is installed.
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
ClassFieldTower.ProP.shiftedClosedAugmentationSubmodule
DocumentationThe subspace killed at cutoff N after a filtration shift shift.
Source context 8 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]
ClassFieldTower.ProP.ShiftedAugmentationTruncation
DocumentationThe completed group algebra truncated at N, with filtration shift shift.
Source context 8 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]
ClassFieldTower.ProP.truncatedAugmentationDimension
DocumentationDimension of the unshifted truncation Λ / I^(N+1).
Source context 8 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]
ClassFieldTower.ProP.shiftedTruncatedAugmentationDimension
DocumentationDimension of the truncation after an arbitrary filtration shift.
Source context 8 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]
ClassFieldTower.ProP.truncatedAugmentationDimensionStar
DocumentationNat-safe shifted dimension: A (N-shift) inside the cutoff and zero outside it.
Source context 8 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]
ClassFieldTower.ProP.closedAugmentationPower_zero_eq_top
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
ClassFieldTower.ProP.shiftedTruncatedAugmentationDimension_eq_star
DocumentationThe quotient definition of a shifted dimension agrees with its Nat-safe piecewise form.
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