ClassFieldTower.Cohomology.exists_finite_nonsplit_extension_of_degree_two_ne_zero
Every nonzero ambient degree-two class is witnessed by a nonsplit finite central p-extension of a finite quotient.
Source context 8 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]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]Lean source · statement
theorem exists_finite_nonsplit_extension_of_degree_two_ne_zero
(hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
{x : continuousCohomologyZModPLifted p G 2}
(hx : x ≠ 0) :
∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
∃ xU : continuousCohomologyZModPLifted p
(G ⧸ (U.1 : Subgroup G)) 2,
continuousCohomologyZModPMapLifted p
(OpenNormalSubgroupInClass.quotientProj U) 2 xU = x ∧
¬ ∃ s : (G ⧸ (U.1 : Subgroup G)) →ₜ*
ProP.DegreeTwoCentralExtension xU,
(ProP.H2CocycleExtension.projection
(ProP.degreeTwoCocycleRepresentative xU)).comp s =
ContinuousMonoidHom.id (G ⧸ (U.1 : Subgroup G))