ClassFieldTower.Cohomology.exists_finiteStage_continuousH1Cup
Two continuous mod-p characters, and their canonical degree-two cup, descend to one common finite p-group quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G]Lean source · statement
theorem exists_finiteStage_continuousH1Cup
(hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
(χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
∃ χU ψU : ContinuousH1ZMod
(p := p) (G := G ⧸ (U.1 : Subgroup G)),
continuousH1ZModRestriction
(OpenNormalSubgroupInClass.quotientProj U) χU = χ ∧
continuousH1ZModRestriction
(OpenNormalSubgroupInClass.quotientProj U) ψU = ψ ∧
(continuousCohomologyZModPMapLifted p
(OpenNormalSubgroupInClass.quotientProj U) 2).hom
(continuousH1CupProductLifted χU ψU) =
continuousH1CupProductLifted χ ψ