NYLL
Module

IdealPowerRadicalSelmer.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadicalSelmer
11 declarations indexed from sourceView source ↗

Module documentation

The empty-support Selmer interpretation of the ideal-power radical

This file identifies the ideal-power condition on a principal fractional ideal with the empty-support Selmer condition on its Kummer class.

Imports2
Imported by3

Declarations

theorem

count_toPrincipalIdeal_eq_neg_valuationOfNeZero

L28 ↗
ClassFieldTower.Martinet.Shafarevich.count_toPrincipalIdeal_eq_neg_valuationOfNeZero
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem count_toPrincipalIdeal_eq_neg_valuationOfNeZero
    (a : Kˣ) (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdeal.count K v
        ((toPrincipalIdeal (𝓞 K) K a : FractionalIdealGroup K) :
          FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      -(v.valuationOfNeZero a).toAdd
theorem

valuationOfNeZeroMod_mk_eq_one_iff

L46 ↗
ClassFieldTower.Martinet.Shafarevich.valuationOfNeZeroMod_mk_eq_one_iff
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem valuationOfNeZeroMod_mk_eq_one_iff
    (n : ℕ+) (a : Kˣ) (v : HeightOneSpectrum (𝓞 K)) :
    v.valuationOfNeZeroMod (n : ℕ)
        (QuotientGroup.mk'
          (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a) = 1 ↔
      (n : ℤ) ∣ (v.valuationOfNeZero a).toAdd
theorem

mem_idealNthPowerRadicalKummerSubgroup_iff_valuation

L61 ↗
ClassFieldTower.Martinet.Shafarevich.mem_idealNthPowerRadicalKummerSubgroup_iff_valuation
Documentation

A field unit lies in the ideal-power radical exactly when all finite valuations are divisible by the exponent.

Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem mem_idealNthPowerRadicalKummerSubgroup_iff_valuation
    (n : ℕ+) (a : Kˣ) :
    a ∈ (idealNthPowerRadicalKummerSubgroup K n).1 ↔
      ∀ v : HeightOneSpectrum (𝓞 K),
        (n : ℤ) ∣ (v.valuationOfNeZero a).toAdd
abbrev

EmptySupportSelmerGroup

L108 ↗
ClassFieldTower.Martinet.Shafarevich.EmptySupportSelmerGroup
Documentation

The empty-support Selmer group, with all finite valuations constrained.

Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
abbrev EmptySupportSelmerGroup (n : ℕ+)
def

idealRadicalRepresentativeToEmptySelmer

L113 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalRepresentativeToEmptySelmer
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · full declaration
def idealRadicalRepresentativeToEmptySelmer
    (n : ℕ+) :
    (idealNthPowerRadicalKummerSubgroup K n).1 →*
      EmptySupportSelmerGroup K n where
  toFun a := ⟨QuotientGroup.mk'
      (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a.1, by
    intro v _
    exact (valuationOfNeZeroMod_mk_eq_one_iff K n a.1 v).2
      ((mem_idealNthPowerRadicalKummerSubgroup_iff_valuation
        K n a.1).1 a.property v)⟩
  map_one' := by
    apply Subtype.ext
    exact map_one _
  map_mul' a b := by
    apply Subtype.ext
    exact map_mul
      (QuotientGroup.mk'
        (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) a.1 b.1
theorem

restrictedNthPowers_le_ker_representativeToEmptySelmer

L132 ↗
ClassFieldTower.Martinet.Shafarevich.restrictedNthPowers_le_ker_representativeToEmptySelmer
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem restrictedNthPowers_le_ker_representativeToEmptySelmer
    (n : ℕ+) :
    restrictedNthPowersSubgroup n
        (idealNthPowerRadicalKummerSubgroup K n) ≤
      MonoidHom.ker (idealRadicalRepresentativeToEmptySelmer K n)
def

idealNthPowerRadicalQuotientToEmptySelmer

L148 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToEmptySelmer
Documentation

The canonical comparison from the ideal-power radical quotient to the empty-support Selmer group.

Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def idealNthPowerRadicalQuotientToEmptySelmer
    (n : ℕ+) :
    IdealNthPowerRadicalQuotient K n →*
      EmptySupportSelmerGroup K n
theorem

idealNthPowerRadicalQuotientToEmptySelmer_mk

L158 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToEmptySelmer_mk
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem idealNthPowerRadicalQuotientToEmptySelmer_mk
    (n : ℕ+)
    (a : (idealNthPowerRadicalKummerSubgroup K n).1) :
    idealNthPowerRadicalQuotientToEmptySelmer K n
        (restrictedRadicalQuotientMk n
          (idealNthPowerRadicalKummerSubgroup K n) a) =
      idealRadicalRepresentativeToEmptySelmer K n a
theorem

idealNthPowerRadicalQuotientToEmptySelmer_injective

L170 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToEmptySelmer_injective
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem idealNthPowerRadicalQuotientToEmptySelmer_injective
    (n : ℕ+) :
    Function.Injective
      (idealNthPowerRadicalQuotientToEmptySelmer K n)
theorem

idealNthPowerRadicalQuotientToEmptySelmer_surjective

L194 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToEmptySelmer_surjective
Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem idealNthPowerRadicalQuotientToEmptySelmer_surjective
    (n : ℕ+) :
    Function.Surjective
      (idealNthPowerRadicalQuotientToEmptySelmer K n)
def

idealNthPowerRadicalQuotientEquivEmptySelmer

L216 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientEquivEmptySelmer
Documentation

The ideal-power radical quotient is canonically the empty-support Selmer group.

Source context 6 commands

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

open scoped NumberField nonZeroDivisors WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def idealNthPowerRadicalQuotientEquivEmptySelmer
    (n : ℕ+) :
    IdealNthPowerRadicalQuotient K n ≃*
      EmptySupportSelmerGroup K n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.