Module

ContinuousH1Bridge.lean

Nyll.GaloisCohomology.ProP.ContinuousH1Bridge

51 declarations indexed from sourceView source ↗

Module documentation

Continuous degree-one cohomology bridge

This file identifies continuous additive ZMod p-characters with Mathlib's degree-one continuous cohomology for the trivial coefficient representation. It supplies both the small-universe coefficient API and the universe-polymorphic API whose coefficient carrier is ULift (ZMod p). The construction is explicit: a character χ is sent to the homogeneous cocycle (g, h) ↦ χ(g⁻¹h), and the inverse evaluates a homogeneous cocycle at (1, g).

Imports2

Imported by5

instance

continuousSMulULiftZMod

L33 ↗

ClassFieldTower.Cohomology.continuousSMulULiftZMod

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p))

instance

continuousH1ZModModuleInstanceLifted

L37 ↗

ClassFieldTower.Cohomology.continuousH1ZModModuleInstanceLifted

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap

Lean source · statement

instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))

def

topModuleLineLifted

L42 ↗

ClassFieldTower.Cohomology.topModuleLineLifted

Documentation

The continuous linear map from the lifted scalar line generated by x.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def topModuleLineLifted {M : TopModuleCat.{u} (ZMod p)} (x : M) :
    TopModuleCat.of (ZMod p) (ULift.{u} (ZMod p)) ⟶ M

theorem

topModule_mono_injective_lifted

L58 ↗

ClassFieldTower.Cohomology.topModule_mono_injective_lifted

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem topModule_mono_injective_lifted
    {M N : TopModuleCat.{u} (ZMod p)} (f : M ⟶ N) [Mono f] :
    Function.Injective f

def

homogeneousOneCochainOfH1Lifted

L76 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfH1Lifted

Documentation

The homogeneous one-cochain (g, h) ↦ χ(g⁻¹h) with lifted values.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def homogeneousOneCochainOfH1Lifted
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    (ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).X 1

theorem

homogeneousOneCochainOfH1Lifted_apply

L99 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfH1Lifted_apply

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfH1Lifted_apply
    (χ : ContinuousH1ZMod (p := p) (G := G)) (g h : G) :
    (homogeneousOneCochainOfH1Lifted χ).1 g h =
      ULift.up (χ (Additive.ofMul (g⁻¹ * h)))

theorem

homogeneousOneCochainOfH1Lifted_mem_cycles

L105 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfH1Lifted_mem_cycles

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfH1Lifted_mem_cycles
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    ((ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).d 1 2).hom
      (homogeneousOneCochainOfH1Lifted χ) = 0

def

homogeneousOneCochainLineOfH1Lifted

L132 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainLineOfH1Lifted

Documentation

The lifted scalar line through the homogeneous cocycle attached to χ.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def homogeneousOneCochainLineOfH1Lifted
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    TopModuleCat.of (ZMod p) (ULift.{u} (ZMod p)) ⟶
      (ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).X 1

theorem

homogeneousOneCochainLineOfH1Lifted_comp_d

L138 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainLineOfH1Lifted_comp_d

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainLineOfH1Lifted_comp_d
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    homogeneousOneCochainLineOfH1Lifted χ ≫
        (ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).d 1 2 = 0

def

cocycleOfH1Lifted

L151 ↗

ClassFieldTower.Cohomology.cocycleOfH1Lifted

Documentation

Regard a continuous additive character as a lifted homogeneous one-cocycle.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def cocycleOfH1Lifted (χ : ContinuousH1ZMod (p := p) (G := G)) :
    ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1

def

homogeneousOneCochainOfCocycleLifted

L158 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted

Documentation

The homogeneous one-cochain underlying a lifted one-cocycle.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def homogeneousOneCochainOfCocycleLifted
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1) :
    (ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).X 1

theorem

homogeneousOneCochainOfCocycleLifted_cocycleOfH1Lifted

L163 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted_cocycleOfH1Lifted

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycleLifted_cocycleOfH1Lifted
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    homogeneousOneCochainOfCocycleLifted (cocycleOfH1Lifted χ) =
      homogeneousOneCochainOfH1Lifted χ

theorem

homogeneousOneCochainOfCocycleLifted_mem_cycles

L177 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted_mem_cycles

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycleLifted_mem_cycles
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1) :
    ((ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).d 1 2).hom
      (homogeneousOneCochainOfCocycleLifted z) = 0

theorem

homogeneousOneCochainOfCocycleLifted_cocycle_identity

L187 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted_cocycle_identity

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycleLifted_cocycle_identity
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1)
    (g h k : G) :
    (homogeneousOneCochainOfCocycleLifted z).1 h k -
        ((homogeneousOneCochainOfCocycleLifted z).1 g k -
          (homogeneousOneCochainOfCocycleLifted z).1 g h) = 0

theorem

homogeneousOneCochainOfCocycleLifted_invariant

L205 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted_invariant

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycleLifted_invariant
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1)
    (a g h : G) :
    (homogeneousOneCochainOfCocycleLifted z).1 (a⁻¹ * g) (a⁻¹ * h) =
      (homogeneousOneCochainOfCocycleLifted z).1 g h

theorem

homogeneousOneCochainOfCocycleLifted_cocycle_identity_down

L220 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted_cocycle_identity_down

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycleLifted_cocycle_identity_down
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1)
    (g h k : G) :
    ((homogeneousOneCochainOfCocycleLifted z).1 h k).down -
        (((homogeneousOneCochainOfCocycleLifted z).1 g k).down -
          ((homogeneousOneCochainOfCocycleLifted z).1 g h).down) = 0

theorem

homogeneousOneCochainOfCocycleLifted_invariant_down

L230 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycleLifted_invariant_down

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycleLifted_invariant_down
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1)
    (a g h : G) :
    ((homogeneousOneCochainOfCocycleLifted z).1 (a⁻¹ * g) (a⁻¹ * h)).down =
      ((homogeneousOneCochainOfCocycleLifted z).1 g h).down

def

h1OfCocycleLifted

L239 ↗

ClassFieldTower.Cohomology.h1OfCocycleLifted

Documentation

Recover a continuous additive character from a lifted homogeneous one-cocycle.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · full declaration

def h1OfCocycleLifted
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1) :
    ContinuousH1ZMod (p := p) (G := G) where
  toFun g := ((homogeneousOneCochainOfCocycleLifted z).1 1 g.toMul).down
  map_zero' := by
    change ((homogeneousOneCochainOfCocycleLifted z).1 1 1).down = 0
    have hz := homogeneousOneCochainOfCocycleLifted_cocycle_identity_down z 1 1 1
    have hz' := sub_eq_zero.mp hz
    abel_nf at hz'
    exact hz'
  map_add' := by
    intro g h
    have hz := homogeneousOneCochainOfCocycleLifted_cocycle_identity_down
      z 1 g.toMul (g.toMul * h.toMul)
    have hinv := homogeneousOneCochainOfCocycleLifted_invariant_down
      z g.toMul g.toMul (g.toMul * h.toMul)
    have hinv' :
        ((homogeneousOneCochainOfCocycleLifted z).1 1 h.toMul).down =
          ((homogeneousOneCochainOfCocycleLifted z).1 g.toMul
            (g.toMul * h.toMul)).down := by
      convert hinv using 1; group
    rw [← hinv'] at hz
    change ((homogeneousOneCochainOfCocycleLifted z).1 1
        (g.toMul * h.toMul)).down =
      ((homogeneousOneCochainOfCocycleLifted z).1 1 g.toMul).down +
        ((homogeneousOneCochainOfCocycleLifted z).1 1 h.toMul).down
    have heq := sub_eq_zero.mp hz
    have hadd := (eq_sub_iff_add_eq).mp heq
    simpa only [add_comm] using hadd.symm
  continuous_toFun := ((ContinuousLinearEquiv.ulift :
      ULift.{u} (ZMod p) ≃L[ZMod p] ZMod p).continuous).comp
    ((homogeneousOneCochainOfCocycleLifted z).1 1 |>.continuous)

theorem

h1OfCocycleLifted_cocycleOfH1Lifted

L272 ↗

ClassFieldTower.Cohomology.h1OfCocycleLifted_cocycleOfH1Lifted

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem h1OfCocycleLifted_cocycleOfH1Lifted
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    h1OfCocycleLifted (cocycleOfH1Lifted χ) = χ

theorem

cocycleOfH1Lifted_h1OfCocycleLifted

L282 ↗

ClassFieldTower.Cohomology.cocycleOfH1Lifted_h1OfCocycleLifted

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem cocycleOfH1Lifted_h1OfCocycleLifted
    (z : ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1) :
    cocycleOfH1Lifted (h1OfCocycleLifted z) = z

theorem

cocycleOfH1Lifted_add

L299 ↗

ClassFieldTower.Cohomology.cocycleOfH1Lifted_add

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem cocycleOfH1Lifted_add
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    cocycleOfH1Lifted (χ + ψ) = cocycleOfH1Lifted χ + cocycleOfH1Lifted ψ

theorem

cocycleOfH1Lifted_smul

L323 ↗

ClassFieldTower.Cohomology.cocycleOfH1Lifted_smul

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem cocycleOfH1Lifted_smul
    (a : ZMod p) (χ : ContinuousH1ZMod (p := p) (G := G)) :
    cocycleOfH1Lifted (a • χ) = a • cocycleOfH1Lifted χ

def

continuousH1ZModEquivCocyclesLifted

L348 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivCocyclesLifted

Documentation

Continuous additive characters are linearly equivalent to lifted homogeneous one-cocycles.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · full declaration

def continuousH1ZModEquivCocyclesLifted :
    ContinuousH1ZMod (p := p) (G := G) ≃ₗ[ZMod p]
      ClassFieldTower.Cohomology.trivialZModPCocyclesLifted p G 1 where
  toFun := cocycleOfH1Lifted
  invFun := h1OfCocycleLifted
  map_add' := cocycleOfH1Lifted_add
  map_smul' := cocycleOfH1Lifted_smul
  left_inv := h1OfCocycleLifted_cocycleOfH1Lifted
  right_inv := cocycleOfH1Lifted_h1OfCocycleLifted

theorem

trivialZModPCochainsLifted_d_zero_one

L359 ↗

ClassFieldTower.Cohomology.trivialZModPCochainsLifted_d_zero_one

Documentation

For trivial lifted coefficients, every homogeneous zero-cochain has zero differential.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem trivialZModPCochainsLifted_d_zero_one :
    (ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).d 0 1 = 0

def

continuousH1ZModEquivContinuousCohomologyLifted

L408 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivContinuousCohomologyLifted

Documentation

The canonical ZMod p-linear equivalence from continuous additive characters to degree-one continuous cohomology with universe-lifted trivial coefficients.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def continuousH1ZModEquivContinuousCohomologyLifted :
    ContinuousH1ZMod (p := p) (G := G) ≃ₗ[ZMod p]
      ClassFieldTower.Cohomology.continuousCohomologyZModPLifted p G 1

theorem

continuousH1ZModEquivContinuousCohomologyLifted_apply

L417 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivContinuousCohomologyLifted_apply

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem continuousH1ZModEquivContinuousCohomologyLifted_apply
    (χ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1ZModEquivContinuousCohomologyLifted χ =
      ContinuousCohomology.π
        (ClassFieldTower.Cohomology.trivialZModPLifted p G) 1 (cocycleOfH1Lifted χ)

theorem

continuousH1ZModEquivContinuousCohomologyLifted_symm_apply

L425 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivContinuousCohomologyLifted_symm_apply

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem continuousH1ZModEquivContinuousCohomologyLifted_symm_apply
    (x : ClassFieldTower.Cohomology.continuousCohomologyZModPLifted p G 1) :
    continuousH1ZModEquivContinuousCohomologyLifted.symm x =
      h1OfCocycleLifted
        (((ClassFieldTower.Cohomology.trivialZModPCochainsLifted p G).isoHomologyπ
          0 1 (CochainComplex.prev_nat_succ 0)
            trivialZModPCochainsLifted_d_zero_one).inv x)

instance

continuousH1ZModModuleInstance

L439 ↗

ClassFieldTower.Cohomology.continuousH1ZModModuleInstance

Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]

Lean source · statement

instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀))

def

topModuleLine

L444 ↗

ClassFieldTower.Cohomology.topModuleLine

Documentation

The continuous linear map from the scalar line generated by x.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

def topModuleLine {M : TopModuleCat.{0} (ZMod p)} (x : M) :
    TopModuleCat.of (ZMod p) (ZMod p) ⟶ M

theorem

topModule_mono_injective

L453 ↗

ClassFieldTower.Cohomology.topModule_mono_injective

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem topModule_mono_injective
    {M N : TopModuleCat.{0} (ZMod p)} (f : M ⟶ N) [Mono f] :
    Function.Injective f

def

homogeneousOneCochainOfH1

L470 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfH1

Documentation

The homogeneous one-cochain (g, h) ↦ χ(g⁻¹h) with small-universe values.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

def homogeneousOneCochainOfH1
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    (ClassFieldTower.Cohomology.trivialZModPCochains p G₀).X 1

theorem

homogeneousOneCochainOfH1_apply

L490 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfH1_apply

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfH1_apply
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) (g h : G₀) :
    (homogeneousOneCochainOfH1 χ).1 g h =
      χ (Additive.ofMul (g⁻¹ * h))

theorem

homogeneousOneCochainOfH1_mem_cycles

L496 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfH1_mem_cycles

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfH1_mem_cycles
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    ((ClassFieldTower.Cohomology.trivialZModPCochains p G₀).d 1 2).hom
      (homogeneousOneCochainOfH1 χ) = 0

def

homogeneousOneCochainLineOfH1

L522 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainLineOfH1

Documentation

The scalar line through the small-universe homogeneous cocycle attached to χ.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

def homogeneousOneCochainLineOfH1
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    TopModuleCat.of (ZMod p) (ZMod p) ⟶
      (ClassFieldTower.Cohomology.trivialZModPCochains p G₀).X 1

theorem

homogeneousOneCochainLineOfH1_comp_d

L533 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainLineOfH1_comp_d

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainLineOfH1_comp_d
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    homogeneousOneCochainLineOfH1 χ ≫
        (ClassFieldTower.Cohomology.trivialZModPCochains p G₀).d 1 2 = 0

def

cocycleOfH1

L546 ↗

ClassFieldTower.Cohomology.cocycleOfH1

Documentation

Regard a continuous additive character as a small-universe homogeneous one-cocycle.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

def cocycleOfH1 (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1

def

homogeneousOneCochainOfCocycle

L553 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycle

Documentation

The homogeneous one-cochain underlying a small-universe one-cocycle.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

def homogeneousOneCochainOfCocycle
    (z : ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1) :
    (ClassFieldTower.Cohomology.trivialZModPCochains p G₀).X 1

theorem

homogeneousOneCochainOfCocycle_cocycleOfH1

L558 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycle_cocycleOfH1

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycle_cocycleOfH1
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    homogeneousOneCochainOfCocycle (cocycleOfH1 χ) =
      homogeneousOneCochainOfH1 χ

theorem

homogeneousOneCochainOfCocycle_mem_cycles

L571 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycle_mem_cycles

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycle_mem_cycles
    (z : ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1) :
    ((ClassFieldTower.Cohomology.trivialZModPCochains p G₀).d 1 2).hom
      (homogeneousOneCochainOfCocycle z) = 0

theorem

homogeneousOneCochainOfCocycle_cocycle_identity

L581 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycle_cocycle_identity

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycle_cocycle_identity
    (z : ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1)
    (g h k : G₀) :
    (homogeneousOneCochainOfCocycle z).1 h k -
        ((homogeneousOneCochainOfCocycle z).1 g k -
          (homogeneousOneCochainOfCocycle z).1 g h) = 0

theorem

homogeneousOneCochainOfCocycle_invariant

L599 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainOfCocycle_invariant

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem homogeneousOneCochainOfCocycle_invariant
    (z : ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1)
    (a g h : G₀) :
    (homogeneousOneCochainOfCocycle z).1 (a⁻¹ * g) (a⁻¹ * h) =
      (homogeneousOneCochainOfCocycle z).1 g h

def

h1OfCocycle

L615 ↗

ClassFieldTower.Cohomology.h1OfCocycle

Documentation

Recover a continuous additive character from a small-universe homogeneous one-cocycle.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · full declaration

def h1OfCocycle
    (z : ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1) :
    ContinuousH1ZMod (p := p) (G := G₀) where
  toFun g := (homogeneousOneCochainOfCocycle z).1 1 g.toMul
  map_zero' := by
    change (homogeneousOneCochainOfCocycle z).1 1 1 = (0 : ZMod p)
    have hz := homogeneousOneCochainOfCocycle_cocycle_identity z 1 1 1
    change (homogeneousOneCochainOfCocycle z).1 1 1 -
      ((homogeneousOneCochainOfCocycle z).1 1 1 -
        (homogeneousOneCochainOfCocycle z).1 1 1) = (0 : ZMod p) at hz
    have hz' := sub_eq_zero.mp hz
    simp only [ClassFieldTower.Cohomology.trivialZModP] at hz'
    abel_nf at hz'
    exact hz'
  map_add' := by
    intro g h
    have hz := homogeneousOneCochainOfCocycle_cocycle_identity
      z 1 g.toMul (g.toMul * h.toMul)
    change (homogeneousOneCochainOfCocycle z).1 g.toMul
        (g.toMul * h.toMul) -
      ((homogeneousOneCochainOfCocycle z).1 1 (g.toMul * h.toMul) -
        (homogeneousOneCochainOfCocycle z).1 1 g.toMul) = (0 : ZMod p) at hz
    have hinv := homogeneousOneCochainOfCocycle_invariant
      z g.toMul g.toMul (g.toMul * h.toMul)
    have hinv' :
        (homogeneousOneCochainOfCocycle z).1 1 h.toMul =
          (homogeneousOneCochainOfCocycle z).1 g.toMul
            (g.toMul * h.toMul) := by
      convert hinv using 1; group
    rw [← hinv'] at hz
    change (homogeneousOneCochainOfCocycle z).1 1 (g.toMul * h.toMul) =
      (homogeneousOneCochainOfCocycle z).1 1 g.toMul +
        (homogeneousOneCochainOfCocycle z).1 1 h.toMul
    have heq := sub_eq_zero.mp hz
    have hadd := (eq_sub_iff_add_eq).mp heq
    simpa only [add_comm] using hadd.symm
  continuous_toFun := (homogeneousOneCochainOfCocycle z).1 1 |>.continuous

theorem

h1OfCocycle_cocycleOfH1

L653 ↗

ClassFieldTower.Cohomology.h1OfCocycle_cocycleOfH1

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem h1OfCocycle_cocycleOfH1
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    h1OfCocycle (cocycleOfH1 χ) = χ

theorem

cocycleOfH1_h1OfCocycle

L662 ↗

ClassFieldTower.Cohomology.cocycleOfH1_h1OfCocycle

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem cocycleOfH1_h1OfCocycle
    (z : ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1) :
    cocycleOfH1 (h1OfCocycle z) = z

theorem

cocycleOfH1_add

L677 ↗

ClassFieldTower.Cohomology.cocycleOfH1_add

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem cocycleOfH1_add
    (χ ψ : ContinuousH1ZMod (p := p) (G := G₀)) :
    cocycleOfH1 (χ + ψ) = cocycleOfH1 χ + cocycleOfH1 ψ

theorem

cocycleOfH1_smul

L698 ↗

ClassFieldTower.Cohomology.cocycleOfH1_smul

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem cocycleOfH1_smul
    (a : ZMod p) (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    cocycleOfH1 (a • χ) = a • cocycleOfH1 χ

def

continuousH1ZModEquivCocycles

L722 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivCocycles

Documentation

Continuous additive characters are linearly equivalent to homogeneous one-cocycles.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · full declaration

def continuousH1ZModEquivCocycles :
    ContinuousH1ZMod (p := p) (G := G₀) ≃ₗ[ZMod p]
      ClassFieldTower.Cohomology.trivialZModPCocycles p G₀ 1 where
  toFun := cocycleOfH1
  invFun := h1OfCocycle
  map_add' := cocycleOfH1_add
  map_smul' := cocycleOfH1_smul
  left_inv := h1OfCocycle_cocycleOfH1
  right_inv := cocycleOfH1_h1OfCocycle

theorem

trivialZModPCochains_d_zero_one

L734 ↗

ClassFieldTower.Cohomology.trivialZModPCochains_d_zero_one

Documentation

For trivial small-universe coefficients, every homogeneous zero-cochain has zero differential.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem trivialZModPCochains_d_zero_one :
    (ClassFieldTower.Cohomology.trivialZModPCochains p G₀).d 0 1 = 0

def

continuousH1ZModEquivContinuousCohomology

L783 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivContinuousCohomology

Documentation

The canonical ZMod p-linear equivalence from continuous additive characters to degree-one continuous cohomology with small-universe trivial coefficients.

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

def continuousH1ZModEquivContinuousCohomology :
    ContinuousH1ZMod (p := p) (G := G₀) ≃ₗ[ZMod p]
      ClassFieldTower.Cohomology.continuousCohomologyZModP p G₀ 1

theorem

continuousH1ZModEquivContinuousCohomology_apply

L792 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivContinuousCohomology_apply

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem continuousH1ZModEquivContinuousCohomology_apply
    (χ : ContinuousH1ZMod (p := p) (G := G₀)) :
    continuousH1ZModEquivContinuousCohomology χ =
      ContinuousCohomology.π
        (ClassFieldTower.Cohomology.trivialZModP p G₀) 1 (cocycleOfH1 χ)

theorem

continuousH1ZModEquivContinuousCohomology_symm_apply

L800 ↗

ClassFieldTower.Cohomology.continuousH1ZModEquivContinuousCohomology_symm_apply

Source context 14 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1ZModModuleInstanceLifted :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section SmallUniverse
variable {p : ℕ}
variable {G₀ : Type} [Group G₀] [TopologicalSpace G₀] [IsTopologicalGroup G₀]
local instance continuousH1ZModModuleInstance :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G₀)) :=
  continuousH1ZModModule

Lean source · statement

theorem continuousH1ZModEquivContinuousCohomology_symm_apply
    (x : ClassFieldTower.Cohomology.continuousCohomologyZModP p G₀ 1) :
    continuousH1ZModEquivContinuousCohomology.symm x =
      h1OfCocycle
        (((ClassFieldTower.Cohomology.trivialZModPCochains p G₀).isoHomologyπ
          0 1 (CochainComplex.prev_nat_succ 0)
            trivialZModPCochains_d_zero_one).inv x)

Module documentation

Continuous degree-one cohomology bridge

Declarations