Module

H2CocycleExtensionPullback.lean

Nyll.GaloisCohomology.ProP.H2CocycleExtensionPullback

10 declarations indexed from sourceView source ↗

Module documentation

Pullback and local lifting for degree-two cocycle extensions

Restriction of a homogeneous degree-two cocycle is evaluated explicitly on the standard continuous resolution. The resulting pullback cocycle extension maps to the original extension, so vanishing of the restricted class produces an honest continuous lift of the restricting group homomorphism.

Imports1

Nyll.GaloisCohomology.ProP.H2CocycleExtensionSplitting

Imported by7

def

pulledBackH2Cocycle

L35 ↗

ClassFieldTower.ProP.pulledBackH2Cocycle

Documentation

Restriction of a lifted homogeneous degree-two cocycle along a continuous group homomorphism.

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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def pulledBackH2Cocycle
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) :
    Cohomology.trivialZModPCocyclesLifted p H 2

theorem

pulledBackH2Cocycle_cochain_apply

L44 ↗

ClassFieldTower.ProP.pulledBackH2Cocycle_cochain_apply

Documentation

Restriction evaluates a homogeneous cocycle by applying the base homomorphism to each argument.

Source context 9 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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [Fact p.Prime] in

Lean source · statement

theorem pulledBackH2Cocycle_cochain_apply
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (x y w : H) :
    (((Cohomology.trivialZModPCochainsLifted p H).iCycles 2).hom
      (pulledBackH2Cocycle f z)).1 x y w =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1
        (f x) (f y) (f w)

theorem

pulledBackH2Cocycle_π

L76 ↗

ClassFieldTower.ProP.pulledBackH2Cocycle_π

Documentation

Restriction commutes with the degree-two cocycle quotient map.

Source context 9 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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [Fact p.Prime] in

Lean source · statement

theorem pulledBackH2Cocycle_π
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) :
    ContinuousCohomology.π (Cohomology.trivialZModPLifted p H) 2
        (pulledBackH2Cocycle f z) =
      (Cohomology.continuousCohomologyZModPMapLifted p f 2).hom
        (ContinuousCohomology.π
          (Cohomology.trivialZModPLifted p G) 2 z)

theorem

normalizedCocycle_pulledBackH2Cocycle

L91 ↗

ClassFieldTower.ProP.normalizedCocycle_pulledBackH2Cocycle

Documentation

The normalized inhomogeneous cocycle also restricts pointwise.

Source context 9 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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [Fact p.Prime] in

Lean source · statement

theorem normalizedCocycle_pulledBackH2Cocycle
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (g h : H) :
    normalizedCocycle (pulledBackH2Cocycle f z) g h =
      normalizedCocycle z (f g) (f h)

def

pullbackToOriginal

L112 ↗

ClassFieldTower.ProP.H2CocycleExtension.pullbackToOriginal

Documentation

The pullback cocycle extension maps continuously to the original extension over the base homomorphism.

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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def H2CocycleExtension.pullbackToOriginal
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) :
    H2CocycleExtension (pulledBackH2Cocycle f z) →ₜ*
      H2CocycleExtension z where
  toFun x := ⟨x.left, f x.right⟩
  map_one' := by
    apply H2CocycleExtension.ext
    · rfl
    · exact f.map_one
  map_mul' x y := by
    apply H2CocycleExtension.ext
    · exact congrArg (x.left + y.left + ·)
        (normalizedCocycle_pulledBackH2Cocycle f z x.right y.right)
    · exact f.map_mul x.right y.right
  continuous_toFun := by
    rw [continuous_induced_rng]
    change Continuous fun x : H2CocycleExtension (pulledBackH2Cocycle f z) =>
      (x.left, f x.right)
    have hecont : Continuous
        (H2CocycleExtension.toProdEquiv (pulledBackH2Cocycle f z)) :=
      continuous_induced_dom
    exact (continuous_fst.comp hecont).prodMk
      (f.continuous_toFun.comp (continuous_snd.comp hecont))

theorem

projection_comp_pullbackToOriginal

L138 ↗

ClassFieldTower.ProP.H2CocycleExtension.projection_comp_pullbackToOriginal

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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem H2CocycleExtension.projection_comp_pullbackToOriginal
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) :
    (H2CocycleExtension.projection z).comp
        (H2CocycleExtension.pullbackToOriginal f z) =
      f.comp (H2CocycleExtension.projection (pulledBackH2Cocycle f z))

theorem

exists_lift_of_pullback_π_eq_zero

L148 ↗

ClassFieldTower.ProP.H2CocycleExtension.exists_lift_of_pullback_π_eq_zero

Documentation

Vanishing of the pulled-back class produces an explicit continuous lift of the base homomorphism to the original cocycle 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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem H2CocycleExtension.exists_lift_of_pullback_π_eq_zero
    [LocallyCompactSpace H]
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (hz : ContinuousCohomology.π
      (Cohomology.trivialZModPLifted p H) 2
        (pulledBackH2Cocycle f z) = 0) :
    ∃ s : H →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s = f

theorem

exists_lift_of_restriction_eq_zero

L169 ↗

ClassFieldTower.ProP.H2CocycleExtension.exists_lift_of_restriction_eq_zero

Documentation

The cohomological restriction being zero is the source-level local splitting criterion for the original cocycle 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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem H2CocycleExtension.exists_lift_of_restriction_eq_zero
    [LocallyCompactSpace H]
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (hz : (Cohomology.continuousCohomologyZModPMapLifted p f 2).hom
      (ContinuousCohomology.π
        (Cohomology.trivialZModPLifted p G) 2 z) = 0) :
    ∃ s : H →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s = f

theorem

restriction_eq_zero_of_lift

L184 ↗

ClassFieldTower.ProP.H2CocycleExtension.restriction_eq_zero_of_lift

Documentation

A continuous lift gives a section of the pullback extension and hence makes the restricted degree-two class vanish.

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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem H2CocycleExtension.restriction_eq_zero_of_lift
    [LocallyCompactSpace H]
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (s : H →ₜ* H2CocycleExtension z)
    (hs : (H2CocycleExtension.projection z).comp s = f) :
    (Cohomology.continuousCohomologyZModPMapLifted p f 2).hom
      (ContinuousCohomology.π
        (Cohomology.trivialZModPLifted p G) 2 z) = 0

theorem

exists_lift_iff_restriction_eq_zero

L230 ↗

ClassFieldTower.ProP.H2CocycleExtension.exists_lift_iff_restriction_eq_zero

Documentation

A homomorphism lifts continuously to the cocycle extension exactly when the corresponding restriction of its degree-two class vanishes.

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 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem H2CocycleExtension.exists_lift_iff_restriction_eq_zero
    [LocallyCompactSpace H]
    (f : H →ₜ* G)
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) :
    (∃ s : H →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s = f) ↔
    (Cohomology.continuousCohomologyZModPMapLifted p f 2).hom
      (ContinuousCohomology.π
        (Cohomology.trivialZModPLifted p G) 2 z) = 0

Module documentation

Pullback and local lifting for degree-two cocycle extensions

Declarations