Module

FiniteKummerMuPCoefficients.lean

Nyll.GaloisCohomology.Kummer.FiniteKummerMuPCoefficients

3 declarations indexed from sourceView source ↗

Module documentation

Coherence of finite Kummer and absolute roots-of-unity coefficients

The finite chosen-root homomorphism and the existing absolute mu_p trivialization use the same supplied primitive root. Their values therefore agree in the algebraic closure. The finite coefficient homomorphism is also natural under field embeddings; its p-th-power property is supplied by the shared finite coefficient module. These identities supply the coefficient comparison for absolute lifts; none is assumed as an extra input.

Imports2

Imported by3

theorem

absoluteMuPLinearEquivZMod_symm_coe_intCast

L31 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPLinearEquivZMod_symm_coe_intCast

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type) [Field K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]

Lean source · statement

theorem absoluteMuPLinearEquivZMod_symm_coe_intCast
    (hmu : (primitiveRoots p K).Nonempty) (i : ℤ) :
    ((absoluteMuPLinearEquivZMod K p hmu).symm (i : ZMod p)).toMul.1 =
      (finiteKummerCoefficientAddHom K (AlgebraicClosure K)
        p hmu (ULift.up.{0} (i : ZMod p))).toMul

theorem

absoluteMuPLinearEquivZMod_symm_coe

L55 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteMuPLinearEquivZMod_symm_coe

Documentation

The inverse absolute trivialization has exactly the finite Kummer coefficient value in the algebraic closure.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type) [Field K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]

Lean source · statement

theorem absoluteMuPLinearEquivZMod_symm_coe
    (hmu : (primitiveRoots p K).Nonempty) (z : ZMod p) :
    ((absoluteMuPLinearEquivZMod K p hmu).symm z).toMul.1 =
      (finiteKummerCoefficientAddHom K (AlgebraicClosure K)
        p hmu (ULift.up.{0} z)).toMul

theorem

finiteKummerCoefficientAddHom_map

L65 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientAddHom_map

Documentation

The chosen-root coefficient homomorphism commutes with field embeddings.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type) [Field K]
variable (p : ℕ+) [Fact (p : ℕ).Prime]
omit [Fact (p : ℕ).Prime] in

Lean source · statement

theorem finiteKummerCoefficientAddHom_map
    {L M : Type} [Field L] [Field M] [Algebra K L] [Algebra K M]
    (f : L →ₐ[K] M) (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : ULift.{0} (ZMod (p : ℕ))) :
    Units.map f (finiteKummerCoefficientAddHom K L p hmu z).toMul =
      (finiteKummerCoefficientAddHom K M p hmu z).toMul

Module documentation

Coherence of finite Kummer and absolute roots-of-unity coefficients

Declarations

absoluteMuPLinearEquivZMod_symm_coe_intCast

absoluteMuPLinearEquivZMod_symm_coe

finiteKummerCoefficientAddHom_map