NYLL
Module

H2CocycleExtensionLiftDifference.lean

Nyll.GaloisCohomology.ProP.H2CocycleExtensionLiftDifference
5 declarations indexed from sourceView source ↗

Module documentation

Differences of lifts to a central cocycle extension

Two continuous lifts of the same group map differ by a continuous coefficient character. The cocycle terms cancel because their base coordinates agree. The construction takes values in ZMod p itself, so it can be restricted to inertia and used directly with arithmetic degree-one character APIs.

Imports2
Imported by5

Declarations

def

liftDifference

L38 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference
Documentation

The coefficient character measuring the difference between two lifts of one base-group map.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP.H2CocycleExtension
open ClassFieldTower.Cohomology FreeProPH2Cocycle
noncomputable section
universe u v
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H]
variable (z : trivialZModPCocyclesLifted p G 2)
variable (s t : H →ₜ* H2CocycleExtension z)
variable (hst : (projection z).comp s = (projection z).comp t)
Lean source · full declaration
def liftDifference : H →ₜ* Multiplicative (ZMod p) where
  toFun h := Multiplicative.ofAdd ((s h).left.down - (t h).left.down)
  map_one' := by
    change (s 1).left.down - (t 1).left.down = 0
    rw [map_one s, map_one t]
    exact sub_self _
  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
    change (s (a * b)).left.down - (t (a * b)).left.down =
      ((s a).left.down - (t a).left.down) +
        ((s b).left.down - (t b).left.down)
    rw [map_mul s, map_mul t]
    change ((s a).left.down + (s b).left.down +
        (normalizedCocycle z (s a).right (s b).right).down) -
      ((t a).left.down + (t b).left.down +
        (normalizedCocycle z (t a).right (t b).right).down) = _
    rw [ha, hb]
    abel
  continuous_toFun := by
    change Continuous fun h => (s h).left.down - (t h).left.down
    have hleft : Continuous fun e : H2CocycleExtension z => e.left :=
      continuous_fst.comp (toProdHomeomorph z).continuous
    exact (continuous_uliftDown.comp (hleft.comp s.continuous_toFun)).sub
      (continuous_uliftDown.comp (hleft.comp t.continuous_toFun))
theorem

liftDifference_apply

L66 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference_apply
Documentation

Evaluation uses the difference of the lifted coefficient coordinates.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP.H2CocycleExtension
open ClassFieldTower.Cohomology FreeProPH2Cocycle
noncomputable section
universe u v
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H]
variable (z : trivialZModPCocyclesLifted p G 2)
variable (s t : H →ₜ* H2CocycleExtension z)
variable (hst : (projection z).comp s = (projection z).comp t)
Lean source · statement
theorem liftDifference_apply (h : H) :
    liftDifference z s t hst h =
      Multiplicative.ofAdd ((s h).left.down - (t h).left.down)
theorem

liftDifference_apply_eq_one_iff

L71 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference_apply_eq_one_iff
Documentation

The difference vanishes at an element precisely when the lifts agree there.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP.H2CocycleExtension
open ClassFieldTower.Cohomology FreeProPH2Cocycle
noncomputable section
universe u v
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H]
variable (z : trivialZModPCocyclesLifted p G 2)
variable (s t : H →ₜ* H2CocycleExtension z)
variable (hst : (projection z).comp s = (projection z).comp t)
Lean source · statement
theorem liftDifference_apply_eq_one_iff (h : H) :
    liftDifference z s t hst h = 1 ↔ s h = t h
theorem

liftDifference_eq_one_iff

L82 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference_eq_one_iff
Documentation

The difference character is trivial precisely when the two lifts coincide.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP.H2CocycleExtension
open ClassFieldTower.Cohomology FreeProPH2Cocycle
noncomputable section
universe u v
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H]
variable (z : trivialZModPCocyclesLifted p G 2)
variable (s t : H →ₜ* H2CocycleExtension z)
variable (hst : (projection z).comp s = (projection z).comp t)
Lean source · statement
theorem liftDifference_eq_one_iff :
    liftDifference z s t hst = 1 ↔ s = t
theorem

liftDifference_restrict_eq_one_iff

L98 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference_restrict_eq_one_iff
Documentation

Relative to a lift killing a subgroup, the difference character restricts trivially exactly when the other lift also kills that subgroup.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP.H2CocycleExtension
open ClassFieldTower.Cohomology FreeProPH2Cocycle
noncomputable section
universe u v
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H]
variable (z : trivialZModPCocyclesLifted p G 2)
variable (s t : H →ₜ* H2CocycleExtension z)
variable (hst : (projection z).comp s = (projection z).comp t)
Lean source · statement
theorem liftDifference_restrict_eq_one_iff (N : Subgroup H)
    (ht : N ≤ t.toMonoidHom.ker) :
    (liftDifference z s t hst).comp (subgroupInclusion N) = 1 ↔
      N ≤ s.toMonoidHom.ker

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