Module

FiniteTransgressionQuotient.lean

Nyll.GaloisCohomology.ProP.FiniteTransgressionQuotient

3 declarations indexed from sourceView source ↗

Module documentation

Quotient presentation of finite transgression

The exact kernel calculation for finite transgression identifies invariant characters modulo ambient restrictions with the range of finite transgression.

Imports2

Nyll.GaloisCohomology.ProP.FiniteTransgressionExact
Mathlib.LinearAlgebra.Isomorphisms

Imported by2

def

finiteTransgressionQuotientEquivRange

L30 ↗

ClassFieldTower.Cohomology.finiteTransgressionQuotientEquivRange

Documentation

The first isomorphism theorem for finite transgression, with its kernel rewritten as the range of ambient character restriction.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]

Lean source · statement

def finiteTransgressionQuotientEquivRange
    (N : Subgroup P) [N.Normal] [Finite (P ⧸ N)] :
    (InvariantFiniteCharacter (p := p) N ⧸
        LinearMap.range (finiteCharacterRestrictionLinearMap (p := p) N)) ≃ₗ[ZMod p]
      LinearMap.range (finiteTransgressionLinearMap (p := p) N)

theorem

finiteTransgressionQuotientEquivRange_apply_mk

L40 ↗

ClassFieldTower.Cohomology.finiteTransgressionQuotientEquivRange_apply_mk

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]

Lean source · statement

theorem finiteTransgressionQuotientEquivRange_apply_mk
    (N : Subgroup P) [N.Normal] [Finite (P ⧸ N)]
    (χ : InvariantFiniteCharacter (p := p) N) :
    finiteTransgressionQuotientEquivRange (p := p) N
        (Submodule.Quotient.mk χ) =
      ⟨finiteTransgressionLinearMap N χ,
        LinearMap.mem_range_self (finiteTransgressionLinearMap N) χ⟩

theorem

finrank_finiteTransgressionCharacterQuotient_eq_range

L51 ↗

ClassFieldTower.Cohomology.finrank_finiteTransgressionCharacterQuotient_eq_range

Documentation

The quotient by ambient restrictions and the finite-transgression range have equal ZMod p-dimension.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]

Lean source · statement

theorem finrank_finiteTransgressionCharacterQuotient_eq_range
    (N : Subgroup P) [N.Normal] [Finite (P ⧸ N)] :
    Module.finrank (ZMod p)
        (InvariantFiniteCharacter (p := p) N ⧸
          LinearMap.range (finiteCharacterRestrictionLinearMap (p := p) N)) =
      Module.finrank (ZMod p)
        (LinearMap.range (finiteTransgressionLinearMap (p := p) N))

Module documentation

Quotient presentation of finite transgression

Declarations

finiteTransgressionQuotientEquivRange

finiteTransgressionQuotientEquivRange_apply_mk

finrank_finiteTransgressionCharacterQuotient_eq_range