Module

FiniteStageTransgressionQuotient.lean

Nyll.GaloisCohomology.ProP.FiniteStageTransgressionQuotient

6 declarations indexed from sourceView source ↗

Module documentation

Quotient presentation of finite-stage transgression

At a finite quotient stage, invariant characters modulo restrictions of continuous degree-one characters identify with the range of finite transgression.

Imports2

Imported by1

Nyll.GaloisCohomology.ProP.All

instance

finiteStageQuotientZModTopology

L30 ↗

ClassFieldTower.ProP.finiteStageQuotientZModTopology

Source context 8 commands

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

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]

Lean source · statement

instance finiteStageQuotientZModTopology : TopologicalSpace (ZMod p)

instance

finiteStageQuotientZModDiscrete

L31 ↗

ClassFieldTower.ProP.finiteStageQuotientZModDiscrete

Source context 9 commands

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

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]
local instance finiteStageQuotientZModTopology : TopologicalSpace (ZMod p) := ⊥

Lean source · statement

instance finiteStageQuotientZModDiscrete : DiscreteTopology (ZMod p)

instance

finiteStageQuotientContinuousH1Module

L34 ↗

ClassFieldTower.ProP.finiteStageQuotientContinuousH1Module

Source context 10 commands

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

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]
local instance finiteStageQuotientZModTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteStageQuotientZModDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _

Lean source · statement

instance finiteStageQuotientContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F)))

def

finiteStageContinuousCharacterQuotientEquivTransgressionRange

L42 ↗

ClassFieldTower.ProP.finiteStageContinuousCharacterQuotientEquivTransgressionRange

Documentation

Invariant finite-stage characters modulo continuous ambient restrictions are linearly equivalent to the finite-transgression range.

Source context 11 commands

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

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]
local instance finiteStageQuotientZModTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteStageQuotientZModDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteStageQuotientContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule

Lean source · statement

def finiteStageContinuousCharacterQuotientEquivTransgressionRange
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    (InvariantFiniteCharacter (p := p) (finiteStageImage R U) ⧸
        LinearMap.range (finiteStageContinuousCharacterRestrictionLinearMap R U)) ≃ₗ[ZMod p]
      LinearMap.range
        (finiteTransgressionLinearMap (p := p) (finiteStageImage R U))

theorem

finiteStageContinuousCharacterQuotientEquivTransgressionRange_apply_mk

L56 ↗

ClassFieldTower.ProP.finiteStageContinuousCharacterQuotientEquivTransgressionRange_apply_mk

Source context 11 commands

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

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]
local instance finiteStageQuotientZModTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteStageQuotientZModDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteStageQuotientContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule

Lean source · statement

theorem finiteStageContinuousCharacterQuotientEquivTransgressionRange_apply_mk
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χ : InvariantFiniteCharacter (p := p) (finiteStageImage R U)) :
    finiteStageContinuousCharacterQuotientEquivTransgressionRange R U
        (Submodule.Quotient.mk χ) =
      ⟨finiteTransgressionLinearMap (finiteStageImage R U) χ,
        LinearMap.mem_range_self
          (finiteTransgressionLinearMap (finiteStageImage R U)) χ⟩

theorem

finrank_finiteStageContinuousCharacterQuotient_eq_transgressionRange

L69 ↗

ClassFieldTower.ProP.finrank_finiteStageContinuousCharacterQuotient_eq_transgressionRange

Documentation

The continuous-character quotient and the finite-stage transgression range have equal ZMod p-dimension.

Source context 11 commands

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

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]
local instance finiteStageQuotientZModTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteStageQuotientZModDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteStageQuotientContinuousH1Module
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module (ZMod p)
      (ContinuousH1ZMod (p := p) (G := F ⧸ (U.1 : Subgroup F))) :=
  continuousH1ZModModule

Lean source · statement

theorem finrank_finiteStageContinuousCharacterQuotient_eq_transgressionRange
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Module.finrank (ZMod p)
        (InvariantFiniteCharacter (p := p) (finiteStageImage R U) ⧸
          LinearMap.range (finiteStageContinuousCharacterRestrictionLinearMap R U)) =
      Module.finrank (ZMod p)
        (LinearMap.range
          (finiteTransgressionLinearMap (p := p) (finiteStageImage R U)))

Module documentation

Quotient presentation of finite-stage transgression

Declarations

finiteStageQuotientZModTopology

finiteStageQuotientZModDiscrete

finiteStageQuotientContinuousH1Module

finiteStageContinuousCharacterQuotientEquivTransgressionRange

finiteStageContinuousCharacterQuotientEquivTransgressionRange_apply_mk

finrank_finiteStageContinuousCharacterQuotient_eq_transgressionRange