NYLL
Module

IdealPowerRadicalExact.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadicalExact
10 declarations indexed from sourceView source ↗

Module documentation

The exact unit--radical--class sequence

This file supplies the missing maps in the empty-support Selmer sequence: ordinary units modulo powers inject into the ideal-power radical, whose ideal-root class map surjects onto class-group power torsion.

Imports4
Imported by5

Declarations

def

integralUnitToIdealNthPowerRadical

L32 ↗
ClassFieldTower.Martinet.Shafarevich.integralUnitToIdealNthPowerRadical
Documentation

Ordinary integral units regarded as elements of the ideal-power radical.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · full declaration
def integralUnitToIdealNthPowerRadical
    (n : ℕ+) :
    (𝓞 K)ˣ →* (idealNthPowerRadicalKummerSubgroup K n).1 where
  toFun u := ⟨RayClass.integralUnitToFieldUnit u, by
    change toPrincipalIdeal (𝓞 K) K
        (RayClass.integralUnitToFieldUnit u) ∈
      (powMonoidHom (n : ℕ) : FractionalIdealGroup K →*
        FractionalIdealGroup K).range
    refine ⟨1, ?_⟩
    rw [powMonoidHom_apply, one_pow]
    exact ((RayClass.toPrincipalIdeal_eq_one_iff_mem_integralUnits _).2
      ⟨u, rfl⟩).symm⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (RayClass.integralUnitToFieldUnit (K := K))
  map_mul' u v := by
    apply Subtype.ext
    exact map_mul (RayClass.integralUnitToFieldUnit (K := K)) u v
def

integralUnitToIdealNthPowerRadicalQuotient

L52 ↗
ClassFieldTower.Martinet.Shafarevich.integralUnitToIdealNthPowerRadicalQuotient
Documentation

The raw map from integral units to the radical quotient.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def integralUnitToIdealNthPowerRadicalQuotient
    (n : ℕ+) :
    (𝓞 K)ˣ →* IdealNthPowerRadicalQuotient K n
theorem

integralUnitToIdealNthPowerRadicalQuotient_ker

L59 ↗
ClassFieldTower.Martinet.Shafarevich.integralUnitToIdealNthPowerRadicalQuotient_ker
Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem integralUnitToIdealNthPowerRadicalQuotient_ker
    (n : ℕ+) :
    MonoidHom.ker (integralUnitToIdealNthPowerRadicalQuotient K n) =
      (powMonoidHom (n : ℕ) : (𝓞 K)ˣ →* (𝓞 K)ˣ).range
def

ordinaryUnitNthPowerQuotientToIdealRadical

L103 ↗
ClassFieldTower.Martinet.Shafarevich.ordinaryUnitNthPowerQuotientToIdealRadical
Documentation

The injection of ordinary units modulo n-th powers into the Shafarevich radical.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def ordinaryUnitNthPowerQuotientToIdealRadical
    (n : ℕ+) :
    OrdinaryUnitNthPowerQuotient K (n : ℕ) →*
      IdealNthPowerRadicalQuotient K n
theorem

ordinaryUnitNthPowerQuotientToIdealRadical_injective

L112 ↗
ClassFieldTower.Martinet.Shafarevich.ordinaryUnitNthPowerQuotientToIdealRadical_injective
Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem ordinaryUnitNthPowerQuotientToIdealRadical_injective
    (n : ℕ+) :
    Function.Injective
      (ordinaryUnitNthPowerQuotientToIdealRadical K n)
theorem

ordinaryUnitNthPowerQuotientToIdealRadical_mk

L123 ↗
ClassFieldTower.Martinet.Shafarevich.ordinaryUnitNthPowerQuotientToIdealRadical_mk
Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem ordinaryUnitNthPowerQuotientToIdealRadical_mk
    (n : ℕ+) (u : (𝓞 K)ˣ) :
    ordinaryUnitNthPowerQuotientToIdealRadical K n
        (QuotientGroup.mk'
          (powMonoidHom (n : ℕ) : (𝓞 K)ˣ →* (𝓞 K)ˣ).range u) =
      restrictedRadicalQuotientMk n
        (idealNthPowerRadicalKummerSubgroup K n)
        (integralUnitToIdealNthPowerRadical K n u)
theorem

range_ordinaryUnitToIdealRadical_eq_ker_toClassTorsion

L134 ↗
ClassFieldTower.Martinet.Shafarevich.range_ordinaryUnitToIdealRadical_eq_ker_toClassTorsion
Documentation

The ordinary-unit injection and ideal-root class map are exact.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem range_ordinaryUnitToIdealRadical_eq_ker_toClassTorsion
    (n : ℕ+) :
    MonoidHom.range (ordinaryUnitNthPowerQuotientToIdealRadical K n) =
      MonoidHom.ker (idealNthPowerRadicalToClassTorsion K n)
instance

finite_idealNthPowerRadicalQuotient

L198 ↗
ClassFieldTower.Martinet.Shafarevich.finite_idealNthPowerRadicalQuotient
Documentation

The empty-support ideal-power radical quotient is finite.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
instance finite_idealNthPowerRadicalQuotient
    (n : ℕ+) :
    Finite (IdealNthPowerRadicalQuotient K n)
theorem

card_idealNthPowerRadicalQuotient

L221 ↗
ClassFieldTower.Martinet.Shafarevich.card_idealNthPowerRadicalQuotient
Documentation

The exact sequence computes the radical cardinality as the product of the ordinary-unit quotient and the n-class quotient cardinalities.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem card_idealNthPowerRadicalQuotient
    (n : ℕ+) :
    Nat.card (IdealNthPowerRadicalQuotient K n) =
      Nat.card (OrdinaryUnitNthPowerQuotient K (n : ℕ)) *
        Nat.card (ClassFieldTower.Martinet.PClassGroup K (n : ℕ))
theorem

card_idealPthPowerRadicalQuotient

L254 ↗
ClassFieldTower.Martinet.Shafarevich.card_idealPthPowerRadicalQuotient
Documentation

For a prime p, the radical cardinality has the Dirichlet-unit rank, the root-of-unity correction, and the elementary p-class factor.

Source context 6 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 KummerTheory
variable (K : Type*) [Field K] [NumberField K]
Lean source · full declaration
theorem card_idealPthPowerRadicalQuotient
    (p : ℕ) (hp : p.Prime) :
    Nat.card
        (IdealNthPowerRadicalQuotient K (p.toPNat hp.pos)) =
      p ^ (NumberField.InfinitePlace.nrRealPlaces K +
          NumberField.InfinitePlace.nrComplexPlaces K - 1 +
            (if (primitiveRoots p K).Nonempty then 1 else 0)) *
        Nat.card (ClassFieldTower.Martinet.PClassGroup K p) := by
  rw [card_idealNthPowerRadicalQuotient K (p.toPNat hp.pos)]
  change Nat.card (OrdinaryUnitNthPowerQuotient K p) *
      Nat.card (ClassFieldTower.Martinet.PClassGroup K p) = _
  rw [card_ordinaryUnitNthPowerQuotient K p hp]

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