NYLL
Module

ContinuousH1InflationExact.lean

Nyll.GaloisCohomology.ProP.ContinuousH1InflationExact
9 declarations indexed from sourceView source ↗

Module documentation

Exactness of continuous degree-one inflation and restriction

For an open normal subgroup U, continuous mod-p characters of G / U inflate to continuous characters of G. Their range is exactly the kernel of restriction to U.

Imports3
Imported by2

Declarations

instance

continuousH1InflationZModAddCommGroup

L32 ↗
ClassFieldTower.Cohomology.continuousH1InflationZModAddCommGroup
Source context 8 commands

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

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

continuousH1InflationModule

L35 ↗
ClassFieldTower.Cohomology.continuousH1InflationModule
Source context 9 commands

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

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

continuousH1InflationAddHom

L41 ↗
ClassFieldTower.Cohomology.continuousH1InflationAddHom
Documentation

Pull a continuous degree-one character on G / U back along the quotient projection.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1InflationZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousH1InflationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def continuousH1InflationAddHom
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    ContinuousH1ZMod (p := p) (G := G ⧸ (U.1 : Subgroup G)) →+
      ContinuousH1ZMod (p := p) (G := G) where
  toFun chi := h1OfCharacter
    ((characterOfH1 chi).comp (OpenNormalSubgroupInClass.quotientProj U))
  map_zero' := by
    ext g
    rfl
  map_add' := by
    intro chi psi
    ext g
    rfl
def

continuousH1InflationLinearMap

L56 ↗
ClassFieldTower.Cohomology.continuousH1InflationLinearMap
Documentation

Continuous degree-one inflation as a ZMod p-linear map.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1InflationZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousH1InflationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1InflationLinearMap
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    ContinuousH1ZMod (p := p) (G := G ⧸ (U.1 : Subgroup G)) →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := G)
theorem

continuousH1InflationLinearMap_apply

L63 ↗
ClassFieldTower.Cohomology.continuousH1InflationLinearMap_apply
Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1InflationZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousH1InflationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1InflationLinearMap_apply
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : ContinuousH1ZMod (p := p) (G := G ⧸ (U.1 : Subgroup G)))
    (g : G) :
    continuousH1InflationLinearMap U chi (Additive.ofMul g) =
      chi (Additive.ofMul (OpenNormalSubgroupInClass.quotientProj U g))
theorem

continuousH1InflationLinearMap_zero

L74 ↗
ClassFieldTower.Cohomology.continuousH1InflationLinearMap_zero
Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1InflationZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousH1InflationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1InflationLinearMap_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    continuousH1InflationLinearMap U 0 = 0
theorem

continuousH1InflationLinearMap_injective

L80 ↗
ClassFieldTower.Cohomology.continuousH1InflationLinearMap_injective
Documentation

Degree-one inflation is injective because the quotient projection is surjective.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1InflationZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousH1InflationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1InflationLinearMap_injective
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    Function.Injective (continuousH1InflationLinearMap U)
theorem

continuousCharacterRestriction_continuousH1Inflation_eq_zero

L94 ↗
ClassFieldTower.Cohomology.continuousCharacterRestriction_continuousH1Inflation_eq_zero
Documentation

Inflated degree-one characters restrict trivially to the kernel of the quotient map.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1InflationZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousH1InflationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousCharacterRestriction_continuousH1Inflation_eq_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : ContinuousH1ZMod (p := p) (G := G ⧸ (U.1 : Subgroup G))) :
    continuousCharacterRestrictionLinearMap U
        (continuousH1InflationLinearMap U chi) = 0
theorem

continuousH1Inflation_range_eq_characterRestriction_ker

L109 ↗
ClassFieldTower.Cohomology.continuousH1Inflation_range_eq_characterRestriction_ker
Documentation

The continuous degree-one inflation--restriction sequence is exact at ambient characters.

Source context 10 commands

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

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

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