NYLL
Module

ContinuousTransgressionExact.lean

Nyll.GaloisCohomology.ProP.ContinuousTransgressionExact
10 declarations indexed from sourceView source ↗

Module documentation

Exactness of continuous transgression

For an open normal subgroup, restriction of an ambient continuous mod-p character lands in the conjugation-invariant continuous characters. Its range is exactly the kernel of the continuous factor-set transgression.

Imports9
Imported by2

Declarations

instance

continuousExactZModAddCommGroup

L41 ↗
ClassFieldTower.Cohomology.continuousExactZModAddCommGroup
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p)
instance

continuousExactH1Module

L44 ↗
ClassFieldTower.Cohomology.continuousExactH1Module
Source context 11 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
def

continuousCharacterRestrictionAddHom

L50 ↗
ClassFieldTower.Cohomology.continuousCharacterRestrictionAddHom
Documentation

Restriction of an ambient continuous character to an open normal subgroup.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def continuousCharacterRestrictionAddHom
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    ContinuousH1ZMod (p := p) (G := G) →+ InvariantContinuousH1 U where
  toFun psi := by
    let restricted : ContinuousH1ZMod (p := p) (G := (U.1 : Subgroup G)) :=
      { toFun := fun n ↦ psi (Additive.ofMul n.1)
        map_zero' := psi.map_zero
        map_add' := fun n m ↦ psi.map_add (Additive.ofMul n.1) (Additive.ofMul m.1)
        continuous_toFun := psi.continuous_toFun.comp continuous_subtype_val }
    exact ⟨restricted, by
      intro g n
      change psi (Additive.ofMul (g * n.1 * g⁻¹)) = psi (Additive.ofMul n.1)
      rw [show Additive.ofMul (g * n.1 * g⁻¹) =
          Additive.ofMul g + Additive.ofMul n.1 + Additive.ofMul g⁻¹ by rfl,
        map_add, map_add,
        show Additive.ofMul g⁻¹ = -(Additive.ofMul g) by rfl, map_neg]
      abel⟩
  map_zero' := by
    apply Subtype.ext
    ext n
    rfl
  map_add' := by
    intro psi phi
    apply Subtype.ext
    ext n
    rfl
def

continuousCharacterRestrictionLinearMap

L78 ↗
ClassFieldTower.Cohomology.continuousCharacterRestrictionLinearMap
Documentation

Linear restriction of ambient continuous degree-one classes.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousCharacterRestrictionLinearMap
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    ContinuousH1ZMod (p := p) (G := G) →ₗ[ZMod p] InvariantContinuousH1 U
def

continuousHomogeneousOneCochainNormalizedValue

L84 ↗
ClassFieldTower.Cohomology.continuousHomogeneousOneCochainNormalizedValue
Documentation

The normalized inhomogeneous value of a continuous homogeneous one-cochain.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousHomogeneousOneCochainNormalizedValue
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (c : (trivialZModPCochainsLifted p (G ⧸ (U.1 : Subgroup G))).X 1)
    (q : G ⧸ (U.1 : Subgroup G)) : ZMod p
theorem

continuousHomogeneousOneCochain_invariant

L91 ↗
ClassFieldTower.Cohomology.continuousHomogeneousOneCochain_invariant
Documentation

Continuous homogeneous one-cochains are invariant under simultaneous left translation.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousHomogeneousOneCochain_invariant
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (c : (trivialZModPCochainsLifted p (G ⧸ (U.1 : Subgroup G))).X 1)
    (a q r : G ⧸ (U.1 : Subgroup G)) :
    c.1 (a⁻¹ * q) (a⁻¹ * r) = c.1 q r
theorem

continuousHomogeneousOneCochainNormalizedValue_primitive

L105 ↗
ClassFieldTower.Cohomology.continuousHomogeneousOneCochainNormalizedValue_primitive
Documentation

A continuous homogeneous primitive gives the inhomogeneous factor-set coboundary.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousHomogeneousOneCochainNormalizedValue_primitive
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U)
    (c : (trivialZModPCochainsLifted p (G ⧸ (U.1 : Subgroup G))).X 1)
    (hc : ((trivialZModPCochainsLifted p
      (G ⧸ (U.1 : Subgroup G))).d 1 2).hom c =
        continuousTransgressionHomogeneousCochain U chi)
    (q r : G ⧸ (U.1 : Subgroup G)) :
    continuousHomogeneousOneCochainNormalizedValue U c r -
        continuousHomogeneousOneCochainNormalizedValue U c (q * r) +
          continuousHomogeneousOneCochainNormalizedValue U c q =
      transgressionFactor (U.1 : Subgroup G)
        (characterOfH1 chi.1).toMonoidHom q r
theorem

continuousTransgressionLinearMap_eq_zero_of_extendsToAmbient

L158 ↗
ClassFieldTower.Cohomology.continuousTransgressionLinearMap_eq_zero_of_extendsToAmbient
Documentation

An invariant continuous character extending abstractly to the ambient group has zero continuous transgression.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousTransgressionLinearMap_eq_zero_of_extendsToAmbient
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U)
    (psi : MonoidHom G (Multiplicative (ZMod p)))
    (hpsi : psi.comp (U.1 : Subgroup G).subtype =
      (characterOfH1 chi.1).toMonoidHom) :
    continuousTransgressionLinearMap U chi = 0
theorem

exists_continuous_extension_of_continuousTransgression_eq_zero

L218 ↗
ClassFieldTower.Cohomology.exists_continuous_extension_of_continuousTransgression_eq_zero
Documentation

Vanishing continuous transgression gives an ambient continuous extension.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem exists_continuous_extension_of_continuousTransgression_eq_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U)
    (hzero : continuousTransgressionLinearMap U chi = 0) :
    ∃ psi : ContinuousH1ZMod (p := p) (G := G),
      continuousCharacterRestrictionLinearMap U psi = chi
theorem

continuousCharacterRestriction_range_eq_transgression_ker

L273 ↗
ClassFieldTower.Cohomology.continuousCharacterRestriction_range_eq_transgression_ker
Documentation

The continuous low-degree transgression sequence is exact at invariant subgroup characters.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousExactZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousExactH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousCharacterRestriction_range_eq_transgression_ker
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    LinearMap.range (continuousCharacterRestrictionLinearMap U) =
      LinearMap.ker (continuousTransgressionLinearMap U)

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