NYLL
Module

Ideal.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Ideal
59 declarations indexed from sourceView source ↗

Module documentation

Ideals prime to a ray-class modulus

This file defines the subgroup of fractional ideals prime to a modulus, connects it with the corresponding finite-idele higher-unit conditions, and develops the approximation maps used in ray-class ideal constructions.

Simultaneous approximation at the places in a modulus

Imports7
Imported by9

Declarations

def

primeToModulusIdeals

L37 ↗
RayClass.primeToModulusIdeals
Documentation

Fractional ideals having valuation zero at every finite prime in the support of the modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def primeToModulusIdeals (m : Modulus K) :
    Subgroup (FractionalIdealGroup K) where
  carrier := {I | ∀ v, v ∈ m.finitePart.support →
    FractionalIdeal.count K v
      (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) = 0}
  one_mem' v _ := FractionalIdeal.count_one K v
  mul_mem' {I J} hI hJ v hv := by
    rw [Units.val_mul,
      FractionalIdeal.count_mul K v (Units.ne_zero I) (Units.ne_zero J),
      hI v hv, hJ v hv, add_zero]
  inv_mem' {I} hI v hv := by
    rw [Units.val_inv_eq_inv_val, FractionalIdeal.count_inv K v,
      hI v hv, neg_zero]
theorem

mem_primeToModulusIdeals_iff

L52 ↗
RayClass.mem_primeToModulusIdeals_iff
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem mem_primeToModulusIdeals_iff
    (m : Modulus K) (I : FractionalIdealGroup K) :
    I ∈ primeToModulusIdeals m ↔
      ∀ v, v ∈ m.finitePart.support →
        FractionalIdeal.count K v
          (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) = 0
def

primeToModulusIdeal

L62 ↗
RayClass.primeToModulusIdeal
Documentation

A finite prime outside the support of m, regarded as an element of the group of fractional ideals prime to m.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def primeToModulusIdeal
    (m : Modulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    primeToModulusIdeals m
theorem

primeToModulusIdeal_coe

L84 ↗
RayClass.primeToModulusIdeal_coe
Documentation

Coercing a prime outside the modulus support recovers its prime fractional ideal.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem primeToModulusIdeal_coe
    (m : Modulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    (primeToModulusIdeal m v hv :
        FractionalIdealGroup K) =
      FractionalIdealGroup.prime v
def

finitePrimeToModulusSubgroup

L95 ↗
RayClass.finitePrimeToModulusSubgroup
Documentation

Finite ideles satisfying the higher-unit condition at every prime in the support of the modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def finitePrimeToModulusSubgroup (m : Modulus K) :
    Subgroup (FiniteIdeleGroup K) where
  carrier := {a | ∀ v, v ∈ m.finitePart.support →
    a v ∈ localHigherUnitGroup v (m.finitePart v)}
  one_mem' v _ := (localHigherUnitGroup v (m.finitePart v)).one_mem
  mul_mem' ha hb v hv :=
    (localHigherUnitGroup v (m.finitePart v)).mul_mem (ha v hv) (hb v hv)
  inv_mem' ha v hv :=
    (localHigherUnitGroup v (m.finitePart v)).inv_mem (ha v hv)
def

idelePrimeToModulusSubgroup

L107 ↗
RayClass.idelePrimeToModulusSubgroup
Documentation

Ideles satisfying the infinite positivity and finite higher-unit conditions of a modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def idelePrimeToModulusSubgroup (m : Modulus K) :
    Subgroup (IdeleGroup K)
theorem

localHigherUnitGroup_le_integralUnits

L112 ↗
RayClass.localHigherUnitGroup_le_integralUnits
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem localHigherUnitGroup_le_integralUnits
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    localHigherUnitGroup v n ≤
      (v.adicCompletionIntegers K).units
theorem

fractionalIdeal_mem_primeToModulusIdeals

L121 ↗
RayClass.fractionalIdeal_mem_primeToModulusIdeals
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem fractionalIdeal_mem_primeToModulusIdeals
    (m : Modulus K) (a : IdeleGroup K)
    (ha : a ∈ idelePrimeToModulusSubgroup m) :
    IdeleGroup.fractionalIdeal a ∈ primeToModulusIdeals m
def

primeToIdealMap

L137 ↗
RayClass.primeToIdealMap
Documentation

The fractional-ideal map restricted to ideles prime to a modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def primeToIdealMap (m : Modulus K) :
    idelePrimeToModulusSubgroup m →*
      primeToModulusIdeals m where
  toFun a :=
    ⟨IdeleGroup.fractionalIdeal a,
      fractionalIdeal_mem_primeToModulusIdeals m a a.property⟩
  map_one' := by
    apply Subtype.ext
    exact map_one _
  map_mul' a b := by
    apply Subtype.ext
    exact map_mul _ _ _
def

valuationVectorSectionPrimeTo

L153 ↗
RayClass.valuationVectorSectionPrimeTo
Documentation

A finite idele with a prescribed valuation vector away from the support of a modulus and value one on its support.

Source context 6 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in
Lean source · statement
def valuationVectorSectionPrimeTo
    (m : Modulus K)
  (e : HeightOneSpectrum (𝓞 K) →₀ ℤ) :
    FiniteIdeleGroup K
theorem

valuationVector_valuationVectorSectionPrimeTo

L169 ↗
RayClass.valuationVector_valuationVectorSectionPrimeTo
Source context 6 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in
Lean source · statement
theorem valuationVector_valuationVectorSectionPrimeTo
    (m : Modulus K)
    (e : HeightOneSpectrum (𝓞 K) →₀ ℤ)
    (he : ∀ v, v ∈ m.finitePart.support → e v = 0) :
    FiniteIdeleGroup.valuationVector
        (valuationVectorSectionPrimeTo m e) =
      Multiplicative.ofAdd e
theorem

primeToIdealMap_surjective

L196 ↗
RayClass.primeToIdealMap_surjective
Source context 6 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in
Lean source · statement
theorem primeToIdealMap_surjective (m : Modulus K) :
    Function.Surjective (primeToIdealMap m)
theorem

ideleCongruenceSubgroup_le_primeTo

L233 ↗
RayClass.ideleCongruenceSubgroup_le_primeTo
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem ideleCongruenceSubgroup_le_primeTo
    (m : Modulus K) :
    m.ideleCongruenceSubgroup ≤
      idelePrimeToModulusSubgroup m
def

congruenceSubgroupInPrimeTo

L242 ↗
RayClass.congruenceSubgroupInPrimeTo
Documentation

The congruence subgroup, viewed inside the subgroup of ideles prime to the modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def congruenceSubgroupInPrimeTo (m : Modulus K) :
    Subgroup (idelePrimeToModulusSubgroup m)
theorem

primeToIdealMap_ker

L248 ↗
RayClass.primeToIdealMap_ker
Source context 6 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in
Lean source · statement
theorem primeToIdealMap_ker (m : Modulus K) :
    (primeToIdealMap m).ker =
      congruenceSubgroupInPrimeTo m
def

quotientCongruenceEquivPrimeToIdeals

L280 ↗
RayClass.quotientCongruenceEquivPrimeToIdeals
Documentation

The quotient of ideles prime to a modulus by the congruence subgroup, identified with fractional ideals prime to the modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def quotientCongruenceEquivPrimeToIdeals (m : Modulus K) :
    idelePrimeToModulusSubgroup m ⧸
        congruenceSubgroupInPrimeTo m ≃*
      primeToModulusIdeals m
def

principalSubgroupInPrimeTo

L290 ↗
RayClass.principalSubgroupInPrimeTo
Documentation

Principal ideles satisfying the modulus conditions, considered inside I_K^(m).

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def principalSubgroupInPrimeTo (m : Modulus K) :
    Subgroup (idelePrimeToModulusSubgroup m)
def

principalRayIdealSubgroup

L297 ↗
RayClass.principalRayIdealSubgroup
Documentation

Principal ideals generated by a totally positive element congruent to one modulo the finite modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def principalRayIdealSubgroup (m : Modulus K) :
    Subgroup (primeToModulusIdeals m)
theorem

mem_principalRayIdealSubgroup_iff

L302 ↗
RayClass.mem_principalRayIdealSubgroup_iff
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem mem_principalRayIdealSubgroup_iff
    (m : Modulus K) (I : primeToModulusIdeals m) :
    I ∈ principalRayIdealSubgroup m ↔
      ∃ x : Kˣ,
        ∃ _hx : IdeleGroup.principalIdele K x ∈
          idelePrimeToModulusSubgroup m,
        toPrincipalIdeal (𝓞 K) K x =
          (I : FractionalIdealGroup K)
abbrev

IdealRayClassGroup

L336 ↗
RayClass.IdealRayClassGroup
Documentation

The ideal-theoretic ray class group J_K^m / P_K^m.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
abbrev IdealRayClassGroup (m : Modulus K)
def

idealRayProjection

L341 ↗
RayClass.idealRayProjection
Documentation

The canonical projection from ideles prime to the modulus to the ideal-theoretic ray class group.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def idealRayProjection (m : Modulus K) :
    idelePrimeToModulusSubgroup m →*
      IdealRayClassGroup m
def

raySubgroupInPrimeTo

L349 ↗
RayClass.raySubgroupInPrimeTo
Documentation

The subgroup generated by congruence ideles and principal ideles inside the ideles prime to a modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def raySubgroupInPrimeTo (m : Modulus K) :
    Subgroup (idelePrimeToModulusSubgroup m)
theorem

idealRayProjection_surjective

L354 ↗
RayClass.idealRayProjection_surjective
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem idealRayProjection_surjective (m : Modulus K) :
    Function.Surjective (idealRayProjection m)
theorem

idealRayProjection_ker

L363 ↗
RayClass.idealRayProjection_ker
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem idealRayProjection_ker (m : Modulus K) :
    (idealRayProjection m).ker =
      raySubgroupInPrimeTo m
def

quotientRaySubgroupEquivIdealRayClassGroup

L402 ↗
RayClass.quotientRaySubgroupEquivIdealRayClassGroup
Documentation

The quotient of ideles prime to the modulus by the full ray subgroup, identified with the ideal-theoretic ray class group.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def quotientRaySubgroupEquivIdealRayClassGroup
    (m : Modulus K) :
    idelePrimeToModulusSubgroup m ⧸
        raySubgroupInPrimeTo m ≃*
      IdealRayClassGroup m
theorem

quotientRaySubgroupEquivIdealRayClassGroup_mk

L416 ↗
RayClass.quotientRaySubgroupEquivIdealRayClassGroup_mk
Documentation

The quotient equivalence induced by the ideal-ray projection evaluates on the class of a prime-to-modulus idele as the original projection.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem quotientRaySubgroupEquivIdealRayClassGroup_mk
    (m : Modulus K) (a : idelePrimeToModulusSubgroup m) :
    quotientRaySubgroupEquivIdealRayClassGroup m
        (QuotientGroup.mk' (raySubgroupInPrimeTo m) a) =
      idealRayProjection m a
abbrev

ApproximationPlace

L429 ↗
RayClass.ApproximationPlace
Documentation

The finite primes in m, together with all infinite places.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
abbrev ApproximationPlace (m : Modulus K)
abbrev

approximationAbsoluteValue

L433 ↗
RayClass.approximationAbsoluteValue
Documentation

The absolute value represented by an approximation place.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
abbrev approximationAbsoluteValue (m : Modulus K) :
    ApproximationPlace m → AbsoluteValue K ℝ
  | Sum.inl v => NumberField.HeightOneSpectrum.adicAbv K v.1
  | Sum.inr w => w.1
theorem

adicAbv_isNontrivial

L438 ↗
RayClass.adicAbv_isNontrivial
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem adicAbv_isNontrivial
    (v : HeightOneSpectrum (𝓞 K)) :
    (NumberField.HeightOneSpectrum.adicAbv K v).IsNontrivial
theorem

adicAbv_not_isEquiv_of_ne

L449 ↗
RayClass.adicAbv_not_isEquiv_of_ne
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem adicAbv_not_isEquiv_of_ne
    {v w : HeightOneSpectrum (𝓞 K)} (hvw : v ≠ w) :
    ¬ (NumberField.HeightOneSpectrum.adicAbv K v).IsEquiv
      (NumberField.HeightOneSpectrum.adicAbv K w)
theorem

adicAbv_not_isEquiv_infinitePlace

L473 ↗
RayClass.adicAbv_not_isEquiv_infinitePlace
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem adicAbv_not_isEquiv_infinitePlace
    (v : HeightOneSpectrum (𝓞 K)) (w : InfinitePlace K) :
    ¬ (NumberField.HeightOneSpectrum.adicAbv K v).IsEquiv w.1
theorem

approximationAbsoluteValue_isNontrivial

L487 ↗
RayClass.approximationAbsoluteValue_isNontrivial
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem approximationAbsoluteValue_isNontrivial
    (m : Modulus K) :
    ∀ i, (approximationAbsoluteValue m i).IsNontrivial
  | Sum.inl v => by
      change
        (NumberField.HeightOneSpectrum.adicAbv K v.1).IsNontrivial
      exact adicAbv_isNontrivial v.1
  | Sum.inr w => by
      change w.1.IsNontrivial
      exact w.isNontrivial
theorem

approximationAbsoluteValue_pairwise

L498 ↗
RayClass.approximationAbsoluteValue_pairwise
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem approximationAbsoluteValue_pairwise
    (m : Modulus K) :
    Pairwise fun i j =>
      ¬ (approximationAbsoluteValue m i).IsEquiv
        (approximationAbsoluteValue m j) := by
  intro i j hij
  cases i with
  | inl v =>
      cases j with
      | inl w =>
          apply adicAbv_not_isEquiv_of_ne
          intro hvw
          apply hij
          exact congrArg Sum.inl (Subtype.ext hvw)
      | inr w =>
          exact adicAbv_not_isEquiv_infinitePlace v.1 w
  | inr v =>
      cases j with
      | inl w =>
          exact fun h =>
            adicAbv_not_isEquiv_infinitePlace w.1 v h.symm
      | inr w =>
          intro h
          apply hij
          congr
          change v.1.IsEquiv w.1 at h
          exact
            (InfinitePlace.eq_iff_isEquiv (K := K)).mpr h
abbrev

approximationCompletion

L528 ↗
RayClass.approximationCompletion
Documentation

The corresponding product of local completions.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
abbrev approximationCompletion (m : Modulus K) :
    ApproximationPlace m → Type _
  | Sum.inl v => v.1.adicCompletion K
  | Sum.inr w => w.Completion
instance

approximationCompletionTopologicalSpace

L533 ↗
RayClass.approximationCompletionTopologicalSpace
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
instance approximationCompletionTopologicalSpace
    (m : Modulus K) (i : ApproximationPlace m) :
    TopologicalSpace (approximationCompletion m i)
def

approximationCompletionMap

L539 ↗
RayClass.approximationCompletionMap
Documentation

Coordinatewise completion of the valued copies of K.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def approximationCompletionMap (m : Modulus K) :
    ∀ i : ApproximationPlace m,
      WithAbs (approximationAbsoluteValue m i) →
        approximationCompletion m i
  | Sum.inl v =>
      fun x =>
        FinitePlace.embedding v.1
          (WithAbs.equiv
            (NumberField.HeightOneSpectrum.adicAbv K v.1) x)
  | Sum.inr w => fun x => (x : w.Completion)
theorem

denseRange_finiteApproximationCompletionMap

L550 ↗
RayClass.denseRange_finiteApproximationCompletionMap
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem denseRange_finiteApproximationCompletionMap
    (v : HeightOneSpectrum (𝓞 K)) :
    DenseRange
      (fun x :
          WithAbs (NumberField.HeightOneSpectrum.adicAbv K v) =>
        FinitePlace.embedding v
          (WithAbs.equiv
            (NumberField.HeightOneSpectrum.adicAbv K v) x)) := by
  have hrange :
      Set.range
          (fun x :
              WithAbs (NumberField.HeightOneSpectrum.adicAbv K v) =>
            FinitePlace.embedding v
              (WithAbs.equiv
                (NumberField.HeightOneSpectrum.adicAbv K v) x)) =
        Set.range (algebraMap K (v.adicCompletion K)) := by
    ext y
    constructor
    · rintro ⟨x, rfl⟩
      exact
        ⟨WithAbs.equiv
            (NumberField.HeightOneSpectrum.adicAbv K v) x, rfl⟩
    · rintro ⟨x, rfl⟩
      refine
        ⟨(WithAbs.equiv
            (NumberField.HeightOneSpectrum.adicAbv K v)).symm x, ?_⟩
      rfl
  rw [DenseRange, hrange]
  exact v.denseRange_algebraMap K
theorem

continuous_finiteApproximationCompletionMap

L580 ↗
RayClass.continuous_finiteApproximationCompletionMap
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem continuous_finiteApproximationCompletionMap
    (v : HeightOneSpectrum (𝓞 K)) :
    Continuous
      (fun x :
          WithAbs (NumberField.HeightOneSpectrum.adicAbv K v) =>
        FinitePlace.embedding v
          (WithAbs.equiv
            (NumberField.HeightOneSpectrum.adicAbv K v) x)) := by
  apply Isometry.continuous
  apply Isometry.of_dist_eq
  intro x y
  rw [dist_eq_norm, dist_eq_norm, ← map_sub,
    FinitePlace.norm_embedding]
  rfl
theorem

denseRange_approximationCompletionMap

L595 ↗
RayClass.denseRange_approximationCompletionMap
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem denseRange_approximationCompletionMap
    (m : Modulus K) :
    ∀ i, DenseRange (approximationCompletionMap m i)
  | Sum.inl v => denseRange_finiteApproximationCompletionMap v.1
  | Sum.inr w =>
      NumberField.InfinitePlace.Completion.denseRange_coe w
theorem

continuous_approximationCompletionMap

L602 ↗
RayClass.continuous_approximationCompletionMap
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem continuous_approximationCompletionMap
    (m : Modulus K) :
    ∀ i, Continuous (approximationCompletionMap m i)
  | Sum.inl v => continuous_finiteApproximationCompletionMap v.1
  | Sum.inr w =>
      NumberField.InfinitePlace.Completion.continuous_coe w
def

approximationEmbedding

L611 ↗
RayClass.approximationEmbedding
Documentation

The diagonal embedding into the finite product of the relevant completions.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def approximationEmbedding (m : Modulus K) :
    K → (i : ApproximationPlace m) → approximationCompletion m i
theorem

approximationEmbedding_finite

L619 ↗
RayClass.approximationEmbedding_finite
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem approximationEmbedding_finite
    (m : Modulus K) (x : K) (v : ↥m.finitePart.support) :
    approximationEmbedding m x (Sum.inl v) =
      FinitePlace.embedding v.1 x
theorem

approximationEmbedding_infinite

L626 ↗
RayClass.approximationEmbedding_infinite
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem approximationEmbedding_infinite
    (m : Modulus K) (x : K) (w : InfinitePlace K) :
    approximationEmbedding m x (Sum.inr w) =
      (x : w.Completion)
theorem

denseRange_approximationEmbedding

L632 ↗
RayClass.denseRange_approximationEmbedding
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem denseRange_approximationEmbedding (m : Modulus K) :
    DenseRange (approximationEmbedding m)
def

unitRatioSet

L644 ↗
RayClass.unitRatioSet
Documentation

The open set of field elements whose ratio with a fixed unit lies in a prescribed open unit set.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def unitRatioSet
    {F : Type*} [Field F] (a : Fˣ) (U : Subgroup Fˣ) :
    Set F
theorem

isOpen_unitRatioSet

L650 ↗
RayClass.isOpen_unitRatioSet
Documentation

The unit-ratio set associated to an open set of units is open.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem isOpen_unitRatioSet
    {F : Type*} [Field F] [TopologicalSpace F]
    [IsTopologicalRing F] [ContinuousInv₀ F] [T1Space F]
    (a : Fˣ) (U : Subgroup Fˣ)
    (hU : IsOpen (U : Set Fˣ)) :
    IsOpen (unitRatioSet a U)
theorem

val_mem_unitRatioSet

L660 ↗
RayClass.val_mem_unitRatioSet
Documentation

The value of the distinguished unit belongs to its unit-ratio set.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem val_mem_unitRatioSet
    {F : Type*} [Field F] (a : Fˣ) (U : Subgroup Fˣ) :
    (a : F) ∈ unitRatioSet a U
def

approximationTarget

L666 ↗
RayClass.approximationTarget
Documentation

The open local conditions that make a / x prime to m.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def approximationTarget (m : Modulus K) (a : IdeleGroup K) :
    ∀ i : ApproximationPlace m, Set (approximationCompletion m i)
  | Sum.inl v =>
      unitRatioSet (a.2 v.1)
        (localHigherUnitGroup v.1 (m.finitePart v.1))
  | Sum.inr w =>
      unitRatioSet
        (ContinuousMulEquiv.piUnits a.1 w)
        (m.localInfiniteCongruenceSubgroup w)
theorem

isOpen_approximationTarget

L676 ↗
RayClass.isOpen_approximationTarget
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
theorem isOpen_approximationTarget
    (m : Modulus K) (a : IdeleGroup K) :
    ∀ i, IsOpen (approximationTarget m a i)
  | Sum.inl v => by
      change IsOpen
        (unitRatioSet (a.2 v.1)
          (localHigherUnitGroup v.1 (m.finitePart v.1)))
      exact isOpen_unitRatioSet _ _
        (isOpen_localHigherUnitGroup v.1 (m.finitePart v.1))
  | Sum.inr w => by
      change IsOpen
        (unitRatioSet
          (ContinuousMulEquiv.piUnits a.1 w)
          (m.localInfiniteCongruenceSubgroup w))
      apply isOpen_unitRatioSet _ _
      classical
      by_cases hw : w.IsReal
      · by_cases hmem : (⟨w, hw⟩ : RealPlace K) ∈ m.infinitePart
        · rw [Modulus.localInfiniteCongruenceSubgroup,
            dite_eq_left hw, dite_eq_left hmem]
          exact isOpen_infinitePositiveSubgroup w
        · rw [Modulus.localInfiniteCongruenceSubgroup,
            dite_eq_left hw, dite_eq_right hmem]
          exact isOpen_univ
      · rw [Modulus.localInfiniteCongruenceSubgroup, dite_eq_right hw]
        exact isOpen_univ
def

approximationTargetPoint

L705 ↗
RayClass.approximationTargetPoint
Documentation

The given idele itself lies in the product of its approximation neighborhoods.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · full declaration
def approximationTargetPoint
    (m : Modulus K) (a : IdeleGroup K) :
    (i : ApproximationPlace m) → approximationCompletion m i
  | Sum.inl v => (a.2 v.1 : v.1.adicCompletion K)
  | Sum.inr w =>
      (ContinuousMulEquiv.piUnits a.1 w : w.Completion)
theorem

approximationTargetPoint_mem

L712 ↗
RayClass.approximationTargetPoint_mem
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem approximationTargetPoint_mem
    (m : Modulus K) (a : IdeleGroup K) :
    approximationTargetPoint m a ∈
      Set.univ.pi (approximationTarget m a)
theorem

exists_principal_quotient_mem_primeTo

L725 ↗
RayClass.exists_principal_quotient_mem_primeTo
Documentation

Weak approximation in the precise open local cosets required by the modulus.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem exists_principal_quotient_mem_primeTo
    (m : Modulus K) (a : IdeleGroup K) :
    ∃ x : Kˣ,
      a * (IdeleGroup.principalIdele K x)⁻¹ ∈
        idelePrimeToModulusSubgroup m
theorem

idelePrimeToModulusSubgroup_sup_principalSubgroup

L819 ↗
RayClass.idelePrimeToModulusSubgroup_sup_principalSubgroup
Documentation

Approximation identifies the idele group as I_K = I_K^(m) Kˣ.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem idelePrimeToModulusSubgroup_sup_principalSubgroup
    (m : Modulus K) :
    idelePrimeToModulusSubgroup m ⊔
        IdeleGroup.principalSubgroup K =
      ⊤
def

primeToRayClassProjection

L836 ↗
RayClass.primeToRayClassProjection
Documentation

The natural map from the prime-to-m ideles to the full idelic ray-class quotient.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def primeToRayClassProjection (m : Modulus K) :
    idelePrimeToModulusSubgroup m →*
      IdeleGroup K ⧸
        (m.ideleCongruenceSubgroup ⊔
          IdeleGroup.principalSubgroup K)
theorem

primeToRayClassProjection_ker

L846 ↗
RayClass.primeToRayClassProjection_ker
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem primeToRayClassProjection_ker (m : Modulus K) :
    (primeToRayClassProjection m).ker =
      raySubgroupInPrimeTo m
theorem

primeToRayClassProjection_surjective

L907 ↗
RayClass.primeToRayClassProjection_surjective
Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem primeToRayClassProjection_surjective (m : Modulus K) :
    Function.Surjective (primeToRayClassProjection m)
def

quotientRaySubgroupEquivIdeleRayQuotient

L951 ↗
RayClass.quotientRaySubgroupEquivIdeleRayQuotient
Documentation

Restricting the full idelic ray-class quotient to prime-to-m ideles is an equivalence.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def quotientRaySubgroupEquivIdeleRayQuotient
    (m : Modulus K) :
    idelePrimeToModulusSubgroup m ⧸
        raySubgroupInPrimeTo m ≃*
      IdeleGroup K ⧸
        (m.ideleCongruenceSubgroup ⊔
          IdeleGroup.principalSubgroup K)
theorem

quotientRaySubgroupEquivIdeleRayQuotient_mk

L967 ↗
RayClass.quotientRaySubgroupEquivIdeleRayQuotient_mk
Documentation

The quotient equivalence induced by the idelic ray projection evaluates on a prime-to-modulus idele class as the original projection.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
theorem quotientRaySubgroupEquivIdeleRayQuotient_mk
    (m : Modulus K) (a : idelePrimeToModulusSubgroup m) :
    quotientRaySubgroupEquivIdeleRayQuotient m
        (QuotientGroup.mk' (raySubgroupInPrimeTo m) a) =
      primeToRayClassProjection m a
def

rayClassGroupEquivIdealRayClassGroup

L979 ↗
RayClass.rayClassGroupEquivIdealRayClassGroup
Documentation

The idelic and ideal-theoretic ray class groups are canonically multiplicatively equivalent.

Source context 5 commands

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

open scoped NumberField WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
Lean source · statement
def rayClassGroupEquivIdealRayClassGroup
    (m : Modulus K) :
    RayClassGroup m ≃* IdealRayClassGroup m

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