Valuation rings: squares 1 + 4c, integrality under domination, and divisibility

In a commutative ring R with total divisibility and regular 2, the element 1 + 4c is a square exactly when c has the form t ^ 2 + t, the witness being 1 + 2t. One direction is an identity valid in every commutative ring. The other says that every square root y of 1 + 4c satisfies 2 ∣ y - 1, using total divisibility and cancellation by 2.

Over the integer ring of a dyadic local field this reduces the question whether a unit of depth 2 v(2) is a square to the residue field, where t ↦ t ^ 2 + t is the Artin–Schreier map. This is how the depth of the local square theorem is shown to be sharp.

A valuation ring R with fraction field K is also integrally closed against every ring that dominates it: if R → S is a local homomorphism and K maps compatibly into a commutative ring L containing S, an element of K whose image lies in S already lies in R. Over a discrete valuation ring this is what lets an integrality statement proved after a ramified extension of the base descend to the base itself.

Finally, on a monoid with total divisibility, a multiplicative map preserving zero and one is determined by divisibility when it is at most 1 everywhere, below 1 on the nonunits and zero only at 0: then v x ≤ v y exactly when y ∣ x. This describes the 𝔪-adic valuation of a discrete valuation ring on its own elements, and the points with zero support of its adic spectrum.

Main results

• TauCeti.ValuationRing.isSquare_one_add_four_mul_iff: 1 + 4c is a square if and only if c = t ^ 2 + t for some t.
• TauCeti.ValuationRing.isInteger_of_isInteger_algebraMap: an element of K whose image in L lies in a ring S dominating R already lies in R.
• MonoidWithZeroHom.le_iff_dvd: a multiplicative map at most 1, below 1 on the nonunits and zero only at 0 compares elements by divisibility.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §5.
• O. T. O'Meara, Introduction to Quadratic Forms, §63A.

theorem TauCeti.ValuationRing.isSquare_one_add_four_mul_iff {R : Type u_1} [CommRing R] [PreValuationRing R] (h2 : IsRegular 2) {c : R} : IsSquare (1 + 4 * c) ↔ ∃ (t : R), t ^ 2 + t = c

In a commutative ring with total divisibility and regular 2, the element 1 + 4c is a square if and only if c lies in the image of the quadratic map t ↦ t ^ 2 + t.

theorem TauCeti.ValuationRing.isInteger_of_isInteger_algebraMap {R : Type u_2} {S : Type u_3} {K : Type u_4} {L : Type u_5} [CommRing R] [IsDomain R] [ValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing S] [CommRing L] [Algebra S L] [Algebra K L] [Algebra R S] [IsLocalHom (algebraMap R S)] (hS : Function.Injective ⇑(algebraMap S L)) (h : (algebraMap S L).comp (algebraMap R S) = (algebraMap K L).comp (algebraMap R K)) {x : K} (hx : IsLocalization.IsInteger S ((algebraMap K L) x)) : IsLocalization.IsInteger R x

A valuation ring is integrally closed against every ring dominating it. Let R be a valuation ring with fraction field K, let R → S be a local homomorphism, and let S and K map compatibly into a commutative ring L, with S → L injective. An element of K whose image in L comes from S already comes from R.

theorem MonoidWithZeroHom.le_iff_dvd {R : Type u_1} {Γ₀ : Type u_2} [MonoidWithZero R] [PreValuationRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : R →*₀ Γ₀) (hle : ∀ (x : R), v x ≤ 1) (hlt : ∀ (x : R), ¬IsUnit x → v x < 1) (hsupp : ∀ (x : R), v x = 0 → x = 0) {x y : R} : v x ≤ v y ↔ y ∣ x

A multiplicative map preserving zero and one on a monoid with total divisibility compares elements by divisibility when it is at most 1 everywhere, strictly below 1 on the nonunits, and zero only at 0: then v x ≤ v y exactly when y ∣ x.