The finite adèle ring of a Dedekind domain

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

Main definitions

• DedekindDomain.FiniteIntegralAdeles : product of adicCompletionIntegers, where v runs over all maximal ideals of R.
• DedekindDomain.ProdAdicCompletions : the product of adicCompletion, where v runs over all maximal ideals of R.
• DedekindDomain.finiteAdeleRing : The finite adèle ring of R, defined as the restricted product Π'_v K_v. We give this ring a K-algebra structure.

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

• J.W.S. Cassels, A. Frölich, Algebraic Number Theory

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

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

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

Equations

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

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

Equations

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

theorem DedekindDomain.instIsTopologicalRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsTopologicalRing (Subtype fun (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) => Membership.mem (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) x)

theorem DedekindDomain.instIsTopologicalRingFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsTopologicalRing (FiniteIntegralAdeles R K)

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

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

• Eq (DedekindDomain.ProdAdicCompletions R K) ((v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

def DedekindDomain.instNonUnitalNonAssocRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : NonUnitalNonAssocRing (ProdAdicCompletions R K)

Equations

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

def DedekindDomain.instTopologicalSpaceProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalSpace (ProdAdicCompletions R K)

Equations

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

theorem DedekindDomain.instIsTopologicalRingProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsTopologicalRing (ProdAdicCompletions R K)

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

Equations

• Eq (DedekindDomain.instCommRingProdAdicCompletions R K) (inferInstanceAs (CommRing ((v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)))

def DedekindDomain.instInhabitedProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Inhabited (ProdAdicCompletions R K)

Equations

• Eq (DedekindDomain.instInhabitedProdAdicCompletions R K) (inferInstanceAs (Inhabited ((v : IsDedekindDomain.HeightOneSpectrum R) → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)))

noncomputable def DedekindDomain.FiniteIntegralAdeles.instCoeProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Coe (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)

Equations

• Eq (DedekindDomain.FiniteIntegralAdeles.instCoeProdAdicCompletions R K) { coe := fun (x : DedekindDomain.FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) => (x v).val }

theorem DedekindDomain.FiniteIntegralAdeles.coe_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : Eq ((fun (v : IsDedekindDomain.HeightOneSpectrum R) => (x v).val) v) (x v).val

def DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : AddMonoidHom (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)

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.

theorem DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : Eq (DFunLike.coe (addMonoidHom R K) x v) (x v).val

def DedekindDomain.FiniteIntegralAdeles.Coe.ringHom (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : RingHom (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)

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.

theorem DedekindDomain.FiniteIntegralAdeles.Coe.ringHom_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : Eq (DFunLike.coe (ringHom R K) x v) (x v).val

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

Equations

• Eq (DedekindDomain.instAlgebraProdAdicCompletions R K) inferInstance

theorem DedekindDomain.ProdAdicCompletions.algebraMap_apply' (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (k : K) : Eq (DFunLike.coe (algebraMap K (ProdAdicCompletions R K)) k v) (UniformSpace.Completion.coe' k)

def DedekindDomain.ProdAdicCompletions.algebra' (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra R (ProdAdicCompletions R K)

Equations

• Eq (DedekindDomain.ProdAdicCompletions.algebra' R K) inferInstance

theorem DedekindDomain.ProdAdicCompletions.algebraMap_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) : Eq (DFunLike.coe (algebraMap R (ProdAdicCompletions R K)) r v) (UniformSpace.Completion.coe' (DFunLike.coe (algebraMap R K) r))

theorem DedekindDomain.instIsScalarTowerProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsScalarTower R K (ProdAdicCompletions R K)

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

Equations

• Eq (DedekindDomain.instAlgebraFiniteIntegralAdeles R K) inferInstance

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

Equations

• Eq (DedekindDomain.ProdAdicCompletions.algebraCompletions R K) (DedekindDomain.FiniteIntegralAdeles.Coe.ringHom R K).toAlgebra

theorem DedekindDomain.ProdAdicCompletions.isScalarTower_completions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsScalarTower R (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)

def DedekindDomain.FiniteIntegralAdeles.Coe.algHom (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : AlgHom R (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)

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.

theorem DedekindDomain.FiniteIntegralAdeles.Coe.algHom_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : FiniteIntegralAdeles R K) (v : IsDedekindDomain.HeightOneSpectrum R) : Eq (DFunLike.coe (algHom R K) x v) (x v).val

theorem DedekindDomain.FiniteIntegralAdeles.instFaithfulSMulProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : FaithfulSMul (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)

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.

def DedekindDomain.ProdAdicCompletions.IsFiniteAdele {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : ProdAdicCompletions R K) : Prop

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

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

theorem DedekindDomain.ProdAdicCompletions.isFiniteAdele_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : ProdAdicCompletions R K) : Iff x.IsFiniteAdele (setOf fun (v : IsDedekindDomain.HeightOneSpectrum R) => Not (Membership.mem (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) (x v))).Finite

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 y : ProdAdicCompletions R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) : (HAdd.hAdd x y).IsFiniteAdele

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

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsFiniteAdele 0

The tuple (0)_v 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 : ProdAdicCompletions R K} (hx : x.IsFiniteAdele) : (Neg.neg 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 y : ProdAdicCompletions R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) : (HMul.hMul x y).IsFiniteAdele

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

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsFiniteAdele 1

The tuple (1)_v is a finite adèle.

theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap' {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (k : K) : (DFunLike.coe (algebraMap K (ProdAdicCompletions R K)) k).IsFiniteAdele

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.

Note that we make this a Type rather than a Subtype (e.g., a Subalgebra) since we wish to endow it with a finer topology than that of the subspace topology.

Equations

• Eq (DedekindDomain.FiniteAdeleRing R K) (Subtype fun (x : DedekindDomain.ProdAdicCompletions R K) => x.IsFiniteAdele)

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

The finite adèle ring of R, regarded as a K-subalgebra of the product of the local completions of K.

Note that this definition exists to streamline the proof that the finite adèles are an algebra over K, rather than to express their relationship to K_hat R K which is essentially a detail of their construction.

Equations

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

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

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instCommRing R K) (DedekindDomain.FiniteAdeleRing.subalgebra R K).toCommRing

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

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instAlgebra R K) (DedekindDomain.FiniteAdeleRing.subalgebra R K).algebra

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

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instAlgebra_1 R K) ((algebraMap K (DedekindDomain.FiniteAdeleRing R K)).comp (algebraMap R K)).toAlgebra

theorem DedekindDomain.FiniteAdeleRing.instIsScalarTower (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsScalarTower R K (FiniteAdeleRing R K)

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

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instCoeProdAdicCompletions R K) { coe := fun (x : DedekindDomain.FiniteAdeleRing R K) => x.val }

theorem DedekindDomain.FiniteAdeleRing.coe_one (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Eq (Subtype.val 1) 1

theorem DedekindDomain.FiniteAdeleRing.coe_zero (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Eq (Subtype.val 0) 0

theorem DedekindDomain.FiniteAdeleRing.coe_add (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x y : FiniteAdeleRing R K) : Eq (HAdd.hAdd x y).val (HAdd.hAdd x.val y.val)

theorem DedekindDomain.FiniteAdeleRing.coe_mul (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x y : FiniteAdeleRing R K) : Eq (HMul.hMul x y).val (HMul.hMul x.val y.val)

theorem DedekindDomain.FiniteAdeleRing.coe_algebraMap (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : K) : Eq (DFunLike.coe (algebraMap K (FiniteAdeleRing R K)) x).val (DFunLike.coe (algebraMap K (ProdAdicCompletions R K)) x)

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₁ a₂ : FiniteAdeleRing R K} (h : Eq a₁.val a₂.val) : Eq a₁ a₂

theorem DedekindDomain.FiniteAdeleRing.ext_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {a₁ a₂ : FiniteAdeleRing R K} : Iff (Eq a₁ a₂) (Eq a₁.val a₂.val)

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

The finite adele ring is an algebra over the finite integral adeles.

Equations

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

def DedekindDomain.FiniteAdeleRing.instDFunLikeHeightOneSpectrumAdicCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : DFunLike (FiniteAdeleRing R K) (IsDedekindDomain.HeightOneSpectrum R) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K)

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instDFunLikeHeightOneSpectrumAdicCompletion R K) { coe := fun (a : DedekindDomain.FiniteAdeleRing R K) => a.val, coe_injective' := ⋯ }

theorem DedekindDomain.FiniteAdeleRing.exists_finiteIntegralAdele_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (a : FiniteAdeleRing R K) : Iff (Exists fun (c : FiniteIntegralAdeles R K) => Eq a (Algebra.cast c)) (∀ (v : IsDedekindDomain.HeightOneSpectrum R), Membership.mem (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) (DFunLike.coe a v))

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

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instAlgebraProdAdicCompletions R K) (DedekindDomain.FiniteAdeleRing.subalgebra R K).toAlgebra

theorem DedekindDomain.FiniteAdeleRing.instIsScalarTowerFiniteIntegralAdelesProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsScalarTower (FiniteIntegralAdeles R K) (FiniteAdeleRing R K) (ProdAdicCompletions R K)

theorem DedekindDomain.FiniteAdeleRing.coe_algebraMap' (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (r : FiniteIntegralAdeles R K) : Eq (Algebra.cast (DFunLike.coe (algebraMap (FiniteIntegralAdeles R K) (FiniteAdeleRing R K)) r)) (DFunLike.coe (algebraMap (FiniteIntegralAdeles R K) (ProdAdicCompletions R K)) r)

theorem DedekindDomain.FiniteAdeleRing.instFaithfulSMulProdAdicCompletions (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : FaithfulSMul (FiniteAdeleRing R K) (ProdAdicCompletions R K)

theorem DedekindDomain.FiniteAdeleRing.instFaithfulSMulFiniteIntegralAdeles (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : FaithfulSMul (FiniteIntegralAdeles R K) (FiniteAdeleRing R K)

theorem DedekindDomain.FiniteAdeleRing.mul_nonZeroDivisor_mem_finiteIntegralAdeles {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (a : FiniteAdeleRing R K) : Exists fun (b : Subtype fun (x : R) => Membership.mem (nonZeroDivisors R) x) => Exists fun (c : FiniteIntegralAdeles R K) => Eq (HMul.hMul a (Algebra.cast b.val)) (Algebra.cast c)

theorem DedekindDomain.FiniteAdeleRing.submodulesRingBasis (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : SubmodulesRingBasis fun (r : Subtype fun (x : R) => Membership.mem (nonZeroDivisors R) x) => Submodule.span (FiniteIntegralAdeles R K) (Singleton.singleton (Algebra.cast r.val))

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

Equations

• Eq (DedekindDomain.FiniteAdeleRing.instTopologicalSpace R K) ⋯.topology