NYLL
Module

H2CocycleExtension.lean

Nyll.GaloisCohomology.ProP.H2CocycleExtension
22 declarations indexed from sourceView source ↗

Module documentation

The central extension attached to a degree-two cocycle

A normalized continuous ZMod p-valued two-cocycle on a topological group Q defines a twisted central extension of Q. This file packages that construction, including its product topology, quotient projection, coefficient kernel, and the finite p-group property needed for finite central embedding problems.

Imports1
Imported by7

Declarations

structure

H2CocycleExtension

L36 ↗
ClassFieldTower.ProP.H2CocycleExtension
Documentation

The twisted extension attached to a homogeneous degree-two cocycle.

Its underlying space is the product of the lifted additive coefficient group and Q; its multiplication is twisted by the associated normalized cocycle.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
Lean source · full declaration
structure H2CocycleExtension
    (z : Cohomology.trivialZModPCocyclesLifted p Q 2) where
  /-- The lifted `ZMod p` coefficient coordinate. -/
  left : A p
  /-- The base-group coordinate. -/
  right : Q
theorem

ext

L48 ↗
ClassFieldTower.ProP.H2CocycleExtension.ext
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
theorem ext {x y : H2CocycleExtension z}
    (hleft : x.left = y.left) (hright : x.right = y.right) : x = y
instance

instGroup

L55 ↗
ClassFieldTower.ProP.H2CocycleExtension.instGroup
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · full declaration
instance instGroup : Group (H2CocycleExtension z) where
  one := ⟨0, 1⟩
  mul x y :=
    ⟨x.left + y.left + normalizedCocycle z x.right y.right, x.right * y.right⟩
  inv x :=
    ⟨-x.left - normalizedCocycle z x.right⁻¹ x.right, x.right⁻¹⟩
  mul_assoc x y w := by
    apply ext
    · change
        (x.left + y.left + normalizedCocycle z x.right y.right) + w.left +
            normalizedCocycle z (x.right * y.right) w.right =
          x.left + (y.left + w.left + normalizedCocycle z y.right w.right) +
            normalizedCocycle z x.right (y.right * w.right)
      have hc := normalizedCocycle_cocycle z x.right y.right w.right
      calc
        _ = x.left + y.left + w.left +
            (normalizedCocycle z x.right y.right +
              normalizedCocycle z (x.right * y.right) w.right) := by abel
        _ = x.left + y.left + w.left +
            (normalizedCocycle z y.right w.right +
              normalizedCocycle z x.right (y.right * w.right)) := by rw [hc]
        _ = _ := by abel
    · exact mul_assoc _ _ _
  one_mul x := by
    apply ext
    · change 0 + x.left + normalizedCocycle z 1 x.right = x.left
      rw [normalizedCocycle_one_left]
      simp
    · exact one_mul _
  mul_one x := by
    apply ext
    · change x.left + 0 + normalizedCocycle z x.right 1 = x.left
      rw [normalizedCocycle_one_right]
      simp
    · exact mul_one _
  inv_mul_cancel x := by
    apply ext
    · change
        (-x.left - normalizedCocycle z x.right⁻¹ x.right) + x.left +
            normalizedCocycle z x.right⁻¹ x.right = 0
      abel
    · exact inv_mul_cancel _
def

toProdEquiv

L99 ↗
ClassFieldTower.ProP.H2CocycleExtension.toProdEquiv
Documentation

The underlying-type equivalence with the coefficient product.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · full declaration
def toProdEquiv : H2CocycleExtension z ≃ A p × Q where
  toFun x := (x.left, x.right)
  invFun x := ⟨x.1, x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
instance

instTopologicalSpace

L105 ↗
ClassFieldTower.ProP.H2CocycleExtension.instTopologicalSpace
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instTopologicalSpace : TopologicalSpace (H2CocycleExtension z)
def

toProdHomeomorph

L109 ↗
ClassFieldTower.ProP.H2CocycleExtension.toProdHomeomorph
Documentation

The product-topology homeomorphism underlying the extension.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
def toProdHomeomorph : H2CocycleExtension z ≃ₜ A p × Q
instance

instCompactSpace

L113 ↗
ClassFieldTower.ProP.H2CocycleExtension.instCompactSpace
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instCompactSpace [Fact p.Prime] [CompactSpace Q] :
    CompactSpace (H2CocycleExtension z)
instance

instT2Space

L117 ↗
ClassFieldTower.ProP.H2CocycleExtension.instT2Space
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instT2Space [T2Space Q] : T2Space (H2CocycleExtension z)
instance

instTotallyDisconnectedSpace

L120 ↗
ClassFieldTower.ProP.H2CocycleExtension.instTotallyDisconnectedSpace
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instTotallyDisconnectedSpace [TotallyDisconnectedSpace Q] :
    TotallyDisconnectedSpace (H2CocycleExtension z)
instance

instContinuousMul

L124 ↗
ClassFieldTower.ProP.H2CocycleExtension.instContinuousMul
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instContinuousMul [LocallyCompactSpace Q] :
    ContinuousMul (H2CocycleExtension z)
instance

instContinuousInv

L142 ↗
ClassFieldTower.ProP.H2CocycleExtension.instContinuousInv
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instContinuousInv [LocallyCompactSpace Q] :
    ContinuousInv (H2CocycleExtension z)
instance

instIsTopologicalGroup

L157 ↗
ClassFieldTower.ProP.H2CocycleExtension.instIsTopologicalGroup
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instIsTopologicalGroup [LocallyCompactSpace Q] :
    IsTopologicalGroup (H2CocycleExtension z)
def

projection

L162 ↗
ClassFieldTower.ProP.H2CocycleExtension.projection
Documentation

The canonical continuous projection from the cocycle extension to Q.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · full declaration
def projection : H2CocycleExtension z →ₜ* Q where
  toFun x := x.right
  map_one' := rfl
  map_mul' _ _ := rfl
  continuous_toFun :=
    continuous_snd.comp
      (show Continuous (toProdEquiv z) from continuous_induced_dom)
theorem

projection_apply

L171 ↗
ClassFieldTower.ProP.H2CocycleExtension.projection_apply
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
theorem projection_apply (x : H2CocycleExtension z) : projection z x = x.right
theorem

projection_surjective

L173 ↗
ClassFieldTower.ProP.H2CocycleExtension.projection_surjective
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
theorem projection_surjective : Function.Surjective (projection z)
def

kernelMulEquiv

L178 ↗
ClassFieldTower.ProP.H2CocycleExtension.kernelMulEquiv
Documentation

The kernel is the multiplicative wrapper of the lifted additive coefficient group.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · full declaration
def kernelMulEquiv : (projection z).ker ≃* Multiplicative (A p) where
  toFun x := x.1.left
  invFun a := ⟨⟨a, 1⟩, rfl⟩
  left_inv x := by
    apply Subtype.ext
    apply ext
    · rfl
    · have hx : x.1.right = 1 := x.property
      exact hx.symm
  right_inv _ := rfl
  map_mul' x y := by
    change x.1.left + y.1.left + normalizedCocycle z x.1.right y.1.right =
      x.1.left + y.1.left
    have hx : x.1.right = 1 := x.property
    have hy : y.1.right = 1 := y.property
    rw [hx, hy, normalizedCocycle_one_left]
    simp
def

kernelAddEquiv

L197 ↗
ClassFieldTower.ProP.H2CocycleExtension.kernelAddEquiv
Documentation

Additively, the kernel is exactly the lifted copy of ZMod p.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
def kernelAddEquiv : Additive ((projection z).ker) ≃+ A p
instance

instFiniteKernel

L200 ↗
ClassFieldTower.ProP.H2CocycleExtension.instFiniteKernel
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instFiniteKernel [Fact p.Prime] : Finite (projection z).ker
theorem

kernel_isPGroup

L203 ↗
ClassFieldTower.ProP.H2CocycleExtension.kernel_isPGroup
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
theorem kernel_isPGroup [Fact p.Prime] : IsPGroup p (projection z).ker
theorem

kernel_le_center

L210 ↗
ClassFieldTower.ProP.H2CocycleExtension.kernel_le_center
Documentation

The coefficient kernel is central in the cocycle extension.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
theorem kernel_le_center : (projection z).ker ≤ Subgroup.center (H2CocycleExtension z)
instance

instFinite

L225 ↗
ClassFieldTower.ProP.H2CocycleExtension.instFinite
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
instance instFinite [Fact p.Prime] [Finite Q] : Finite (H2CocycleExtension z)
theorem

isPGroup

L229 ↗
ClassFieldTower.ProP.H2CocycleExtension.isPGroup
Documentation

A cocycle extension of a finite p-group by ZMod p is again a finite p-group.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ}
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
namespace H2CocycleExtension
variable (z : Cohomology.trivialZModPCocyclesLifted p Q 2)
Lean source · statement
theorem isPGroup [Fact p.Prime] [Finite Q] (hQ : IsPGroup p Q) :
    IsPGroup p (H2CocycleExtension z)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.