ClassGroup.exists_min
theorem ClassGroup.exists_min :
∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) (I : ↥(nonZeroDivisors (Ideal S))),
∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
The theorem `ClassGroup.exists_min` states that for any Euclidean domain `R`, commutative ring `S` where `S` is also a domain, and any algebra structure over `R` and `S`, given an absolute value `abv` from `R` to integers and a non-zero divisor of an ideal in `S`, there exists an element `b` in the ideal which is non-zero and has minimal norm. This means, if there is any other element `c` in the ideal whose norm (determined by the function `Algebra.norm R`) is less than the norm of `b`, then `c` must be zero.
More concisely: For any Euclidean domain R, commutative domain S with 1, algebra structure over R and S, absolute value abv from R to integers, and non-zero divisor I in S, there exists an element b in I with minimal norm in I such that any c in I with norm less than b is zero.
|
ClassGroup.exists_mem_finsetApprox
theorem ClassGroup.exists_mem_finsetApprox :
∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
(bS : Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R] (a : S) {b : R},
b ≠ 0 →
∃ q,
∃ r ∈ ClassGroup.finsetApprox bS adm,
abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
This theorem, titled `ClassGroup.exists_mem_finsetApprox`, states that for any Euclidean domain `R`, commutative ring `S` where `S` is also a domain, and given an algebra structure over `R` and `S`, an absolute value `abv` from `R` to integers, and a finite basis `bS`, if absolute value `abv` is admissible, `R` is infinite, and for any element `a` of `S` and non-zero element `b` of `R`, there exist elements `q` and `r` (where `r` is in the finite set `ClassGroup.finsetApprox bS adm`) such that the absolute value of the norm of `(r*a - b*q)` is less than the absolute value of the norm of the algebra map of `b` from `R` to `S`. This theorem essentially provides a way of approximating the division of `a` by `b` (in `L`) with the fraction `q / r`, where `r` has finitely many possibilities for `L`.
More concisely: For any Euclidean domain R with commutative domain S, algebra structure over R and S, admissible absolute value abv from R to integers, infinite R, and non-zero b in R, there exist q in S and r in the finite set ClassGroup.finsetApprox bS such that the norm of r*a - b*q has smaller absolute value than the absolute value of the norm of the algebra map of b for all a in S.
|
ClassGroup.exists_mem_finset_approx'
theorem ClassGroup.exists_mem_finset_approx' :
∀ {R : Type u_1} {S : Type u_2} (L : Type u_4) [inst : EuclideanDomain R] [inst_1 : CommRing S]
[inst_2 : IsDomain S] [inst_3 : Field L] [algRL : Algebra R L] [inst_4 : Algebra R S] [inst_5 : Algebra S L]
[ist : IsScalarTower R S L] [iic : IsIntegralClosure S R L] {abv : AbsoluteValue R ℤ} {ι : Type u_5}
[inst_6 : DecidableEq ι] [inst_7 : Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [inst_8 : Infinite R]
[inst_9 : DecidableEq R],
Algebra.IsAlgebraic R L →
∀ (a : S) {b : S},
b ≠ 0 →
∃ q,
∃ r ∈ ClassGroup.finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)
This theorem, `ClassGroup.exists_mem_finset_approx'`, states that given a Euclidean domain `R`, a commutative ring `S`, and a field `L` that are all related by a scalar tower, along with some additional structures, we can approximate the division of any two elements `a` and `b` in `L` with `q / r`, where `r` is an element from a finite set of options for `L`. This approximation works in the sense that the absolute value of the norm of the difference between `r` times `a` and `q` times `b` is strictly less than the absolute value of the norm of `b`. This is under the condition that `b` is not equal to zero and that all elements of `L` are algebraic over `R`. The finite set of options for `r` is represented by `ClassGroup.finsetApprox bS adm`, where `bS` is a basis of `R`-module `S` and `adm` is a structure indicating the admissibility of the absolute value function `abv`. The elements in this set are indexed by a type `ι`, which is assumed to be finite and have decidable equality. The domain `R` is assumed to be infinite and to have decidable equality.
More concisely: Given a Euclidean domain R, a commutative ring S, a field L related by a scalar tower, and additional structures, for any non-zero algebraic elements a and b in L, there exists r in the finite set of options ClassGroup.finsetApprox bS adm such that the norm of r * a - q * b has strict absolute value smaller than that of b.
|
ClassGroup.norm_le
theorem ClassGroup.norm_le :
∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
(bS : Basis ι R S) (a : S) {y : ℤ},
(∀ (k : ι), abv ((bS.repr a) k) ≤ y) →
abv ((Algebra.norm R) a) ≤ ClassGroup.normBound abv bS * y ^ Fintype.card ι
This theorem states that for any Euclidean domain `R`, commutative ring `S` which is also a domain, algebra structure on `R` and `S`, absolute value function `abv` from `R` to integers, and a basis `bS` of `R` on `S` indexed over a finite type `ι`, if an `R`-integral element `a` of `S` has coordinates `≤ y` with respect to the basis `bS` (i.e., for every index `k` of type `ι`, the absolute value of the `k`-th coordinate of `a` with respect to `bS` is less than or equal to `y`), then the absolute value of the algebra norm of `a` is less than or equal to the product of the norm bound of the absolute value function `abv` with respect to `bS` and `y` to the power of the number of elements in `ι`.
More concisely: For any Euclidean domain R, commutative domain S with algebra structure over R, absolute value function abv from R to integers, and finite basis bS of R over S, if an R-integral element a in S has coordinates less than or equal to y with respect to bS, then |N(a)| ≤ norm\_bound(abv) * y^(card ι), where |N(a)| denotes the algebra norm of a and norm\_bound(abv) is the norm bound of abv with respect to bS.
|
ClassGroup.norm_lt
theorem ClassGroup.norm_lt :
∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
(bS : Basis ι R S) {T : Type u_6} [inst_6 : LinearOrderedRing T] (a : S) {y : T},
(∀ (k : ι), ↑(abv ((bS.repr a) k)) < y) →
↑(abv ((Algebra.norm R) a)) < ↑(ClassGroup.normBound abv bS) * y ^ Fintype.card ι
This theorem, named `ClassGroup.norm_lt`, states that if we have an `R`-integral element `a` of type `S`, and this element `a` has coordinates less than `y` with respect to a certain basis `b`, then the norm of `a` is strictly less than the product of the `normBound` of `abv` and `b` and the `y` raised to the power of dimension of `S`.
More formally, for an Euclidean domain `R`, a commutative ring `S`, and an algebra structure between `R` and `S`, given an absolute value `abv : AbsoluteValue R ℤ`, a decidable equality on some type `ι`, a fintype structure on `ι`, a basis `bS : Basis ι R S`, a linear ordered ring `T`, an element `a : S` and a number `y : T`, if for all `k : ι`, the absolute value of coordinate `k` of `a` with respect to basis `bS` is strictly less than `y`, then the absolute value of the norm of `a` is strictly less than the product of `normBound abv bS` and `y` raised to the power of the cardinality (i.e., number of elements) of `ι`.
More concisely: If `a` is an integral element of commutative ring `S` over Euclidean domain `R`, with respect to a basis `bS` and absolute value `abv`, and the absolute value of each coordinate of `a` with respect to `bS` is strictly less than a number `y`, then the norm of `a` is strictly less than the product of `normBound abv` multiplied by `y` raised to the power of the cardinality of the basis.
|