NYLL
Module

NumberFieldFractionalIdealFactorization.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.NumberFieldFractionalIdealFactorization
11 declarations indexed from sourceView source ↗

Module documentation

Prime factorization of nonzero fractional ideals

Mathlib's FractionalIdeal.count and unique-factorization theorems identify the multiplicative group of nonzero fractional ideals with the finitely supported integer exponents of finite primes. This equivalence is formulated entirely in Mathlib and public Definitions vocabulary.

Imports4
Imported by2

Declarations

def

primePowerHom

L37 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.primePowerHom
Documentation

The integer exponent of one finite prime, viewed multiplicatively.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def primePowerHom (v : HeightOneSpectrum (𝓞 K)) :
    Multiplicative ℤ →* NumberFieldFractionalIdealGroup K
def

factorization

L45 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.factorization
Documentation

Reconstruct a nonzero fractional ideal from finitely many prime exponents.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def factorization :
    Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ) →*
      NumberFieldFractionalIdealGroup K
theorem

factorization_val

L55 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.factorization_val
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · full declaration
theorem factorization_val
    (exps : Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ)) :
    ((factorization exps : NumberFieldFractionalIdealGroup K) :
      FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      exps.toAdd.prod fun v n =>
        (v.asIdeal : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) ^ n := by
  classical
  simp [factorization, primePowerHom, finitePrimeFractionalIdeal, Finsupp.prod]
theorem

finite_count_support

L66 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.finite_count_support
Documentation

Only finitely many finite primes occur with nonzero exponent in a nonzero fractional ideal.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem finite_count_support (I : NumberFieldFractionalIdealGroup K) :
    {v : HeightOneSpectrum (𝓞 K) |
      FractionalIdeal.count K v
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) ≠ 0}.Finite
def

countVector

L76 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.countVector
Documentation

The finitely supported prime-exponent vector of a nonzero fractional ideal.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def countVector (I : NumberFieldFractionalIdealGroup K) :
    HeightOneSpectrum (𝓞 K) →₀ ℤ
theorem

countVector_apply

L86 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.countVector_apply
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem countVector_apply (I : NumberFieldFractionalIdealGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    countVector I v =
      FractionalIdeal.count K v
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K)
theorem

count_factorization

L94 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.count_factorization
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem count_factorization
    (exps : Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ))
    (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdeal.count K v
      ((factorization exps : NumberFieldFractionalIdealGroup K) :
        FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      exps.toAdd v
theorem

ext_count

L104 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.ext_count
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem ext_count {I J : NumberFieldFractionalIdealGroup K}
    (h : ∀ v : HeightOneSpectrum (𝓞 K),
      FractionalIdeal.count K v
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      FractionalIdeal.count K v
        (J : FractionalIdeal (nonZeroDivisors (𝓞 K)) K)) :
    I = J
theorem

factorization_injective

L120 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.factorization_injective
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem factorization_injective :
    Function.Injective (factorization (K := K))
theorem

factorization_surjective

L127 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.factorization_surjective
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem factorization_surjective :
    Function.Surjective (factorization (K := K))
def

factorizationEquiv

L140 ↗
ClassFieldTheory.NumberFieldFractionalIdealGroup.factorizationEquiv
Documentation

Multiplicative prime factorization of nonzero fractional ideals.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u
namespace NumberFieldFractionalIdealGroup
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
def factorizationEquiv :
    Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ) ≃*
      NumberFieldFractionalIdealGroup K

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