Module

H2CocycleExtensionLinearLifts.lean

Nyll.GaloisCohomology.ProP.H2CocycleExtensionLinearLifts

14 declarations indexed from sourceView source ↗

Module documentation

Linear operations and character corrections on cocycle lifts

The chosen degree-two representatives are linear. Their normalized cocycles therefore respect addition and scalar multiplication. These identities construct actual sums and scalar multiples of lifts, while subtracting a continuous coefficient character corrects a lift without changing its projection.

Imports1

Nyll.GaloisCohomology.ProP.H2CentralExtensionClass

Imported by5

theorem

degreeTwoCocycleRepresentative_add

L33 ↗

ClassFieldTower.ProP.degreeTwoCocycleRepresentative_add

Documentation

The fixed representative section respects addition.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem degreeTwoCocycleRepresentative_add
    (x y : continuousCohomologyZModPLifted p Q 2) :
    degreeTwoCocycleRepresentative (x + y) =
      degreeTwoCocycleRepresentative x + degreeTwoCocycleRepresentative y

theorem

degreeTwoCocycleRepresentative_smul

L40 ↗

ClassFieldTower.ProP.degreeTwoCocycleRepresentative_smul

Documentation

The fixed representative section respects coefficient scalars.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem degreeTwoCocycleRepresentative_smul
    (c : ZMod p) (x : continuousCohomologyZModPLifted p Q 2) :
    degreeTwoCocycleRepresentative (c • x) = c • degreeTwoCocycleRepresentative x

theorem

degreeTwoCocycleRepresentative_zero

L46 ↗

ClassFieldTower.ProP.degreeTwoCocycleRepresentative_zero

Documentation

The fixed representative of zero is zero.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem degreeTwoCocycleRepresentative_zero :
    degreeTwoCocycleRepresentative (0 : continuousCohomologyZModPLifted p Q 2) = 0

theorem

normalizedCocycle_add

L51 ↗

ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_add

Documentation

Normalizing a homogeneous cocycle is additive.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem FreeProPH2Cocycle.normalizedCocycle_add
    (z w : trivialZModPCocyclesLifted p Q 2) (g h : Q) :
    normalizedCocycle (z + w) g h = normalizedCocycle z g h + normalizedCocycle w g h

theorem

normalizedCocycle_smul

L66 ↗

ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_smul

Documentation

Normalizing a homogeneous cocycle respects coefficient scalars.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem FreeProPH2Cocycle.normalizedCocycle_smul
    (c : ZMod p) (z : trivialZModPCocyclesLifted p Q 2) (g h : Q) :
    normalizedCocycle (c • z) g h = c • normalizedCocycle z g h

theorem

normalizedCocycle_zero

L76 ↗

ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_zero

Documentation

The normalized zero cocycle is zero.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem FreeProPH2Cocycle.normalizedCocycle_zero (g h : Q) :
    normalizedCocycle (0 : trivialZModPCocyclesLifted p Q 2) g h = 0

def

twistByCharacter

L84 ↗

ClassFieldTower.ProP.H2CocycleExtension.twistByCharacter

Documentation

Subtracting a continuous coefficient character corrects a lift's coefficient coordinate.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · full declaration

def H2CocycleExtension.twistByCharacter
    (z : trivialZModPCocyclesLifted p Q 2) (s : H →ₜ* H2CocycleExtension z)
    (chi : H →ₜ* Multiplicative (ZMod p)) : H →ₜ* H2CocycleExtension z where
  toFun h := ⟨(s h).left - ULift.up (chi h).toAdd, (s h).right⟩
  map_one' := by
    apply H2CocycleExtension.ext
    · change (s 1).left - ULift.up (chi 1).toAdd = 0
      rw [map_one s, map_one chi]
      exact sub_self _
    · change (s 1).right = 1
      rw [map_one s]
      rfl
  map_mul' a b := by
    apply H2CocycleExtension.ext
    · change (s (a * b)).left - ULift.up (chi (a * b)).toAdd =
        ((s a).left - ULift.up (chi a).toAdd) +
        ((s b).left - ULift.up (chi b).toAdd) +
        normalizedCocycle z (s a).right (s b).right
      rw [map_mul s, map_mul chi]
      apply ULift.ext
      change ((s a).left.down + (s b).left.down +
        (normalizedCocycle z (s a).right (s b).right).down) -
        ((chi a).toAdd + (chi b).toAdd) = _
      change _ = ((s a).left.down - (chi a).toAdd) +
        ((s b).left.down - (chi b).toAdd) +
        (normalizedCocycle z (s a).right (s b).right).down
      abel
    · change (s (a * b)).right = (s a).right * (s b).right
      exact congrArg (fun e : H2CocycleExtension z => e.right) (s.map_mul a b)
  continuous_toFun := by
    rw [continuous_induced_rng]
    have hs := (H2CocycleExtension.toProdHomeomorph z).continuous.comp s.continuous_toFun
    exact (hs.fst.sub (continuous_uliftUp.comp chi.continuous_toFun)).prodMk hs.snd

theorem

twistByCharacter_projection

L119 ↗

ClassFieldTower.ProP.H2CocycleExtension.twistByCharacter_projection

Documentation

Character correction preserves the projected group map.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem H2CocycleExtension.twistByCharacter_projection
    (z : trivialZModPCocyclesLifted p Q 2) (s : H →ₜ* H2CocycleExtension z)
    (chi : H →ₜ* Multiplicative (ZMod p)) :
    (H2CocycleExtension.projection z).comp (H2CocycleExtension.twistByCharacter z s chi) =
      (H2CocycleExtension.projection z).comp s

def

degreeTwoAddLift

L128 ↗

ClassFieldTower.ProP.degreeTwoAddLift

Documentation

Add the coefficient coordinates of two lifts with the same base projection.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · full declaration

def degreeTwoAddLift
    (x y : continuousCohomologyZModPLifted p Q 2)
    (s : H →ₜ* DegreeTwoCentralExtension x) (t : H →ₜ* DegreeTwoCentralExtension y)
    (hst : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative y)).comp t) :
    H →ₜ* DegreeTwoCentralExtension (x + y) where
  toFun h := ⟨(s h).left + (t h).left, (s h).right⟩
  map_one' := by
    apply H2CocycleExtension.ext
    · change (s 1).left + (t 1).left = 0
      rw [map_one s, map_one t]
      exact add_zero _
    · change (s 1).right = 1
      rw [map_one s]
      rfl
  map_mul' a b := by
    have ha : (s a).right = (t a).right := DFunLike.congr_fun hst a
    have hb : (s b).right = (t b).right := DFunLike.congr_fun hst b
    apply H2CocycleExtension.ext
    · change (s (a * b)).left + (t (a * b)).left =
        ((s a).left + (t a).left) + ((s b).left + (t b).left) +
          normalizedCocycle (degreeTwoCocycleRepresentative (x + y)) (s a).right (s b).right
      rw [map_mul s, map_mul t, degreeTwoCocycleRepresentative_add, normalizedCocycle_add]
      change ((s a).left + (s b).left +
          normalizedCocycle (degreeTwoCocycleRepresentative x) (s a).right (s b).right) +
        ((t a).left + (t b).left +
          normalizedCocycle (degreeTwoCocycleRepresentative y) (t a).right (t b).right) = _
      rw [← ha, ← hb]
      abel
    · change (s (a * b)).right = (s a).right * (s b).right
      exact congrArg (fun e : DegreeTwoCentralExtension x => e.right) (s.map_mul a b)
  continuous_toFun := by
    rw [continuous_induced_rng]
    have hs := (H2CocycleExtension.toProdHomeomorph
      (degreeTwoCocycleRepresentative x)).continuous.comp s.continuous_toFun
    have ht := (H2CocycleExtension.toProdHomeomorph
      (degreeTwoCocycleRepresentative y)).continuous.comp t.continuous_toFun
    exact (hs.fst.add ht.fst).prodMk hs.snd

theorem

degreeTwoAddLift_projection

L168 ↗

ClassFieldTower.ProP.degreeTwoAddLift_projection

Documentation

The added lift keeps the common base projection.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem degreeTwoAddLift_projection
    (x y : continuousCohomologyZModPLifted p Q 2)
    (s : H →ₜ* DegreeTwoCentralExtension x) (t : H →ₜ* DegreeTwoCentralExtension y)
    (hst : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative y)).comp t) :
    (H2CocycleExtension.projection (degreeTwoCocycleRepresentative (x + y))).comp
      (degreeTwoAddLift x y s t hst) =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s

def

degreeTwoSmulLift

L180 ↗

ClassFieldTower.ProP.degreeTwoSmulLift

Documentation

Scaling the coefficient coordinate lifts the scaled degree-two class.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · full declaration

def degreeTwoSmulLift (c : ZMod p) (x : continuousCohomologyZModPLifted p Q 2)
    (s : H →ₜ* DegreeTwoCentralExtension x) : H →ₜ* DegreeTwoCentralExtension (c • x) where
  toFun h := ⟨c • (s h).left, (s h).right⟩
  map_one' := by
    apply H2CocycleExtension.ext
    · change c • (s 1).left = 0
      rw [map_one s]
      exact smul_zero c
    · change (s 1).right = 1
      rw [map_one s]
      rfl
  map_mul' a b := by
    apply H2CocycleExtension.ext
    · change c • (s (a * b)).left =
        c • (s a).left + c • (s b).left +
          normalizedCocycle (degreeTwoCocycleRepresentative (c • x)) (s a).right (s b).right
      rw [map_mul s, degreeTwoCocycleRepresentative_smul, normalizedCocycle_smul]
      change c • ((s a).left + (s b).left +
        normalizedCocycle (degreeTwoCocycleRepresentative x) (s a).right (s b).right) = _
      rw [smul_add, smul_add]
    · change (s (a * b)).right = (s a).right * (s b).right
      exact congrArg (fun e : DegreeTwoCentralExtension x => e.right) (s.map_mul a b)
  continuous_toFun := by
    rw [continuous_induced_rng]
    have hs := (H2CocycleExtension.toProdHomeomorph
      (degreeTwoCocycleRepresentative x)).continuous.comp s.continuous_toFun
    exact (hs.fst.const_smul c).prodMk hs.snd

theorem

degreeTwoSmulLift_projection

L209 ↗

ClassFieldTower.ProP.degreeTwoSmulLift_projection

Documentation

The scaled lift has the same base projection.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem degreeTwoSmulLift_projection
    (c : ZMod p) (x : continuousCohomologyZModPLifted p Q 2)
    (s : H →ₜ* DegreeTwoCentralExtension x) :
    (H2CocycleExtension.projection (degreeTwoCocycleRepresentative (c • x))).comp
      (degreeTwoSmulLift c x s) =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s

def

degreeTwoZeroLift

L219 ↗

ClassFieldTower.ProP.degreeTwoZeroLift

Documentation

The zero degree-two class has a zero-coordinate lift of every base group map.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · full declaration

def degreeTwoZeroLift (q : H →ₜ* Q) :
    H →ₜ* DegreeTwoCentralExtension (0 : continuousCohomologyZModPLifted p Q 2) where
  toFun h := ⟨0, q h⟩
  map_one' := by
    apply H2CocycleExtension.ext
    · rfl
    · exact map_one q
  map_mul' a b := by
    apply H2CocycleExtension.ext
    · change 0 = 0 + 0 + normalizedCocycle
        (degreeTwoCocycleRepresentative (0 : continuousCohomologyZModPLifted p Q 2)) (q a) (q b)
      rw [degreeTwoCocycleRepresentative_zero, normalizedCocycle_zero, add_zero, add_zero]
    · exact map_mul q a b
  continuous_toFun := by
    rw [continuous_induced_rng]
    exact continuous_const.prodMk q.continuous_toFun

theorem

degreeTwoZeroLift_projection

L237 ↗

ClassFieldTower.ProP.degreeTwoZeroLift_projection

Documentation

The zero-coordinate lift projects to the input map.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology FreeProPH2Cocycle
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]

Lean source · statement

theorem degreeTwoZeroLift_projection (q : H →ₜ* Q) :
    (H2CocycleExtension.projection
      (degreeTwoCocycleRepresentative (0 : continuousCohomologyZModPLifted p Q 2))).comp
      (degreeTwoZeroLift q) = q

Module documentation

Linear operations and character corrections on cocycle lifts

Declarations