Documentation

Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

The finite adèle ring of a Dedekind domain #

We define the ring of finite adèles of a Dedekind domain R.

Main definitions #

Implementation notes #

We are only interested on Dedekind domains of Krull dimension 1 (i.e., not fields). If R is a field, its finite adèle ring is just defined to be the trivial ring.

References #

Tags #

finite adèle ring, dedekind domain

def DedekindDomain.FiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] :
Type (max u_1 u_2)

The product of all adicCompletionIntegers, where v runs over the maximal ideals of R.

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    def DedekindDomain.ProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] :
    Type (max u_1 u_2)

    The product of all adicCompletion, where v runs over the maximal ideals of R.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.

      The inclusion of R_hat in K_hat as a homomorphism of additive monoids.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The inclusion of R_hat in K_hat as a ring homomorphism.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The inclusion of R_hat in K_hat as an algebra homomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The finite adèle ring of a Dedekind domain #

            We define the finite adèle ring of R as the restricted product over all maximal ideals v of R of adicCompletion with respect to adicCompletionIntegers. We prove that it is a commutative ring. TODO: show that it is a topological ring with the restricted product topology.

            An element x : K_hat R K is a finite adèle if for all but finitely many height one ideals v, the component x v is a v-adic integer.

            Equations
            Instances For
              theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) :
              (x + y).IsFiniteAdele

              The sum of two finite adèles is a finite adèle.

              theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.neg {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} (hx : x.IsFiniteAdele) :
              (-x).IsFiniteAdele

              The negative of a finite adèle is a finite adèle.

              theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.mul {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K} {y : DedekindDomain.ProdAdicCompletions R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) :
              (x * y).IsFiniteAdele

              The product of two finite adèles is a finite adèle.

              def DedekindDomain.FiniteAdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] :
              Type (max u_1 u_2)

              The finite adèle ring of R is the restricted product over all maximal ideals v of R of adicCompletion with respect to adicCompletionIntegers.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                theorem DedekindDomain.FiniteAdeleRing.ext (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {a₁ : DedekindDomain.FiniteAdeleRing R K} {a₂ : DedekindDomain.FiniteAdeleRing R K} (h : a₁ = a₂) :
                a₁ = a₂