NYLL
Module

H2CocycleExtensionLinearLiftDifference.lean

Nyll.GaloisCohomology.ProP.H2CocycleExtensionLinearLiftDifference
8 declarations indexed from sourceView source ↗

Module documentation

Difference calculations for linear and character-corrected lifts

These formulas use the actual coefficient coordinates of the existing lifts. In particular, agreement of a correction character with the lift difference on a subgroup is exactly the condition for the corrected lift to kill that subgroup.

Imports4
Imported by2

Declarations

instance

linearLiftDifferenceCanonicalZModAddCommGroup

L32 ↗
ClassFieldTower.ProP.linearLiftDifferenceCanonicalZModAddCommGroup
Source context 6 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 w
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
theorem

liftDifference_trans

L40 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference_trans
Documentation

Differences of three lifts add, with multiplicative notation for characters.

Source context 10 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
namespace H2CocycleExtension
Lean source · statement
theorem liftDifference_trans
    (z : trivialZModPCocyclesLifted p Q 2)
    (s t r : H →ₜ* H2CocycleExtension z)
    (hst : (projection z).comp s = (projection z).comp t)
    (htr : (projection z).comp t = (projection z).comp r) :
    liftDifference z s r (hst.trans htr) =
      liftDifference z s t hst * liftDifference z t r htr
theorem

liftDifference_comp

L55 ↗
ClassFieldTower.ProP.H2CocycleExtension.liftDifference_comp
Documentation

Lift differences commute with actual restriction along a continuous homomorphism.

Source context 11 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
namespace H2CocycleExtension
omit [Fact p.Prime] in
Lean source · full declaration
theorem liftDifference_comp
    {J : Type w} [Group J] [TopologicalSpace J]
    (z : trivialZModPCocyclesLifted p Q 2)
    (s t : H →ₜ* H2CocycleExtension z)
    (hst : (projection z).comp s = (projection z).comp t)
    (f : J →ₜ* H) :
    (liftDifference z s t hst).comp f =
      liftDifference z (s.comp f) (t.comp f)
        (by ext h; exact DFunLike.congr_fun hst (f h)) := by
  ext h
  rfl
theorem

twistByCharacter_liftDifference

L68 ↗
ClassFieldTower.ProP.H2CocycleExtension.twistByCharacter_liftDifference
Documentation

Character correction subtracts that character from the lift difference.

Source context 10 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
namespace H2CocycleExtension
Lean source · statement
theorem twistByCharacter_liftDifference
    (z : trivialZModPCocyclesLifted p Q 2)
    (s t : H →ₜ* H2CocycleExtension z)
    (hst : (projection z).comp s = (projection z).comp t)
    (chi : H →ₜ* Multiplicative (ZMod p)) :
    liftDifference z (twistByCharacter z s chi) t
        ((twistByCharacter_projection z s chi).trans hst) =
      liftDifference z s t hst / chi
theorem

twistByCharacter_kills_subgroup_iff

L84 ↗
ClassFieldTower.ProP.H2CocycleExtension.twistByCharacter_kills_subgroup_iff
Documentation

Relative to a lift killing N, a character correction kills N exactly when its restriction agrees with the original difference character.

Source context 10 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
namespace H2CocycleExtension
Lean source · statement
theorem twistByCharacter_kills_subgroup_iff
    (z : trivialZModPCocyclesLifted p Q 2)
    (s t : H →ₜ* H2CocycleExtension z)
    (hst : (projection z).comp s = (projection z).comp t)
    (chi : H →ₜ* Multiplicative (ZMod p))
    (N : Subgroup H) (ht : N ≤ t.toMonoidHom.ker) :
    N ≤ (twistByCharacter z s chi).toMonoidHom.ker ↔
      (liftDifference z s t hst).comp (subgroupInclusion N) =
        chi.comp (subgroupInclusion N)
theorem

degreeTwoAddLift_liftDifference

L111 ↗
ClassFieldTower.ProP.degreeTwoAddLift_liftDifference
Documentation

Differences of added lifts are the sums of the two original differences.

Source context 9 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
Lean source · full declaration
theorem degreeTwoAddLift_liftDifference
    (x y : continuousCohomologyZModPLifted p Q 2)
    (s s' : H →ₜ* DegreeTwoCentralExtension x)
    (t t' : H →ₜ* DegreeTwoCentralExtension y)
    (hs : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s')
    (ht : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative y)).comp t =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative y)).comp t')
    (hst : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative x)).comp s =
      (H2CocycleExtension.projection (degreeTwoCocycleRepresentative y)).comp t) :
    H2CocycleExtension.liftDifference (degreeTwoCocycleRepresentative (x + y))
        (degreeTwoAddLift x y s t hst)
        (degreeTwoAddLift x y s' t' (hs.symm.trans (hst.trans ht)))
        (by rw [degreeTwoAddLift_projection, degreeTwoAddLift_projection]; exact hs) =
      H2CocycleExtension.liftDifference (degreeTwoCocycleRepresentative x) s s' hs *
        H2CocycleExtension.liftDifference (degreeTwoCocycleRepresentative y) t t' ht := by
  ext h
  apply Multiplicative.toAdd.injective
  change ((s h).left.down + (t h).left.down) - ((s' h).left.down + (t' h).left.down) =
    ((s h).left.down - (s' h).left.down) + ((t h).left.down - (t' h).left.down)
  abel
theorem

degreeTwoAddLift_kills_subgroup

L134 ↗
ClassFieldTower.ProP.degreeTwoAddLift_kills_subgroup
Documentation

An added lift kills every subgroup killed by both summands.

Source context 9 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
Lean source · statement
theorem degreeTwoAddLift_kills_subgroup
    (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)
    (N : Subgroup H) (hs : N ≤ s.toMonoidHom.ker) (ht : N ≤ t.toMonoidHom.ker) :
    N ≤ (degreeTwoAddLift x y s t hst).toMonoidHom.ker
theorem

degreeTwoZeroLift_ker

L151 ↗
ClassFieldTower.ProP.degreeTwoZeroLift_ker
Documentation

The zero-coordinate lift kills exactly the kernel of its base map.

Source context 9 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 w
variable {p : ℕ} [Fact p.Prime]
local instance linearLiftDifferenceCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable {H : Type v} [Group H] [TopologicalSpace H]
Lean source · statement
theorem degreeTwoZeroLift_ker (q : H →ₜ* Q) :
    (degreeTwoZeroLift (p := p) q).toMonoidHom.ker = q.toMonoidHom.ker

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