Module

IdealRadicalCyclotomicDualDescent.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealRadicalCyclotomicDualDescent

5 declarations indexed from sourceView source ↗

Module documentation

Descent from the cyclotomic ideal-radical dual

The restricted ideal radical over the chosen cyclotomic base is a quotient of the base-field ideal radical. Its dual therefore embeds canonically into the base-field radical dual. This file applies that embedding functorially to an entire space of linear maps with fixed source.

In particular, a linear map constructed first with cyclotomic target can be descended without changing its kernel. Thus injectivity at the cyclotomic stage is exactly injectivity after descent to the target used in the final Shafarevich bound.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealRadicalCyclotomicModule

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.All

def

idealRadicalCyclotomicDualDescent

L38 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualDescent

Documentation

Postcomposition with the canonical cyclotomic-dual injection, linear in the input map. This is the descent endpoint for maps whose source is fixed and whose initial target is the restricted cyclotomic ideal-radical dual.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
universe u
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (M : Type u) [AddCommGroup M] [Module (ZMod p) M]

Lean source · statement

def idealRadicalCyclotomicDualDescent :
    (M →ₗ[ZMod p]
        Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p)) →ₗ[ZMod p]
      (M →ₗ[ZMod p]
        Module.Dual (ZMod p) (idealPowerRadicalModP F p))

theorem

idealRadicalCyclotomicDualDescent_apply

L46 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualDescent_apply

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
universe u
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (M : Type u) [AddCommGroup M] [Module (ZMod p) M]

Lean source · statement

theorem idealRadicalCyclotomicDualDescent_apply
    (f : M →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p))
    (x : M) :
    idealRadicalCyclotomicDualDescent F p M f x =
      idealRadicalCyclotomicDualInjection F p (f x)

theorem

idealRadicalCyclotomicDualDescent_injective

L55 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualDescent_injective

Documentation

Descent is faithful on the whole space of maps with a fixed source.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
universe u
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (M : Type u) [AddCommGroup M] [Module (ZMod p) M]

Lean source · statement

theorem idealRadicalCyclotomicDualDescent_injective :
    Function.Injective (idealRadicalCyclotomicDualDescent F p M)

theorem

idealRadicalCyclotomicDualDescent_ker

L65 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualDescent_ker

Documentation

Postcomposition with cyclotomic descent does not change the kernel of the input map.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
universe u
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (M : Type u) [AddCommGroup M] [Module (ZMod p) M]

Lean source · statement

theorem idealRadicalCyclotomicDualDescent_ker
    (f : M →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p)) :
    LinearMap.ker (idealRadicalCyclotomicDualDescent F p M f) =
      LinearMap.ker f

theorem

idealRadicalCyclotomicDualDescent_apply_injective_iff

L82 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualDescent_apply_injective_iff

Documentation

A map into the cyclotomic radical dual is injective exactly when its canonical descent to the base-field radical dual is injective.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
universe u
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (M : Type u) [AddCommGroup M] [Module (ZMod p) M]

Lean source · statement

theorem idealRadicalCyclotomicDualDescent_apply_injective_iff
    (f : M →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p)) :
    Function.Injective (idealRadicalCyclotomicDualDescent F p M f) ↔
      Function.Injective f

Module documentation

Descent from the cyclotomic ideal-radical dual

Declarations

idealRadicalCyclotomicDualDescent

idealRadicalCyclotomicDualDescent_apply

idealRadicalCyclotomicDualDescent_injective

idealRadicalCyclotomicDualDescent_ker

idealRadicalCyclotomicDualDescent_apply_injective_iff