DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one
theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one :
∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K], DedekindDomain.ProdAdicCompletions.IsFiniteAdele 1
The theorem `DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one` states that for any given Type `R` that is a commutative ring and a Dedekind domain, and any given Type `K` that is a field as well as a fraction field of `R`, the tuple `(1)_v`, where `v` is any place of `R`, is a finite adèle. In this context, a place `v` of a Dedekind domain `R` is an equivalence class of absolute values on the fraction field of `R`, and an adèle is an element of the restricted product over all places `v` of `R` of the completions of `R` with respect to `v`. The Adèle ring forms an important part of the global structure of the Dedekind domain.
More concisely: For any commutative ring and Dedekind domain R, and its fraction field K, the tuple of 1's in the completion of R with respect to any place v forms a finite adèle in the Adèle ring of R.
|
DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero
theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero :
∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K], DedekindDomain.ProdAdicCompletions.IsFiniteAdele 0
This theorem states that for any integral domain `R` which is a Dedekind domain, and any field `K` that is the field of fractions of `R`, the tuple `(0)_v`, which represents the zero element in the product of the completions of `R` with respect to all non-zero prime ideals, is a finite adèle. Here, an adèle is a system of elements of local fields, and a finite adèle is one that is non-zero in only finitely many places.
More concisely: For any Dedekind domain `R` with field of fractions `K`, the zero element in the product of the completions of `R` with respect to all non-zero prime ideals forms a finite adèle.
|
DedekindDomain.ProdAdicCompletions.IsFiniteAdele.mul
theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.mul :
∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {x y : DedekindDomain.ProdAdicCompletions R K},
x.IsFiniteAdele → y.IsFiniteAdele → (x * y).IsFiniteAdele
This theorem states that in a Dedekind domain `R` with a field of fractions `K`, the product of two finite "adèles" (which are elements of the product of all `adicCompletion`s over the maximal ideals of `R`) is also a finite adèle. In other words, if `x` and `y` are finite adèles in the product of the adic completions of `R` with respect to `K`, then their product `x * y` is also a finite adèle.
More concisely: In a Dedekind domain `R` with a field of fractions `K`, the product of two finite adèles in the product of their adic completions is a finite adèle.
|
DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add
theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add :
∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {x y : DedekindDomain.ProdAdicCompletions R K},
x.IsFiniteAdele → y.IsFiniteAdele → (x + y).IsFiniteAdele
The theorem `DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add` states that given any two finite adèles `x` and `y` in the product of adic completions of a Dedekind domain `R` with fraction field `K`, their sum is also a finite adèle. This is under the conditions that `R` is an integral domain with a commutative ring structure, `K` is a field which is the field of fractions of `R` with a commutative ring structure and an algebra structure over `R`.
More concisely: Given two finite adeles `x` and `y` in the product of adic completions of a commutative Dedekind domain `R` with field of fractions `K`, their sum is also a finite adèle.
|
DedekindDomain.ProdAdicCompletions.IsFiniteAdele.neg
theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.neg :
∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
[inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {x : DedekindDomain.ProdAdicCompletions R K},
x.IsFiniteAdele → (-x).IsFiniteAdele
This theorem states that the negation of a finite adèle is also a finite adèle. Specifically, given any commutative ring `R` which is a Dedekind domain, a field `K` that is a field of fractions of `R`, and an element `x` from the product of all adic completions (adèles) of `K` over `R` that is a finite adèle, then the negative of `x` is also a finite adèle. In other words, the set of finite adèles is closed under the operation of negation.
More concisely: In a commutative Dedekind domain `R` with field of fractions `K`, the set of finite adèles is closed under negation.
|