Module

AbsoluteMuPTrivialization.lean

Nyll.GaloisCohomology.Kummer.AbsoluteMuPTrivialization

5 declarations indexed from sourceView source ↗

Module documentation

Trivializing natural `mu_p` coefficients over a cyclotomic base

When the base field contains a primitive p-th root of unity, the natural absolute-Galois action on mu_p is trivial. A chosen primitive root gives a continuous ZMod p-linear equivalence with the standard trivial coefficient line and hence an isomorphism of topological representations.

Imports3

Imported by3

theorem

absoluteMuPAction_eq_self_of_primitiveRoots

L35 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPAction_eq_self_of_primitiveRoots

Documentation

The natural Galois action on mu_p is trivial when the base field already contains a primitive p-th root.

Source context 8 commands

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

open CategoryTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ContRepresentation KummerTheory TopRep
variable (K : Type) [Field K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteMuPAction_eq_self_of_primitiveRoots
    (hmu : (primitiveRoots p K).Nonempty)
    (sigma : Field.absoluteGaloisGroup K) (x : AbsoluteMuP K p) :
    absoluteMuPActionContinuousLinearMap K p sigma x = x

def

absoluteMuPMulEquivMultiplicativeZMod

L52 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPMulEquivMultiplicativeZMod

Documentation

The coefficient equivalence from roots of unity in the algebraic closure to the multiplicative copy of ZMod p, using the supplied primitive root.

Source context 8 commands

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

open CategoryTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ContRepresentation KummerTheory TopRep
variable (K : Type) [Field K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def absoluteMuPMulEquivMultiplicativeZMod
    (hmu : (primitiveRoots p K).Nonempty) :
    DiscreteNthRootsSubgroup (AlgebraicClosure K) p ≃*
      Multiplicative (ZMod p)

def

absoluteMuPLinearEquivZMod

L70 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPLinearEquivZMod

Documentation

Additive roots of unity are linearly equivalent to the standard ZMod p coefficient line.

Source context 8 commands

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

open CategoryTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ContRepresentation KummerTheory TopRep
variable (K : Type) [Field K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def absoluteMuPLinearEquivZMod
    (hmu : (primitiveRoots p K).Nonempty) :
    AbsoluteMuP K p ≃ₗ[ZMod p] ZMod p

def

absoluteMuPContinuousLinearEquivZMod

L90 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPContinuousLinearEquivZMod

Documentation

The coefficient trivialization is a homeomorphism because both coefficient spaces are discrete.

Source context 8 commands

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

open CategoryTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ContRepresentation KummerTheory TopRep
variable (K : Type) [Field K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def absoluteMuPContinuousLinearEquivZMod
    (hmu : (primitiveRoots p K).Nonempty) :
    AbsoluteMuP K p ≃L[ZMod p] ZMod p

def

absoluteMuPTopRepTrivialIso

L99 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPTopRepTrivialIso

Documentation

Over a field containing mu_p, the natural coefficient representation is isomorphic to the standard trivial ZMod p representation.

Source context 8 commands

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

open CategoryTheory
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ContRepresentation KummerTheory TopRep
variable (K : Type) [Field K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def absoluteMuPTopRepTrivialIso
    (hmu : (primitiveRoots p K).Nonempty) :
    absoluteMuPTopRep K p ≅
      trivialZModP p (Field.absoluteGaloisGroup K)

Module documentation

Trivializing natural mu_p coefficients over a cyclotomic base

Declarations

absoluteMuPAction_eq_self_of_primitiveRoots

absoluteMuPMulEquivMultiplicativeZMod

absoluteMuPLinearEquivZMod

absoluteMuPContinuousLinearEquivZMod

absoluteMuPTopRepTrivialIso

Trivializing natural `mu_p` coefficients over a cyclotomic base