Module

FiniteRootIdeleSupport.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteRootIdeleSupport

5 declarations indexed from sourceView source ↗

Module documentation

Root-of-unity coefficients are integral at every finite place

A torsion field unit has valuation one at every finite place. Its principal relative idele therefore lies in the actual empty-support subgroup. This gives the supported coefficient map needed to apply the unramified local-to-global primitive construction.

Imports2

Imported by3

theorem

principalIdele_mem_emptySupport_of_pow_eq_one

L30 ↗

ClassFieldTower.Martinet.Shafarevich.principalIdele_mem_emptySupport_of_pow_eq_one

Documentation

A torsion field unit gives a principal idele integral at every finite place.

Source context 6 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]

Lean source · statement

theorem principalIdele_mem_emptySupport_of_pow_eq_one
    (n : ℕ) (hn : n ≠ 0) (x : Lˣ) (hx : x ^ n = 1) :
    RelativeIdeleGroup.principalIdele K L x ∈
      relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅

theorem

finiteKummerCoefficient_principalIdele_mem_emptySupport

L45 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficient_principalIdele_mem_emptySupport

Documentation

The actual principal idele of a Kummer coefficient has empty finite support.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
variable (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficient_principalIdele_mem_emptySupport
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : ULift (ZMod (p : ℕ))) :
    RelativeIdeleGroup.principalIdele K L
        (finiteKummerCoefficientAddHom K L p hmu z).toMul ∈
      relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅

def

finiteKummerSupportedIdeleAddHom

L55 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSupportedIdeleAddHom

Documentation

Finite Kummer coefficients mapped into the actual empty-support idele subgroup.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
variable (p : ℕ+)

Lean source · full declaration

def finiteKummerSupportedIdeleAddHom
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    ULift.{0} (ZMod (p : ℕ)) →+
      Additive (relativeIdeleLocalTensorDecompositionSupportedSubgroup
        (K := K) (L := L) ∅) where
  toFun z := Additive.ofMul ⟨RelativeIdeleGroup.principalIdele K L
    (finiteKummerCoefficientAddHom K L p hmu z).toMul,
    finiteKummerCoefficient_principalIdele_mem_emptySupport K L p hmu z⟩
  map_zero' := by
    apply Additive.toMul.injective
    apply Subtype.ext
    change RelativeIdeleGroup.principalIdele K L
      (finiteKummerCoefficientAddHom K L p hmu (0 : ULift.{0} (ZMod (p : ℕ)))).toMul = 1
    rw [map_zero]
    exact map_one _
  map_add' z w := by
    apply Additive.toMul.injective
    apply Subtype.ext
    change RelativeIdeleGroup.principalIdele K L
      (finiteKummerCoefficientAddHom K L p hmu (z + w)).toMul = _
    rw [map_add]
    exact map_mul _ _ _

instance

finiteRootSupportedIdeleAction

L78 ↗

ClassFieldTower.Martinet.Shafarevich.finiteRootSupportedIdeleAction

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
variable (p : ℕ+)

Lean source · statement

instance finiteRootSupportedIdeleAction : MulDistribMulAction (Gal(L/K))
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅)

def

finiteKummerSupportedIdeleRepHom

L83 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSupportedIdeleRepHom

Documentation

The supported coefficient map is equivariant for the actual Galois action.

Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
variable (p : ℕ+)
local instance finiteRootSupportedIdeleAction : MulDistribMulAction (Gal(L/K))
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) ∅

Lean source · statement

def finiteKummerSupportedIdeleRepHom
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ))) ⟶
      Rep.ofMulDistribMulAction (Gal(L/K))
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅)

Module documentation

Root-of-unity coefficients are integral at every finite place

Declarations

principalIdele_mem_emptySupport_of_pow_eq_one

finiteKummerCoefficient_principalIdele_mem_emptySupport

finiteKummerSupportedIdeleAddHom

finiteRootSupportedIdeleAction

finiteKummerSupportedIdeleRepHom