Adeles and ideles

TheoremFinite residue field of a completed number ring#βœ“fully proved

Let \(K\) be a number field and \(v\) a nonzero prime ideal of its ring of integers \(\mathcal{O}_K\). The residue field of the ring of integers \(\mathcal{O}_v\) of the \(v\)-adic completion \(K_v\) of \(K\) is finite.

theorem finite_residueField (v : HeightOneSpectrum (π“ž K)) :
    Finite (IsLocalRing.ResidueField (v.adicCompletionIntegers K))
Uses 1 Β· Used by 2
Proof usesResidue field of the completion
Used byCompactness of the completed ring of integers Β· The local degree is the product of ramification index and inertia degree

TheoremCompactness of the completed ring of integers#βœ“fully proved

Let \(K\) be a number field and \(v\) a nonzero prime ideal of its ring of integers \(\mathcal{O}_K\). The ring of integers \(\mathcal{O}_v\) of the \(v\)-adic completion \(K_v\) of \(K\) is a compact subset of \(K_v\).

theorem isCompact_adicCompletionIntegers (v : HeightOneSpectrum (π“ž K)) :
    IsCompact (↑(v.adicCompletionIntegers K) : Set (v.adicCompletion K))
Uses 1 Β· Used by 1
Proof usesFinite residue field of a completed number ring
Used byCompactness of the local integral units

AbbreviationLocal integral unit subgroup#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), let \(v\) be a height-one prime of \(R\), and let \(\mathcal{O}_v\) be the ring of integers of the \(v\)-adic completion \(K_v\) of \(K\). The local integral unit subgroup is the subgroup \(\mathcal{O}_v^\times\) of \(K_v^\times\), consisting of the units \(u\) of \(K_v\) with \(u \in \mathcal{O}_v\) and \(u^{-1} \in \mathcal{O}_v\).

abbrev localIntegralUnitSubgroup (v : HeightOneSpectrum R) :
    Subgroup ((v.adicCompletion K)Λ£) :=
  (Submonoid.ofClass (v.adicCompletionIntegers K)).units
Used by 19
Used byAdelic norm Β· Formula for the adelic norm Β· Product formula for principal ideles Β· Finite idele group Β· Diagonal map into the finite ideles Β· Compactness of the local integral units Β· The local integral units are open Β· Membership in the norm-one ideles Β· Norm-one idele class group Β· Norm-one ideles Β· Principal ideles are trivial in the norm-one idele class group Β· Principal ideles of norm one Β· Diagonal map into the ideles Β· The diagonal map into the ideles is injective Β· Principal ideles Β· The principal ideles are discrete Β· Principal ideles have norm one Β· Topological idele class group Β· Ideles as units of the adele ring

DefinitionFinite idele group#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). For each height-one prime \(v\) of \(R\), let \(K_v\) be the \(v\)-adic completion of \(K\) and \(\mathcal{O}_v\) its ring of integers. The finite idele group is the restricted product of the unit groups \(K_v^\times\) over all height-one primes \(v\) of \(R\) with respect to the subgroups \(\mathcal{O}_v^\times\): the families \((x_v)_v\) with \(x_v \in K_v^\times\) for every \(v\) and \(x_v \in \mathcal{O}_v^\times\) for all but finitely many \(v\), with componentwise multiplication and the restricted-product topology.

def FiniteIdeleGroup :=
  Ξ Κ³ v : HeightOneSpectrum R,
    [(v.adicCompletion K)Λ£, localIntegralUnitSubgroup R K v]
Uses 1 Β· Used by 17
Statement usesLocal integral unit subgroup
Used byAdelic norm Β· Formula for the adelic norm Β· Product formula for principal ideles Β· Diagonal map into the finite ideles Β· Membership in the norm-one ideles Β· Norm-one idele class group Β· Norm-one ideles Β· Principal ideles are trivial in the norm-one idele class group Β· Principal ideles of norm one Β· Diagonal map into the ideles Β· The diagonal map into the ideles is injective Β· Principal ideles Β· The principal ideles are discrete Β· Principal ideles have norm one Β· Topological idele class group Β· Topological idele group Β· Ideles as units of the adele ring

TheoremThe local integral units are open#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), let \(v\) be a height-one prime of \(R\), and let \(\mathcal{O}_v\) be the ring of integers of the \(v\)-adic completion \(K_v\) of \(K\). Then \(\mathcal{O}_v^\times\) is an open subset of the unit group \(K_v^\times\).

theorem isOpen_localIntegralUnitSubgroup (v : HeightOneSpectrum R) :
    IsOpen (localIntegralUnitSubgroup R K v : Set ((v.adicCompletion K)Λ£))
Uses 1 Β· Used by 1
Statement usesLocal integral unit subgroup
Used byThe principal ideles are discrete

DefinitionInfinite idele group#βœ“fully proved

For a field \(K\), the infinite idele group is the product \(\prod_v K_v^\times\) of the unit groups of the completions \(K_v\) of \(K\) over all infinite places \(v\) of \(K\), with componentwise multiplication and the product topology.

def InfiniteIdeleGroup := (v : InfinitePlace K) β†’ (v.Completion)Λ£
Used by 17
Used byAdelic norm Β· Formula for the adelic norm Β· Product formula for principal ideles Β· Diagonal map into the infinite ideles Β· Membership in the norm-one ideles Β· Norm-one idele class group Β· Norm-one ideles Β· Principal ideles are trivial in the norm-one idele class group Β· Principal ideles of norm one Β· Diagonal map into the ideles Β· The diagonal map into the ideles is injective Β· Principal ideles Β· The principal ideles are discrete Β· Principal ideles have norm one Β· Topological idele class group Β· Topological idele group Β· Ideles as units of the adele ring

DefinitionTopological idele group#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). The topological idele group is the product \(\mathbb{I}_{K,\infty} \times \mathbb{I}_{K,f}\) of the infinite idele group \(\mathbb{I}_{K,\infty} = \prod_w K_w^\times\), the product of the unit groups of the completions of \(K\) at its infinite places \(w\), and the finite idele group \(\mathbb{I}_{K,f}\), the restricted product of the unit groups \(K_v^\times\) of the completions at the height-one primes \(v\) of \(R\) with respect to the integral unit groups \(\mathcal{O}_v^\times\). It carries the componentwise group structure and the product of the product topology on \(\mathbb{I}_{K,\infty}\) and the restricted-product topology on \(\mathbb{I}_{K,f}\).

As a group it is isomorphic to the unit group of the adele ring of \(K\), but its topology differs from the subspace topology on those units.

def TopologicalIdeleGroup :=
  (InfiniteIdeleGroup K Γ— FiniteIdeleGroup R K)
Uses 2 Β· Used by 15
Statement usesFinite idele group Β· Infinite idele group
Used byAdelic norm Β· Formula for the adelic norm Β· Product formula for principal ideles Β· Membership in the norm-one ideles Β· Norm-one idele class group Β· Norm-one ideles Β· Principal ideles are trivial in the norm-one idele class group Β· Principal ideles of norm one Β· Diagonal map into the ideles Β· The diagonal map into the ideles is injective Β· Principal ideles Β· The principal ideles are discrete Β· Principal ideles have norm one Β· Topological idele class group Β· Ideles as units of the adele ring

DefinitionDiagonal map into the infinite ideles#βœ“fully proved

For a field \(K\), this is the group homomorphism from \(K^\times\) to the infinite idele group of \(K\) that sends \(x\) to the family of its images in the completions \(K_v\) of \(K\), one for each infinite place \(v\) of \(K\).

def infinitePrincipalEmbedding : KΛ£ β†’* InfiniteIdeleGroup K :=
  MulEquiv.piUnits.toMonoidHom.comp <|
    Units.map (algebraMap K (InfiniteAdeleRing K)).toMonoidHom
Uses 1 Β· Used by 3
Statement usesInfinite idele group
Used byProduct formula for principal ideles Β· Diagonal map into the ideles Β· The principal ideles are discrete

DefinitionDiagonal map into the finite ideles#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). This is the group homomorphism from \(K^\times\) to the finite idele group of \(R\) and \(K\) that sends \(x\) to the family of its images in the \(v\)-adic completions \(K_v\) of \(K\), one for each height-one prime \(v\) of \(R\).

def finitePrincipalEmbedding : KΛ£ β†’* FiniteIdeleGroup R K :=
  (RestrictedProduct.unitsEquiv
    (fun v : HeightOneSpectrum R ↦ v.adicCompletion K)).toMonoidHom.comp <|
      FiniteAdeleRing.unitEmbedding R K
Uses 2 Β· Used by 3
Statement usesFinite idele group Β· Local integral unit subgroup
Used byProduct formula for principal ideles Β· Diagonal map into the ideles Β· The principal ideles are discrete

DefinitionDiagonal map into the ideles#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). This is the group homomorphism from \(K^\times\) to the topological idele group of \(R\) and \(K\) whose infinite component sends \(x\) to its images in the completions of \(K\) at all infinite places of \(K\), and whose finite component sends \(x\) to its images in the \(v\)-adic completions \(K_v\) of \(K\) at all height-one primes \(v\) of \(R\).

def principalEmbedding : KΛ£ β†’* TopologicalIdeleGroup R K :=
  (infinitePrincipalEmbedding K).prod (finitePrincipalEmbedding R K)
Uses 6 Β· Used by 6
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Diagonal map into the finite ideles Β· Diagonal map into the infinite ideles Β· Local integral unit subgroup
Used byProduct formula for principal ideles Β· Principal ideles are trivial in the norm-one idele class group Β· The diagonal map into the ideles is injective Β· Principal ideles Β· The principal ideles are discrete Β· Principal ideles have norm one

DefinitionPrincipal ideles#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). The subgroup of principal ideles is the image of the diagonal homomorphism from \(K^\times\) to the topological idele group of \(R\) and \(K\), which sends \(x\) to its images in the completions of \(K\) at all infinite places of \(K\) and at all height-one primes of \(R\).

def principalIdeles : Subgroup (TopologicalIdeleGroup R K) :=
  (principalEmbedding R K).range
Uses 5 Β· Used by 4
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Diagonal map into the ideles Β· Local integral unit subgroup
Used byPrincipal ideles of norm one Β· The principal ideles are discrete Β· Principal ideles have norm one Β· Topological idele class group

DefinitionIdeles as units of the adele ring#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\), and let \(\mathbb{A}_K\) be the adele ring of \(K\) built from the infinite places of \(K\) and the height-one primes of \(R\). For an infinite place \(w\) of \(K\) write \(K_w\) for the completion of \(K\) at \(w\), and for a height-one prime \(v\) of \(R\) write \(K_v\) for the \(v\)-adic completion of \(K\). This is the group isomorphism from the unit group \(\mathbb{A}_K^\times\) to the topological idele group that sends a unit adele \(a\) to the idele whose component at each infinite place \(w\) is the component \(a_w \in K_w^\times\) of \(a\) and whose component at each height-one prime \(v\) is the component \(a_v \in K_v^\times\) of \(a\).

It is stated only as an isomorphism of groups: the topological idele group carries the restricted-product topology, not the topology induced on the units of the adele ring.

def unitsEquiv :
    (AdeleRing R K)Λ£ ≃* TopologicalIdeleGroup R K :=
  MulEquiv.prodUnits.trans <| MulEquiv.prodCongr MulEquiv.piUnits <|
    RestrictedProduct.unitsEquiv (fun v : HeightOneSpectrum R ↦ v.adicCompletion K)
Uses 4 Β· Used by 1
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Local integral unit subgroup
Used byThe diagonal map into the ideles is injective

TheoremThe diagonal map into the ideles is injective#βœ“fully proved

Let \(K\) be a number field and let \(R\) be a Dedekind domain with fraction field \(K\). The diagonal homomorphism from \(K^\times\) to the topological idele group of \(R\) and \(K\), which sends \(x\) to its images in the completions of \(K\) at all infinite places of \(K\) and at all height-one primes of \(R\), is injective.

theorem principalEmbedding_injective [NumberField K] :
    Function.Injective (principalEmbedding R K)
Uses 6
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Diagonal map into the ideles Β· Local integral unit subgroup
Proof usesIdeles as units of the adele ring

AbbreviationTopological idele class group#βœ“fully proved

Let \(R\) be a Dedekind domain with fraction field \(K\). The topological idele class group is the quotient group of the topological idele group of \(R\) and \(K\) by its subgroup of principal ideles, the image of the diagonal homomorphism from \(K^\times\).

abbrev TopologicalIdeleClassGroup :=
  (TopologicalIdeleGroup R K) β§Έ (TopologicalIdeleGroup.principalIdeles R K)
Uses 5
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Principal ideles Β· Local integral unit subgroup

TheoremCompactness of the local integral units#βœ“fully proved

Let \(K\) be a number field, let \(v\) be a height-one prime of its ring of integers \(\mathcal{O}_K\), and let \(\mathcal{O}_v\) be the ring of integers of the \(v\)-adic completion \(K_v\) of \(K\). Then the local integral unit subgroup \(\mathcal{O}_v^\times\) is a compact subset of the unit group \(K_v^\times\).

It is the unit group of the compact valuation subring \(\mathcal{O}_v\).

theorem isCompact_localIntegralUnitSubgroup
    (v : HeightOneSpectrum (π“ž K)) :
    IsCompact (localIntegralUnitSubgroup (π“ž K) K v : Set ((v.adicCompletion K)Λ£))
Uses 2
Statement usesLocal integral unit subgroup
Proof usesCompactness of the completed ring of integers

DefinitionAdelic norm#βœ“fully proved

Let \(K\) be a number field with ring of integers \(\mathcal{O}_K\). For each infinite place \(w\) of \(K\) let \(K_w\) be the completion of \(K\) at \(w\), with the absolute value \(\|\cdot\|_w\) extending \(w\), and let \(m_w\) be \(1\) if \(w\) is real and \(2\) if \(w\) is complex. For each height-one prime \(v\) of \(\mathcal{O}_K\) let \(K_v\) be the \(v\)-adic completion of \(K\), with the normalized absolute value \(\|\cdot\|_v\). The adelic norm is the monoid homomorphism from the topological idele group of \(K\) over the Dedekind domain \(\mathcal{O}_K\) to the real numbers under multiplication that sends an idele \(a\), with components \(a_w \in K_w^\times\) and \(a_v \in K_v^\times\), to \(\bigl(\prod_w \|a_w\|_w^{m_w}\bigr) \cdot \prod_v \|a_v\|_v\), where the product over \(v\) is the product of its finitely many factors different from \(1\).

NumberField.TopologicalIdeleGroup.adelicNorm Β· 74 lines 
public noncomputable def adelicNorm : TopologicalIdeleGroup (π“ž K) K β†’* ℝ :=
  show (InfiniteIdeleGroup K Γ— FiniteIdeleGroup (π“ž K) K) β†’* ℝ from
  { toFun a :=
      (∏ w : InfinitePlace K, β€–(a.1 w : w.Completion)β€– ^ w.mult) *
        ∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
          β€–(a.2 v : v.adicCompletion K)β€–
    map_one' := by
      change
        (∏ w : InfinitePlace K, β€–(((1 : InfiniteIdeleGroup K) w : w.Completion))β€– ^ w.mult) *
        ∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
          β€–((((1 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€– = 1
      have hinf : (∏ w : InfinitePlace K,
          β€–(((1 : InfiniteIdeleGroup K) w : w.Completion))β€– ^ w.mult) = 1 := by
        apply Finset.prod_eq_one
        intro w _
        change β€–(((1 : InfiniteIdeleGroup K) w : w.Completion))β€– ^ w.mult = 1
        change β€–((1 : (w.Completion)Λ£) : w.Completion)β€– ^ w.mult = 1
        simp
      have hfin : (∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
          β€–((((1 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€–) = 1 := by
        have hfun : (fun v : IsDedekindDomain.HeightOneSpectrum (π“ž K) =>
            β€–((((1 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€–) =
            (fun _ => (1 : ℝ)) := by
          funext v
          change β€–((1 : (v.adicCompletion K)Λ£) : v.adicCompletion K)β€– = 1
          simp
        rw [hfun]
        exact finprod_one
      rw [hinf, hfin, mul_one]
    map_mul' := by
      intro a b
      have hinf : (∏ w : InfinitePlace K,
          β€–((((a.1 * b.1 : InfiniteIdeleGroup K) w : w.Completion)))β€– ^ w.mult) =
          (∏ w : InfinitePlace K, β€–((a.1 w : w.Completion))β€– ^ w.mult) *
            (∏ w : InfinitePlace K, β€–((b.1 w : w.Completion))β€– ^ w.mult) := by
        rw [← Finset.prod_mul_distrib]
        apply Finset.prod_congr rfl
        intro w _
        have hdef : (a.1 * b.1 : InfiniteIdeleGroup K) w = a.1 w * b.1 w := rfl
        rw [hdef, Units.val_mul, norm_mul, mul_pow]
      have hfmul : βˆ€ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
          β€–((((a.2 * b.2 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€– =
            β€–((a.2 v : v.adicCompletion K))β€– * β€–((b.2 v : v.adicCompletion K))β€– := by
        intro v
        have hdef : (a.2 * b.2 : FiniteIdeleGroup (π“ž K) K) v = a.2 v * b.2 v := rfl
        rw [hdef, Units.val_mul, norm_mul]
      have hfin : (∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
          β€–((((a.2 * b.2 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€–) =
          (∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
            β€–((a.2 v : v.adicCompletion K))β€–) *
          (∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
            β€–((b.2 v : v.adicCompletion K))β€–) := by
        have hfun : (fun v : IsDedekindDomain.HeightOneSpectrum (π“ž K) =>
            β€–((((a.2 * b.2 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€–) =
            (fun v => β€–((a.2 v : v.adicCompletion K))β€– *
              β€–((b.2 v : v.adicCompletion K))β€–) := by
          funext v
          exact hfmul v
        rw [hfun]
        exact finprod_mul_distrib (finite_mulSupport_norm K a.2)
          (finite_mulSupport_norm K b.2)
      change
        (∏ w : InfinitePlace K,
          β€–(((a.1 * b.1 : InfiniteIdeleGroup K) w : w.Completion))β€– ^ w.mult) *
          ∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
            β€–((((a.2 * b.2 : FiniteIdeleGroup (π“ž K) K) v : v.adicCompletion K)))β€– =
          ((∏ w : InfinitePlace K, β€–((a.1 w : w.Completion))β€– ^ w.mult) *
            ∏ᢠ (v : IsDedekindDomain.HeightOneSpectrum (π“ž K)),
              β€–((a.2 v : v.adicCompletion K))β€–) *
          ((∏ w : InfinitePlace K, β€–((b.1 w : w.Completion))β€– ^ w.mult) *
            ∏ᢠ (v : IsDedekindDomain.HeightOneSpectrum (π“ž K)),
              β€–((b.2 v : v.adicCompletion K))β€–)
      rw [hinf, hfin]
      ring }
Uses 4 Β· Used by 5
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Local integral unit subgroup
Used byFormula for the adelic norm Β· Product formula for principal ideles Β· Membership in the norm-one ideles Β· Norm-one ideles Β· Principal ideles have norm one

TheoremFormula for the adelic norm#βœ“fully proved

Let \(K\) be a number field. For every idele \(a\) of \(K\) (with \(R = \mathcal{O}_K\)), the adelic norm of \(a\) equals \(\bigl(\prod_w \|a_w\|_w^{m_w}\bigr) \cdot \prod_v \|a_v\|_v\), where \(w\) runs over the infinite places of \(K\), \(\|\cdot\|_w\) is the absolute value on the completion \(K_w\) extending \(w\), \(m_w\) is \(1\) for a real place and \(2\) for a complex place, \(v\) runs over the height-one primes of \(\mathcal{O}_K\), \(\|\cdot\|_v\) is the normalized absolute value on the completion \(K_v\), and the product over \(v\) is the product of its finitely many factors different from \(1\).

public theorem adelicNorm_apply (a : TopologicalIdeleGroup (π“ž K) K) :
    adelicNorm K a =
      (∏ w : InfinitePlace K, β€–(a.1 w : w.Completion)β€– ^ w.mult) *
        ∏ᢠ v : IsDedekindDomain.HeightOneSpectrum (π“ž K),
          β€–(a.2 v : v.adicCompletion K)β€–
Uses 5 Β· Used by 1
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Adelic norm Β· Local integral unit subgroup
Used byProduct formula for principal ideles

DefinitionNorm-one ideles#βœ“fully proved

Let \(K\) be a number field. The norm-one ideles of \(K\) form the kernel of the adelic norm, the subgroup of the topological idele group of \(K\) (with \(R = \mathcal{O}_K\)) consisting of the ideles whose adelic norm is \(1\).

public def normOneIdeles : Subgroup (TopologicalIdeleGroup (π“ž K) K) :=
  (adelicNorm K).ker
Uses 5 Β· Used by 5
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Adelic norm Β· Local integral unit subgroup
Used byMembership in the norm-one ideles Β· Norm-one idele class group Β· Principal ideles are trivial in the norm-one idele class group Β· Principal ideles of norm one Β· Principal ideles have norm one

TheoremMembership in the norm-one ideles#βœ“fully proved

Let \(K\) be a number field. An idele \(a\) of \(K\) (with \(R = \mathcal{O}_K\)) lies in the subgroup of norm-one ideles if and only if its adelic norm is \(1\).

@[simp]
public theorem mem_normOneIdeles {a : TopologicalIdeleGroup (π“ž K) K} :
    a ∈ normOneIdeles K ↔ adelicNorm K a = 1
Uses 6 Β· Used by 1
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Adelic norm Β· Norm-one ideles Β· Local integral unit subgroup
Used byPrincipal ideles have norm one

TheoremProduct formula for principal ideles#βœ“fully proved

Let \(K\) be a number field. For every \(x \in K^\times\), the principal idele of \(x\) (its image under the diagonal embedding of \(K^\times\) into the topological idele group, with \(R = \mathcal{O}_K\)) has adelic norm \(1\).

@[simp]
public theorem adelicNorm_principalEmbedding (x : KΛ£) :
    adelicNorm K (principalEmbedding (π“ž K) K x) = 1
Uses 9 Β· Used by 1
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Adelic norm Β· Diagonal map into the ideles Β· Local integral unit subgroup
Proof usesFormula for the adelic norm Β· Diagonal map into the finite ideles Β· Diagonal map into the infinite ideles
Used byPrincipal ideles have norm one

TheoremPrincipal ideles have norm one#βœ“fully proved

Let \(K\) be a number field. The subgroup of principal ideles of \(K\) (with \(R = \mathcal{O}_K\)) is contained in the subgroup of norm-one ideles; that is, every principal idele has adelic norm \(1\).

public theorem principalIdeles_le_normOneIdeles :
    principalIdeles (π“ž K) K ≀ normOneIdeles K
Uses 10 Β· Used by 1
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Norm-one ideles Β· Principal ideles Β· Local integral unit subgroup
Proof usesAdelic norm Β· Product formula for principal ideles Β· Membership in the norm-one ideles Β· Diagonal map into the ideles
Used byPrincipal ideles are trivial in the norm-one idele class group

DefinitionPrincipal ideles of norm one#βœ“fully proved

For a number field \(K\), this is the subgroup of the group \(I_K^1\) of ideles of \(K\) with adelic norm \(1\) consisting of the principal ideles, that is, of the elements of \(I_K^1\) that are images of elements of \(K^\times\) under the diagonal embedding.

public def normOnePrincipalIdeles : Subgroup (normOneIdeles K) :=
  (principalIdeles (NumberField.RingOfIntegers K) K).subgroupOf (normOneIdeles K)
Uses 6 Β· Used by 2
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Norm-one ideles Β· Principal ideles Β· Local integral unit subgroup
Used byNorm-one idele class group Β· Principal ideles are trivial in the norm-one idele class group

AbbreviationNorm-one idele class group#βœ“fully proved

For a number field \(K\), the norm-one idele class group \(C_K^1 = I_K^1 / K^\times\) is the quotient of the group \(I_K^1\) of ideles of \(K\) with adelic norm \(1\) by its subgroup of principal ideles, the images of the elements of \(K^\times\) under the diagonal embedding.

public abbrev NormOneIdeleClassGroup :=
  (normOneIdeles K) β§Έ (normOnePrincipalIdeles K)
Uses 6
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Norm-one ideles Β· Principal ideles of norm one Β· Local integral unit subgroup

TheoremPrincipal ideles are trivial in the norm-one idele class group#βœ“fully proved

Let \(K\) be a number field. For every \(x \in K^\times\), the principal idele of \(x\), viewed as an element of the group \(I_K^1\) of ideles of \(K\) with adelic norm \(1\), has trivial class in the norm-one idele class group \(C_K^1 = I_K^1 / K^\times\).

@[simp]
public theorem normOne_mk_principalEmbedding (x : KΛ£) :
    QuotientGroup.mk (s := normOnePrincipalIdeles K)
        ⟨principalEmbedding (NumberField.RingOfIntegers K) K x,
          principalIdeles_le_normOneIdeles K ⟨x, rfl⟩⟩ = 1
Uses 8
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Norm-one ideles Β· Principal ideles of norm one Β· Diagonal map into the ideles Β· Principal ideles have norm one Β· Local integral unit subgroup

TheoremThe principal ideles are discrete#βœ“fully proved

For a number field \(K\), the subgroup of principal ideles is discrete in the idele group of \(K\), where the idele group carries the product of the product topology at the infinite places and the restricted-product topology at the finite places.

public theorem principalIdeles_discrete :
    DiscreteTopology (principalIdeles (π“ž K) K)
Uses 9
Statement usesFinite idele group Β· Infinite idele group Β· Topological idele group Β· Principal ideles Β· Local integral unit subgroup
Proof usesThe local integral units are open Β· Diagonal map into the finite ideles Β· Diagonal map into the infinite ideles Β· Diagonal map into the ideles
25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.