Module

FiniteTransgressionExact.lean

Nyll.GaloisCohomology.ProP.FiniteTransgressionExact

8 declarations indexed from sourceView source ↗

Module documentation

Exactness of finite transgression

Restriction of an ambient mod-p character to a normal subgroup is conjugation invariant. This file proves the missing converse to the finite transgression kernel theorem: an invariant character has zero factor-set class exactly when it is such a restriction.

Imports2

Imported by4

instance

exactQuotientTopology

L32 ↗

ClassFieldTower.Cohomology.exactQuotientTopology

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]

Lean source · statement

instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N)

instance

exactQuotientDiscrete

L33 ↗

ClassFieldTower.Cohomology.exactQuotientDiscrete

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥

Lean source · statement

instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N)

def

finiteCharacterRestrictionAddHom

L37 ↗

ClassFieldTower.Cohomology.finiteCharacterRestrictionAddHom

Documentation

Restriction of finite ambient characters to invariant subgroup characters.

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 ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _

Lean source · full declaration

def finiteCharacterRestrictionAddHom (N : Subgroup P) [N.Normal] :
    FiniteCharacter p P →+ InvariantFiniteCharacter (p := p) N where
  toFun ψ := ⟨Additive.ofMul (ψ.toMul.comp N.subtype), by
    intro g n
    change ψ.toMul (g * n.1 * g⁻¹) = ψ.toMul n.1
    simp only [map_mul, map_inv]
    calc
      ψ.toMul g * ψ.toMul n.1 * (ψ.toMul g)⁻¹ =
          ψ.toMul n.1 * (ψ.toMul g * (ψ.toMul g)⁻¹) := by ac_rfl
      _ = ψ.toMul n.1 := by simp⟩
  map_zero' := by
    apply Subtype.ext
    rfl
  map_add' ψ φ := by
    apply Subtype.ext
    rfl

def

finiteCharacterRestrictionLinearMap

L55 ↗

ClassFieldTower.Cohomology.finiteCharacterRestrictionLinearMap

Documentation

Linear restriction from ambient characters to invariant subgroup characters.

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 ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _

Lean source · statement

def finiteCharacterRestrictionLinearMap
    (N : Subgroup P) [N.Normal] :
    FiniteCharacter p P →ₗ[ZMod p] InvariantFiniteCharacter (p := p) N

theorem

transgressionFactor_eq_extension_coboundary

L61 ↗

ClassFieldTower.Cohomology.transgressionFactor_eq_extension_coboundary

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 ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
omit [Fact p.Prime] in

Lean source · statement

theorem transgressionFactor_eq_extension_coboundary
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (ψ : MonoidHom P (Multiplicative (ZMod p)))
    (hψ : ψ.comp N.subtype = χ)
    (q r : P ⧸ N) :
    transgressionFactor N χ q r =
      (ψ (Quotient.out q)).toAdd + (ψ (Quotient.out r)).toAdd -
        (ψ (Quotient.out (q * r))).toAdd

theorem

transgressionFactor_one_one_eq_extension_value

L83 ↗

ClassFieldTower.Cohomology.transgressionFactor_one_one_eq_extension_value

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 ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
omit [Fact p.Prime] in

Lean source · statement

theorem transgressionFactor_one_one_eq_extension_value
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (ψ : MonoidHom P (Multiplicative (ZMod p)))
    (hψ : ψ.comp N.subtype = χ) :
    transgressionFactor N χ 1 1 = (ψ (Quotient.out (1 : P ⧸ N))).toAdd

theorem

finiteTransgressionLinearMap_eq_zero_of_extendsToAmbient

L94 ↗

ClassFieldTower.Cohomology.finiteTransgressionLinearMap_eq_zero_of_extendsToAmbient

Documentation

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

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 ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
omit [Fact p.Prime] in

Lean source · statement

theorem finiteTransgressionLinearMap_eq_zero_of_extendsToAmbient
    (N : Subgroup P) [N.Normal] [Finite (P ⧸ N)]
    (χ : InvariantFiniteCharacter (p := p) N)
    (hχ : InvariantFiniteCharacter.ExtendsToAmbient N χ) :
    finiteTransgressionLinearMap N χ = 0

theorem

finiteCharacterRestriction_range_eq_transgression_ker

L163 ↗

ClassFieldTower.Cohomology.finiteCharacterRestriction_range_eq_transgression_ker

Documentation

Exact kernel statement for finite transgression.

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 ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {P : Type u} [Group P]
local instance exactQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance exactQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
omit [Fact p.Prime] in

Lean source · statement

theorem finiteCharacterRestriction_range_eq_transgression_ker
    (N : Subgroup P) [N.Normal] [Finite (P ⧸ N)] :
    LinearMap.range (finiteCharacterRestrictionLinearMap (p := p) N) =
      LinearMap.ker (finiteTransgressionLinearMap (p := p) N)

Module documentation

Exactness of finite transgression

Declarations