ModuleH2CentralExtensionClass.lean
Nyll.GaloisCohomology.ProP.H2CentralExtensionClass
5 declarations indexed from sourceView source ↗ Module documentation
Degree-two classes as nonsplit central extensions
This file chooses a homogeneous cocycle representative of a lifted continuous degree-two class and attaches its explicit central extension. A continuous group-theoretic section of the extension forces the represented cohomology class to vanish.
Declarations
ClassFieldTower.ProP.degreeTwoCocycleRepresentative
DocumentationA linear choice of cocycle representative of a lifted degree-two class.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
ClassFieldTower.ProP.degreeTwoCocycleRepresentative_π
DocumentationThe chosen cocycle represents the prescribed degree-two class.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
ClassFieldTower.ProP.DegreeTwoCentralExtension
DocumentationThe explicit central extension attached to a lifted degree-two class.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
ClassFieldTower.ProP.eq_zero_of_degreeTwoCentralExtension_section
DocumentationA continuous splitting of the cocycle extension makes its degree-two class zero.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
ClassFieldTower.ProP.degreeTwoCentralExtension_no_section_of_ne_zero
DocumentationA nonzero degree-two class gives a nonsplit continuous central extension.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]