The fraction t/s in an away localisation

A localisation S of A away from s inverts s, so it contains t/s for every t : A. Mathlib names the inverse itself — IsLocalization.Away.invSelf s is 1/s — but not the general fraction; this file names it and gives the identities that manipulating it needs: scaling 1/s by t, and clearing the denominator on either side.

Nothing here is topological or Huber-specific — it is IsLocalization algebra over an arbitrary commutative semiring, for an arbitrary localisation away from s — so it is stated outside the Huber namespace, alongside TauCeti/RingTheory/Localization/DenIdeal.lean.

Main definitions

• TauCeti.Localization.divBy: the element t/s of a localisation away from s.

Main results

• TauCeti.Localization.divBy_one: 1/s is Mathlib's IsLocalization.Away.invSelf.
• TauCeti.Localization.invSelf_mul_algebraMap: scaling 1/s by t gives t/s.
• TauCeti.Localization.algebraMap_mul_divBy and TauCeti.Localization.divBy_mul_algebraMap: s · (t/s) = t in both orders.
• TauCeti.Localization.divBy_zero, TauCeti.Localization.divBy_add and TauCeti.Localization.divBy_mul: t/s is additive and A-linear in the numerator.
• TauCeti.Localization.divBy_mul_cancel_left and TauCeti.Localization.divBy_mul_cancel_right: (s · t)/s = t and (t · s)/s = t.
• TauCeti.Localization.divBy_mul_mul_left and TauCeti.Localization.divBy_mul_mul_right: (u · t)/(u · s) = t/s and (t · u)/(s · u) = t/s, given that S is a localisation away from the rescaled denominator as well.
• TauCeti.Localization.divBy_self: s/s = 1.
• TauCeti.Localization.adjoin_invSelf_eq_top: S is generated over A by 1/s.
• TauCeti.Localization.adjoin_divBy_eq_top: as soon as the numerators T together with the denominator s generate the unit ideal, the fractions t/s alone already generate S over A.
• TauCeti.Localization.divBy_mul_divBy_of_eq_mul: for s = u * r, the fraction (a · b)/s splits as (a · r)/s · (b · u)/s, each half carrying one factor of the denominator.
• TauCeti.Localization.isUnit_of_comp_algebraMap: a ring homomorphism out of the localisation whose restriction along algebraMap A S is φ makes φ s a unit.
• TauCeti.Localization.map_divBy_eq_mul_inv: such a homomorphism sends t/s to φ t * (φ s)⁻¹.
• TauCeti.Localization.awayLift_divBy: the comparison map to a localisation at a multiple w = u * r rescales fractions by the cofactor, sending a/u to (a · r)/w.
• RingHom.awayMap_divBy: the map induced on localisations by a ring homomorphism f pushes fractions along f, sending a/u to f(a)/f(u).

Provenance

divBy and its identities are ported from AINTLIB's projects/AdicSpaces/Adic spaces/LocalizationTopology.lean, branch dev/adic-spaces, commit d9f2fbbb, where they are stated for the concrete Localization.Away s over a commutative ring inside the Huber development. They are generalised here to an arbitrary IsLocalization.Away over a commutative semiring, linked to Mathlib's IsLocalization.Away.invSelf, and moved out of the Huber namespace because nothing about them is topological. The topological part of that port is TauCeti/RingTheory/Huber/LocalizationTopology/Basic.lean, which records the same provenance.

divBy_mul_divBy_of_eq_mul, awayLift_divBy and awayMap_divBy are later additions with no AINTLIB analogue — checked against dev/adic-spaces at commit 37bbdaeb9, which has neither the splitting identity for a factored denominator nor any statement about IsLocalization.Away.lift on distinguished fractions, and does not mention IsLocalization.Away.map at all. All three are proved here directly from Mathlib's mk' API.

adjoin_invSelf_eq_top and adjoin_divBy_eq_top are also later additions with no AINTLIB analogue, checked against the same commit. What that source has is locSubring_isNoetherianRing, which presents the ring of definition A₀[t₁/s, …, tₙ/s] as an image of MvPolynomial T A₀; that surjectivity is true by construction, since locSubring is defined as the adjoin, and it says nothing about the localisation S itself. Generating the whole of S over A is a strictly stronger statement and needs the hypothesis on T below, which the source never states.

map_divBy_eq_mul_inv is a generalisation of an AINTLIB statement, checked against the same commit. There, awayLift_divByS_one_eq_unit_inv in projects/AdicSpaces/Adic spaces/WedhornAwayMapSaturation.lean records the numerator-1 case for IsLocalization.Away.lift into Localization.Away s; the version here has an arbitrary numerator, an arbitrary localisation away from s, and an arbitrary homomorphism out of it, asking only that it restrict to φ along algebraMap, from which isUnit_of_comp_algebraMap recovers the unit the inverse is taken at. The proof is written here directly from divBy_mul_algebraMap.

References

• C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit d9f2fbbb, projects/AdicSpaces/Adic spaces/LocalizationTopology.lean

noncomputable def TauCeti.Localization.divBy {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : S

The element t/s in a localisation S of A away from s — numerator first, the element being inverted second. The name follows Mathlib's LocalizedModule.divBy, division by the distinguished element.

Equations

• TauCeti.Localization.divBy t s = IsLocalization.mk' S t ⟨s, ⋯⟩

theorem TauCeti.Localization.divBy_def {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : divBy t s = IsLocalization.mk' S t ⟨s, ⋯⟩

t/s is the fraction mk' t s. The body of divBy is not exported, so this is how a consumer reaches Mathlib's IsLocalization API for it.

@[simp]

theorem TauCeti.Localization.divBy_one {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] : divBy 1 s = IsLocalization.Away.invSelf s

1/s is Mathlib's IsLocalization.Away.invSelf, so its simp set applies to divBy 1 s.

@[simp]

theorem TauCeti.Localization.invSelf_mul_algebraMap {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : IsLocalization.Away.invSelf s * (algebraMap A S) t = divBy t s

Scaling 1/s by t gives t/s. Stated with IsLocalization.Away.invSelf rather than divBy 1 s on the left, because divBy_one makes invSelf the simp-normal form of 1/s; the two together normalise a product of a unit fraction and a scalar to a single divBy.

@[simp]

theorem TauCeti.Localization.algebraMap_mul_divBy {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : (algebraMap A S) s * divBy t s = (algebraMap A S) t

Clearing the denominator: s · (t/s) = t.

@[simp]

theorem TauCeti.Localization.divBy_mul_cancel_left {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : divBy (s * t) s = (algebraMap A S) t

Clearing the denominator inside the numerator: (s · t)/s = t.

@[simp]

theorem TauCeti.Localization.divBy_mul_cancel_right {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : divBy (t * s) s = (algebraMap A S) t

The same on the other side: (t · s)/s = t.

@[simp]

theorem TauCeti.Localization.divBy_mul_algebraMap {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : divBy t s * (algebraMap A S) s = (algebraMap A S) t

Clearing the denominator on the right: (t/s) · s = t. The mirror of algebraMap_mul_divBy; S is only a CommSemiring, mul_comm is not simp, and Mathlib's IsLocalization.Away.mul_invSelf fixes the other order, so without this the reversed goal is left open.

@[simp]

theorem TauCeti.Localization.divBy_mul_mul_left {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] {u : A} [IsLocalization.Away (u * s) S] : divBy (u * t) (u * s) = divBy t s

Scaling numerator and denominator by the same element leaves the fraction alone: (u · t)/(u · s) = t/s, whenever S is also a localisation away from u · s.

That extra instance is what the hypothesis really is: for a unit u it comes for free, since u * s and s are then associated and IsLocalization.Away.of_associated transports the localisation. Rescaling a denominator alone need not preserve the fraction; rescaling numerator and denominator together always does, which is what a construction indexed by a presentation needs.

@[simp]

theorem TauCeti.Localization.divBy_mul_mul_right {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] {u : A} [IsLocalization.Away (s * u) S] : divBy (t * u) (s * u) = divBy t s

The same on the other side: (t · u)/(s · u) = t/s.

@[simp]

theorem TauCeti.Localization.algebraMap_mul_invSelf {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] : (algebraMap A S) t * IsLocalization.Away.invSelf s = divBy t s

The mirror of invSelf_mul_algebraMap, for the same reason.

The numerator

divBy is additive and A-linear in its numerator. The body is not exported, so without these a consumer computing with t/s — products of the generators of a localisation subring are exactly such fractions — has to rw [divBy_def] down to IsLocalization.mk'. Each is read off invSelf_mul_algebraMap, which turns the fraction into a product with a fixed left factor.

@[simp]

theorem TauCeti.Localization.divBy_zero {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] : divBy 0 s = 0

0/s = 0.

@[simp]

theorem TauCeti.Localization.divBy_add {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] (u : A) : divBy (t + u) s = divBy t s + divBy u s

t/s is additive in the numerator.

theorem TauCeti.Localization.divBy_mul {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] (a : A) : divBy (a * t) s = (algebraMap A S) a * divBy t s

t/s is A-linear in the numerator.

@[simp]

theorem TauCeti.Localization.divBy_self {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] : divBy s s = 1

s/s = 1. Without this the simp set turns invSelf s * algebraMap A S s into divBy s s and stops, where before invSelf_mul_algebraMap it could reach 1 through Mathlib's IsLocalization.Away.mul_invSelf.

A factored denominator

When s factors as u * r, a fraction over s can be split so that each half carries one factor, and a fraction over u alone can be rewritten over s. These are the identities that let a presentation be replaced by one with a larger denominator.

theorem TauCeti.Localization.divBy_mul_divBy_of_eq_mul {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] {u r : A} (h : s = u * r) (a b : A) : divBy (a * b) s = divBy (a * r) s * divBy (b * u) s

Splitting a fraction over a factored denominator. If s = u * r then (a · b)/s factors as (a · r)/s · (b · u)/s: each half keeps one factor of the denominator, so a/u and b/r are recovered as fractions over s itself.

Both sides agree after multiplying by s, which is a unit. This is what turns a product of denominators into a product of two fractions over the common denominator, so that each can be recognised separately.

Maps out of the localisation

A ring homomorphism out of S is determined by its restriction along algebraMap A S, and what it does to a distinguished fraction is forced: t/s goes to the ratio of the images. Nothing is asked of the target, and nothing of the homomorphism beyond its restriction — that restriction already makes the image of the denominator a unit — so this covers every map out of S at once rather than the particular ones IsLocalization.Away.lift and IsLocalization.Away.map build below.

theorem TauCeti.Localization.isUnit_of_comp_algebraMap {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] {B : Type u_3} [Semiring B] {φ : A →+* B} {ψ : S →+* B} (hψ : ∀ (a : A), ψ ((algebraMap A S) a) = φ a) : IsUnit (φ s)

A homomorphism out of the localisation makes the denominator a unit. If ψ : S →+* B restricts along algebraMap A S to φ, then φ s is a unit: it is the image under ψ of algebraMap A S s, which S inverts.

theorem TauCeti.Localization.map_divBy_eq_mul_inv {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (t s : A) [IsLocalization.Away s S] {B : Type u_3} [Semiring B] {φ : A →+* B} {ψ : S →+* B} (hψ : ∀ (a : A), ψ ((algebraMap A S) a) = φ a) : ψ (divBy t s) = φ t * ↑⋯.unit⁻¹

A homomorphism out of the localisation sends t/s to φ t / φ s. If ψ : S →+* B restricts along algebraMap A S to φ, then ψ (t/s) = φ t * (φ s)⁻¹, the inverse taken at the unit isUnit_of_comp_algebraMap supplies.

Nothing is asked of ψ beyond the factoring hypothesis, so the statement holds for every homomorphism out of S restricting to φ, and it records the value they are all forced to take on a distinguished fraction.

Passing to a localisation at a multiple

A localisation away from u maps to a localisation away from any multiple w = u * r, by IsLocalization.Away.lift at the unit IsLocalization.Away.isUnit_of_dvd supplies. The one thing a consumer needs to know about that map is what it does to fractions, and the answer is that it rescales numerator and denominator by the cofactor.

theorem TauCeti.Localization.awayLift_divBy {A : Type u_1} [CommSemiring A] {V : Type u_3} {W : Type u_4} [CommSemiring V] [CommSemiring W] [Algebra A V] [Algebra A W] (u r w : A) (hw : w = u * r) [IsLocalization.Away u V] [IsLocalization.Away w W] (hu : IsUnit ((algebraMap A W) u)) (a : A) : (IsLocalization.Away.lift u hu) (divBy a u) = divBy (a * r) w

The comparison map rescales fractions by the cofactor: if w = u * r then the map Aᵤ → A_w induced by IsLocalization.Away.lift sends a/u to (a · r)/w.

Both sides become a after multiplying by u, which is a unit in A_w, so they agree. This is what lets a fraction over the coarser denominator be recognised as a distinguished fraction of the finer presentation.

Changing the base ring

A ring homomorphism f : A →+* B carries a localisation away from u to one away from f u, by IsLocalization.Away.map. As above, the one thing a consumer needs to know about that map is what it does to fractions, and the answer is that it pushes numerator and denominator along f.

@[simp]

theorem RingHom.awayMap_divBy {A : Type u_1} [CommSemiring A] {B : Type u_3} [CommSemiring B] {V : Type u_4} {W : Type u_5} [CommSemiring V] [CommSemiring W] [Algebra A V] [Algebra B W] (f : A →+* B) (u : A) [IsLocalization.Away u V] [IsLocalization.Away (f u) W] (a : A) : (IsLocalization.Away.map V W f u) (TauCeti.Localization.divBy a u) = TauCeti.Localization.divBy (f a) (f u)

The induced map pushes a fraction along the homomorphism: the map A_u → B_{f(u)} that IsLocalization.Away.map builds from f : A →+* B sends a/u to f(a)/f(u).

Both sides are the fraction IsLocalization.mk' of the images, so nothing is rescaled. This is the companion of awayLift_divBy for a moving base ring: there the base ring is fixed and the denominator is replaced by a multiple, here the denominator is carried along and the base ring changes.

The fractions generate

A localisation away from s is generated over A by 1/s alone; and as soon as the numerators together with s generate the unit ideal, already by the fractions t/s themselves. Including s among the generators is what makes the second statement usable: its own fraction s/s is 1, so the term it contributes after dividing through is a constant, not a further fraction. Nothing topological enters — this is the algebraic half of the statement that a rational localisation is a quotient of a polynomial ring, one variable per numerator.

Neither statement is phrased as a surjectivity of MvPolynomial.aeval, although that is what each of them says: Mathlib's Algebra.adjoin_range_eq_range_aeval rewrites one into the other, and stating it here would cost the file an MvPolynomial import to say what a consumer can already say in a line.

theorem TauCeti.Localization.adjoin_invSelf_eq_top {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] : A[IsLocalization.Away.invSelf s] = ⊤

A localisation away from s is generated over A by 1/s. Every element is a/sⁿ, which is a · (1/s)ⁿ.

theorem TauCeti.Localization.adjoin_divBy_eq_top {A : Type u_1} [CommSemiring A] {S : Type u_2} [CommSemiring S] [Algebra A S] (s : A) [IsLocalization.Away s S] {T : Set A} (hT : Ideal.span (insert s T) = ⊤) : Algebra.adjoin A (Set.range fun (t : ↑T) => divBy (↑t) s) = ⊤

Numerators generating the unit ideal together with s make their fractions generate the localisation. If T ∪ {s} spans A as an ideal then S is already A[t/s : t ∈ T] — no separate 1/s is needed.

Including s among the generators costs nothing and is what the intended application supplies: writing 1 = c · s + ∑ cₜ · t and dividing by s exhibits 1/s as c + ∑ cₜ · (t/s), after which adjoin_invSelf_eq_top finishes. The c · s term contributes the coefficient c, which lies in A and so is already in the subalgebra; that is why s may be one of the generators without being one of the numerators. The hypothesis cannot be dropped: over A = ℤ with s = p and T = ∅ the fractions generate only ℤ, not ℤ[1/p].

The hypothesis is exactly what Wedhorn's rational subsets supply: there T · A is required to be open, and an open ideal of a Tate ring is ⊤ by TauCeti.Huber.IsTateRing.eq_top_of_isOpen.

The trivial denominator

A ring is its own localisation away from 1, and there the fraction t/1 is t. This is the degenerate presentation (T, 1), which the adic structure presheaf uses to present the whole adic spectrum.

instance TauCeti.Localization.isLocalizationAwayOne (R : Type u_3) [CommSemiring R] : IsLocalization.Away 1 R

A ring is its own localisation away from 1: 1 is already a unit and the identity is bijective.