NYLL
Module

Rational.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Rational
69 declarations indexed from sourceView source ↗

Module documentation

Ray class groups of the rational numbers

This file computes ray class groups of the rational numbers. A positive integer m determines a full narrow ray modulus: its finite part has exponent m.factorization p at p, and its real place imposes positivity. The positive generator of an ideal prime to this modulus gives the explicit isomorphism with (ZMod m)ˣ.

The local congruence condition over ℚ

Imports7
Imported by6

Declarations

instance

rationalRingOfIntegersIsPrincipalIdealRing

L35 ↗
RayClass.rationalRingOfIntegersIsPrincipalIdealRing
Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
Lean source · statement
instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ)
instance

rationalNatGeneratorPrimeFact

L41 ↗
RayClass.rationalNatGeneratorPrimeFact
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
Lean source · statement
instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v))
instance

rationalPrimesEquivPrimeFact

L46 ↗
RayClass.rationalPrimesEquivPrimeFact
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
Lean source · statement
instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ))
abbrev

rationalPrime

L56 ↗
RayClass.rationalPrime
Documentation

The height-one prime of 𝓞 ℚ associated with a natural prime.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
abbrev rationalPrime (p : Nat.Primes) :
    HeightOneSpectrum (𝓞 ℚ)
theorem

natGenerator_rationalPrime

L61 ↗
RayClass.natGenerator_rationalPrime
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem natGenerator_rationalPrime (p : Nat.Primes) :
    Rat.HeightOneSpectrum.natGenerator (rationalPrime p) = p
theorem

rational_natGenerator_injective

L66 ↗
RayClass.rational_natGenerator_injective
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rational_natGenerator_injective :
    Function.Injective
      (Rat.HeightOneSpectrum.natGenerator :
        HeightOneSpectrum (𝓞 ℚ) → ℕ)
def

rationalFiniteModulus

L78 ↗
RayClass.rationalFiniteModulus
Documentation

The finite part of the modulus (m) of ℚ. At the prime over p it has exponent m.factorization p. The later equivalences use the hypothesis 0 < m; the definition itself is harmless at m = 0.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalFiniteModulus (m : ℕ) : FiniteModulus ℚ
theorem

rationalFiniteModulus_apply

L85 ↗
RayClass.rationalFiniteModulus_apply
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalFiniteModulus_apply
    (m : ℕ) (v : HeightOneSpectrum (𝓞 ℚ)) :
    rationalFiniteModulus m v =
      m.factorization (Rat.HeightOneSpectrum.natGenerator v)
def

rationalModulus

L93 ↗
RayClass.rationalModulus
Documentation

The full rational ray modulus has the finite part (m) and positivity at the unique real place.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalModulus (m : ℕ) : Modulus ℚ
theorem

rationalModulus_finitePart_apply

L97 ↗
RayClass.rationalModulus_finitePart_apply
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalModulus_finitePart_apply
    (m : ℕ) (v : HeightOneSpectrum (𝓞 ℚ)) :
    (rationalModulus m).finitePart v =
      m.factorization (Rat.HeightOneSpectrum.natGenerator v)
theorem

mem_rationalFiniteModulus_support_iff

L104 ↗
RayClass.mem_rationalFiniteModulus_support_iff
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem mem_rationalFiniteModulus_support_iff
    {m : ℕ} (hm : m ≠ 0) (v : HeightOneSpectrum (𝓞 ℚ)) :
    v ∈ (rationalFiniteModulus m).support ↔
      Rat.HeightOneSpectrum.natGenerator v ∣ m
abbrev

rationalFractionalIdeal

L115 ↗
RayClass.rationalFractionalIdeal
Documentation

The fractional ideal underlying a rational fractional-ideal unit.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
abbrev rationalFractionalIdeal (I : FractionalIdealGroup ℚ) :
    FractionalIdeal (nonZeroDivisors (𝓞 ℚ)) ℚ
def

rawRationalIdealGenerator

L121 ↗
RayClass.rawRationalIdealGenerator
Documentation

An arbitrary principal generator of a nonzero rational fractional ideal, before choosing its sign.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rawRationalIdealGenerator
    (I : FractionalIdealGroup ℚ) : ℚ
theorem

rawRationalIdealGenerator_ne_zero

L127 ↗
RayClass.rawRationalIdealGenerator_ne_zero
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rawRationalIdealGenerator_ne_zero
    (I : FractionalIdealGroup ℚ) :
    rawRationalIdealGenerator I ≠ 0
def

positiveRationalIdealGenerator

L137 ↗
RayClass.positiveRationalIdealGenerator
Documentation

The unique positive generator of a nonzero rational 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 RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def positiveRationalIdealGenerator
    (I : FractionalIdealGroup ℚ) : ℚ
theorem

positiveRationalIdealGenerator_pos

L144 ↗
RayClass.positiveRationalIdealGenerator_pos
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveRationalIdealGenerator_pos
    (I : FractionalIdealGroup ℚ) :
    0 < positiveRationalIdealGenerator I
theorem

rationalFractionalIdeal_eq_span_positiveGenerator

L154 ↗
RayClass.rationalFractionalIdeal_eq_span_positiveGenerator
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalFractionalIdeal_eq_span_positiveGenerator
    (I : FractionalIdealGroup ℚ) :
    rationalFractionalIdeal I =
      FractionalIdeal.spanSingleton (nonZeroDivisors (𝓞 ℚ))
        (positiveRationalIdealGenerator I)
theorem

eq_of_spanSingleton_eq_of_pos

L177 ↗
RayClass.eq_of_spanSingleton_eq_of_pos
Documentation

Positive rational generators of the same principal fractional ideal are equal.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem eq_of_spanSingleton_eq_of_pos
    {x y : ℚ} (hx : 0 < x) (hy : 0 < y)
    (h :
      FractionalIdeal.spanSingleton (nonZeroDivisors (𝓞 ℚ)) x =
        FractionalIdeal.spanSingleton (nonZeroDivisors (𝓞 ℚ)) y) :
    x = y
theorem

positiveRationalIdealGenerator_one

L193 ↗
RayClass.positiveRationalIdealGenerator_one
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveRationalIdealGenerator_one :
    positiveRationalIdealGenerator (1 : FractionalIdealGroup ℚ) = 1
theorem

positiveRationalIdealGenerator_mul

L200 ↗
RayClass.positiveRationalIdealGenerator_mul
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveRationalIdealGenerator_mul
    (I J : FractionalIdealGroup ℚ) :
    positiveRationalIdealGenerator (I * J) =
      positiveRationalIdealGenerator I *
        positiveRationalIdealGenerator J
def

positiveRationalIdealGeneratorUnit

L216 ↗
RayClass.positiveRationalIdealGeneratorUnit
Documentation

The positive generator, regarded as a nonzero rational number.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def positiveRationalIdealGeneratorUnit
    (I : FractionalIdealGroup ℚ) : ℚˣ
theorem

positiveRationalIdealGeneratorUnit_val

L222 ↗
RayClass.positiveRationalIdealGeneratorUnit_val
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveRationalIdealGeneratorUnit_val
    (I : FractionalIdealGroup ℚ) :
    (positiveRationalIdealGeneratorUnit I : ℚ) =
      positiveRationalIdealGenerator I
theorem

toPrincipalIdeal_positiveRationalIdealGeneratorUnit

L228 ↗
RayClass.toPrincipalIdeal_positiveRationalIdealGeneratorUnit
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem toPrincipalIdeal_positiveRationalIdealGeneratorUnit
    (I : FractionalIdealGroup ℚ) :
    toPrincipalIdeal (𝓞 ℚ) ℚ
        (positiveRationalIdealGeneratorUnit I) = I
theorem

positiveRationalIdealGeneratorUnit_one

L241 ↗
RayClass.positiveRationalIdealGeneratorUnit_one
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveRationalIdealGeneratorUnit_one :
    positiveRationalIdealGeneratorUnit
      (1 : FractionalIdealGroup ℚ) = 1
theorem

positiveRationalIdealGeneratorUnit_mul

L247 ↗
RayClass.positiveRationalIdealGeneratorUnit_mul
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveRationalIdealGeneratorUnit_mul
    (I J : FractionalIdealGroup ℚ) :
    positiveRationalIdealGeneratorUnit (I * J) =
      positiveRationalIdealGeneratorUnit I *
        positiveRationalIdealGeneratorUnit J
theorem

withZero_eq_one_of_log_eq_zero

L257 ↗
RayClass.withZero_eq_one_of_log_eq_zero
Documentation

An element of WithZero (Multiplicative ℤ) with logarithm zero is one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem withZero_eq_one_of_log_eq_zero
    {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0)
    (hlog : WithZero.log x = 0) :
    x = 1
theorem

valuation_eq_one_of_principal_count_eq_zero

L269 ↗
RayClass.valuation_eq_one_of_principal_count_eq_zero
Documentation

Zero principal-ideal exponent at a rational finite place forces valuation one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem valuation_eq_one_of_principal_count_eq_zero
    (x : ℚˣ) (v : HeightOneSpectrum (𝓞 ℚ))
    (hcount :
      FractionalIdeal.count ℚ v
        (toPrincipalIdeal (𝓞 ℚ) ℚ x :
          FractionalIdeal (nonZeroDivisors (𝓞 ℚ)) ℚ) = 0) :
    v.valuation ℚ (x : ℚ) = 1
theorem

not_dvd_den_of_principal_count_eq_zero

L286 ↗
RayClass.not_dvd_den_of_principal_count_eq_zero
Documentation

A rational prime with zero principal-ideal exponent does not divide the denominator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem not_dvd_den_of_principal_count_eq_zero
    (x : ℚˣ) (v : HeightOneSpectrum (𝓞 ℚ))
    (hcount :
      FractionalIdeal.count ℚ v
        (toPrincipalIdeal (𝓞 ℚ) ℚ x :
          FractionalIdeal (nonZeroDivisors (𝓞 ℚ)) ℚ) = 0) :
    ¬ Rat.HeightOneSpectrum.natGenerator v ∣ (x : ℚ).den
theorem

not_dvd_num_of_principal_count_eq_zero

L306 ↗
RayClass.not_dvd_num_of_principal_count_eq_zero
Documentation

A rational prime with zero principal-ideal exponent does not divide the numerator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem not_dvd_num_of_principal_count_eq_zero
    (x : ℚˣ) (v : HeightOneSpectrum (𝓞 ℚ))
    (hcount :
      FractionalIdeal.count ℚ v
        (toPrincipalIdeal (𝓞 ℚ) ℚ x :
          FractionalIdeal (nonZeroDivisors (𝓞 ℚ)) ℚ) = 0) :
    ¬ Rat.HeightOneSpectrum.natGenerator v ∣ (x : ℚ).num.natAbs
theorem

positiveGenerator_den_coprime

L333 ↗
RayClass.positiveGenerator_den_coprime
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveGenerator_den_coprime
    {m : ℕ} (hm : m ≠ 0)
    (I : primeToModulusIdeals (rationalModulus m)) :
    Nat.Coprime
      (positiveRationalIdealGenerator (I : FractionalIdealGroup ℚ)).den m
theorem

positiveGenerator_num_coprime

L361 ↗
RayClass.positiveGenerator_num_coprime
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem positiveGenerator_num_coprime
    {m : ℕ} (hm : m ≠ 0)
    (I : primeToModulusIdeals (rationalModulus m)) :
    Nat.Coprime
      (positiveRationalIdealGenerator
        (I : FractionalIdealGroup ℚ)).num.natAbs m
def

rationalNumeratorResidueUnit

L391 ↗
RayClass.rationalNumeratorResidueUnit
Documentation

The numerator of a rational number as a residue-class unit.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalNumeratorResidueUnit
    (m : ℕ) (q : ℚ) (hq : Nat.Coprime q.num.natAbs m) :
    (ZMod m)ˣ
def

rationalDenominatorResidueUnit

L398 ↗
RayClass.rationalDenominatorResidueUnit
Documentation

The denominator of a rational number as a residue-class unit.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalDenominatorResidueUnit
    (m : ℕ) (q : ℚ) (hq : Nat.Coprime q.den m) :
    (ZMod m)ˣ
def

rationalResidueUnit

L406 ↗
RayClass.rationalResidueUnit
Documentation

Reduction of a rational number whose numerator and denominator are both prime to m.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalResidueUnit
    (m : ℕ) (q : ℚ)
    (hnum : Nat.Coprime q.num.natAbs m)
    (hden : Nat.Coprime q.den m) :
    (ZMod m)ˣ
theorem

rationalResidueUnit_congr

L415 ↗
RayClass.rationalResidueUnit_congr
Documentation

Rational residue units are independent of the chosen equality proof.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalResidueUnit_congr
    (m : ℕ) {q r : ℚ} (hqr : q = r)
    (hqnum : Nat.Coprime q.num.natAbs m)
    (hqden : Nat.Coprime q.den m)
    (hrnum : Nat.Coprime r.num.natAbs m)
    (hrden : Nat.Coprime r.den m) :
    rationalResidueUnit m q hqnum hqden =
      rationalResidueUnit m r hrnum hrden
theorem

rationalResidueUnit_mul

L427 ↗
RayClass.rationalResidueUnit_mul
Documentation

Reduction of rational numbers prime to a modulus is multiplicative.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalResidueUnit_mul
    (m : ℕ) (q r : ℚ)
    (hqnum : Nat.Coprime q.num.natAbs m)
    (hqden : Nat.Coprime q.den m)
    (hrnum : Nat.Coprime r.num.natAbs m)
    (hrden : Nat.Coprime r.den m)
    (hqrnum : Nat.Coprime (q * r).num.natAbs m)
    (hqrden : Nat.Coprime (q * r).den m) :
    rationalResidueUnit m (q * r) hqrnum hqrden =
      rationalResidueUnit m q hqnum hqden *
        rationalResidueUnit m r hrnum hrden
theorem

rationalResidueUnit_one

L462 ↗
RayClass.rationalResidueUnit_one
Documentation

The rational residue unit of one is one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · full declaration
theorem rationalResidueUnit_one (m : ℕ) :
    rationalResidueUnit m 1 (by simp) (by simp) = 1 := by
  apply Units.ext
  simp [rationalResidueUnit, rationalNumeratorResidueUnit,
    rationalDenominatorResidueUnit]
theorem

rationalResidueUnit_eq_one_iff_modEq

L470 ↗
RayClass.rationalResidueUnit_eq_one_iff_modEq
Documentation

A rational residue unit is one exactly when its numerator and denominator are congruent modulo the modulus.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalResidueUnit_eq_one_iff_modEq
    (m : ℕ) (q : ℚ)
    (hnum : Nat.Coprime q.num.natAbs m)
    (hden : Nat.Coprime q.den m) :
    rationalResidueUnit m q hnum hden = 1 ↔
      q.num ≡ (q.den : ℤ) [ZMOD m]
def

primeToIdealResidueHom

L499 ↗
RayClass.primeToIdealResidueHom
Documentation

Send an ideal prime to (m) to the residue class of its positive generator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · full declaration
def primeToIdealResidueHom
    (m : ℕ) (hm : m ≠ 0) :
    primeToModulusIdeals (rationalModulus m) →* (ZMod m)ˣ where
  toFun I :=
    rationalResidueUnit m
      (positiveRationalIdealGenerator (I : FractionalIdealGroup ℚ))
      (positiveGenerator_num_coprime hm I)
      (positiveGenerator_den_coprime hm I)
  map_one' := by
    change rationalResidueUnit m
      (positiveRationalIdealGenerator
        (1 : FractionalIdealGroup ℚ)) _ _ = 1
    calc
      rationalResidueUnit m
          (positiveRationalIdealGenerator
            (1 : FractionalIdealGroup ℚ)) _ _ =
        rationalResidueUnit m 1 (by simp) (by simp) :=
          rationalResidueUnit_congr m
            positiveRationalIdealGenerator_one _ _ _ _
      _ = 1 := rationalResidueUnit_one m
  map_mul' I J := by
    let q :=
      positiveRationalIdealGenerator (I : FractionalIdealGroup ℚ)
    let r :=
      positiveRationalIdealGenerator (J : FractionalIdealGroup ℚ)
    have hprodnum : Nat.Coprime (q * r).num.natAbs m := by
      rw [← positiveRationalIdealGenerator_mul]
      exact positiveGenerator_num_coprime hm (I * J)
    have hprodden : Nat.Coprime (q * r).den m := by
      rw [← positiveRationalIdealGenerator_mul]
      exact positiveGenerator_den_coprime hm (I * J)
    change rationalResidueUnit m
        (positiveRationalIdealGenerator
          ((I : FractionalIdealGroup ℚ) *
            (J : FractionalIdealGroup ℚ))) _ _ =
      rationalResidueUnit m q _ _ * rationalResidueUnit m r _ _
    calc
      rationalResidueUnit m
          (positiveRationalIdealGenerator
            ((I : FractionalIdealGroup ℚ) *
              (J : FractionalIdealGroup ℚ))) _ _ =
        rationalResidueUnit m (q * r) hprodnum hprodden :=
          rationalResidueUnit_congr m
            (positiveRationalIdealGenerator_mul I J) _ _ _ _
      _ = rationalResidueUnit m q
              (positiveGenerator_num_coprime hm I)
              (positiveGenerator_den_coprime hm I) *
            rationalResidueUnit m r
              (positiveGenerator_num_coprime hm J)
              (positiveGenerator_den_coprime hm J) :=
        rationalResidueUnit_mul m q r
          (positiveGenerator_num_coprime hm I)
          (positiveGenerator_den_coprime hm I)
          (positiveGenerator_num_coprime hm J)
          (positiveGenerator_den_coprime hm J)
          hprodnum hprodden
theorem

primeToIdealResidueHom_apply

L557 ↗
RayClass.primeToIdealResidueHom_apply
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem primeToIdealResidueHom_apply
    (m : ℕ) (hm : m ≠ 0)
    (I : primeToModulusIdeals (rationalModulus m)) :
    primeToIdealResidueHom m hm I =
      rationalResidueUnit m
        (positiveRationalIdealGenerator
          (I : FractionalIdealGroup ℚ))
        (positiveGenerator_num_coprime hm I)
        (positiveGenerator_den_coprime hm I)
theorem

principalNat_mem_primeToModulusIdeals

L570 ↗
RayClass.principalNat_mem_primeToModulusIdeals
Documentation

A positive integer prime to the modulus defines a principal ideal in the prime-to-modulus ideal group.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · full declaration
theorem principalNat_mem_primeToModulusIdeals
    {m a : ℕ} (hm : m ≠ 0) (ha : a ≠ 0)
    (hcop : Nat.Coprime a m) :
    toPrincipalIdeal (𝓞 ℚ) ℚ
        (Units.mk0 (a : ℚ) (by exact_mod_cast ha)) ∈
      primeToModulusIdeals (rationalModulus m) := by
  intro v hv
  let p := Rat.HeightOneSpectrum.natGenerator v
  have hp : p.Prime :=
    Rat.HeightOneSpectrum.prime_natGenerator v
  have hpm : p ∣ m :=
    (by
      rw [rationalModulus, Modulus.finitePart_narrowOfFinite] at hv
      exact (mem_rationalFiniteModulus_support_iff hm v).mp hv)
  have hpa : ¬ p ∣ a :=
    hp.coprime_iff_not_dvd.mp
      (hcop.coprime_dvd_right hpm).symm
  let : Fact p.Prime := ⟨hp⟩
  have hpval : Rat.padicValuation p (a : ℚ) = 1 := by
    rw [← Int.cast_natCast, Rat.padicValuation_cast]
    exact Int.padicValuation_eq_one_iff.mpr
      (by simpa only [Int.natCast_dvd_natCast] using hpa)
  have hequiv :=
    Rat.HeightOneSpectrum.valuation_equiv_padicValuation v
  have hvval : v.valuation ℚ (a : ℚ) = 1 :=
    hequiv.eq_one_iff_eq_one.mpr hpval
  rw [IdeleGroup.count_toPrincipalIdeal]
  change -WithZero.log (v.valuation ℚ (a : ℚ)) = 0
  rw [hvval]
  rfl
theorem

positiveGenerator_toPrincipalIdeal_nat

L603 ↗
RayClass.positiveGenerator_toPrincipalIdeal_nat
Documentation

The positive generator of the principal ideal of a positive integer is that integer.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · full declaration
theorem positiveGenerator_toPrincipalIdeal_nat
    {a : ℕ} (ha : 0 < a) :
    positiveRationalIdealGenerator
        (toPrincipalIdeal (𝓞 ℚ) ℚ
          (Units.mk0 (a : ℚ) (by exact_mod_cast ha.ne'))) =
      (a : ℚ) := by
  let x : ℚˣ :=
    Units.mk0 (a : ℚ) (by exact_mod_cast ha.ne')
  apply eq_of_spanSingleton_eq_of_pos
    (positiveRationalIdealGenerator_pos _)
    (by exact_mod_cast ha)
  rw [← rationalFractionalIdeal_eq_span_positiveGenerator]
  calc
    rationalFractionalIdeal
        (toPrincipalIdeal (𝓞 ℚ) ℚ x) =
      FractionalIdeal.spanSingleton (nonZeroDivisors (𝓞 ℚ))
        (x : ℚ) := by
          simpa only [rationalFractionalIdeal] using
            (coe_toPrincipalIdeal (R := 𝓞 ℚ) (K := ℚ) x)
    _ = FractionalIdeal.spanSingleton
        (nonZeroDivisors (𝓞 ℚ)) (a : ℚ) := rfl
theorem

rationalNumeratorResidueUnit_natCast

L627 ↗
RayClass.rationalNumeratorResidueUnit_natCast
Documentation

The numerator residue unit of a positive natural cast is its residue unit.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · full declaration
theorem rationalNumeratorResidueUnit_natCast
    (m a : ℕ) (hcop : Nat.Coprime a m) :
    (rationalNumeratorResidueUnit m (a : ℚ)
        (by simpa using hcop) : ZMod m) =
      (a : ZMod m) := by
  simp [rationalNumeratorResidueUnit]
theorem

rationalDenominatorResidueUnit_natCast

L635 ↗
RayClass.rationalDenominatorResidueUnit_natCast
Documentation

The denominator residue unit of a positive natural cast is one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalDenominatorResidueUnit_natCast
    (m a : ℕ) (hden : Nat.Coprime ((a : ℚ).den) m) :
    rationalDenominatorResidueUnit m (a : ℚ) hden = 1
theorem

rationalResidueUnit_natCast

L643 ↗
RayClass.rationalResidueUnit_natCast
Documentation

Rational reduction of a positive natural cast agrees with ordinary residue reduction.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · full declaration
theorem rationalResidueUnit_natCast
    (m a : ℕ) (hcop : Nat.Coprime a m) :
    (rationalResidueUnit m (a : ℚ)
        (by simpa using hcop) (by simp) : ZMod m) =
      (a : ZMod m) := by
  have hden :
      rationalDenominatorResidueUnit m (a : ℚ) (by simp) = 1 :=
    rationalDenominatorResidueUnit_natCast m a (by simp)
  change
    (rationalNumeratorResidueUnit m (a : ℚ) _ *
      (rationalDenominatorResidueUnit m (a : ℚ) _)⁻¹ :
        (ZMod m)ˣ) =
      (a : ZMod m)
  rw [hden, inv_one, mul_one]
  exact rationalNumeratorResidueUnit_natCast m a hcop
theorem

primeToIdealResidueHom_surjective

L659 ↗
RayClass.primeToIdealResidueHom_surjective
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem primeToIdealResidueHom_surjective
    (m : ℕ) (hm : m ≠ 0) :
    Function.Surjective (primeToIdealResidueHom m hm)
def

principalLocalIntegralUnit

L710 ↗
RayClass.principalLocalIntegralUnit
Documentation

The integral local unit attached to a rational principal idele component.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def principalLocalIntegralUnit
    (v : HeightOneSpectrum (𝓞 ℚ)) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    (v.adicCompletionIntegers ℚ).units
def

rationalLocalIntegralValue

L723 ↗
RayClass.rationalLocalIntegralValue
Documentation

The integral value underlying a rational principal local unit.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalLocalIntegralValue
    (v : HeightOneSpectrum (𝓞 ℚ))
    (y : (v.adicCompletionIntegers ℚ).units) :
    v.adicCompletionIntegers ℚ
theorem

rationalLocalHigherUnitMap_eq_one_iff

L732 ↗
RayClass.rationalLocalHigherUnitMap_eq_one_iff
Documentation

The residue criterion for a rational principal local unit to lie in a higher-unit group.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalLocalHigherUnitMap_eq_one_iff
    (v : HeightOneSpectrum (𝓞 ℚ)) (n : ℕ)
    (y : (v.adicCompletionIntegers ℚ).units) :
    localHigherUnitMap v n y = 1 ↔
      rationalLocalIntegralValue v y - 1 ∈
        (IsLocalRing.maximalIdeal
          (v.adicCompletionIntegers ℚ)) ^ n
theorem

principalLocalIntegralValue_coe

L755 ↗
RayClass.principalLocalIntegralValue_coe
Documentation

Coercing the integral local value recovers the principal finite component.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalLocalIntegralValue_coe
    (v : HeightOneSpectrum (𝓞 ℚ)) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    (rationalLocalIntegralValue v
      (principalLocalIntegralUnit v x hx) :
        v.adicCompletion ℚ) =
      NumberField.FinitePlace.embedding v (x : ℚ)
theorem

map_maximalIdeal_pow_padicIntEquiv

L773 ↗
RayClass.map_maximalIdeal_pow_padicIntEquiv
Documentation

The rational adic-completion equivalence maps powers of maximal ideals to the corresponding powers in the padic integers.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem map_maximalIdeal_pow_padicIntEquiv
    (v : HeightOneSpectrum (𝓞 ℚ)) (n : ℕ) :
    ((IsLocalRing.maximalIdeal
        (v.adicCompletionIntegers ℚ)) ^ n).map
        (Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v).toRingEquiv =
      Ideal.span
        {(((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ) :
          ℤ_[((Rat.HeightOneSpectrum.primesEquiv
            (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)]) ^ n}
theorem

rationalLocalIntegralValue_sub_mem_iff

L788 ↗
RayClass.rationalLocalIntegralValue_sub_mem_iff
Documentation

Membership of the local integral difference in a maximal-ideal power is equivalent to the corresponding padic divisibility condition.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rationalLocalIntegralValue_sub_mem_iff
    (v : HeightOneSpectrum (𝓞 ℚ)) (n : ℕ)
    (z : v.adicCompletionIntegers ℚ) :
    z - 1 ∈
        (IsLocalRing.maximalIdeal
          (v.adicCompletionIntegers ℚ)) ^ n ↔
      PadicInt.toZModPow n
          (Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v z) =
        1
theorem

primesEquiv_val_eq_natGenerator

L829 ↗
RayClass.primesEquiv_val_eq_natGenerator
Documentation

The rational-prime equivalence identifies the local prime value with the natural prime generator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem primesEquiv_val_eq_natGenerator
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    ((Rat.HeightOneSpectrum.primesEquiv
      (R := 𝓞 ℚ) v : Nat.Primes) : ℕ) =
      Rat.HeightOneSpectrum.natGenerator v
theorem

principalFiniteComponent_mem_localHigherUnitGroup_iff

L838 ↗
RayClass.principalFiniteComponent_mem_localHigherUnitGroup_iff
Documentation

A rational principal finite component lies in a higher-unit group exactly when its numerator and denominator satisfy the local congruence.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalFiniteComponent_mem_localHigherUnitGroup_iff
    (v : HeightOneSpectrum (𝓞 ℚ)) (n : ℕ) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    (IdeleGroup.principalIdele ℚ x).2 v ∈
        localHigherUnitGroup v n ↔
      localHigherUnitMap v n
        (principalLocalIntegralUnit v x hx) = 1
theorem

rational_den_mul_self_eq_num

L857 ↗
RayClass.rational_den_mul_self_eq_num
Documentation

Multiplying a rational number by its denominator gives its numerator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem rational_den_mul_self_eq_num (q : ℚ) :
    (q.den : ℚ) * q = q.num
theorem

principalLocalIntegralValue_den_mul

L866 ↗
RayClass.principalLocalIntegralValue_den_mul
Documentation

Multiplying the principal local integral value by the denominator gives the numerator in the completion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalLocalIntegralValue_den_mul
    (v : HeightOneSpectrum (𝓞 ℚ)) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    algebraMap ℤ (v.adicCompletionIntegers ℚ) (x : ℚ).den *
        rationalLocalIntegralValue v
          (principalLocalIntegralUnit v x hx) =
      algebraMap ℤ (v.adicCompletionIntegers ℚ) (x : ℚ).num
abbrev

rationalPadicPrime

L883 ↗
RayClass.rationalPadicPrime
Documentation

The positive rational prime attached to a finite place.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
abbrev rationalPadicPrime
    (v : HeightOneSpectrum (𝓞 ℚ)) : ℕ
theorem

principalLocalResidue_den_mul

L890 ↗
RayClass.principalLocalResidue_den_mul
Documentation

In the local residue ring, the denominator times the principal value equals the numerator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalLocalResidue_den_mul
    (v : HeightOneSpectrum (𝓞 ℚ)) (n : ℕ) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    ((x : ℚ).den : ZMod (rationalPadicPrime v ^ n)) *
        PadicInt.toZModPow n
          (Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v
            (rationalLocalIntegralValue v
              (principalLocalIntegralUnit v x hx))) =
      ((x : ℚ).num : ZMod (rationalPadicPrime v ^ n))
theorem

not_dvd_den_of_valuation_eq_one

L943 ↗
RayClass.not_dvd_den_of_valuation_eq_one
Documentation

Valuation one at a rational finite place implies that its prime does not divide the denominator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem not_dvd_den_of_valuation_eq_one
    (v : HeightOneSpectrum (𝓞 ℚ)) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    ¬ Rat.HeightOneSpectrum.natGenerator v ∣ (x : ℚ).den
theorem

principalLocalHigherUnit_iff_modEq

L956 ↗
RayClass.principalLocalHigherUnit_iff_modEq
Documentation

Rational principal higher-unit membership is equivalent to a prime-power congruence of numerator and denominator.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalLocalHigherUnit_iff_modEq
    (v : HeightOneSpectrum (𝓞 ℚ)) (n : ℕ) (x : ℚˣ)
    (hx : v.valuation ℚ (x : ℚ) = 1) :
    (IdeleGroup.principalIdele ℚ x).2 v ∈
        localHigherUnitGroup v n ↔
      (x : ℚ).num ≡ ((x : ℚ).den : ℤ)
        [ZMOD (Rat.HeightOneSpectrum.natGenerator v) ^ n]
theorem

intModEq_finset_prod_of_pairwise_coprime

L1004 ↗
RayClass.intModEq_finset_prod_of_pairwise_coprime
Documentation

Congruences modulo pairwise coprime moduli combine to a congruence modulo their finite product.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem intModEq_finset_prod_of_pairwise_coprime
    {ι : Type*}
    (s : Finset ι) (f : ι → ℕ)
    (hpair :
      ∀ i ∈ s, ∀ j ∈ s, i ≠ j →
        Nat.Coprime (f i) (f j))
    {a b : ℤ}
    (hmod : ∀ i ∈ s, a ≡ b [ZMOD f i]) :
    a ≡ b [ZMOD ∏ i ∈ s, f i]
theorem

intModEq_of_primePower_modEq

L1045 ↗
RayClass.intModEq_of_primePower_modEq
Documentation

Congruences modulo every prime-power factor of a natural number combine to a congruence modulo that number.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem intModEq_of_primePower_modEq
    {m : ℕ} (hm : m ≠ 0) {a b : ℤ}
    (h :
      ∀ p : m.primeFactors,
        a ≡ b [ZMOD (p : ℕ) ^ m.factorization p]) :
    a ≡ b [ZMOD m]
theorem

primePower_factorization_dvd

L1071 ↗
RayClass.primePower_factorization_dvd
Documentation

Every prime-power factor determined by a factorization divides the original natural number.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem primePower_factorization_dvd
    {m p : ℕ} (hm : m ≠ 0) (hp : p.Prime) :
    p ^ m.factorization p ∣ m
theorem

principalIdele_infinite_mem_iff_pos

L1078 ↗
RayClass.principalIdele_infinite_mem_iff_pos
Documentation

The infinite component of a rational principal idele is positive exactly when the rational number is positive.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalIdele_infinite_mem_iff_pos
    (x : ℚˣ) :
    (IdeleGroup.principalIdele ℚ x).1 ∈
        narrowInfiniteCongruenceSubgroup (K := ℚ) ↔
      0 < (x : ℚ)
theorem

principalIdele_positiveGenerator_mem_primeTo_iff_modEq

L1124 ↗
RayClass.principalIdele_positiveGenerator_mem_primeTo_iff_modEq
Documentation

The principal idele of the positive generator satisfies the prime-to-modulus congruence condition exactly when its rational residue is one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem principalIdele_positiveGenerator_mem_primeTo_iff_modEq
    {m : ℕ} (hm : m ≠ 0)
    (I : primeToModulusIdeals (rationalModulus m)) :
    IdeleGroup.principalIdele ℚ
        (positiveRationalIdealGeneratorUnit
          (I : FractionalIdealGroup ℚ)) ∈
        idelePrimeToModulusSubgroup (rationalModulus m) ↔
      (positiveRationalIdealGenerator
          (I : FractionalIdealGroup ℚ)).num ≡
        (positiveRationalIdealGenerator
          (I : FractionalIdealGroup ℚ)).den
        [ZMOD m]
theorem

mem_principalRayIdealSubgroup_iff_modEq

L1199 ↗
RayClass.mem_principalRayIdealSubgroup_iff_modEq
Documentation

Over ℚ, the ideal-theoretic ray subgroup consists precisely of the positive principal generators congruent to one modulo m.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem mem_principalRayIdealSubgroup_iff_modEq
    {m : ℕ} (hm : m ≠ 0)
    (I : primeToModulusIdeals (rationalModulus m)) :
    I ∈ principalRayIdealSubgroup (rationalModulus m) ↔
      (positiveRationalIdealGenerator
          (I : FractionalIdealGroup ℚ)).num ≡
        (positiveRationalIdealGenerator
          (I : FractionalIdealGroup ℚ)).den
        [ZMOD m]
theorem

primeToIdealResidueHom_ker

L1272 ↗
RayClass.primeToIdealResidueHom_ker
Documentation

The residue map on ideals prime to (m) has exactly the ray-principal ideals as its kernel.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
theorem primeToIdealResidueHom_ker
    (m : ℕ) (hm : m ≠ 0) :
    (primeToIdealResidueHom m hm).ker =
      principalRayIdealSubgroup (rationalModulus m)
def

idealRayClassGroupEquivZModUnits

L1289 ↗
RayClass.idealRayClassGroupEquivZModUnits
Documentation

In ideal-theoretic form, the ray ideal class group of ℚ modulo (m) is (ℤ/mℤ)ˣ.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def idealRayClassGroupEquivZModUnits
    (m : ℕ) (hm : m ≠ 0) :
    IdealRayClassGroup (rationalModulus m) ≃*
      (ZMod m)ˣ
def

rationalRayClassGroupEquivZModUnits

L1302 ↗
RayClass.rationalRayClassGroupEquivZModUnits
Documentation

In idelic form, the idelic ray class group of ℚ modulo (m) is (ℤ/mℤ)ˣ.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace RayClass
local instance rationalRingOfIntegersIsPrincipalIdealRing :
    IsPrincipalIdealRing (𝓞 ℚ) :=
  IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm
    Rat.ringOfIntegersEquiv.symm.surjective
local instance rationalNatGeneratorPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact (Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)) :=
  ⟨Rat.HeightOneSpectrum.prime_natGenerator v⟩
local instance rationalPrimesEquivPrimeFact
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Fact
      (Nat.Prime
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ) v : Nat.Primes) : ℕ)) :=
  ⟨(Rat.HeightOneSpectrum.primesEquiv
    (R := 𝓞 ℚ) v).property⟩
Lean source · statement
def rationalRayClassGroupEquivZModUnits
    (m : ℕ) (hm : m ≠ 0) :
    RayClassGroup (rationalModulus m) ≃*
      (ZMod m)ˣ

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