Nyll.GaloisCohomology.ProP.H2InflationRangeBound

Module documentation

Bounding degree two from finite-stage inflation ranges

If every finite-stage inflation range embeds in one fixed finite-dimensional target, then finite families of ambient classes descending to a common stage force the whole ambient degree-two cohomology to have the same dimension bound. The stage embeddings need not be compatible.

theorem

finiteDimensional_and_finrank_degree_two_le_of_inflationRange_embeddings

L35 ↗

ClassFieldTower.Cohomology.finiteDimensional_and_finrank_degree_two_le_of_inflationRange_embeddings

Documentation

A uniform finite-dimensional target for the finite-stage inflation ranges bounds the ambient lifted degree-two cohomology. No compatibility between the stagewise embeddings is required.

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 v
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {W : Type v} [AddCommGroup W] [Module (ZMod p) W]

Lean source · statement

theorem finiteDimensional_and_finrank_degree_two_le_of_inflationRange_embeddings
    [FiniteDimensional (ZMod p) W]
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
    (hEmbed : ∀ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
      ∃ f : degreeTwoInflationRange (p := p) U →ₗ[ZMod p] W,
        Function.Injective f) :
    FiniteDimensional (ZMod p) (continuousCohomologyZModPLifted p G 2) ∧
      Module.finrank (ZMod p) (continuousCohomologyZModPLifted p G 2) ≤
        Module.finrank (ZMod p) W

Module documentation

Bounding degree two from finite-stage inflation ranges

Declarations

finiteDimensional_and_finrank_degree_two_le_of_inflationRange_embeddings