NYLL
Module

FiniteStageTransgressionExact.lean

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

Module documentation

Exactness of finite-stage transgression

At an open finite quotient stage, every abstract mod-p character is continuous. This file therefore upgrades finite transgression exactness to the continuous degree-one characters of the ambient finite quotient: their restriction range is exactly the kernel of finite transgression.

Imports4
Imported by2

Declarations

instance

finiteStageExactCanonicalZModAddCommGroup

L35 ↗
ClassFieldTower.ProP.finiteStageExactCanonicalZModAddCommGroup
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

finiteStageContinuousH1Module

L38 ↗
ClassFieldTower.ProP.finiteStageContinuousH1Module
Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F)))
def

continuousH1OfFiniteStageCharacter

L46 ↗
ClassFieldTower.ProP.continuousH1OfFiniteStageCharacter
Documentation

Regard an abstract character of an open finite quotient as a continuous degree-one character.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule
Lean source · full declaration
def continuousH1OfFiniteStageCharacter
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (ψ : FiniteCharacter p (F ⧸ (U.1 : Subgroup F))) :
    ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F)) where
  toFun g := (ψ.toMul g.toMul).toAdd
  map_zero' := by
    change (ψ.toMul 1).toAdd = 0
    rw [map_one]
    rfl
  map_add' := by
    intro g h
    change (ψ.toMul (g.toMul * h.toMul)).toAdd =
      (ψ.toMul g.toMul).toAdd + (ψ.toMul h.toMul).toAdd
    rw [map_mul, toAdd_mul]
  continuous_toFun := continuous_of_discreteTopology
theorem

characterOfH1_continuousH1OfFiniteStageCharacter

L64 ↗
ClassFieldTower.ProP.characterOfH1_continuousH1OfFiniteStageCharacter
Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem characterOfH1_continuousH1OfFiniteStageCharacter
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (ψ : FiniteCharacter p (F ⧸ (U.1 : Subgroup F))) :
    Additive.ofMul
        (characterOfH1 (continuousH1OfFiniteStageCharacter U ψ)).toMonoidHom =
      ψ
def

finiteStageContinuousCharacterRestrictionAddHom

L74 ↗
ClassFieldTower.ProP.finiteStageContinuousCharacterRestrictionAddHom
Documentation

Restriction from continuous degree-one characters of an ambient finite quotient to conjugation-invariant characters of the image of R.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule
Lean source · full declaration
def finiteStageContinuousCharacterRestrictionAddHom
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F)) →+
      InvariantFiniteCharacter (p := p) (finiteStageImage R U) where
  toFun ψ := finiteCharacterRestrictionAddHom (p := p) (finiteStageImage R U)
    (Additive.ofMul (characterOfH1 ψ).toMonoidHom)
  map_zero' := by
    apply Subtype.ext
    rfl
  map_add' := by
    intro ψ φ
    apply Subtype.ext
    rfl
def

finiteStageContinuousCharacterRestrictionLinearMap

L90 ↗
ClassFieldTower.ProP.finiteStageContinuousCharacterRestrictionLinearMap
Documentation

Linear restriction from continuous degree-one characters of an ambient finite quotient.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule
Lean source · statement
def finiteStageContinuousCharacterRestrictionLinearMap
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F)) →ₗ[ZMod p]
      InvariantFiniteCharacter (p := p) (finiteStageImage R U)
theorem

finiteStageContinuousCharacterRestrictionLinearMap_realize

L99 ↗
ClassFieldTower.ProP.finiteStageContinuousCharacterRestrictionLinearMap_realize
Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule
omit [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem finiteStageContinuousCharacterRestrictionLinearMap_realize
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (ψ : FiniteCharacter p (F ⧸ (U.1 : Subgroup F))) :
    finiteStageContinuousCharacterRestrictionLinearMap R U
        (continuousH1OfFiniteStageCharacter U ψ) =
      finiteCharacterRestrictionLinearMap (p := p) (finiteStageImage R U) ψ
theorem

finiteStageContinuousCharacterRestriction_range_eq_transgression_ker

L111 ↗
ClassFieldTower.ProP.finiteStageContinuousCharacterRestriction_range_eq_transgression_ker
Documentation

At a finite quotient stage, continuous restriction is exact at invariant characters: its range is the kernel of finite transgression.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
local instance finiteStageExactCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteStageContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule
omit [T2Space F] [TotallyDisconnectedSpace F] in
Lean source · statement
theorem finiteStageContinuousCharacterRestriction_range_eq_transgression_ker
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    LinearMap.range (finiteStageContinuousCharacterRestrictionLinearMap R U) =
      LinearMap.ker
        (finiteTransgressionLinearMap (p := p) (finiteStageImage R U))

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