ModuleH2InflationRangeCardinality.lean
Nyll.GaloisCohomology.ProP.H2InflationRangeCardinality
2 declarations indexed from sourceView source ↗ Module documentation
Cardinality bounds on finite-stage degree-two inflation
A uniform bound p^d on finite-stage inflation images gives finite continuous H² of dimension at most d. Finiteness of the finite-stage cohomology and its image is constructed, rather than assumed.
Declarations
ClassFieldTower.Cohomology.h2InflationRangeCanonicalZModAddCommGroup
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
ClassFieldTower.Cohomology.finiteDimensional_and_finrank_degree_two_le_of_inflationRange_natCard
DocumentationA uniform cardinality bound for finite-stage images bounds the full continuous degree-two cohomology dimension.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance h2InflationRangeCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
(ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]