NYLL
Module

NormOneCompact.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormOneCompact
43 declarations indexed from sourceView source ↗

Module documentation

Compactness of norm-one idele classes

This module combines local compactness, the logarithmic unit lattice, and the principal-idele norm formula to prove compactness of the norm-one subgroup of the idele class group.

Imports7
Imported by7

Declarations

def

integralStructureMap

L38 ↗
FiniteIdeleGroup.integralStructureMap
Documentation

The product of all local integral-unit groups, embedded in the finite idele group.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup
Lean source · statement
def integralStructureMap :
    (∀ v : HeightOneSpectrum (𝓞 K),
      (v.adicCompletionIntegers K).units) → FiniteIdeleGroup K
theorem

range_integralStructureMap

L47 ↗
FiniteIdeleGroup.range_integralStructureMap
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup
Lean source · statement
theorem range_integralStructureMap :
    Set.range (integralStructureMap (K := K)) =
      (integralSubgroup (K := K) : Set (FiniteIdeleGroup K))
theorem

isCompact_integralSubgroup

L61 ↗
FiniteIdeleGroup.isCompact_integralSubgroup
Documentation

The everywhere integral finite ideles form a compact group.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup
Lean source · statement
theorem isCompact_integralSubgroup :
    IsCompact
      ((integralSubgroup (K := K) :
        Subgroup (FiniteIdeleGroup K)) : Set (FiniteIdeleGroup K))
def

localAnnulus

L91 ↗
InfiniteIdeleGroup.localAnnulus
Documentation

A compact annulus in one archimedean local multiplicative group.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
def localAnnulus (w : InfinitePlace K) (B : ℝ) :
    Set w.Completionˣ
theorem

isCompact_localAnnulus

L97 ↗
InfiniteIdeleGroup.isCompact_localAnnulus
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
omit [NumberField K] in
Lean source · statement
theorem isCompact_localAnnulus (w : InfinitePlace K) (B : ℝ) :
    IsCompact (localAnnulus w B)
def

annulus

L149 ↗
InfiniteIdeleGroup.annulus
Documentation

A compact product of local archimedean annuli.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
def annulus (B : ℝ) : Set (InfiniteIdeleGroup K)
theorem

isCompact_annulus

L154 ↗
InfiniteIdeleGroup.isCompact_annulus
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
omit [NumberField K] in
Lean source · statement
theorem isCompact_annulus (B : ℝ) :
    IsCompact (annulus (K := K) B)
theorem

mem_annulus_iff

L161 ↗
InfiniteIdeleGroup.mem_annulus_iff
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
omit [NumberField K] in
Lean source · statement
theorem mem_annulus_iff (a : InfiniteIdeleGroup K) (B : ℝ) :
    a ∈ annulus (K := K) B ↔
      ∀ w : InfinitePlace K,
        Real.exp (-B) ≤
            ‖((component w a : w.Completionˣ) : w.Completion)‖ ∧
          ‖((component w a : w.Completionˣ) : w.Completion)‖ ≤
            Real.exp B
theorem

continuous_archimedeanNorm

L180 ↗
InfiniteIdeleGroup.continuous_archimedeanNorm
Documentation

The archimedean norm is continuous.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
theorem continuous_archimedeanNorm :
    Continuous (archimedeanNorm (K := K))
def

logNorm

L197 ↗
InfiniteIdeleGroup.logNorm
Documentation

The logarithms of the normalized archimedean absolute values, with the distinguished place omitted as in Dirichlet's unit theorem.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
def logNorm (a : InfiniteIdeleGroup K) :
    logSpace K
theorem

logNorm_mul

L203 ↗
InfiniteIdeleGroup.logNorm_mul
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
theorem logNorm_mul (a b : InfiniteIdeleGroup K) :
    logNorm (a * b) = logNorm a + logNorm b
def

ringUnitToFieldUnit

L218 ↗
InfiniteIdeleGroup.ringUnitToFieldUnit
Documentation

Ring-of-integers units, viewed as units of the number field.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
def ringUnitToFieldUnit :
    (𝓞 K)ˣ →* Kˣ
theorem

norm_infiniteComponent_principalIdele

L222 ↗
InfiniteIdeleGroup.norm_infiniteComponent_principalIdele
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
theorem norm_infiniteComponent_principalIdele (x : Kˣ)
    (w : InfinitePlace K) :
    ‖((component w (IdeleGroup.principalIdele K x).1 :
        w.Completionˣ) : w.Completion)‖ =
      w (x : K)
theorem

logNorm_principalRingUnit

L234 ↗
InfiniteIdeleGroup.logNorm_principalRingUnit
Documentation

On an algebraic integer unit, the archimedean idele log is exactly Dirichlet's logarithmic embedding.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
Lean source · statement
theorem logNorm_principalRingUnit (u : (𝓞 K)ˣ) :
    logNorm (IdeleGroup.principalIdele K
        (ringUnitToFieldUnit (K := K) u)).1 =
      NumberField.Units.logEmbedding K (Additive.ofMul u)
theorem

logNorm_component_le

L244 ↗
InfiniteIdeleGroup.logNorm_component_le
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · full declaration
theorem logNorm_component_le {r : ℝ} (a : InfiniteIdeleGroup K)
    (h : ‖logNorm a‖ ≤ r)
    (w : {w : InfinitePlace K //
      w ≠ w₀ (K := K)}) :
    |logNorm a w| ≤ r := by
  simpa only [Real.norm_eq_abs] using
    (norm_le_pi_norm (logNorm a) w).trans h
theorem

sum_logNorm_eq_neg_distinguished

L255 ↗
InfiniteIdeleGroup.sum_logNorm_eq_neg_distinguished
Documentation

If the total archimedean norm is one, the omitted logarithmic coordinate is the negative sum of all the other coordinates.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · statement
theorem sum_logNorm_eq_neg_distinguished
    (a : InfiniteIdeleGroup K)
    (ha : archimedeanNorm a = 1) :
    ∑ w, logNorm a w =
      -(w₀ (K := K)).mult *
        Real.log
          ‖((component (w₀ (K := K)) a :
              (w₀ (K := K)).Completionˣ) :
            (w₀ (K := K)).Completion)‖
theorem

abs_log_norm_component_le

L316 ↗
InfiniteIdeleGroup.abs_log_norm_component_le
Documentation

A norm bound in the logarithmic space bounds every local logarithm. The harmless factor #S∞ also covers the omitted coordinate.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · full declaration
theorem abs_log_norm_component_le
    {r : ℝ} (hr : 0 ≤ r) (a : InfiniteIdeleGroup K)
    (hlog : ‖logNorm a‖ ≤ r)
    (hnorm : archimedeanNorm a = 1)
    (w : InfinitePlace K) :
    |Real.log
        ‖((component w a : w.Completionˣ) : w.Completion)‖| ≤
      (Fintype.card (InfinitePlace K) : ℝ) * r := by
  have hmult :
      ∀ x : ℝ, 0 ≤ x → x ≤ w.mult * x := by
    intro x hx
    nth_rw 1 [← one_mul x]
    refine mul_le_mul ?_ le_rfl hx ?_
    all_goals
      rw [NumberField.InfinitePlace.mult]
      split_ifs <;> norm_num
  by_cases hw : w = w₀ (K := K)
  · have h := congrArg (‖·‖)
      (sum_logNorm_eq_neg_distinguished a hnorm).symm
    replace h := (le_of_eq h).trans (norm_sum_le _ _)
    simp_rw [norm_mul, norm_neg, Real.norm_eq_abs, Nat.abs_cast] at h
    refine (le_trans ?_ h).trans ?_
    · rw [← hw]
      exact hmult _ (abs_nonneg _)
    · refine (Finset.sum_le_card_nsmul _ _ _
          (fun v _ ↦ logNorm_component_le a hlog v)).trans ?_
      rw [nsmul_eq_mul]
      apply mul_le_mul_of_nonneg_right _ hr
      exact_mod_cast
        (Fintype.card_subtype_le
          (fun w : InfinitePlace K ↦ w ≠ w₀ (K := K)))
  · have h := logNorm_component_le a hlog ⟨w, hw⟩
    rw [logNorm, abs_mul, Nat.abs_cast] at h
    refine (le_trans ?_ h).trans ?_
    · exact hmult _ (abs_nonneg _)
    · nth_rw 1 [← one_mul r]
      exact mul_le_mul
        (Nat.one_le_cast.mpr Fintype.card_pos)
        le_rfl hr (Nat.cast_nonneg _)
theorem

mem_annulus_of_logNorm_le

L359 ↗
InfiniteIdeleGroup.mem_annulus_of_logNorm_le
Documentation

Exponentiating the preceding logarithmic estimate gives a compact annulus containing the idele.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · statement
theorem mem_annulus_of_logNorm_le
    {r : ℝ} (hr : 0 ≤ r) (a : InfiniteIdeleGroup K)
    (hlog : ‖logNorm a‖ ≤ r)
    (hnorm : archimedeanNorm a = 1) :
    a ∈ annulus (K := K)
      ((Fintype.card (InfinitePlace K) : ℝ) * r)
def

unitLatticeRealBasis

L407 ↗
InfiniteIdeleGroup.unitLatticeRealBasis
Documentation

A real basis obtained from the full unit lattice.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · statement
def unitLatticeRealBasis :
    Module.Basis
      (Module.Free.ChooseBasisIndex ℤ
        (NumberField.Units.unitLattice K))
      ℝ (logSpace K)
def

logFundamentalBound

L419 ↗
InfiniteIdeleGroup.logFundamentalBound
Documentation

An explicit uniform logarithmic bound for representatives modulo the ordinary unit lattice.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · statement
def logFundamentalBound : ℝ
theorem

logFundamentalBound_nonneg

L423 ↗
InfiniteIdeleGroup.logFundamentalBound_nonneg
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · statement
theorem logFundamentalBound_nonneg :
    0 ≤ logFundamentalBound (K := K)
theorem

exists_ringUnit_logNorm_le

L431 ↗
InfiniteIdeleGroup.exists_ringUnit_logNorm_le
Documentation

Every archimedean idele can be multiplied by an algebraic integer unit so that its logarithmic vector lies in a fixed bounded fundamental parallelepiped.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroup
open scoped Classical in
Lean source · statement
theorem exists_ringUnit_logNorm_le (a : InfiniteIdeleGroup K) :
    ∃ u : (𝓞 K)ˣ,
      ‖logNorm
          (a * (IdeleGroup.principalIdele K
            (ringUnitToFieldUnit (K := K) u)).1)‖ ≤
        logFundamentalBound (K := K)
theorem

principalRingUnit_mem_integralAtFinitePlaces

L478 ↗
IdeleGroup.principalRingUnit_mem_integralAtFinitePlaces
Documentation

A principal idele coming from a unit of the ring of integers is integral at every finite place.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem principalRingUnit_mem_integralAtFinitePlaces
    (u : (𝓞 K)ˣ) :
    principalIdele K
        (InfiniteIdeleGroup.ringUnitToFieldUnit (K := K) u) ∈
      integralAtFinitePlaces (K := K)
theorem

finite_absoluteNorm_eq_one_of_integral

L495 ↗
IdeleGroup.finite_absoluteNorm_eq_one_of_integral
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem finite_absoluteNorm_eq_one_of_integral
    (a : FiniteIdeleGroup K)
    (ha : a ∈ FiniteIdeleGroup.integralSubgroup (K := K)) :
    FiniteIdeleGroup.absoluteNorm a = 1
theorem

archimedeanNorm_eq_one_of_normOne_integral

L509 ↗
IdeleGroup.archimedeanNorm_eq_one_of_normOne_integral
Documentation

For an idele which is integral at all finite places, the global norm-one condition is exactly the archimedean norm-one condition.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem archimedeanNorm_eq_one_of_normOne_integral
    (a : IdeleGroup K)
    (hnorm : a ∈ normOneSubgroup (K := K))
    (hintegral :
      a.2 ∈ FiniteIdeleGroup.integralSubgroup (K := K)) :
    InfiniteIdeleGroup.archimedeanNorm a.1 = 1
def

compactIntegralNormOneSet

L523 ↗
IdeleGroup.compactIntegralNormOneSet
Documentation

The fixed compact set of norm-one ideles which are integral at every finite place and logarithmically reduced modulo the ordinary units.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
def compactIntegralNormOneSet : Set (IdeleGroup K)
theorem

isCompact_compactIntegralNormOneSet

L531 ↗
IdeleGroup.isCompact_compactIntegralNormOneSet
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem isCompact_compactIntegralNormOneSet :
    IsCompact (compactIntegralNormOneSet (K := K))
theorem

mem_compactIntegralNormOneSet_iff

L542 ↗
IdeleGroup.mem_compactIntegralNormOneSet_iff
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem mem_compactIntegralNormOneSet_iff (a : IdeleGroup K) :
    a ∈ compactIntegralNormOneSet (K := K) ↔
      a.1 ∈ InfiniteIdeleGroup.annulus (K := K)
          ((Fintype.card (InfinitePlace K) : ℝ) *
            InfiniteIdeleGroup.logFundamentalBound (K := K)) ∧
        a.2 ∈ FiniteIdeleGroup.integralSubgroup (K := K) ∧
        InfiniteIdeleGroup.archimedeanNorm a.1 = 1
theorem

exists_compactIntegralNormOneSet_representative

L560 ↗
IdeleGroup.exists_compactIntegralNormOneSet_representative
Documentation

A norm-one idele integral at every finite place is principal-equivalent to an element of the fixed compact representative set.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
open scoped Classical in
Lean source · statement
theorem exists_compactIntegralNormOneSet_representative
    (a : IdeleGroup K)
    (hnorm : a ∈ normOneSubgroup (K := K))
    (hintegral :
      a.2 ∈ FiniteIdeleGroup.integralSubgroup (K := K)) :
    ∃ b ∈ compactIntegralNormOneSet (K := K),
      QuotientGroup.mk' (principalSubgroup K) b =
        QuotientGroup.mk' (principalSubgroup K) a
def

normOneIdealClassRepresentative

L620 ↗
IdeleGroup.normOneIdealClassRepresentative
Documentation

For every ordinary ideal class which occurs on a norm-one idele, choose one such representative; use 1 for the (irrelevant) remaining classes.

Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
open scoped Classical in
Lean source · statement
def normOneIdealClassRepresentative
    (c : ClassGroup (𝓞 K)) : IdeleGroup K
theorem

normOneIdealClassRepresentative_mem

L629 ↗
IdeleGroup.normOneIdealClassRepresentative_mem
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
open scoped Classical in
Lean source · statement
theorem normOneIdealClassRepresentative_mem
    (c : ClassGroup (𝓞 K)) :
    normOneIdealClassRepresentative (K := K) c ∈
      normOneSubgroup (K := K)
theorem

idealClass_normOneIdealClassRepresentative

L639 ↗
IdeleGroup.idealClass_normOneIdealClassRepresentative
Source context 7 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
open scoped Classical in
Lean source · statement
theorem idealClass_normOneIdealClassRepresentative
    (c : ClassGroup (𝓞 K))
    (h : ∃ a : IdeleGroup K,
      a ∈ normOneSubgroup (K := K) ∧ idealClass a = c) :
    idealClass (normOneIdealClassRepresentative (K := K) c) = c
def

normOneIdealClassRepresentativeSet

L649 ↗
IdeleGroup.normOneIdealClassRepresentativeSet
Documentation

The finite set of chosen norm-one representatives of ordinary ideal classes.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
def normOneIdealClassRepresentativeSet : Set (IdeleGroup K)
theorem

isCompact_normOneIdealClassRepresentativeSet

L652 ↗
IdeleGroup.isCompact_normOneIdealClassRepresentativeSet
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem isCompact_normOneIdealClassRepresentativeSet :
    IsCompact (normOneIdealClassRepresentativeSet (K := K))
theorem

normOneIdealClassRepresentativeSet_subset_normOne

L657 ↗
IdeleGroup.normOneIdealClassRepresentativeSet_subset_normOne
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem normOneIdealClassRepresentativeSet_subset_normOne :
    normOneIdealClassRepresentativeSet (K := K) ⊆
      (normOneSubgroup (K := K) : Set (IdeleGroup K))
theorem

exists_integral_normOne_reduction

L666 ↗
IdeleGroup.exists_integral_normOne_reduction
Documentation

Remove the ordinary ideal class of a norm-one idele. The result is integral at every finite place, and multiplying back by the chosen representative recovers the original idele class.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem exists_integral_normOne_reduction
    (a : IdeleGroup K)
    (ha : a ∈ normOneSubgroup (K := K)) :
    ∃ b : IdeleGroup K,
      b.2 ∈ FiniteIdeleGroup.integralSubgroup (K := K) ∧
      b ∈ normOneSubgroup (K := K) ∧
      QuotientGroup.mk' (principalSubgroup K)
          (b * normOneIdealClassRepresentative
            (K := K) (idealClass a)) =
        QuotientGroup.mk' (principalSubgroup K) a
def

compactNormOneClassCover

L728 ↗
IdeleGroup.compactNormOneClassCover
Documentation

A compact set of ideles meeting every norm-one idele class.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
def compactNormOneClassCover : Set (IdeleGroup K)
theorem

isCompact_compactNormOneClassCover

L732 ↗
IdeleGroup.isCompact_compactNormOneClassCover
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem isCompact_compactNormOneClassCover :
    IsCompact (compactNormOneClassCover (K := K))
theorem

compactIntegralNormOneSet_subset_normOne

L739 ↗
IdeleGroup.compactIntegralNormOneSet_subset_normOne
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem compactIntegralNormOneSet_subset_normOne :
    compactIntegralNormOneSet (K := K) ⊆
      (normOneSubgroup (K := K) : Set (IdeleGroup K))
theorem

compactNormOneClassCover_subset_normOne

L749 ↗
IdeleGroup.compactNormOneClassCover_subset_normOne
Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup
Lean source · statement
theorem compactNormOneClassCover_subset_normOne :
    compactNormOneClassCover (K := K) ⊆
      (normOneSubgroup (K := K) : Set (IdeleGroup K))
theorem

image_compactNormOneClassCover

L763 ↗
IdeleClassGroup.image_compactNormOneClassCover
Documentation

The image of the compact idele cover is exactly the group of norm-one idele classes.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleClassGroup
Lean source · statement
theorem image_compactNormOneClassCover :
    (QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K)) ''
        IdeleGroup.compactNormOneClassCover (K := K) =
      (normOneSubgroup (K := K) : Set (IdeleClassGroup K))
theorem

normOneSubgroup_isCompact

L815 ↗
IdeleClassGroup.normOneSubgroup_isCompact
Documentation

The norm-one idele class group is compact.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleClassGroup
Lean source · statement
theorem normOneSubgroup_isCompact :
    IsCompact
      ((normOneSubgroup (K := K) :
        Subgroup (IdeleClassGroup K)) : Set (IdeleClassGroup K))
instance

normOneSubgroupCompactSpace

L825 ↗
IdeleClassGroup.normOneSubgroupCompactSpace
Documentation

Compact-space form of the compactness theorem for norm-one idele classes.

Source context 6 commands

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

open scoped NumberField Pointwise RestrictedProduct NNReal
open NumberField IsDedekindDomain
open NumberField.Units.dirichletUnitTheorem
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleClassGroup
Lean source · statement
instance normOneSubgroupCompactSpace :
    CompactSpace (normOneSubgroup (K := K))

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