Module

Approximation.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Approximation

22 declarations indexed from sourceView source ↗

Module documentation

Multiplicative weak approximation for ideles

This file extracts the simultaneous approximation statement needed for ray class groups. At finitely many finite places one may prescribe an arbitrary open multiplicative coset and move a given idele into all of those cosets by a single principal idele.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Ideal

Imported by6

def

modulusOfFinset

L33 ↗

IdeleGroup.modulusOfFinset

Documentation

The full modulus whose finite part has exponent one exactly at the places of a finite set and whose infinite part is empty. It lets the ray-class approximation space serve as an arbitrary finite-place approximation space.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def modulusOfFinset
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    RayClass.Modulus K

theorem

modulusOfFinset_apply

L46 ↗

IdeleGroup.modulusOfFinset_apply

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
open scoped Classical in

Lean source · full declaration

theorem modulusOfFinset_apply
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (v : HeightOneSpectrum (𝓞 K)) :
    (modulusOfFinset S).finitePart v = if v ∈ S then 1 else 0 := by
  classical
  rfl

theorem

modulusOfFinset_support

L54 ↗

IdeleGroup.modulusOfFinset_support

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem modulusOfFinset_support
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (modulusOfFinset S).finitePart.support = S

def

openLocalCosetTarget

L64 ↗

IdeleGroup.openLocalCosetTarget

Documentation

The product of the prescribed finite local cosets and harmless nonzero cosets at the infinite places. The latter ensure that the global approximating element is nonzero.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · full declaration

def openLocalCosetTarget
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ) :
    ∀ i : RayClass.ApproximationPlace m,
      Set (RayClass.approximationCompletion m i)
  | Sum.inl v => RayClass.unitRatioSet (a.2 v.1) (U v)
  | Sum.inr w =>
      RayClass.unitRatioSet
        (ContinuousMulEquiv.piUnits a.1 w) ⊤

theorem

isOpen_openLocalCosetTarget

L76 ↗

IdeleGroup.isOpen_openLocalCosetTarget

Documentation

Every coordinate of openLocalCosetTarget is open.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · full declaration

theorem isOpen_openLocalCosetTarget
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ)
    (hU : ∀ v, IsOpen (U v : Set (v.1.adicCompletion K)ˣ)) :
    ∀ i, IsOpen (openLocalCosetTarget m a U i)
  | Sum.inl v => by
      change IsOpen (RayClass.unitRatioSet (a.2 v.1) (U v))
      exact RayClass.isOpen_unitRatioSet _ _ (hU v)
  | Sum.inr w => by
      change IsOpen
        (RayClass.unitRatioSet
          (ContinuousMulEquiv.piUnits a.1 w) ⊤)
      exact RayClass.isOpen_unitRatioSet _ _ isOpen_univ

def

openLocalCosetTargetPoint

L93 ↗

IdeleGroup.openLocalCosetTargetPoint

Documentation

The given idele supplies a point in the product of the prescribed local cosets.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · full declaration

def openLocalCosetTargetPoint
    (m : RayClass.Modulus K) (a : IdeleGroup K) :
    (i : RayClass.ApproximationPlace m) →
      RayClass.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

openLocalCosetTargetPoint_mem

L103 ↗

IdeleGroup.openLocalCosetTargetPoint_mem

Documentation

The target product used for multiplicative weak approximation is nonempty.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem openLocalCosetTargetPoint_mem
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ) :
    openLocalCosetTargetPoint m a ∈
      Set.univ.pi (openLocalCosetTarget m a U)

theorem

exists_principal_quotient_mem_openLocalSubgroups

L122 ↗

IdeleGroup.exists_principal_quotient_mem_openLocalSubgroups

Documentation

Multiplicative weak approximation at finitely many finite places.

For arbitrary open subgroups U_v ≤ K_vˣ and an idele a, a single global element x ∈ Kˣ makes every local quotient a_v / x lie in U_v. This is the precise approximation input in the proof of the cyclic prime-power norm argument, and it is also used in roots-of-unity descent.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem exists_principal_quotient_mem_openLocalSubgroups
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ)
    (hU : ∀ v, IsOpen (U v : Set (v.1.adicCompletion K)ˣ)) :
    ∃ x : Kˣ, ∀ v : ↥m.finitePart.support,
      a.2 v.1 *
          ((principalIdele K x).2 v.1)⁻¹ ∈ U v

theorem

exists_principal_quotient_mem_openLocalSubgroups_finset

L180 ↗

IdeleGroup.exists_principal_quotient_mem_openLocalSubgroups_finset

Documentation

Finset-indexed form of multiplicative weak approximation.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem exists_principal_quotient_mem_openLocalSubgroups_finset
    (S : Finset (HeightOneSpectrum (𝓞 K))) (a : IdeleGroup K)
    (U : ∀ v : ↥S, Subgroup (v.1.adicCompletion K)ˣ)
    (hU : ∀ v, IsOpen (U v : Set (v.1.adicCompletion K)ˣ)) :
    ∃ x : Kˣ, ∀ v : ↥S,
      a.2 v.1 *
          ((principalIdele K x).2 v.1)⁻¹ ∈ U v

def

openAllLocalCosetTarget

L206 ↗

IdeleGroup.openAllLocalCosetTarget

Documentation

The product of prescribed open multiplicative cosets at every archimedean place and at the finite places in a modulus.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · full declaration

def openAllLocalCosetTarget
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ)
    (V : ∀ w : InfinitePlace K,
      Subgroup w.Completionˣ) :
    ∀ i : RayClass.ApproximationPlace m,
      Set (RayClass.approximationCompletion m i)
  | Sum.inl v => RayClass.unitRatioSet (a.2 v.1) (U v)
  | Sum.inr w =>
      RayClass.unitRatioSet
        (IdeleGroup.infiniteComponent w a) (V w)

theorem

isOpen_openAllLocalCosetTarget

L220 ↗

IdeleGroup.isOpen_openAllLocalCosetTarget

Documentation

Every coordinate of the all-place multiplicative target is open.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · full declaration

theorem isOpen_openAllLocalCosetTarget
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ)
    (V : ∀ w : InfinitePlace K,
      Subgroup w.Completionˣ)
    (hU : ∀ v, IsOpen
      (U v : Set (v.1.adicCompletion K)ˣ))
    (hV : ∀ w, IsOpen
      (V w : Set w.Completionˣ)) :
    ∀ i, IsOpen
      (openAllLocalCosetTarget m a U V i)
  | Sum.inl v => by
      change IsOpen
        (RayClass.unitRatioSet (a.2 v.1) (U v))
      exact RayClass.isOpen_unitRatioSet _ _ (hU v)
  | Sum.inr w => by
      change IsOpen
        (RayClass.unitRatioSet
          (IdeleGroup.infiniteComponent w a) (V w))
      exact RayClass.isOpen_unitRatioSet _ _ (hV w)

theorem

openLocalCosetTargetPoint_mem_all

L244 ↗

IdeleGroup.openLocalCosetTargetPoint_mem_all

Documentation

The given idele supplies a point in the simultaneous all-place multiplicative target.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem openLocalCosetTargetPoint_mem_all
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ)
    (V : ∀ w : InfinitePlace K,
      Subgroup w.Completionˣ) :
    openLocalCosetTargetPoint m a ∈
      Set.univ.pi
        (openAllLocalCosetTarget m a U V)

theorem

exists_principal_quotient_mem_openAllLocalSubgroups

L266 ↗

IdeleGroup.exists_principal_quotient_mem_openAllLocalSubgroups

Documentation

Multiplicative weak approximation simultaneously at all archimedean places and at the finite support of a modulus.

For prescribed open subgroups U_v ≤ K_vˣ and V_w ≤ K_wˣ, one global x ∈ Kˣ makes every quotient a_v / x lie in the corresponding subgroup.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem exists_principal_quotient_mem_openAllLocalSubgroups
    (m : RayClass.Modulus K) (a : IdeleGroup K)
    (U : ∀ v : ↥m.finitePart.support,
      Subgroup (v.1.adicCompletion K)ˣ)
    (V : ∀ w : InfinitePlace K,
      Subgroup w.Completionˣ)
    (hU : ∀ v, IsOpen
      (U v : Set (v.1.adicCompletion K)ˣ))
    (hV : ∀ w, IsOpen
      (V w : Set w.Completionˣ)) :
    ∃ x : Kˣ,
      (∀ v : ↥m.finitePart.support,
        a.2 v.1 *
            ((principalIdele K x).2 v.1)⁻¹ ∈ U v) ∧
      (∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a *
            (IdeleGroup.infiniteComponent w
              (principalIdele K x))⁻¹ ∈ V w)

theorem

exists_principal_quotient_mem_openAllLocalSubgroups_finset

L360 ↗

IdeleGroup.exists_principal_quotient_mem_openAllLocalSubgroups_finset

Documentation

Finset-indexed simultaneous finite-and-infinite multiplicative weak approximation.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem exists_principal_quotient_mem_openAllLocalSubgroups_finset
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : IdeleGroup K)
    (U : ∀ v : ↥S,
      Subgroup (v.1.adicCompletion K)ˣ)
    (V : ∀ w : InfinitePlace K,
      Subgroup w.Completionˣ)
    (hU : ∀ v, IsOpen
      (U v : Set (v.1.adicCompletion K)ˣ))
    (hV : ∀ w, IsOpen
      (V w : Set w.Completionˣ)) :
    ∃ x : Kˣ,
      (∀ v : ↥S,
        a.2 v.1 *
            ((principalIdele K x).2 v.1)⁻¹ ∈ U v) ∧
      (∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a *
            (IdeleGroup.infiniteComponent w
              (principalIdele K x))⁻¹ ∈ V w)

def

finiteIdeleOfFinset

L398 ↗

IdeleGroup.finiteIdeleOfFinset

Documentation

A finite local family, extended by 1, is a finite idele.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
open scoped Classical in

Lean source · statement

def finiteIdeleOfFinset
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ) :
    FiniteIdeleGroup K

theorem

finiteIdeleOfFinset_apply_mem

L418 ↗

IdeleGroup.finiteIdeleOfFinset_apply_mem

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem finiteIdeleOfFinset_apply_mem
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ)
    (v : ↥S) :
    finiteIdeleOfFinset S a v.1 = a v

theorem

finiteIdeleOfFinset_apply_notMem

L428 ↗

IdeleGroup.finiteIdeleOfFinset_apply_notMem

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem finiteIdeleOfFinset_apply_notMem
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ)
    (v : HeightOneSpectrum (𝓞 K)) (hv : v ∉ S) :
    finiteIdeleOfFinset S a v = 1

def

ideleOfFiniteLocalFamily

L440 ↗

IdeleGroup.ideleOfFiniteLocalFamily

Documentation

The idele whose prescribed finite components are a and whose other finite and all infinite components are 1.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def ideleOfFiniteLocalFamily
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ) :
    IdeleGroup K

theorem

ideleOfFiniteLocalFamily_finiteComponent

L447 ↗

IdeleGroup.ideleOfFiniteLocalFamily_finiteComponent

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem ideleOfFiniteLocalFamily_finiteComponent
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ)
    (v : ↥S) :
    (ideleOfFiniteLocalFamily S a).2 v.1 = a v

def

principalLocalQuotientMap

L456 ↗

IdeleGroup.principalLocalQuotientMap

Documentation

The diagonal map from Kˣ to a finite product of local multiplicative quotients.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def principalLocalQuotientMap
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (U : ∀ v : ↥S, Subgroup (v.1.adicCompletion K)ˣ) :
    Kˣ →* (∀ v : ↥S, (v.1.adicCompletion K)ˣ ⧸ U v)

theorem

principalLocalQuotientMap_apply

L465 ↗

IdeleGroup.principalLocalQuotientMap_apply

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem principalLocalQuotientMap_apply
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (U : ∀ v : ↥S, Subgroup (v.1.adicCompletion K)ˣ)
    (x : Kˣ) (v : ↥S) :
    principalLocalQuotientMap S U x v =
      QuotientGroup.mk' (U v) ((principalIdele K x).2 v.1)

theorem

principalLocalQuotientMap_surjective

L475 ↗

IdeleGroup.principalLocalQuotientMap_surjective

Documentation

Multiplicative weak approximation is equivalently surjectivity of the diagonal map to every finite product of quotients by open local subgroups.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem principalLocalQuotientMap_surjective
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (U : ∀ v : ↥S, Subgroup (v.1.adicCompletion K)ˣ)
    (hU : ∀ v, IsOpen (U v : Set (v.1.adicCompletion K)ˣ)) :
    Function.Surjective (principalLocalQuotientMap S U)

Module documentation

Multiplicative weak approximation for ideles

Declarations