ClassFieldTower.Cohomology.exists_openNormalSubgroupInClass_inflation_eq_degree_two
Every lifted degree-two class of a pro-p group is inflated from one finite p-group quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.Cohomology
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open H2FiniteStageAux
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]Lean source · statement
theorem exists_openNormalSubgroupInClass_inflation_eq_degree_two
(hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
(x : continuousCohomologyZModPLifted p G 2) :
∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
∃ xU : continuousCohomologyZModPLifted p
(G ⧸ (U.1 : Subgroup G)) 2,
continuousCohomologyZModPMapLifted p
(OpenNormalSubgroupInClass.quotientProj U) 2 xU = x