NYLL
Module

IdealPowerRadical.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadical
19 declarations indexed from sourceView source ↗

Module documentation

The empty-support Shafarevich radical

This file defines the field elements whose principal fractional ideals are positive powers, quotients them by field powers, and maps the resulting radical onto the matching torsion subgroup of the ordinary ideal class group.

Imports4
Imported by6

Declarations

def

idealNthPowerRadicalKummerSubgroup

L33 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalKummerSubgroup
Documentation

The field elements whose principal fractional ideal is an n-th power.

Source context 7 commands

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

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

mem_idealNthPowerRadicalKummerSubgroup_iff

L45 ↗
ClassFieldTower.Martinet.Shafarevich.mem_idealNthPowerRadicalKummerSubgroup_iff
Documentation

Membership in the ideal-power radical is exactly the existence of an n-th root for the principal fractional ideal.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem mem_idealNthPowerRadicalKummerSubgroup_iff
    (n : ℕ+) (a : Kˣ) :
    a ∈ (idealNthPowerRadicalKummerSubgroup K n).1 ↔
      ∃ I : FractionalIdealGroup K,
        I ^ (n : ℕ) = toPrincipalIdeal (𝓞 K) K a
abbrev

IdealNthPowerRadicalQuotient

L53 ↗
ClassFieldTower.Martinet.Shafarevich.IdealNthPowerRadicalQuotient
Documentation

The empty-support Shafarevich radical V_{K,n}/K×^n.

Source context 7 commands

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

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

fractionalIdealGroup_pow_injective

L56 ↗
ClassFieldTower.Martinet.Shafarevich.fractionalIdealGroup_pow_injective
Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · full declaration
theorem fractionalIdealGroup_pow_injective (n : ℕ+) :
    Function.Injective
      (fun I : FractionalIdealGroup K ↦ I ^ (n : ℕ)) := by
  intro I J hIJ
  apply FractionalIdealGroup.ext_count
  intro v
  have hcount := congrArg
    (fun L : FractionalIdealGroup K ↦
      FractionalIdeal.count K v
        (L : FractionalIdeal (nonZeroDivisors (𝓞 K)) K)) hIJ
  have hcount' :
      FractionalIdeal.count K v
          ((I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) ^ (n : ℕ)) =
        FractionalIdeal.count K v
          ((J : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) ^ (n : ℕ)) := by
    simpa only [Units.val_pow_eq_pow_val] using hcount
  rw [FractionalIdeal.count_pow, FractionalIdeal.count_pow] at hcount'
  exact mul_left_cancel₀ (by exact_mod_cast n.ne_zero) hcount'
def

idealNthRoot

L77 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRoot
Documentation

The unique fractional-ideal n-th root of a radical element's principal ideal.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def idealNthRoot
    (n : ℕ+)
    (a : (idealNthPowerRadicalKummerSubgroup K n).1) :
    FractionalIdealGroup K
theorem

idealNthRoot_pow

L85 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRoot_pow
Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem idealNthRoot_pow
    (n : ℕ+)
    (a : (idealNthPowerRadicalKummerSubgroup K n).1) :
    idealNthRoot K n a ^ (n : ℕ) =
      toPrincipalIdeal (𝓞 K) K a.1
theorem

idealNthRoot_eq_of_pow_eq

L95 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRoot_eq_of_pow_eq
Documentation

The chosen ideal root agrees with any ideal having the required power.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem idealNthRoot_eq_of_pow_eq
    (n : ℕ+)
    (a : (idealNthPowerRadicalKummerSubgroup K n).1)
    (I : FractionalIdealGroup K)
    (hI : I ^ (n : ℕ) = toPrincipalIdeal (𝓞 K) K a.1) :
    idealNthRoot K n a = I
def

idealNthRootHom

L106 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRootHom
Documentation

Taking the unique ideal root is multiplicative.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · full declaration
def idealNthRootHom (n : ℕ+) :
    (idealNthPowerRadicalKummerSubgroup K n).1 →*
      FractionalIdealGroup K where
  toFun := idealNthRoot K n
  map_one' := by
    apply idealNthRoot_eq_of_pow_eq K n 1 1
    simp
  map_mul' a b := by
    apply idealNthRoot_eq_of_pow_eq K n (a * b)
      (idealNthRoot K n a * idealNthRoot K n b)
    rw [mul_pow, idealNthRoot_pow K n a, idealNthRoot_pow K n b]
    change
      toPrincipalIdeal (𝓞 K) K a.1 *
          toPrincipalIdeal (𝓞 K) K b.1 =
        toPrincipalIdeal (𝓞 K) K (a.1 * b.1)
    exact (map_mul (toPrincipalIdeal (𝓞 K) K) a.1 b.1).symm
abbrev

ClassGroupNthPowerTorsion

L124 ↗
ClassFieldTower.Martinet.Shafarevich.ClassGroupNthPowerTorsion
Documentation

The n-torsion subgroup of the ordinary ideal class group.

Source context 7 commands

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

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

pClassPowerSubgroup_eq_nthPowerRange

L130 ↗
ClassFieldTower.Martinet.Shafarevich.pClassPowerSubgroup_eq_nthPowerRange
Documentation

For the abelian ideal class group, the subgroup generated by n-th powers is exactly the range of the power endomorphism.

Source context 8 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem pClassPowerSubgroup_eq_nthPowerRange (n : ℕ) :
    pClassPowerSubgroup K n =
      (powMonoidHom n : ClassGroup (𝓞 K) →* ClassGroup (𝓞 K)).range
def

pClassGroupEquivNthPowerQuotient

L143 ↗
ClassFieldTower.Martinet.Shafarevich.pClassGroupEquivNthPowerQuotient
Documentation

The n-class quotient is the cokernel of the class-group power map.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def pClassGroupEquivNthPowerQuotient (n : ℕ) :
    PClassGroup K n ≃*
      ClassGroup (𝓞 K) ⧸
        (powMonoidHom n : ClassGroup (𝓞 K) →*
          ClassGroup (𝓞 K)).range
theorem

card_classGroupNthPowerTorsion_eq_card_pClassGroup

L154 ↗
ClassFieldTower.Martinet.Shafarevich.card_classGroupNthPowerTorsion_eq_card_pClassGroup
Documentation

The class-group n-torsion and the n-class quotient have equal cardinality. This avoids asserting a nonexistent canonical map between them.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem card_classGroupNthPowerTorsion_eq_card_pClassGroup (n : ℕ) :
    Nat.card (ClassGroupNthPowerTorsion K n) =
      Nat.card (PClassGroup K n)
def

idealNthRootClassHom

L163 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRootClassHom
Documentation

Send a radical element to the class of the unique ideal root of its principal ideal.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def idealNthRootClassHom (n : ℕ+) :
    (idealNthPowerRadicalKummerSubgroup K n).1 →*
      ClassGroup (𝓞 K)
theorem

idealNthRootClassHom_mem_torsion

L169 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRootClassHom_mem_torsion
Documentation

The ideal-root class is killed by n.

Source context 7 commands

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

open scoped NumberField nonZeroDivisors
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem idealNthRootClassHom_mem_torsion
    (n : ℕ+)
    (a : (idealNthPowerRadicalKummerSubgroup K n).1) :
    idealNthRootClassHom K n a ∈ ClassGroupNthPowerTorsion K (n : ℕ)
def

idealNthRootClassTorsionHom

L180 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthRootClassTorsionHom
Documentation

The ideal-root class map with codomain restricted to class-group n-torsion.

Source context 7 commands

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

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

restrictedNthPowers_le_ker_idealNthRootClassTorsionHom

L187 ↗
ClassFieldTower.Martinet.Shafarevich.restrictedNthPowers_le_ker_idealNthRootClassTorsionHom
Source context 7 commands

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

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

idealNthPowerRadicalToClassTorsion

L204 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalToClassTorsion
Documentation

The canonical ideal-root class map from the Shafarevich radical.

Source context 7 commands

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

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

idealNthPowerRadicalToClassTorsion_mk

L214 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalToClassTorsion_mk
Source context 7 commands

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

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

idealNthPowerRadicalToClassTorsion_surjective

L228 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalToClassTorsion_surjective
Documentation

Every n-torsion ideal class is represented by an ideal whose n-th power supplies a radical element.

Source context 7 commands

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

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

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