ValuationRing.mem_integer_iff
theorem ValuationRing.mem_integer_iff :
∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
[inst_4 : ValuationRing A] [inst_5 : IsFractionRing A K] (x : K),
x ∈ (ValuationRing.valuation A K).integer ↔ ∃ a, (algebraMap A K) a = x
This theorem states that for any integral domain `A` (with `A` being a commutative ring and a domain), any field of fractions `K` of `A` (given the algebra structure from `A` to `K` and `K` being a field), and any element `x` from `K`, `x` belongs to the ring of integers under the valuation induced by the valuation ring of `A` if and only if there exists an element `a` from `A` such that `a` maps to `x` under the algebraic map from `A` to `K`. In other words, `x` is in the valuation ring if and only if it is the image of some integer under the canonical map from `A` to its fraction field `K`.
More concisely: For any commutative domain `A` with a valuation ring, an element `x` in its field of fractions `K` belongs to the valuation ring if and only if there exists an integer `a` in `A` mapping to `x` under the canonical homomorphism from `A` to `K`.
|
ValuationRing.cond
theorem ValuationRing.cond :
∀ {A : Type u} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : ValuationRing A] (a b : A),
∃ c, a * c = b ∨ b * c = a
The theorem `ValuationRing.cond` states that for any type `A` which is a commutative ring and a domain, and for which `A` is a valuation ring, given any two elements `a` and `b` of `A`, there exists another element `c` in `A` such that either `a` multiplied by `c` equals `b`, or `b` multiplied by `c` equals `a`. In other words, for any two elements in a valuation ring, one of them can be expressed as the other one multiplied by some element in the ring.
More concisely: In a commutative ring and domain `A` that is a valuation ring, for any two elements `a`, `b` in `A`, there exists `c` in `A` such that either `ac = b` or `bc = a`.
|
ValuationRing.of_integers
theorem ValuationRing.of_integers :
∀ {𝒪 : Type u} {K : Type v} {Γ : Type w} [inst : CommRing 𝒪] [inst_1 : IsDomain 𝒪] [inst_2 : Field K]
[inst_3 : Algebra 𝒪 K] [inst_4 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
v.Integers 𝒪 → ValuationRing 𝒪
This theorem states that for any types `𝒪`, `K`, and `Γ`, if `𝒪` is a commutative ring and a domain, `K` is a field, `𝒪` is an algebra over `K`, `Γ` is a linearly ordered commutative group with zero, and `v` is a valuation on `K`, then if `𝒪` satisfies the condition `v.integers 𝒪` (which typically means that `𝒪` is the ring of integers with respect to the valuation `v`), then `𝒪` is a valuation ring. A valuation ring is a specific type of ring in algebraic geometry and algebraic number theory that arises in the study of valuations of fields.
More concisely: If `𝒪` is a commutative ring and domain, a `K`-algebra, `Γ` is a linearly ordered commutative group with zero, `K` is a field, `v` is a valuation on `K` with `𝒪` as the ring of integers, then `𝒪` is a valuation ring.
|