Mathlib.RingTheory.Localization.Defs

IsLocalization structure

Full source

/-- The typeclass `IsLocalization (M : Submonoid R) S` where `S` is an `R`-algebra
expresses that `S` is isomorphic to the localization of `R` at `M`. -/
@[mk_iff] class IsLocalization : Prop where
  -- Porting note: add ' to fields, and made new versions of these with either `S` or `M` explicit.
  /-- Everything in the image of `algebraMap` is a unit -/
  map_units' : ∀ y : M, IsUnit (algebraMap R S y)
  /-- The `algebraMap` is surjective -/
  surj' : ∀ z : S, ∃ x : R × M, z * algebraMap R S x.2 = algebraMap R S x.1
  /-- The kernel of `algebraMap` is contained in the annihilator of `M`;
      it is then equal to the annihilator by `map_units'` -/
  exists_of_eq : ∀ {x y}, algebraMap R S x = algebraMap R S y → ∃ c : M, ↑c * x = ↑c * y

Localization of a commutative ring at a submonoid

Informal description

The typeclass `IsLocalization (M : Submonoid R) S` asserts that the commutative ring `S` is a localization of the commutative ring `R` at the submonoid `M`. This means there exists a ring homomorphism `f : R →+* S` satisfying the following properties: 1. For every element `y ∈ M`, the image `f y` is a unit in `S`; 2. For every element `z ∈ S`, there exists a pair `(x, y) ∈ R × M` such that `z * f y = f x`; 3. For any two elements `x, y ∈ R`, if `f x = f y`, then there exists an element `c ∈ M` such that `x * c = y * c`.

IsLocalization.map_units theorem

: ∀ y : M, IsUnit (algebraMap R S y)

Full source

@[inherit_doc IsLocalization.map_units']
theorem map_units : ∀ y : M, IsUnit (algebraMap R S y) :=
  IsLocalization.map_units'

Units in Localization: Images of Submonoid Elements are Units

Informal description

For every element $y$ in the submonoid $M$ of a commutative ring $R$, the image of $y$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S : R \to S$ is a unit in the localization $S$.

IsLocalization.surj theorem

: ∀ z : S, ∃ x : R × M, z * algebraMap R S x.2 = algebraMap R S x.1

Full source

@[inherit_doc IsLocalization.surj']
theorem surj : ∀ z : S, ∃ x : R × M, z * algebraMap R S x.2 = algebraMap R S x.1 :=
  IsLocalization.surj'

Surjectivity of Localization: Every Element is a Fraction

Informal description

For every element $z$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, there exists a pair $(x, y) \in R \times M$ such that $z \cdot f(y) = f(x)$, where $f: R \to S$ is the canonical ring homomorphism.

IsLocalization.injective_iff_isRegular theorem

: Injective (algebraMap R S) ↔ ∀ c : M, IsRegular (c : R)

Full source

theorem injective_iff_isRegular : InjectiveInjective (algebraMap R S) ↔ ∀ c : M, IsRegular (c : R) := by
  simp_rw [Commute.isRegular_iff (Commute.all _), IsLeftRegular,
    Injective, eq_iff_exists M, exists_imp, forall_comm (α := M)]

Injectivity of Localization Map vs Regularity of Submonoid Elements

Informal description

The canonical ring homomorphism $\text{algebraMap}\, R\, S : R \to S$ is injective if and only if every element $c$ in the submonoid $M$ is a regular element in $R$ (i.e., $c$ is neither a left nor right zero divisor).

IsLocalization.of_le theorem

(N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ r ∈ N, IsUnit (algebraMap R S r)) : IsLocalization N S

Full source

theorem of_le (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ r ∈ N, IsUnit (algebraMap R S r)) :
    IsLocalization N S where
  map_units' r := h₂ r r.2
  surj' s :=
    have ⟨⟨x, y, hy⟩, H⟩ := IsLocalization.surj M s
    ⟨⟨x, y, h₁ hy⟩, H⟩
  exists_of_eq {x y} := by
    rw [IsLocalization.eq_iff_exists M]
    rintro ⟨c, hc⟩
    exact ⟨⟨c, h₁ c.2⟩, hc⟩

Localization at Larger Submonoid Preserves Localization Property

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be submonoids of $R$ with $M \subseteq N$, and $S$ be a commutative ring that is a localization of $R$ at $M$. If for every element $r \in N$, the image of $r$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$ is a unit in $S$, then $S$ is also a localization of $R$ at $N$.

IsLocalization.of_le_of_exists_dvd theorem

(N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) : IsLocalization N S

Full source

theorem of_le_of_exists_dvd (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) :
    IsLocalization N S :=
  of_le M N h₁ fun n hn ↦ have ⟨m, hm, dvd⟩ := h₂ n hn
    isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)

Localization at Larger Submonoid via Divisibility Condition

Informal description

Let $R$ be a commutative ring, $M$ and $N$ be submonoids of $R$ with $M \subseteq N$. Suppose that for every element $n \in N$, there exists an element $m \in M$ such that $n$ divides $m$. Then $S$ is a localization of $R$ at $N$.

IsLocalization.algebraMap_isUnit_iff theorem

{x : R} : IsUnit (algebraMap R S x) ↔ ∃ m ∈ M, x ∣ m

Full source

theorem algebraMap_isUnit_iff {x : R} : IsUnitIsUnit (algebraMap R S x) ↔ ∃ m ∈ M, x ∣ m := by
  refine ⟨fun h ↦ ?_, fun ⟨m, hm, dvd⟩ ↦ isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)⟩
  have ⟨s, hxs⟩ := isUnit_iff_dvd_one.mp h
  have ⟨⟨r, m⟩, hrm⟩ := surj M s
  apply_fun (algebraMap R S x * ·) at hrm
  rw [← mul_assoc, ← hxs, one_mul, ← map_mul] at hrm
  have ⟨m', eq⟩ := exists_of_eq (M := M) hrm
  exact ⟨m' * m, mul_mem m'.2 m.2, _, mul_left_comm _ x _ ▸ eq⟩

Characterization of Units in Localization: $\text{algebraMap}\, R\, S\, x$ is a Unit iff $x$ Divides an Element of $M$

Informal description

Let $R$ be a commutative ring and $S$ be a localization of $R$ at a submonoid $M$. For any element $x \in R$, the image of $x$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S : R \to S$ is a unit in $S$ if and only if there exists an element $m \in M$ such that $x$ divides $m$.

IsLocalization.toLocalizationWithZeroMap definition

: Submonoid.LocalizationWithZeroMap M S

Full source

/-- `IsLocalization.toLocalizationWithZeroMap M S` shows `S` is the monoid localization of
`R` at `M`. -/
@[simps]
def toLocalizationWithZeroMap : Submonoid.LocalizationWithZeroMap M S where
  __ := algebraMap R S
  toFun := algebraMap R S
  map_units' := IsLocalization.map_units _
  surj' := IsLocalization.surj _
  exists_of_eq _ _ := IsLocalization.exists_of_eq

Localization of a commutative ring at a submonoid as a monoid with zero

Informal description

Given a commutative ring $R$ and a submonoid $M$ of $R$, the function `IsLocalization.toLocalizationWithZeroMap` provides evidence that $S$ is the localization of $R$ at $M$ as a monoid with zero. This means there exists a canonical ring homomorphism $\text{algebraMap}\, R\, S : R \to S$ that satisfies: 1. For every $y \in M$, $\text{algebraMap}\, R\, S\, y$ is a unit in $S$ 2. For every $z \in S$, there exists $(x, y) \in R \times M$ such that $z \cdot \text{algebraMap}\, R\, S\, y = \text{algebraMap}\, R\, S\, x$ 3. For any $x, y \in R$, if $\text{algebraMap}\, R\, S\, x = \text{algebraMap}\, R\, S\, y$, then there exists $c \in M$ such that $x \cdot c = y \cdot c$

IsLocalization.toLocalizationMap abbrev

: Submonoid.LocalizationMap M S

Full source

/-- `IsLocalization.toLocalizationMap M S` shows `S` is the monoid localization of `R` at `M`. -/
abbrev toLocalizationMap : Submonoid.LocalizationMap M S :=
  (toLocalizationWithZeroMap M S).toLocalizationMap

Localization of a Commutative Ring at a Submonoid as a Monoid

Informal description

Given a commutative ring $R$ and a submonoid $M$ of $R$, the function `IsLocalization.toLocalizationMap` provides evidence that $S$ is the localization of $R$ at $M$ as a monoid. This means there exists a canonical ring homomorphism $\text{algebraMap}\, R\, S : R \to S$ that satisfies: 1. For every $y \in M$, $\text{algebraMap}\, R\, S\, y$ is a unit in $S$; 2. For every $z \in S$, there exists $(x, y) \in R \times M$ such that $z \cdot \text{algebraMap}\, R\, S\, y = \text{algebraMap}\, R\, S\, x$; 3. For any $x, y \in R$, if $\text{algebraMap}\, R\, S\, x = \text{algebraMap}\, R\, S\, y$, then there exists $c \in M$ such that $x \cdot c = y \cdot c$.

IsLocalization.toLocalizationMap_toMap theorem

: (toLocalizationMap M S).toMap = (algebraMap R S : R →*₀ S)

Full source

@[simp]
theorem toLocalizationMap_toMap : (toLocalizationMap M S).toMap = (algebraMap R S : R →*₀ S) :=
  rfl

Localization Map Equals Algebra Map as Monoid Homomorphism

Informal description

The underlying monoid homomorphism of the localization map from $R$ to $S$ at the submonoid $M$ is equal to the algebra map from $R$ to $S$, considered as a monoid homomorphism with zero.

IsLocalization.toLocalizationMap_toMap_apply theorem

(x) : (toLocalizationMap M S).toMap x = algebraMap R S x

Full source

theorem toLocalizationMap_toMap_apply (x) : (toLocalizationMap M S).toMap x = algebraMap R S x :=
  rfl

Equality of Localization and Algebra Maps on Elements

Informal description

For any element $x \in R$, the monoid homomorphism $\text{toMap}$ associated with the localization map of $R$ at $M$ evaluated at $x$ is equal to the algebra map $\text{algebraMap}\, R\, S$ evaluated at $x$, i.e., $\text{toMap}(x) = \text{algebraMap}\, R\, S\, x$.

IsLocalization.surj₂ theorem

 :
  ∀ z w : S,
    ∃ z' w' : R, ∃ d : M, (z * algebraMap R S d = algebraMap R S z') ∧ (w * algebraMap R S d = algebraMap R S w')

Full source

theorem surj₂ : ∀ z w : S, ∃ z' w' : R, ∃ d : M,
    (z * algebraMap R S d = algebraMap R S z') ∧ (w * algebraMap R S d = algebraMap R S w') :=
  (toLocalizationMap M S).surj₂

Simultaneous Fraction Representation in Localization

Informal description

For any elements $z$ and $w$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, there exist elements $z', w' \in R$ and $d \in M$ such that: \[ z \cdot f(d) = f(z') \quad \text{and} \quad w \cdot f(d) = f(w'), \] where $f = \text{algebraMap}\, R\, S$ is the canonical ring homomorphism from $R$ to $S$.

IsLocalization.sec definition

(z : S) : R × M

Full source

/-- Given a localization map `f : M →* N`, a section function sending `z : N` to some
`(x, y) : M × S` such that `f x * (f y)⁻¹ = z`. -/
noncomputable def sec (z : S) : R × M :=
  Classical.choose <| IsLocalization.surj _ z

Section function for localization elements

Informal description

Given a localization map $f \colon R \to S$ at a submonoid $M \subseteq R$, for any element $z \in S$, the function returns a pair $(x, y) \in R \times M$ such that $z \cdot f(y) = f(x)$. This means every element of the localization can be represented as a fraction $f(x)/f(y)$ where $x \in R$ and $y \in M$.

IsLocalization.toLocalizationMap_sec theorem

: (toLocalizationMap M S).sec = sec M

Full source

@[simp]
theorem toLocalizationMap_sec : (toLocalizationMap M S).sec = sec M :=
  rfl

Equality of Section Functions in Localization

Informal description

The section function of the localization map from $R$ to $S$ at submonoid $M$ coincides with the section function `sec M` for the localization.

IsLocalization.sec_spec theorem

(z : S) : z * algebraMap R S (IsLocalization.sec M z).2 = algebraMap R S (IsLocalization.sec M z).1

Full source

/-- Given `z : S`, `IsLocalization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x` (so this lemma is true by definition). -/
theorem sec_spec (z : S) :
    z * algebraMap R S (IsLocalization.sec M z).2 = algebraMap R S (IsLocalization.sec M z).1 :=
  Classical.choose_spec <| IsLocalization.surj _ z

Representation of Localization Elements as Fractions

Informal description

For any element $z$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, if $(x, y) \in R \times M$ is the pair obtained from `IsLocalization.sec M z`, then $z \cdot f(y) = f(x)$, where $f \colon R \to S$ is the canonical ring homomorphism.

IsLocalization.sec_spec' theorem

(z : S) : algebraMap R S (IsLocalization.sec M z).1 = algebraMap R S (IsLocalization.sec M z).2 * z

Full source

/-- Given `z : S`, `IsLocalization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x`, so this lemma is just an application of `S`'s commutativity. -/
theorem sec_spec' (z : S) :
    algebraMap R S (IsLocalization.sec M z).1 = algebraMap R S (IsLocalization.sec M z).2 * z := by
  rw [mul_comm, sec_spec]

Fraction Representation in Localization: $f(x) = f(y) \cdot z$

Informal description

For any element $z$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, if $(x, y) \in R \times M$ is the pair obtained from the section function $\mathrm{sec}_M(z)$, then the canonical ring homomorphism $f \colon R \to S$ satisfies $f(x) = f(y) \cdot z$.

IsLocalization.subsingleton theorem

(h : 0 ∈ M) : Subsingleton S

Full source

/-- If `M` contains `0` then the localization at `M` is trivial. -/
theorem subsingleton (h : 0 ∈ M) : Subsingleton S := (toLocalizationMap M S).subsingleton h

Localization at a submonoid containing zero is trivial

Informal description

If the submonoid $M$ of a commutative ring $R$ contains the zero element, then the localization $S$ of $R$ at $M$ is a subsingleton (i.e., has at most one element).

IsLocalization.subsingleton_iff theorem

: Subsingleton S ↔ 0 ∈ M

Full source

protected theorem subsingleton_iff : SubsingletonSubsingleton S ↔ 0 ∈ M :=
  ⟨fun _ ↦ have ⟨c, eq⟩ := exists_of_eq (M := M) (S := S) (x := 0) (y := 1) (Subsingleton.elim _ _)
    by rw [mul_zero, mul_one] at eq; exact eq ▸ c.2, subsingleton⟩

Localization is Trivial if and only if Submonoid Contains Zero

Informal description

The localization $S$ of a commutative ring $R$ at a submonoid $M$ is a subsingleton (i.e., has at most one element) if and only if the submonoid $M$ contains the zero element of $R$.

IsLocalization.map_right_cancel theorem

{x y} {c : M} (h : algebraMap R S (c * x) = algebraMap R S (c * y)) : algebraMap R S x = algebraMap R S y

Full source

theorem map_right_cancel {x y} {c : M} (h : algebraMap R S (c * x) = algebraMap R S (c * y)) :
    algebraMap R S x = algebraMap R S y :=
  (toLocalizationMap M S).map_right_cancel h

Right Cancellation Property in Localization

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any elements $x, y \in R$ and $c \in M$, if the images of $c \cdot x$ and $c \cdot y$ under the localization map $\text{algebraMap}\, R\, S$ are equal, then the images of $x$ and $y$ under $\text{algebraMap}\, R\, S$ are also equal.

IsLocalization.map_left_cancel theorem

{x y} {c : M} (h : algebraMap R S (x * c) = algebraMap R S (y * c)) : algebraMap R S x = algebraMap R S y

Full source

theorem map_left_cancel {x y} {c : M} (h : algebraMap R S (x * c) = algebraMap R S (y * c)) :
    algebraMap R S x = algebraMap R S y :=
  (toLocalizationMap M S).map_left_cancel h

Left Cancellation Property in Localization: $x \cdot c = y \cdot c \Rightarrow x = y$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any elements $x, y \in R$ and $c \in M$, if $\text{algebraMap}\, R\, S\, (x \cdot c) = \text{algebraMap}\, R\, S\, (y \cdot c)$, then $\text{algebraMap}\, R\, S\, x = \text{algebraMap}\, R\, S\, y$.

IsLocalization.map_eq_zero_iff theorem

(r : R) : algebraMap R S r = 0 ↔ ∃ m : M, ↑m * r = 0

Full source

theorem map_eq_zero_iff (r : R) : algebraMapalgebraMap R S r = 0 ↔ ∃ m : M, ↑m * r = 0 := by
  constructor
  · intro h
    obtain ⟨m, hm⟩ := (IsLocalization.eq_iff_exists M S).mp ((algebraMap R S).map_zero.trans h.symm)
    exact ⟨m, by simpa using hm.symm⟩
  · rintro ⟨m, hm⟩
    rw [← (IsLocalization.map_units S m).mul_right_inj, mul_zero, ← RingHom.map_mul, hm,
      RingHom.map_zero]

Characterization of Zero in Localization: $\text{algebraMap}\, R\, S\, r = 0 \leftrightarrow \exists m \in M, m \cdot r = 0$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any element $r \in R$, the image of $r$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S : R \to S$ is zero if and only if there exists an element $m \in M$ such that $m \cdot r = 0$ in $R$.

IsLocalization.mk' definition

(x : R) (y : M) : S

Full source

/-- `IsLocalization.mk' S` is the surjection sending `(x, y) : R × M` to
`f x * (f y)⁻¹`. -/
noncomputable def mk' (x : R) (y : M) : S :=
  (toLocalizationMap M S).mk' x y

Construction of localization elements as fractions

Informal description

Given a commutative ring $ R $ with a submonoid $ M $ and its localization $ S $ at $ M $, the function $ \text{mk'} $ sends a pair $(x, y) \in R \times M$ to the element $ f(x) \cdot (f(y))^{-1} $ in $ S $, where $ f : R \to S $ is the canonical ring homomorphism.

IsLocalization.mk'_sec theorem

(z : S) : mk' S (IsLocalization.sec M z).1 (IsLocalization.sec M z).2 = z

Full source

@[simp]
theorem mk'_sec (z : S) : mk' S (IsLocalization.sec M z).1 (IsLocalization.sec M z).2 = z :=
  (toLocalizationMap M S).mk'_sec _

Localization Element as Fraction: $\text{mk'}_S(\text{sec}_M(z)) = z$

Informal description

For any element $z$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, the construction of $z$ as a fraction $\text{mk'}_S(x, y)$ equals $z$, where $(x, y) \in R \times M$ is the pair obtained from the section function $\text{sec}_M(z)$.

IsLocalization.mk'_mul theorem

(x₁ x₂ : R) (y₁ y₂ : M) : mk' S (x₁ * x₂) (y₁ * y₂) = mk' S x₁ y₁ * mk' S x₂ y₂

Full source

theorem mk'_mul (x₁ x₂ : R) (y₁ y₂ : M) : mk' S (x₁ * x₂) (y₁ * y₂) = mk' S x₁ y₁ * mk' S x₂ y₂ :=
  (toLocalizationMap M S).mk'_mul _ _ _ _

Multiplicativity of Localization Construction: $\text{mk'}_S(x₁x₂, y₁y₂) = \text{mk'}_S(x₁, y₁) \cdot \text{mk'}_S(x₂, y₂)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x₁, x₂ \in R$ and $y₁, y₂ \in M$, the following equality holds in $S$: \[ \text{mk'}_S(x₁x₂, y₁y₂) = \text{mk'}_S(x₁, y₁) \cdot \text{mk'}_S(x₂, y₂), \] where $\text{mk'}_S(x, y) = f(x) \cdot f(y)^{-1}$ for the canonical ring homomorphism $f \colon R \to S$.

IsLocalization.mk'_one theorem

(x) : mk' S x (1 : M) = algebraMap R S x

Full source

theorem mk'_one (x) : mk' S x (1 : M) = algebraMap R S x :=
  (toLocalizationMap M S).mk'_one _

Localization of an Element at the Identity: $\text{mk'}_S(x, 1) = \text{algebraMap}_R^S(x)$

Informal description

For any element $x$ in a commutative ring $R$ and the multiplicative identity $1$ in a submonoid $M$ of $R$, the localization of $x$ at $1$ is equal to the image of $x$ under the canonical ring homomorphism from $R$ to its localization $S$ at $M$, i.e., \[ \text{mk'}_S(x, 1) = \text{algebraMap}_R^S(x). \]

IsLocalization.mk'_spec theorem

(x) (y : M) : mk' S x y * algebraMap R S y = algebraMap R S x

Full source

@[simp]
theorem mk'_spec (x) (y : M) : mk' S x y * algebraMap R S y = algebraMap R S x :=
  (toLocalizationMap M S).mk'_spec _ _

Characterization of Localized Elements via Canonical Homomorphism

Informal description

For any element $x$ in a commutative ring $R$ and any element $y$ in a submonoid $M$ of $R$, the product of the localized element $\text{mk'}_S(x, y)$ and the image of $y$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S\, y$ equals the image of $x$ under $\text{algebraMap}\, R\, S$, i.e., \[ \text{mk'}_S(x, y) \cdot \text{algebraMap}\, R\, S\, y = \text{algebraMap}\, R\, S\, x. \]

IsLocalization.mk'_spec' theorem

(x) (y : M) : algebraMap R S y * mk' S x y = algebraMap R S x

Full source

@[simp]
theorem mk'_spec' (x) (y : M) : algebraMap R S y * mk' S x y = algebraMap R S x :=
  (toLocalizationMap M S).mk'_spec' _ _

Localization Fraction Multiplication Identity

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$ and $y \in M$, the element $\text{algebraMap}\, R\, S\, y$ multiplied by the localized fraction $\text{mk'}\, S\, x\, y$ equals $\text{algebraMap}\, R\, S\, x$. In other words, \[ f(y) \cdot \left( \frac{f(x)}{f(y)} \right) = f(x) \] where $f = \text{algebraMap}\, R\, S$ is the canonical ring homomorphism.

IsLocalization.mk'_spec_mk theorem

(x) (y : R) (hy : y ∈ M) : mk' S x ⟨y, hy⟩ * algebraMap R S y = algebraMap R S x

Full source

@[simp]
theorem mk'_spec_mk (x) (y : R) (hy : y ∈ M) :
    mk' S x ⟨y, hy⟩ * algebraMap R S y = algebraMap R S x :=
  mk'_spec S x ⟨y, hy⟩

Localization Fraction Multiplication Identity with Explicit Membership Proof

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$ and $y \in R$ such that $y \in M$, the product of the localized fraction $\text{mk'}_S(x, \langle y, hy \rangle)$ and the image of $y$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S\, y$ equals the image of $x$ under $\text{algebraMap}\, R\, S$, i.e., \[ \text{mk'}_S(x, \langle y, hy \rangle) \cdot f(y) = f(x) \] where $f = \text{algebraMap}\, R\, S$ is the canonical ring homomorphism and $\langle y, hy \rangle$ denotes the element $y$ together with the proof $hy$ that $y \in M$.

IsLocalization.mk'_spec'_mk theorem

(x) (y : R) (hy : y ∈ M) : algebraMap R S y * mk' S x ⟨y, hy⟩ = algebraMap R S x

Full source

@[simp]
theorem mk'_spec'_mk (x) (y : R) (hy : y ∈ M) :
    algebraMap R S y * mk' S x ⟨y, hy⟩ = algebraMap R S x :=
  mk'_spec' S x ⟨y, hy⟩

Localization Fraction Multiplication Identity for Elements in Submonoid

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$ and $y \in R$ such that $y \in M$, the following identity holds in $S$: \[ f(y) \cdot \left( \frac{f(x)}{f(y)} \right) = f(x), \] where $f = \text{algebraMap}\, R\, S$ is the canonical ring homomorphism from $R$ to $S$, and $\langle y, hy \rangle$ denotes the element $y$ viewed as a member of $M$ via the proof $hy$ that $y \in M$.

IsLocalization.mk'_eq_iff_eq_mul theorem

{x} {y : M} {z} : mk' S x y = z ↔ algebraMap R S x = z * algebraMap R S y

Full source

theorem mk'_eq_iff_eq_mul {x} {y : M} {z} :
    mk'mk' S x y = z ↔ algebraMap R S x = z * algebraMap R S y :=
  (toLocalizationMap M S).mk'_eq_iff_eq_mul

Characterization of Localization Elements as Fractions: $\text{mk'}(x, y) = z \leftrightarrow \text{algebraMap}(x) = z \cdot \text{algebraMap}(y)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$, $y \in M$, and $z \in S$, the equality $\text{mk'}(x, y) = z$ holds if and only if the canonical ring homomorphism $\text{algebraMap}\, R\, S$ satisfies $\text{algebraMap}\, R\, S\, x = z \cdot \text{algebraMap}\, R\, S\, y$.

IsLocalization.mk'_add_eq_iff_add_mul_eq_mul theorem

 {x} {y : M} {z₁ z₂} : mk' S x y + z₁ = z₂ ↔ algebraMap R S x + z₁ * algebraMap R S y = z₂ * algebraMap R S y

Full source

theorem mk'_add_eq_iff_add_mul_eq_mul {x} {y : M} {z₁ z₂} :
    mk'mk' S x y + z₁ = z₂ ↔ algebraMap R S x + z₁ * algebraMap R S y = z₂ * algebraMap R S y := by
  rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]

Characterization of Addition in Localization: $\frac{x}{y} + z_1 = z_2 \leftrightarrow x + z_1 y = z_2 y$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$, $y \in M$, and $z_1, z_2 \in S$, the following equivalence holds: \[ \text{mk'}_S(x,y) + z_1 = z_2 \leftrightarrow \text{algebraMap}_R^S(x) + z_1 \cdot \text{algebraMap}_R^S(y) = z_2 \cdot \text{algebraMap}_R^S(y). \] Here, $\text{mk'}_S(x,y)$ denotes the element $f(x) \cdot f(y)^{-1}$ in $S$, where $f = \text{algebraMap}_R^S$ is the canonical ring homomorphism from $R$ to $S$.

IsLocalization.mk'_pow theorem

(x : R) (y : M) (n : ℕ) : mk' S (x ^ n) (y ^ n) = mk' S x y ^ n

Full source

theorem mk'_pow (x : R) (y : M) (n : ℕ) : mk' S (x ^ n) (y ^ n) = mk' S x y ^ n := by
  simp_rw [IsLocalization.mk'_eq_iff_eq_mul, SubmonoidClass.coe_pow, map_pow, ← mul_pow]
  simp

Power of Fractions in Localization: $\frac{x^n}{y^n} = \left(\frac{x}{y}\right)^n$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$, $y \in M$, and natural number $n$, the fraction $\frac{x^n}{y^n}$ in $S$ equals the $n$-th power of the fraction $\frac{x}{y}$, i.e., \[ \text{mk'}_S(x^n, y^n) = (\text{mk'}_S(x, y))^n. \]

IsLocalization.mk'_surjective theorem

(z : S) : ∃ (x : _) (y : M), mk' S x y = z

Full source

theorem mk'_surjective (z : S) : ∃ (x : _) (y : M), mk' S x y = z :=
  let ⟨r, hr⟩ := IsLocalization.surj _ z
  ⟨r.1, r.2, (eq_mk'_iff_mul_eq.2 hr).symm⟩

Surjectivity of Fraction Representation in Localization

Informal description

For every element $z$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, there exist an element $x \in R$ and an element $y \in M$ such that the fraction $\frac{x}{y}$ (represented as $\text{mk'}_S(x,y)$) equals $z$.

IsLocalization.fintype' definition

[Fintype R] : Fintype S

Full source

/-- The localization of a `Fintype` is a `Fintype`. Cannot be an instance. -/
noncomputable def fintype' [Fintype R] : Fintype S :=
  have := Classical.propDecidable
  Fintype.ofSurjective (Function.uncurry <| IsLocalization.mk' S) fun a =>
    Prod.exists'.mpr <| IsLocalization.mk'_surjective M a

Finiteness of localization at a submonoid for finite rings

Informal description

Given a commutative ring $ R $ with a submonoid $ M $ and its localization $ S $ at $ M $, if $ R $ is a finite type (i.e., has finitely many elements), then $ S $ is also a finite type. This is constructed by showing that the function mapping pairs $(x, y) \in R \times M$ to the fraction $ \frac{x}{y} $ in $ S $ is surjective, and since $ R \times M $ is finite when $ R $ is finite, $ S $ must also be finite.

IsLocalization.uniqueOfZeroMem definition

(h : (0 : R) ∈ M) : Unique S

Full source

/-- Localizing at a submonoid with 0 inside it leads to the trivial ring. -/
def uniqueOfZeroMem (h : (0 : R) ∈ M) : Unique S :=
  uniqueOfZeroEqOne <| by simpa using IsLocalization.map_units S ⟨0, h⟩

Trivial localization when zero is in the submonoid

Informal description

If the zero element $0$ of a commutative ring $R$ is contained in a submonoid $M$ of $R$, then the localization $S$ of $R$ at $M$ is the trivial ring (i.e., a unique up to isomorphism ring with one element).

IsLocalization.mk'_eq_iff_eq theorem

 {x₁ x₂} {y₁ y₂ : M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebraMap R S (y₂ * x₁) = algebraMap R S (y₁ * x₂)

Full source

theorem mk'_eq_iff_eq {x₁ x₂} {y₁ y₂ : M} :
    mk'mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebraMap R S (y₂ * x₁) = algebraMap R S (y₁ * x₂) :=
  (toLocalizationMap M S).mk'_eq_iff_eq

Equality of Localization Fractions via Cross-Multiplication

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x_1, x_2 \in R$ and $y_1, y_2 \in M$, the equality $\frac{x_1}{y_1} = \frac{x_2}{y_2}$ holds in $S$ if and only if the canonical ring homomorphism $\text{algebraMap}\, R\, S$ satisfies $\text{algebraMap}\, R\, S\, (y_2 \cdot x_1) = \text{algebraMap}\, R\, S\, (y_1 \cdot x_2)$.

IsLocalization.mk'_eq_iff_eq' theorem

 {x₁ x₂} {y₁ y₂ : M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebraMap R S (x₁ * y₂) = algebraMap R S (x₂ * y₁)

Full source

theorem mk'_eq_iff_eq' {x₁ x₂} {y₁ y₂ : M} :
    mk'mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebraMap R S (x₁ * y₂) = algebraMap R S (x₂ * y₁) :=
  (toLocalizationMap M S).mk'_eq_iff_eq'

Equality of Localization Elements via Cross-Multiplication

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x_1, x_2 \in R$ and $y_1, y_2 \in M$, the equality $\text{mk'}_S(x_1, y_1) = \text{mk'}_S(x_2, y_2)$ holds if and only if the images of $x_1 y_2$ and $x_2 y_1$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$ are equal, i.e., $\text{algebraMap}\, R\, S\, (x_1 y_2) = \text{algebraMap}\, R\, S\, (x_2 y_1)$.

IsLocalization.eq theorem

 {a₁ b₁} {a₂ b₂ : M} : mk' S a₁ a₂ = mk' S b₁ b₂ ↔ ∃ c : M, ↑c * (↑b₂ * a₁) = c * (a₂ * b₁)

Full source

protected theorem eq {a₁ b₁} {a₂ b₂ : M} :
    mk'mk' S a₁ a₂ = mk' S b₁ b₂ ↔ ∃ c : M, ↑c * (↑b₂ * a₁) = c * (a₂ * b₁) :=
  (toLocalizationMap M S).eq

Equality Criterion for Fractions in Localization: $\frac{a_1}{a_2} = \frac{b_1}{b_2} \leftrightarrow \exists c \in M, c \cdot (b_2 \cdot a_1) = c \cdot (a_2 \cdot b_1)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $a_1, b_1 \in R$ and $a_2, b_2 \in M$, the equality $\frac{a_1}{a_2} = \frac{b_1}{b_2}$ holds in $S$ if and only if there exists an element $c \in M$ such that $c \cdot (b_2 \cdot a_1) = c \cdot (a_2 \cdot b_1)$ in $R$.

IsLocalization.mk'_eq_zero_iff theorem

(x : R) (s : M) : mk' S x s = 0 ↔ ∃ m : M, ↑m * x = 0

Full source

theorem mk'_eq_zero_iff (x : R) (s : M) : mk'mk' S x s = 0 ↔ ∃ m : M, ↑m * x = 0 := by
  rw [← (map_units S s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff M]

Characterization of Zero in Localization: $\frac{x}{s} = 0 \leftrightarrow \exists m \in M, m \cdot x = 0$

Informal description

For any element $x$ in a commutative ring $R$ and any element $s$ in a submonoid $M$ of $R$, the localized element $\frac{x}{s}$ is zero in the localization $S$ of $R$ at $M$ if and only if there exists an element $m \in M$ such that $m \cdot x = 0$ in $R$.

IsLocalization.mk'_zero theorem

(s : M) : IsLocalization.mk' S 0 s = 0

Full source

@[simp]
theorem mk'_zero (s : M) : IsLocalization.mk' S 0 s = 0 := by
  rw [eq_comm, IsLocalization.eq_mk'_iff_mul_eq, zero_mul, map_zero]

Localization of Zero is Zero

Informal description

For any element $s$ in the submonoid $M$ of a commutative ring $R$, the localization of $0$ at $s$ in the ring $S$ is equal to $0$, i.e., $\text{mk'}_S(0, s) = 0$.

IsLocalization.ne_zero_of_mk'_ne_zero theorem

{x : R} {y : M} (hxy : IsLocalization.mk' S x y ≠ 0) : x ≠ 0

Full source

theorem ne_zero_of_mk'_ne_zero {x : R} {y : M} (hxy : IsLocalization.mk'IsLocalization.mk' S x y ≠ 0) : x ≠ 0 := by
  rintro rfl
  exact hxy (IsLocalization.mk'_zero _)

Nonzero Localization Implies Nonzero Numerator

Informal description

For any elements $x \in R$ and $y \in M$, if the localized element $\text{mk'}_S(x, y) \neq 0$ in $S$, then $x \neq 0$ in $R$.

IsLocalization.noZeroDivisors theorem

[NoZeroDivisors R] : NoZeroDivisors S

Full source

/-- Any localization of a commutative semiring without zero-divisors also has no zero-divisors. -/
theorem noZeroDivisors [NoZeroDivisors R] : NoZeroDivisors S where
  eq_zero_or_eq_zero_of_mul_eq_zero {x y} eq := by
    nontriviality S
    obtain ⟨x, s, rfl⟩ := mk'_surjective M x
    obtain ⟨y, t, rfl⟩ := mk'_surjective M y
    rw [← mk'_mul, mk'_eq_zero_iff] at eq
    have ⟨m, eq⟩ := eq
    obtain eq | eq := eq_zero_or_eq_zero_of_mul_eq_zero eq
    · exact absurd (subsingleton (eq ▸ m.2)) (not_subsingleton S)
    obtain rfl | rfl := eq_zero_or_eq_zero_of_mul_eq_zero eq <;> simp

Preservation of No-Zero-Divisors Property under Localization

Informal description

If a commutative ring $R$ has no zero divisors, then any localization $S$ of $R$ at a submonoid $M$ also has no zero divisors.

IsLocalization.sec_fst_ne_zero theorem

{x : S} (hx : x ≠ 0) : (sec M x).fst ≠ 0

Full source

theorem sec_fst_ne_zero {x : S} (hx : x ≠ 0) : (sec M x).fst ≠ 0 :=
  mt (fun h ↦ by rw [← mk'_sec (M := M) S x, h, mk'_zero]) hx

Nonzero Localization Elements Have Nonzero Numerators

Informal description

For any nonzero element $x$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, the first component of the pair $\text{sec}_M(x) \in R \times M$ is nonzero. That is, if $x \neq 0$ in $S$, then the numerator in any representation of $x$ as a fraction $\frac{a}{b}$ with $a \in R$ and $b \in M$ must satisfy $a \neq 0$.

IsLocalization.mk'_eq_iff_mk'_eq theorem

 [Algebra R P] [IsLocalization M P] {x₁ x₂} {y₁ y₂ : M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ mk' P x₁ y₁ = mk' P x₂ y₂

Full source

theorem mk'_eq_iff_mk'_eq [Algebra R P] [IsLocalization M P] {x₁ x₂} {y₁ y₂ : M} :
    mk'mk' S x₁ y₁ = mk' S x₂ y₂ ↔ mk' P x₁ y₁ = mk' P x₂ y₂ :=
  (toLocalizationMap M S).mk'_eq_iff_mk'_eq (toLocalizationMap M P)

Equality of Fractions in Localizations is Independent of the Localization Chosen

Informal description

Let $R$ be a commutative ring with submonoid $M$, and let $S$ and $P$ be localizations of $R$ at $M$ (i.e., $S$ and $P$ are $R$-algebras satisfying the `IsLocalization` conditions for $M$). For any elements $x₁, x₂ \in R$ and $y₁, y₂ \in M$, the equality of fractions $\frac{x₁}{y₁} = \frac{x₂}{y₂}$ holds in $S$ if and only if it holds in $P$. Here, $\frac{x}{y}$ denotes the element $\text{mk'}\, x\, y$ in the respective localization.

IsLocalization.mk'_eq_of_eq theorem

{a₁ b₁ : R} {a₂ b₂ : M} (H : ↑a₂ * b₁ = ↑b₂ * a₁) : mk' S a₁ a₂ = mk' S b₁ b₂

Full source

theorem mk'_eq_of_eq {a₁ b₁ : R} {a₂ b₂ : M} (H : ↑a₂ * b₁ = ↑b₂ * a₁) :
    mk' S a₁ a₂ = mk' S b₁ b₂ :=
  (toLocalizationMap M S).mk'_eq_of_eq H

Equality of Localized Fractions via Cross-Multiplication

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $a_1, b_1 \in R$ and $a_2, b_2 \in M$, if $a_2 \cdot b_1 = b_2 \cdot a_1$ holds in $R$, then the fractions $\text{mk'}_S(a_1, a_2)$ and $\text{mk'}_S(b_1, b_2)$ are equal in $S$.

IsLocalization.mk'_eq_of_eq' theorem

{a₁ b₁ : R} {a₂ b₂ : M} (H : b₁ * ↑a₂ = a₁ * ↑b₂) : mk' S a₁ a₂ = mk' S b₁ b₂

Full source

theorem mk'_eq_of_eq' {a₁ b₁ : R} {a₂ b₂ : M} (H : b₁ * ↑a₂ = a₁ * ↑b₂) :
    mk' S a₁ a₂ = mk' S b₁ b₂ :=
  (toLocalizationMap M S).mk'_eq_of_eq' H

Equality of Localized Fractions via Cross-Multiplication

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $a_1, b_1 \in R$ and $a_2, b_2 \in M$, if $b_1 \cdot a_2 = a_1 \cdot b_2$ holds in $R$, then the fractions $\text{mk'}_S(a_1, a_2)$ and $\text{mk'}_S(b_1, b_2)$ are equal in $S$.

IsLocalization.mk'_cancel theorem

(a : R) (b c : M) : mk' S (a * c) (b * c) = mk' S a b

Full source

theorem mk'_cancel (a : R) (b c : M) :
    mk' S (a * c) (b * c) = mk' S a b := (toLocalizationMap M S).mk'_cancel _ _ _

Cancellation property of localization fractions: $\text{mk'}_S(a \cdot c, b \cdot c) = \text{mk'}_S(a, b)$

Informal description

For any element $a$ in a commutative ring $R$ and any elements $b, c$ in a submonoid $M$ of $R$, the localization element $\text{mk'}_S(a \cdot c, b \cdot c)$ is equal to $\text{mk'}_S(a, b)$ in the localization $S$ of $R$ at $M$.

IsLocalization.mk'_self theorem

{x : R} (hx : x ∈ M) : mk' S x ⟨x, hx⟩ = 1

Full source

@[simp]
theorem mk'_self {x : R} (hx : x ∈ M) : mk' S x ⟨x, hx⟩ = 1 :=
  (toLocalizationMap M S).mk'_self _ hx

Localization of a Ring Element at Itself Yields the Identity

Informal description

For any element $x$ in a commutative ring $R$ that belongs to a submonoid $M$ of $R$, the localization of $x$ at itself in the localized ring $S$ is equal to the multiplicative identity, i.e., $\text{mk'}_S\, x\, \langle x, hx \rangle = 1$, where $hx$ is a proof that $x \in M$.

IsLocalization.mk'_self' theorem

{x : M} : mk' S (x : R) x = 1

Full source

@[simp]
theorem mk'_self' {x : M} : mk' S (x : R) x = 1 :=
  (toLocalizationMap M S).mk'_self' _

Localization of a submonoid element at itself yields the identity: $\text{mk'}_S(x, x) = 1$

Informal description

For any element $x$ in the submonoid $M$ of a commutative ring $R$, the localization of $x$ at itself in the localized ring $S$ equals the multiplicative identity, i.e., $\text{mk'}_S(x, x) = 1$.

IsLocalization.mk'_self'' theorem

{x : M} : mk' S x.1 x = 1

Full source

theorem mk'_self'' {x : M} : mk' S x.1 x = 1 :=
  mk'_self' _

Localization of Submonoid Element at Itself Yields Identity

Informal description

For any element $x$ in the submonoid $M$ of a commutative ring $R$, the localization of $x$ (viewed as an element of $R$) at itself in the localized ring $S$ equals the multiplicative identity, i.e., $\text{mk'}_S(x.1, x) = 1$.

IsLocalization.mul_mk'_eq_mk'_of_mul theorem

(x y : R) (z : M) : (algebraMap R S) x * mk' S y z = mk' S (x * y) z

Full source

theorem mul_mk'_eq_mk'_of_mul (x y : R) (z : M) :
    (algebraMap R S) x * mk' S y z = mk' S (x * y) z :=
  (toLocalizationMap M S).mul_mk'_eq_mk'_of_mul _ _ _

Multiplication of Canonical Image and Localized Element in Localization

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x, y \in R$ and $z \in M$, the product of the image of $x$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$ and the localized element $\text{mk'}\, S\, y\, z$ is equal to the localized element $\text{mk'}\, S\, (x \cdot y)\, z$. In other words, we have: \[ \text{algebraMap}\, R\, S\, x \cdot \text{mk'}\, S\, y\, z = \text{mk'}\, S\, (x \cdot y)\, z \]

IsLocalization.mk'_eq_mul_mk'_one theorem

(x : R) (y : M) : mk' S x y = (algebraMap R S) x * mk' S 1 y

Full source

theorem mk'_eq_mul_mk'_one (x : R) (y : M) : mk' S x y = (algebraMap R S) x * mk' S 1 y :=
  ((toLocalizationMap M S).mul_mk'_one_eq_mk' _ _).symm

Localization Element as Product of Canonical Image and Unit Localization

Informal description

For any element $x$ in a commutative ring $R$ and any element $y$ in a submonoid $M$ of $R$, the localization element $\text{mk'}_S(x, y)$ in the localization $S$ of $R$ at $M$ can be expressed as the product of the image of $x$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$ and the localization element $\text{mk'}_S(1, y)$. In other words, \[ \text{mk'}_S(x, y) = (\text{algebraMap}\, R\, S)(x) \cdot \text{mk'}_S(1, y). \]

IsLocalization.mk'_mul_cancel_left theorem

(x : R) (y : M) : mk' S (y * x : R) y = (algebraMap R S) x

Full source

@[simp]
theorem mk'_mul_cancel_left (x : R) (y : M) : mk' S (y * x : R) y = (algebraMap R S) x :=
  (toLocalizationMap M S).mk'_mul_cancel_left _ _

Cancellation property of left multiplication in localization: $\text{mk'}_S(yx, y) = \text{algebraMap}\, R\, S\, x$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $x \in R$ and $y \in M$, the element $\text{mk'}_S(y \cdot x, y)$ in $S$ equals the image of $x$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$.

IsLocalization.mk'_mul_cancel_right theorem

(x : R) (y : M) : mk' S (x * y) y = (algebraMap R S) x

Full source

theorem mk'_mul_cancel_right (x : R) (y : M) : mk' S (x * y) y = (algebraMap R S) x :=
  (toLocalizationMap M S).mk'_mul_cancel_right _ _

Cancellation property of fractions in localization: $\text{mk'}_S(x \cdot y, y) = \text{algebraMap}\, R\, S\, x$

Informal description

For any element $x$ in a commutative ring $R$ and any element $y$ in a submonoid $M$ of $R$, the fraction $\text{mk'}_S(x \cdot y, y)$ in the localization $S$ of $R$ at $M$ equals the image of $x$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$.

IsLocalization.mk'_mul_mk'_eq_one theorem

(x y : M) : mk' S (x : R) y * mk' S (y : R) x = 1

Full source

@[simp]
theorem mk'_mul_mk'_eq_one (x y : M) : mk' S (x : R) y * mk' S (y : R) x = 1 := by
  rw [← mk'_mul, mul_comm]; exact mk'_self _ _

Inverse Relation in Localization: $\text{mk'}_S(x, y) \cdot \text{mk'}_S(y, x) = 1$

Informal description

For any elements $x, y$ in a submonoid $M$ of a commutative ring $R$, the product of the localized elements $\text{mk'}_S(x, y)$ and $\text{mk'}_S(y, x)$ in the localization $S$ of $R$ at $M$ equals the multiplicative identity $1$, i.e., \[ \text{mk'}_S(x, y) \cdot \text{mk'}_S(y, x) = 1. \] Here, $\text{mk'}_S(a, b) = f(a) \cdot f(b)^{-1}$ for the canonical ring homomorphism $f \colon R \to S$.

IsLocalization.mk'_mul_mk'_eq_one' theorem

(x : R) (y : M) (h : x ∈ M) : mk' S x y * mk' S (y : R) ⟨x, h⟩ = 1

Full source

theorem mk'_mul_mk'_eq_one' (x : R) (y : M) (h : x ∈ M) : mk' S x y * mk' S (y : R) ⟨x, h⟩ = 1 :=
  mk'_mul_mk'_eq_one ⟨x, h⟩ _

Inverse Relation in Localization for Elements in Submonoid: $\text{mk'}_S(x, y) \cdot \text{mk'}_S(y, x) = 1$

Informal description

For any element $x \in R$ in a submonoid $M$ of a commutative ring $R$ (with $h$ being a proof that $x \in M$), and any element $y \in M$, the product of the localized elements $\text{mk'}_S(x, y)$ and $\text{mk'}_S(y, x)$ in the localization $S$ of $R$ at $M$ equals the multiplicative identity $1$, i.e., \[ \text{mk'}_S(x, y) \cdot \text{mk'}_S(y, x) = 1. \] Here, $\text{mk'}_S(a, b) = f(a) \cdot f(b)^{-1}$ for the canonical ring homomorphism $f \colon R \to S$.

IsLocalization.smul_mk' theorem

(x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m

Full source

theorem smul_mk' (x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m := by
  nth_rw 2 [← one_mul m]
  rw [mk'_mul, mk'_one, Algebra.smul_def]

Scalar Multiplication Commutes with Localization: $x \cdot \text{mk'}_S(y, m) = \text{mk'}_S(x \cdot y, m)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x, y \in R$ and $m \in M$, the scalar multiplication of $x$ with the localized element $\text{mk'}_S(y, m)$ satisfies: \[ x \cdot \text{mk'}_S(y, m) = \text{mk'}_S(x \cdot y, m), \] where $\text{mk'}_S(y, m) = f(y) \cdot f(m)^{-1}$ for the canonical ring homomorphism $f \colon R \to S$.

IsLocalization.smul_mk'_one theorem

(x : R) (m : M) : x • mk' S 1 m = mk' S x m

Full source

@[simp] theorem smul_mk'_one (x : R) (m : M) : x • mk' S 1 m = mk' S x m := by
  rw [smul_mk', mul_one]

Scalar Multiplication of Unity in Localization: $x \cdot \text{mk'}_S(1, m) = \text{mk'}_S(x, m)$

Informal description

For any element $x \in R$ and any element $m \in M$ of a submonoid $M$ of a commutative ring $R$, the scalar multiplication of $x$ with the localized element $\text{mk'}_S(1, m)$ in the localization $S$ of $R$ at $M$ satisfies: \[ x \cdot \text{mk'}_S(1, m) = \text{mk'}_S(x, m), \] where $\text{mk'}_S(a, b) = f(a) \cdot f(b)^{-1}$ for the canonical ring homomorphism $f \colon R \to S$.

IsLocalization.smul_mk'_self theorem

{m : M} {r : R} : (m : R) • mk' S r m = algebraMap R S r

Full source

@[simp] lemma smul_mk'_self {m : M} {r : R} :
    (m : R) • mk' S r m = algebraMap R S r := by
  rw [smul_mk', mk'_mul_cancel_left]

Scalar Multiplication by Denominator in Localization: $m \cdot \text{mk'}_S(r, m) = f(r)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any $r \in R$ and $m \in M$, the scalar multiplication of $m$ (viewed as an element of $R$) with the localized element $\text{mk'}_S(r, m)$ equals the image of $r$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S$. In other words: \[ m \cdot \text{mk'}_S(r, m) = \text{algebraMap}\, R\, S\, r \] where $\text{mk'}_S(r, m) = f(r) \cdot f(m)^{-1}$ for the canonical ring homomorphism $f \colon R \to S$.

IsLocalization.invertible_mk'_one instance

(s : M) : Invertible (IsLocalization.mk' S (1 : R) s)

Full source

@[simps]
instance invertible_mk'_one (s : M) : Invertible (IsLocalization.mk' S (1 : R) s) where
  invOf := algebraMap R S s
  invOf_mul_self := by simp
  mul_invOf_self := by simp

Invertibility of the Fraction $1/s$ in Localization

Informal description

For any localization $S$ of a commutative ring $R$ at a submonoid $M$, and any element $s \in M$, the element $\text{mk'}_S(1, s) \in S$ (representing the fraction $1/s$) is invertible.

IsLocalization.isUnit_comp theorem

(j : S →+* P) (y : M) : IsUnit (j.comp (algebraMap R S) y)

Full source

theorem isUnit_comp (j : S →+* P) (y : M) : IsUnit (j.comp (algebraMap R S) y) :=
  (toLocalizationMap M S).isUnit_comp j.toMonoidHom _

Composition of Localization Map with Ring Homomorphism Preserves Units

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any ring homomorphism $j : S \to P$ and any element $y \in M$, the composition $j \circ (\text{algebraMap}\, R\, S)$ evaluated at $y$ is a unit in $P$.

IsLocalization.mk'_add theorem

(x₁ x₂ : R) (y₁ y₂ : M) : mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂

Full source

theorem mk'_add (x₁ x₂ : R) (y₁ y₂ : M) :
    mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂ :=
  mk'_eq_iff_eq_mul.2 <|
    Eq.symm
      (by
        rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
          mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
          mk'_add_eq_iff_add_mul_eq_mul]
        simp only [map_add, Submonoid.coe_mul, map_mul]
        ring)

Addition Formula for Localized Elements: $\frac{x_1}{y_1} + \frac{x_2}{y_2} = \frac{x_1 y_2 + x_2 y_1}{y_1 y_2}$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x_1, x_2 \in R$ and $y_1, y₂ \in M$, the sum of the localized elements $\text{mk'}_S(x_1, y_1)$ and $\text{mk'}_S(x_2, y_2)$ is equal to the localized element $\text{mk'}_S(x_1 y_2 + x_2 y_1, y_1 y_2)$. In other words: \[ \frac{x_1}{y_1} + \frac{x_2}{y_2} = \frac{x_1 y_2 + x_2 y_1}{y_1 y_2} \]

IsLocalization.mul_add_inv_left theorem

 {g : R →+* P} (h : ∀ y : M, IsUnit (g y)) (y : M) (w z₁ z₂ : P) :
  w * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) h y)⁻¹ + z₁ = z₂ ↔ w + g y * z₁ = g y * z₂

Full source

theorem mul_add_inv_left {g : R →+* P} (h : ∀ y : M, IsUnit (g y)) (y : M) (w z₁ z₂ : P) :
    w * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) h y)⁻¹ + z₁ =
    z₂ ↔ w + g y * z₁ = g y * z₂ := by
  rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.restrict M) h y),
    mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
    IsUnit.coe_liftRight]
  simp [RingHom.toMonoidHom_eq_coe, MonoidHom.restrict_apply]

Equivalence of Linear Equations Under Localization: $w/g(y) + z_1 = z_2 \leftrightarrow w + g(y)z_1 = g(y)z_2$

Informal description

Let $R$ and $P$ be commutative rings, $M$ a submonoid of $R$, and $g: R \to P$ a ring homomorphism such that $g(y)$ is a unit in $P$ for every $y \in M$. Then for any $y \in M$ and $w, z_1, z_2 \in P$, we have the equivalence: $$w \cdot (g(y))^{-1} + z_1 = z_2 \leftrightarrow w + g(y) \cdot z_1 = g(y) \cdot z_2$$ where $(g(y))^{-1}$ denotes the multiplicative inverse of $g(y)$ in $P$.

IsLocalization.lift_spec_mul_add theorem

 {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) (z w w' v) :
  ((toLocalizationMap M S).lift hg) z * w + w' = v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ((toLocalizationMap M S).sec z).2 * w' =
      g ((toLocalizationMap M S).sec z).2 * v

Full source

theorem lift_spec_mul_add {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) (z w w' v) :
    ((toLocalizationMap M S).lift hg) z * w + w' = v ↔
      g ((toLocalizationMap M S).sec z).1 * w + g ((toLocalizationMap M S).sec z).2 * w' =
        g ((toLocalizationMap M S).sec z).2 * v := by
  rw [mul_comm, Submonoid.LocalizationMap.lift_apply, ← mul_assoc, mul_add_inv_left hg,
    mul_comm]
  rfl

Equivalence of Linear Equations Under Localization: $\varphi(z)w + w' = v \leftrightarrow g(x)w + g(y)w' = g(y)v$

Informal description

Let $R$ and $P$ be commutative rings, $M$ a submonoid of $R$, and $S$ a localization of $R$ at $M$. Given a ring homomorphism $g: R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, then for any $z \in S$ and $w, w', v \in P$, the following equivalence holds: $$ \varphi(z) \cdot w + w' = v \leftrightarrow g(x) \cdot w + g(y) \cdot w' = g(y) \cdot v $$ where $\varphi = \text{lift}(g)$ is the induced homomorphism from $S$ to $P$, and $(x, y) \in R \times M$ is any pair such that $z$ is represented as $f(x) \cdot (f(y))^{-1}$ under the localization map $f: R \to S$.

IsLocalization.lift definition

{g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) : S →+* P

Full source

/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →+* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` sending `z : S` to `g x * (g y)⁻¹`, where `(x, y) : R × M` are such that
`z = f x * (f y)⁻¹`. -/
noncomputable def lift {g : R →+* P} (hg : ∀ y : M, IsUnit (g y)) : S →+* P :=
  { Submonoid.LocalizationWithZeroMap.lift (toLocalizationWithZeroMap M S)
      g.toMonoidWithZeroHom hg with
    map_add' := by
      intro x y
      dsimp
      rw [(toLocalizationWithZeroMap M S).lift_def, (toLocalizationWithZeroMap M S).lift_spec,
        mul_add, mul_comm, eq_comm, lift_spec_mul_add, add_comm, mul_comm, mul_assoc, mul_comm,
        mul_assoc, lift_spec_mul_add]
      simp_rw [← mul_assoc]
      show g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _
      simp_rw [← map_mul g, ← map_add g]
      apply eq_of_eq (S := S) hg
      simp only [sec_spec', toLocalizationMap_sec, map_add, map_mul]
      ring }

Lift of a ring homomorphism through localization

Informal description

Given a commutative ring $ R $ with a submonoid $ M \subseteq R $, a commutative ring $ S $ that is a localization of $ R $ at $ M $, and a ring homomorphism $ g : R \to P $ such that $ g(y) $ is a unit in $ P $ for every $ y \in M $, the function `IsLocalization.lift` constructs a ring homomorphism from $ S $ to $ P $. For any $ z \in S $, this homomorphism sends $ z $ to $ g(x) \cdot (g(y))^{-1} $, where $ (x, y) \in R \times M $ is any pair such that $ z $ is represented as $ f(x) \cdot (f(y))^{-1} $ under the localization map $ f : R \to S $.

IsLocalization.lift_mk' theorem

(x y) : lift hg (mk' S x y) = g x * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) hg y)⁻¹

Full source

/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : R, y ∈ M`. -/
theorem lift_mk' (x y) :
    lift hg (mk' S x y) = g x * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) hg y)⁻¹ :=
  (toLocalizationMap M S).lift_mk' _ _ _

Lifted Homomorphism Evaluates Fractions as $g(x) \cdot g(y)^{-1}$

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, the lifted homomorphism $\text{lift}\, hg : S \to P$ satisfies \[ \text{lift}\, hg \left( \frac{x}{y} \right) = g(x) \cdot (g(y))^{-1} \] for any $x \in R$ and $y \in M$, where $\frac{x}{y}$ denotes the element $f(x) \cdot (f(y))^{-1}$ in $S$ under the localization map $f : R \to S$.

IsLocalization.lift_mk'_spec theorem

(x v) (y : M) : lift hg (mk' S x y) = v ↔ g x = g y * v

Full source

theorem lift_mk'_spec (x v) (y : M) : liftlift hg (mk' S x y) = v ↔ g x = g y * v :=
  (toLocalizationMap M S).lift_mk'_spec _ _ _ _

Characterization of Lifted Homomorphism on Localization Fractions

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, then for any $x \in R$, $v \in P$, and $y \in M$, the lifted homomorphism $\text{lift}\, hg$ satisfies \[ \text{lift}\, hg (f(x) \cdot (f(y))^{-1}) = v \quad \text{if and only if} \quad g(x) = g(y) \cdot v, \] where $f : R \to S$ is the canonical localization map.

IsLocalization.lift_eq theorem

(x : R) : lift hg ((algebraMap R S) x) = g x

Full source

@[simp]
theorem lift_eq (x : R) : lift hg ((algebraMap R S) x) = g x :=
  (toLocalizationMap M S).lift_eq _ _

Lifted Homomorphism Commutes with Localization Map on $R$

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, the lifted homomorphism $\text{lift}\, hg : S \to P$ satisfies $\text{lift}\, hg (\text{algebraMap}\, R\, S\, x) = g(x)$ for every $x \in R$.

IsLocalization.lift_eq_iff theorem

{x y : R × M} : lift hg (mk' S x.1 x.2) = lift hg (mk' S y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2)

Full source

theorem lift_eq_iff {x y : R × M} :
    liftlift hg (mk' S x.1 x.2) = lift hg (mk' S y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2) :=
  (toLocalizationMap M S).lift_eq_iff _

Equality of Lifted Fractions in Localization via Homomorphism Condition

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, and two pairs $(x_1, y_1), (x_2, y_2) \in R \times M$, the following equivalence holds: \[ \text{lift}\, hg \left(\frac{x_1}{y_1}\right) = \text{lift}\, hg \left(\frac{x_2}{y_2}\right) \iff g(x_1 y_2) = g(x_2 y_1). \] Here, $\frac{x}{y}$ denotes the element $\text{mk'}\, S\, x\, y$ in $S$.

IsLocalization.lift_comp theorem

: (lift hg).comp (algebraMap R S) = g

Full source

@[simp]
theorem lift_comp : (lift hg).comp (algebraMap R S) = g :=
  RingHom.ext <| (DFunLike.ext_iff (F := MonoidHom _ _)).1 <| (toLocalizationMap M S).lift_comp _

Composition of Lift with Canonical Map Equals Original Homomorphism

Informal description

Given a commutative ring $R$ with a submonoid $M \subseteq R$, a commutative ring $S$ that is a localization of $R$ at $M$, and a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, the composition of the induced homomorphism $\text{lift}\, hg : S \to P$ with the canonical map $\text{algebraMap}\, R\, S : R \to S$ equals $g$. In other words, $(\text{lift}\, hg) \circ (\text{algebraMap}\, R\, S) = g$.

IsLocalization.lift_of_comp theorem

(j : S →+* P) : lift (isUnit_comp M j) = j

Full source

@[simp]
theorem lift_of_comp (j : S →+* P) : lift (isUnit_comp M j) = j :=
  RingHom.ext <| (DFunLike.ext_iff (F := MonoidHom _ _)).1 <|
    (toLocalizationMap M S).lift_of_comp j.toMonoidHom

Lift of Composition Equals Original Homomorphism in Localization

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. For any ring homomorphism $j : S \to P$, the homomorphism $\text{lift}(j \circ \text{algebraMap}\, R\, S)$ induced by the composition $j \circ \text{algebraMap}\, R\, S$ equals $j$. That is, $\text{lift}(j \circ \text{algebraMap}\, R\, S) = j$.

IsLocalization.monoidHom_ext theorem

⦃j k : S →* P⦄ (h : j.comp (algebraMap R S : R →* S) = k.comp (algebraMap R S)) : j = k

Full source

/-- See note [partially-applied ext lemmas] -/
theorem monoidHom_ext ⦃j k : S →* P⦄
    (h : j.comp (algebraMap R S : R →* S) = k.comp (algebraMap R S)) : j = k :=
  Submonoid.LocalizationMap.epic_of_localizationMap (toLocalizationMap M S) <| DFunLike.congr_fun h

Uniqueness of Monoid Homomorphisms from Localization via Composition with Algebra Map

Informal description

Let $S$ be a localization of a commutative ring $R$ at a submonoid $M$, and let $P$ be another commutative ring. For any two monoid homomorphisms $j, k \colon S \to P$, if the compositions $j \circ (\text{algebraMap}\, R\, S)$ and $k \circ (\text{algebraMap}\, R\, S)$ are equal, then $j = k$.

IsLocalization.ringHom_ext theorem

⦃j k : S →+* P⦄ (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) : j = k

Full source

/-- See note [partially-applied ext lemmas] -/
theorem ringHom_ext ⦃j k : S →+* P⦄ (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) :
    j = k :=
  RingHom.coe_monoidHom_injective <| monoidHom_ext M <| MonoidHom.ext <| RingHom.congr_fun h

Uniqueness of Ring Homomorphisms from Localization via Composition with Algebra Map

Informal description

Let $S$ be a localization of a commutative ring $R$ at a submonoid $M$, and let $P$ be another commutative ring. For any two ring homomorphisms $j, k \colon S \to P$, if the compositions $j \circ (\text{algebraMap}\, R\, S)$ and $k \circ (\text{algebraMap}\, R\, S)$ are equal, then $j = k$.

IsLocalization.ext theorem

 (j k : S → P) (hj1 : j 1 = 1) (hk1 : k 1 = 1) (hjm : ∀ a b, j (a * b) = j a * j b) (hkm : ∀ a b, k (a * b) = k a * k b)
  (h : ∀ a, j (algebraMap R S a) = k (algebraMap R S a)) : j = k

Full source

/-- To show `j` and `k` agree on the whole localization, it suffices to show they agree
on the image of the base ring, if they preserve `1` and `*`. -/
protected theorem ext (j k : S → P) (hj1 : j 1 = 1) (hk1 : k 1 = 1)
    (hjm : ∀ a b, j (a * b) = j a * j b) (hkm : ∀ a b, k (a * b) = k a * k b)
    (h : ∀ a, j (algebraMap R S a) = k (algebraMap R S a)) : j = k :=
  let j' : MonoidHom S P :=
    { toFun := j, map_one' := hj1, map_mul' := hjm }
  let k' : MonoidHom S P :=
    { toFun := k, map_one' := hk1, map_mul' := hkm }
  have : j' = k' := monoidHom_ext M (MonoidHom.ext h)
  show j'.toFun = k'.toFun by rw [this]

Uniqueness of Multiplicative Maps from Localization via Agreement on Base Ring

Informal description

Let $S$ be a localization of a commutative ring $R$ at a submonoid $M$, and let $P$ be another commutative ring. For any two functions $j, k \colon S \to P$ that preserve the multiplicative identity and multiplication (i.e., $j(1) = 1$, $k(1) = 1$, $j(a \cdot b) = j(a) \cdot j(b)$, and $k(a \cdot b) = k(a) \cdot k(b)$ for all $a, b \in S$), if $j$ and $k$ agree on the image of $R$ in $S$ (i.e., $j(\text{algebraMap}\, R\, S\, a) = k(\text{algebraMap}\, R\, S\, a)$ for all $a \in R$), then $j = k$.

IsLocalization.lift_unique theorem

{j : S →+* P} (hj : ∀ x, j ((algebraMap R S) x) = g x) : lift hg = j

Full source

theorem lift_unique {j : S →+* P} (hj : ∀ x, j ((algebraMap R S) x) = g x) : lift hg = j :=
  RingHom.ext <|
    (DFunLike.ext_iff (F := MonoidHom _ _)).1 <|
      Submonoid.LocalizationMap.lift_unique (toLocalizationMap M S) (g := g.toMonoidHom) hg
        (j := j.toMonoidHom) hj

Uniqueness of the Lift in Localization

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, and a ring homomorphism $j : S \to P$ satisfying $j \circ \text{algebraMap}\, R\, S = g$, then the induced homomorphism $\text{lift}\, hg$ (where $hg$ witnesses that $g$ maps elements of $M$ to units) is equal to $j$.

IsLocalization.lift_id theorem

(x) : lift (map_units S : ∀ _ : M, IsUnit _) x = x

Full source

@[simp]
theorem lift_id (x) : lift (map_units S : ∀ _ : M, IsUnit _) x = x :=
  (toLocalizationMap M S).lift_id _

Identity Property of Lift in Localization

Informal description

For any element $x$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, the lift of the canonical ring homomorphism $\text{algebraMap}\, R\, S$ (which maps elements of $M$ to units in $S$) is the identity map on $S$. That is, $\text{lift}(\text{algebraMap}\, R\, S)(x) = x$.

IsLocalization.lift_surjective_iff theorem

: Surjective (lift hg : S → P) ↔ ∀ v : P, ∃ x : R × M, v * g x.2 = g x.1

Full source

theorem lift_surjective_iff :
    SurjectiveSurjective (lift hg : S → P) ↔ ∀ v : P, ∃ x : R × M, v * g x.2 = g x.1 :=
  (toLocalizationMap M S).lift_surjective_iff hg

Surjectivity Criterion for Localization Lift Homomorphism

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be the localization of $R$ at $M$. Given a ring homomorphism $g \colon R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, the induced homomorphism $\text{lift}\, hg \colon S \to P$ is surjective if and only if for every $v \in P$, there exists a pair $(x, y) \in R \times M$ such that $v \cdot g(y) = g(x)$.

IsLocalization.lift_injective_iff theorem

: Injective (lift hg : S → P) ↔ ∀ x y, algebraMap R S x = algebraMap R S y ↔ g x = g y

Full source

theorem lift_injective_iff :
    InjectiveInjective (lift hg : S → P) ↔ ∀ x y, algebraMap R S x = algebraMap R S y ↔ g x = g y :=
  (toLocalizationMap M S).lift_injective_iff hg

Injectivity Criterion for Lift of Localization Homomorphism

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, the induced homomorphism $\text{lift}\, hg : S \to P$ is injective if and only if for all $x, y \in R$, the equality $\text{algebraMap}\, R\, S\, x = \text{algebraMap}\, R\, S\, y$ holds if and only if $g(x) = g(y)$.

IsLocalization.injective_iff_map_algebraMap_eq theorem

 {T} [CommSemiring T] (f : S →+* T) :
  Function.Injective f ↔ ∀ x y, algebraMap R S x = algebraMap R S y ↔ f (algebraMap R S x) = f (algebraMap R S y)

Full source

lemma injective_iff_map_algebraMap_eq {T} [CommSemiring T] (f : S →+* T) :
    Function.InjectiveFunction.Injective f ↔ ∀ x y,
      algebraMap R S x = algebraMap R S y ↔ f (algebraMap R S x) = f (algebraMap R S y) := by
  rw [← IsLocalization.lift_of_comp (M := M) f, IsLocalization.lift_injective_iff]
  simp

Injectivity Criterion for Homomorphisms from Localization via Algebra Map Equality

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any commutative semiring $T$ and ring homomorphism $f \colon S \to T$, the following are equivalent: 1. The homomorphism $f$ is injective. 2. For all $x, y \in R$, the equality $\text{algebraMap}\, R\, S\, x = \text{algebraMap}\, R\, S\, y$ holds if and only if $f(\text{algebraMap}\, R\, S\, x) = f(\text{algebraMap}\, R\, S\, y)$.

IsLocalization.map definition

(g : R →+* P) (hy : M ≤ T.comap g) : S →+* Q

Full source

/-- Map a homomorphism `g : R →+* P` to `S →+* Q`, where `S` and `Q` are
localizations of `R` and `P` at `M` and `T` respectively,
such that `g(M) ⊆ T`.

We send `z : S` to `algebraMap P Q (g x) * (algebraMap P Q (g y))⁻¹`, where
`(x, y) : R × M` are such that `z = f x * (f y)⁻¹`. -/
noncomputable def map (g : R →+* P) (hy : M ≤ T.comap g) : S →+* Q :=
  lift (M := M) (g := (algebraMap P Q).comp g) fun y => map_units _ ⟨g y, hy y.2⟩

Induced homomorphism between localizations

Informal description

Given commutative rings $ R $ and $ P $ with submonoids $ M \subseteq R $ and $ T \subseteq P $, and localizations $ S $ of $ R $ at $ M $ and $ Q $ of $ P $ at $ T $, the function `IsLocalization.map` constructs a ring homomorphism from $ S $ to $ Q $ induced by a ring homomorphism $ g : R \to P $ such that $ g(M) \subseteq T $. For any $ z \in S $, this homomorphism sends $ z $ to $ \text{algebraMap}_P Q (g x) \cdot (\text{algebraMap}_P Q (g y))^{-1} $, where $ (x, y) \in R \times M $ is any pair such that $ z $ is represented as $ \text{algebraMap}_R S x \cdot (\text{algebraMap}_R S y)^{-1} $.

IsLocalization.map_eq theorem

(x) : map Q g hy ((algebraMap R S) x) = algebraMap P Q (g x)

Full source

@[simp]
theorem map_eq (x) : map Q g hy ((algebraMap R S) x) = algebraMap P Q (g x) :=
  lift_eq (fun y => map_units _ ⟨g y, hy y.2⟩) x

Commutativity of Localization Map with Induced Homomorphism on $R$

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring homomorphism $g : R \to P$ such that $g(M) \subseteq T$, the induced homomorphism $\text{map}\, Q\, g\, hy : S \to Q$ satisfies $\text{map}\, Q\, g\, hy (\text{algebraMap}\, R\, S\, x) = \text{algebraMap}\, P\, Q (g x)$ for every $x \in R$.

IsLocalization.map_comp theorem

: (map Q g hy).comp (algebraMap R S) = (algebraMap P Q).comp g

Full source

@[simp]
theorem map_comp : (map Q g hy).comp (algebraMap R S) = (algebraMap P Q).comp g :=
  lift_comp fun y => map_units _ ⟨g y, hy y.2⟩

Composition of Localization Maps with Induced Homomorphism

Informal description

Given commutative rings $R$ and $P$ with submonoids $M \subseteq R$ and $T \subseteq P$, and localizations $S$ of $R$ at $M$ and $Q$ of $P$ at $T$, for any ring homomorphism $g : R \to P$ such that $g(M) \subseteq T$, the composition of the induced homomorphism $\text{map}\, Q\, g\, hy : S \to Q$ with the canonical map $\text{algebraMap}\, R\, S : R \to S$ equals the composition of the canonical map $\text{algebraMap}\, P\, Q : P \to Q$ with $g$. In other words, $(\text{map}\, Q\, g\, hy) \circ (\text{algebraMap}\, R\, S) = (\text{algebraMap}\, P\, Q) \circ g$.

IsLocalization.map_mk' theorem

(x) (y : M) : map Q g hy (mk' S x y) = mk' Q (g x) ⟨g y, hy y.2⟩

Full source

theorem map_mk' (x) (y : M) : map Q g hy (mk' S x y) = mk' Q (g x) ⟨g y, hy y.2⟩ :=
  Submonoid.LocalizationMap.map_mk' (toLocalizationMap M S) (g := g.toMonoidHom)
    (fun y => hy y.2) (k := toLocalizationMap T Q) ..

Localization Map Preserves Fraction Construction: $\text{map}\, Q\, g\, \text{hy}\, (\text{mk'}_S\, x\, y) = \text{mk'}_Q\, (g x)\, \langle g y, \text{hy}\, y.2 \rangle$

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring homomorphism $g : R \to P$ such that $g(M) \subseteq T$, the induced localization map $\text{map}\, Q\, g\, \text{hy} : S \to Q$ satisfies the following property: for any $x \in R$ and $y \in M$, the image of the fraction $\text{mk'}_S\, x\, y$ under this map equals $\text{mk'}_Q\, (g x)\, \langle g y, \text{hy}\, y.2 \rangle$, where $\text{mk'}_S$ and $\text{mk'}_Q$ construct elements in the localizations $S$ and $Q$ respectively.

IsLocalization.map_unique theorem

(j : S →+* Q) (hj : ∀ x : R, j (algebraMap R S x) = algebraMap P Q (g x)) : map Q g hy = j

Full source

theorem map_unique (j : S →+* Q) (hj : ∀ x : R, j (algebraMap R S x) = algebraMap P Q (g x)) :
    map Q g hy = j :=
  lift_unique (fun y => map_units _ ⟨g y, hy y.2⟩) hj

Uniqueness of the Localization Map Induced by $g$

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring homomorphism $g : R \to P$ such that $g(M) \subseteq T$, and a ring homomorphism $j : S \to Q$ satisfying $j \circ \text{algebraMap}_R S = \text{algebraMap}_P Q \circ g$, then the induced localization map $\text{map}_Q g \text{hy}$ is equal to $j$.

IsLocalization.map_comp_map theorem

 {A : Type*} [CommSemiring A] {U : Submonoid A} {W} [CommSemiring W] [Algebra A W] [IsLocalization U W] {l : P →+* A}
  (hl : T ≤ U.comap l) : (map W l hl).comp (map Q g hy : S →+* _) = map W (l.comp g) fun _ hx => hl (hy hx)

Full source

/-- If `CommSemiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
theorem map_comp_map {A : Type*} [CommSemiring A] {U : Submonoid A} {W} [CommSemiring W]
    [Algebra A W] [IsLocalization U W] {l : P →+* A} (hl : T ≤ U.comap l) :
    (map W l hl).comp (map Q g hy : S →+* _) = map W (l.comp g) fun _ hx => hl (hy hx) :=
  RingHom.ext fun x =>
    Submonoid.LocalizationMap.map_map (P := P) (toLocalizationMap M S) (fun y => hy y.2)
      (toLocalizationMap U W) (fun w => hl w.2) x

Composition of Localization Maps

Informal description

Let $R$, $P$, and $A$ be commutative semirings with submonoids $M \subseteq R$, $T \subseteq P$, and $U \subseteq A$ respectively. Let $S$ be a localization of $R$ at $M$, $Q$ a localization of $P$ at $T$, and $W$ a localization of $A$ at $U$. Given ring homomorphisms $g : R \to P$ and $l : P \to A$ such that $g(M) \subseteq T$ and $l(T) \subseteq U$, the composition of the induced localization maps satisfies \[ \text{map}_W\, l\, \text{hl} \circ \text{map}_Q\, g\, \text{hy} = \text{map}_W\, (l \circ g)\, (\lambda \_\, \text{hx}, \text{hl}\, (\text{hy}\, \text{hx})) \] where $\text{hy} : M \leq T \circ g$ and $\text{hl} : T \leq U \circ l$ are the given inclusion conditions.

IsLocalization.map_map theorem

 {A : Type*} [CommSemiring A] {U : Submonoid A} {W} [CommSemiring W] [Algebra A W] [IsLocalization U W] {l : P →+* A}
  (hl : T ≤ U.comap l) (x : S) : map W l hl (map Q g hy x) = map W (l.comp g) (fun _ hx => hl (hy hx)) x

Full source

/-- If `CommSemiring` homs `g : R →+* P, l : P →+* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
theorem map_map {A : Type*} [CommSemiring A] {U : Submonoid A} {W} [CommSemiring W] [Algebra A W]
    [IsLocalization U W] {l : P →+* A} (hl : T ≤ U.comap l) (x : S) :
    map W l hl (map Q g hy x) = map W (l.comp g) (fun _ hx => hl (hy hx)) x := by
  rw [← map_comp_map (Q := Q) hy hl]; rfl

Compatibility of Localization Maps under Composition

Informal description

Let $R$, $P$, and $A$ be commutative semirings with submonoids $M \subseteq R$, $T \subseteq P$, and $U \subseteq A$ respectively. Let $S$ be a localization of $R$ at $M$, $Q$ a localization of $P$ at $T$, and $W$ a localization of $A$ at $U$. Given ring homomorphisms $g : R \to P$ and $l : P \to A$ such that $g(M) \subseteq T$ and $l(T) \subseteq U$, then for any $x \in S$ we have: \[ \text{map}_W\, l\, \text{hl}\, (\text{map}_Q\, g\, \text{hy}\, x) = \text{map}_W\, (l \circ g)\, (\lambda \_\, \text{hx}, \text{hl}\, (\text{hy}\, \text{hx}))\, x \] where $\text{hy} : M \leq T \circ g$ and $\text{hl} : T \leq U \circ l$ are the given inclusion conditions.

IsLocalization.map_smul theorem

(x : S) (z : R) : map Q g hy (z • x : S) = g z • map Q g hy x

Full source

protected theorem map_smul (x : S) (z : R) : map Q g hy (z • x : S) = g z • map Q g hy x := by
  rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul, map_eq]

Compatibility of Localization Map with Scalar Multiplication: $\text{map}\, Q\, g\, hy (z \cdot x) = g(z) \cdot \text{map}\, Q\, g\, hy (x)$

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring homomorphism $g : R \to P$ such that $g(M) \subseteq T$, the induced localization map $\text{map}\, Q\, g\, hy : S \to Q$ satisfies $\text{map}\, Q\, g\, hy (z \cdot x) = g(z) \cdot \text{map}\, Q\, g\, hy (x)$ for all $x \in S$ and $z \in R$, where $\cdot$ denotes the scalar multiplication action of $R$ on $S$ and $P$ on $Q$.

IsLocalization.map_id_mk' theorem

 {Q : Type*} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (x) (y : M) :
  map Q (RingHom.id R) (le_refl M) (mk' S x y) = mk' Q x y

Full source

@[simp]
theorem map_id_mk' {Q : Type*} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (x) (y : M) :
    map Q (RingHom.id R) (le_refl M) (mk' S x y) = mk' Q x y :=
  map_mk' ..

Localization Map Preserves Fraction Construction under Identity Homomorphism: $\text{map}_Q\, \text{id}_R\, (\text{mk'}_S\, x\, y) = \text{mk'}_Q\, x\, y$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ and $Q$ be localizations of $R$ at $M$. For any $x \in R$ and $y \in M$, the induced localization map $\text{map}_Q (\text{id}_R)$ sends the fraction $\text{mk'}_S\, x\, y$ to $\text{mk'}_Q\, x\, y$.

IsLocalization.ringEquivOfRingEquiv definition

(h : R ≃+* P) (H : M.map h.toMonoidHom = T) : S ≃+* Q

Full source

/-- If `S`, `Q` are localizations of `R` and `P` at submonoids `M, T` respectively, an
isomorphism `j : R ≃+* P` such that `j(M) = T` induces an isomorphism of localizations
`S ≃+* Q`. -/
@[simps]
noncomputable def ringEquivOfRingEquiv (h : R ≃+* P) (H : M.map h.toMonoidHom = T) : S ≃+* Q :=
  have H' : T.map h.symm.toMonoidHom = M := by
    rw [← M.map_id, ← H, Submonoid.map_map]
    congr
    ext
    apply h.symm_apply_apply
  { map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) with
    toFun := map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H))
    invFun := map S (h.symm : P →+* R) (T.le_comap_of_map_le (le_of_eq H'))
    left_inv := fun x => by
      rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
      simp
    right_inv := fun x => by
      rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
      simp }

Isomorphism of localizations induced by a ring isomorphism

Informal description

Given commutative rings $ R $ and $ P $ with submonoids $ M \subseteq R $ and $ T \subseteq P $, and localizations $ S $ of $ R $ at $ M $ and $ Q $ of $ P $ at $ T $, an isomorphism $ h : R \simeq+* P $ such that $ h(M) = T $ induces a ring isomorphism $ S \simeq+* Q $.

IsLocalization.ringEquivOfRingEquiv_eq_map theorem

 {j : R ≃+* P} (H : M.map j.toMonoidHom = T) :
  (ringEquivOfRingEquiv S Q j H : S →+* Q) = map Q (j : R →+* P) (M.le_comap_of_map_le (le_of_eq H))

Full source

theorem ringEquivOfRingEquiv_eq_map {j : R ≃+* P} (H : M.map j.toMonoidHom = T) :
    (ringEquivOfRingEquiv S Q j H : S →+* Q) =
      map Q (j : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) :=
  rfl

Localization Isomorphism Equals Induced Map

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring isomorphism $j : R \simeq+* P$ such that $j(M) = T$, the induced ring homomorphism $\text{ringEquivOfRingEquiv}\, S\, Q\, j\, H : S \to Q$ equals the localization map $\text{map}\, Q\, j$ (where $H$ is the proof that $j(M) = T$ and the inclusion $M \leq T.comap\, j$ is derived from $H$).

IsLocalization.ringEquivOfRingEquiv_eq theorem

 {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x) :
  ringEquivOfRingEquiv S Q j H ((algebraMap R S) x) = algebraMap P Q (j x)

Full source

theorem ringEquivOfRingEquiv_eq {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x) :
    ringEquivOfRingEquiv S Q j H ((algebraMap R S) x) = algebraMap P Q (j x) := by
  simp

Commutativity of Localization Isomorphism with Algebra Maps

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring isomorphism $j : R \simeq+* P$ such that $j(M) = T$, the induced isomorphism $\text{ringEquivOfRingEquiv}\, S\, Q\, j\, H : S \simeq+* Q$ satisfies \[ \text{ringEquivOfRingEquiv}\, S\, Q\, j\, H (\text{algebraMap}\, R\, S\, x) = \text{algebraMap}\, P\, Q (j x) \] for every $x \in R$.

IsLocalization.ringEquivOfRingEquiv_mk' theorem

 {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x : R) (y : M) :
  ringEquivOfRingEquiv S Q j H (mk' S x y) = mk' Q (j x) ⟨j y, show j y ∈ T from H ▸ Set.mem_image_of_mem j y.2⟩

Full source

theorem ringEquivOfRingEquiv_mk' {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x : R) (y : M) :
    ringEquivOfRingEquiv S Q j H (mk' S x y) =
      mk' Q (j x) ⟨j y, show j y ∈ T from H ▸ Set.mem_image_of_mem j y.2⟩ := by
  simp [map_mk']

Localization Isomorphism Preserves Fraction Construction: $\text{ringEquivOfRingEquiv}\, S\, Q\, j\, H\, (\text{mk'}_S\, x\, y) = \text{mk'}_Q\, (j x)\, \langle j y, H \rangle$

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring isomorphism $j: R \simeq+* P$ such that $j(M) = T$, the induced isomorphism $\text{ringEquivOfRingEquiv}\, S\, Q\, j\, H : S \simeq+* Q$ satisfies the following property: for any $x \in R$ and $y \in M$, the image of the fraction $\text{mk'}_S\, x\, y$ under this isomorphism equals $\text{mk'}_Q\, (j x)\, \langle j y, H \rangle$, where $\text{mk'}_S$ and $\text{mk'}_Q$ construct elements in the localizations $S$ and $Q$ respectively, and $\langle j y, H \rangle$ denotes that $j y \in T$ by virtue of $H$.

IsLocalization.ringEquivOfRingEquiv_symm theorem

 {j : R ≃+* P} (H : M.map j = T) :
  (ringEquivOfRingEquiv S Q j H).symm =
    ringEquivOfRingEquiv Q S j.symm
      (show T.map (j : R ≃* P).symm = M by
        rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
          Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective])

Full source

@[simp]
theorem ringEquivOfRingEquiv_symm {j : R ≃+* P} (H : M.map j = T) :
    (ringEquivOfRingEquiv S Q j H).symm =
      ringEquivOfRingEquiv Q S j.symm (show T.map (j : R ≃* P).symm = M by
        rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
          Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]) := rfl

Inverse of Localization Isomorphism Induced by Ring Isomorphism

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a ring isomorphism $j : R \simeq+* P$ such that $j(M) = T$, the inverse of the induced isomorphism $\text{ringEquivOfRingEquiv}\, S\, Q\, j\, H : S \simeq+* Q$ is equal to the isomorphism $\text{ringEquivOfRingEquiv}\, Q\, S\, j^{-1}\, H'$, where $H'$ is the proof that $j^{-1}(T) = M$.

IsLocalization.at_units theorem

(S : Submonoid R) (hS : S ≤ IsUnit.submonoid R) : IsLocalization S R

Full source

lemma at_units (S : Submonoid R)
    (hS : S ≤ IsUnit.submonoid R) : IsLocalization S R where
  map_units' y := hS y.prop
  surj' := fun s ↦ ⟨⟨s, 1⟩, by simp⟩
  exists_of_eq := fun {x y} (e : x = y) ↦ ⟨1, e ▸ rfl⟩

Localization at Units is Trivial

Informal description

Let $R$ be a commutative ring and $S$ be a submonoid of $R$ consisting entirely of units (i.e., $S \subseteq R^\times$). Then $R$ is isomorphic to its own localization at $S$, i.e., the canonical map $R \to S^{-1}R$ is an isomorphism.

IsLocalization.map_injective_of_injective theorem

(h : Function.Injective g) [IsLocalization (M.map g) Q] : Function.Injective (map Q g M.le_comap_map : S → Q)

Full source

/-- Injectivity of a map descends to the map induced on localizations. -/
theorem map_injective_of_injective (h : Function.Injective g) [IsLocalization (M.map g) Q] :
    Function.Injective (map Q g M.le_comap_map : S → Q) :=
  (toLocalizationMap M S).map_injective_of_injective h (toLocalizationMap (M.map g) Q)

Injectivity of Localization-Induced Homomorphism Preserved from Base Ring Homomorphism

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given an injective ring homomorphism $g : R \to P$ such that $g(M) \subseteq T$, the induced homomorphism $\text{map}_Q\, g : S \to Q$ is also injective.

IsLocalization.map_surjective_of_surjective theorem

(h : Function.Surjective g) [IsLocalization (M.map g) Q] : Function.Surjective (map Q g M.le_comap_map : S → Q)

Full source

/-- Surjectivity of a map descends to the map induced on localizations. -/
theorem map_surjective_of_surjective (h : Function.Surjective g) [IsLocalization (M.map g) Q] :
    Function.Surjective (map Q g M.le_comap_map : S → Q) :=
  (toLocalizationMap M S).map_surjective_of_surjective h (toLocalizationMap (M.map g) Q)

Surjectivity of Induced Homomorphism Between Localizations

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given a surjective ring homomorphism $g \colon R \to P$ such that $g(M) \subseteq T$, the induced homomorphism $\text{map}_Q\, g\, M.\text{le\_comap\_map} \colon S \to Q$ between the localizations is also surjective.

IsLocalization.isLocalization_of_base_ringEquiv theorem

 [IsLocalization M S] (h : R ≃+* P) :
  haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
  IsLocalization (M.map h) S

Full source

theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) :
    haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
    IsLocalization (M.map h) S := by
  letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
  constructor
  · rintro ⟨_, ⟨y, hy, rfl⟩⟩
    convert IsLocalization.map_units S ⟨y, hy⟩
    dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]
    exact congr_arg _ (h.symm_apply_apply _)
  · intro y
    obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y
    refine ⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩
    dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢
    convert e <;> exact h.symm_apply_apply _
  · intro x y
    rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply,
      IsLocalization.eq_iff_exists M S]
    simp [← h.toEquiv.apply_eq_iff_eq]

Localization Preservation under Base Ring Isomorphism

Informal description

Let $R$ and $P$ be commutative rings with $S$ being a localization of $R$ at a submonoid $M \subseteq R$. Given a ring isomorphism $h : R \simeq P$, then $S$ is also a localization of $P$ at the submonoid $h(M) \subseteq P$ (where $h(M)$ denotes the image of $M$ under $h$).

IsLocalization.isLocalization_iff_of_base_ringEquiv theorem

 (h : R ≃+* P) :
  IsLocalization M S ↔
    haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
    IsLocalization (M.map h) S

Full source

theorem isLocalization_iff_of_base_ringEquiv (h : R ≃+* P) :
    IsLocalizationIsLocalization M S ↔
      haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
      IsLocalization (M.map h) S := by
  letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
  refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩
  intro (H : IsLocalization (Submonoid.map (h : R ≃* P) M) S)
  convert isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm
  · rw [← Submonoid.map_coe_toMulEquiv, RingEquiv.coe_toMulEquiv_symm, ←
      Submonoid.comap_equiv_eq_map_symm, Submonoid.comap_map_eq_of_injective]
    exact h.toEquiv.injective
  rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc]
  simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom]
  apply Algebra.algebra_ext
  intro r
  rw [RingHom.algebraMap_toAlgebra]

Localization Characterization via Base Ring Isomorphism

Informal description

Let $R$ and $P$ be commutative rings with a ring isomorphism $h : R \simeq P$, and let $M$ be a submonoid of $R$. Then $S$ is a localization of $R$ at $M$ if and only if, under the induced algebra structure, $S$ is a localization of $P$ at the image submonoid $h(M) \subseteq P$.

IsLocalization.nonZeroDivisors_le_comap theorem

[IsLocalization M S] : nonZeroDivisors R ≤ (nonZeroDivisors S).comap (algebraMap R S)

Full source

theorem nonZeroDivisors_le_comap [IsLocalization M S] :
    nonZeroDivisors R ≤ (nonZeroDivisors S).comap (algebraMap R S) := by
  rintro a ha b (e : b * algebraMap R S a = 0)
  obtain ⟨x, s, rfl⟩ := mk'_surjective M b
  rw [← @mk'_one R _ M, ← mk'_mul, ← (algebraMap R S).map_zero, ← @mk'_one R _ M,
    IsLocalization.eq] at e
  obtain ⟨c, e⟩ := e
  rw [mul_zero, mul_zero, Submonoid.coe_one, one_mul, ← mul_assoc] at e
  rw [mk'_eq_zero_iff]
  exact ⟨c, ha _ e⟩

Inclusion of Non-Zero Divisors in Localization Preimage: $\text{nonZeroDivisors}(R) \subseteq (\text{algebraMap}_R^S)^{-1}(\text{nonZeroDivisors}(S))$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. Then the non-zero divisors of $R$ are contained in the preimage of the non-zero divisors of $S$ under the canonical ring homomorphism $\text{algebraMap}_R^S \colon R \to S$.

IsLocalization.map_nonZeroDivisors_le theorem

[IsLocalization M S] : (nonZeroDivisors R).map (algebraMap R S) ≤ nonZeroDivisors S

Full source

theorem map_nonZeroDivisors_le [IsLocalization M S] :
    (nonZeroDivisors R).map (algebraMap R S) ≤ nonZeroDivisors S :=
  Submonoid.map_le_iff_le_comap.mpr (nonZeroDivisors_le_comap M S)

Image of Non-Zero Divisors in Localization is Contained in Non-Zero Divisors: $\text{algebraMap}_R^S(\text{nonZeroDivisors}(R)) \subseteq \text{nonZeroDivisors}(S)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. Then the image of the non-zero divisors of $R$ under the canonical ring homomorphism $\text{algebraMap}_R^S \colon R \to S$ is contained in the set of non-zero divisors of $S$.

Localization.instUniqueLocalization instance

[Subsingleton R] : Unique (Localization M)

Full source

instance instUniqueLocalization [Subsingleton R] : Unique (Localization M) where
  uniq a := by
    with_unfolding_all show a = mk 1 1
    exact Localization.induction_on a fun _ => by
      congr <;> apply Subsingleton.elim

Uniqueness of Localization for Subsingleton Rings

Informal description

If $R$ is a subsingleton (i.e., has at most one element), then the localization of $R$ at any submonoid $M$ is also a unique type (i.e., has exactly one element).

Localization.add_mk theorem

(a b c d) : (mk a b : Localization M) + mk c d = mk ((b : R) * c + (d : R) * a) (b * d)

Full source

theorem add_mk (a b c d) : (mk a b : Localization M) + mk c d =
    mk ((b : R) * c + (d : R) * a) (b * d) := by
  rw [add_comm (b * c) (d * a), mul_comm b d]
  exact OreLocalization.oreDiv_add_oreDiv

Addition Formula for Localized Fractions: $\frac{a}{b} + \frac{c}{d} = \frac{bc + da}{bd}$

Informal description

Let $R$ be a commutative ring and $M$ a submonoid of $R$. For any elements $a, c \in R$ and $b, d \in M$, the sum of the fractions $\frac{a}{b}$ and $\frac{c}{d}$ in the localization $R[M^{-1}]$ is given by: \[ \frac{a}{b} + \frac{c}{d} = \frac{b \cdot c + d \cdot a}{b \cdot d} \] where $b \cdot d \in M$ since $M$ is closed under multiplication.

Localization.add_mk_self theorem

(a b c) : (mk a b : Localization M) + mk c b = mk (a + c) b

Full source

theorem add_mk_self (a b c) : (mk a b : Localization M) + mk c b = mk (a + c) b := by
  rw [add_mk, mk_eq_mk_iff, r_eq_r']
  refine (r' M).symm ⟨1, ?_⟩
  simp only [Submonoid.coe_one, Submonoid.coe_mul]
  ring

Addition of Fractions with Common Denominator in Localization: $\frac{a}{b} + \frac{c}{b} = \frac{a + c}{b}$

Informal description

For any elements $a, c \in R$ and $b \in M$ in the localization of a commutative ring $R$ at a submonoid $M$, the sum of the fractions $\frac{a}{b}$ and $\frac{c}{b}$ is equal to $\frac{a + c}{b}$.

Localization.mkAddMonoidHom definition

(b : M) : R →+ Localization M

Full source

/-- For any given denominator `b : M`, the map `a ↦ a / b` is an `AddMonoidHom` from `R` to
  `Localization M`. -/
@[simps]
def mkAddMonoidHom (b : M) : R →+ Localization M where
  toFun a := mk a b
  map_zero' := mk_zero _
  map_add' _ _ := (add_mk_self _ _ _).symm

Additive monoid homomorphism from numerators to localized fractions with fixed denominator

Informal description

For a fixed denominator $b \in M$ in a submonoid $M$ of a commutative ring $R$, the function that maps a numerator $a \in R$ to the fraction $\frac{a}{b}$ in the localization $R[M^{-1}]$ is an additive monoid homomorphism. This means it satisfies: 1. $\frac{0}{b} = 0$ 2. $\frac{a_1 + a_2}{b} = \frac{a_1}{b} + \frac{a_2}{b}$ for all $a_1, a_2 \in R$

Localization.mk_sum theorem

{ι : Type*} (f : ι → R) (s : Finset ι) (b : M) : mk (∑ i ∈ s, f i) b = ∑ i ∈ s, mk (f i) b

Full source

theorem mk_sum {ι : Type*} (f : ι → R) (s : Finset ι) (b : M) :
    mk (∑ i ∈ s, f i) b = ∑ i ∈ s, mk (f i) b :=
  map_sum (mkAddMonoidHom b) f s

Summation Formula in Localization: $\frac{\sum f}{b} = \sum \frac{f}{b}$

Informal description

Let $R$ be a commutative ring and $M$ a submonoid of $R$. For any index set $\iota$, function $f \colon \iota \to R$, finite subset $s \subseteq \iota$, and fixed denominator $b \in M$, we have the equality in the localization $R[M^{-1}]$: \[ \frac{\sum_{i \in s} f(i)}{b} = \sum_{i \in s} \frac{f(i)}{b} \]

Localization.mk_list_sum theorem

(l : List R) (b : M) : mk l.sum b = (l.map fun a => mk a b).sum

Full source

theorem mk_list_sum (l : List R) (b : M) : mk l.sum b = (l.map fun a => mk a b).sum :=
  map_list_sum (mkAddMonoidHom b) l

Localization Preserves List Sums

Informal description

For any list $l$ of elements in a commutative ring $R$ and any element $b$ in a submonoid $M$ of $R$, the localization of the sum of $l$ at $b$ equals the sum of the localizations of each element in $l$ at $b$. In other words: \[ \text{mk}\left(\sum_{a \in l} a, b\right) = \sum_{a \in l} \text{mk}(a, b) \]

Localization.mk_multiset_sum theorem

(l : Multiset R) (b : M) : mk l.sum b = (l.map fun a => mk a b).sum

Full source

theorem mk_multiset_sum (l : Multiset R) (b : M) : mk l.sum b = (l.map fun a => mk a b).sum :=
  (mkAddMonoidHom b).map_multiset_sum l

Localization Preserves Multiset Summation

Informal description

For any multiset $l$ of elements in a commutative ring $R$ and any element $b$ in a submonoid $M$ of $R$, the fraction $\frac{\sum l}{b}$ in the localization $R[M^{-1}]$ is equal to the sum of the fractions $\frac{a}{b}$ for each $a$ in $l$. In other words, the localization map $\frac{\cdot}{b}$ commutes with multiset summation: \[ \frac{\sum l}{b} = \sum_{a \in l} \frac{a}{b} \]

Localization.isLocalization instance

: IsLocalization M (Localization M)

Full source

instance isLocalization : IsLocalization M (Localization M) where
  map_units' := (Localization.monoidOf M).map_units
  surj' := (Localization.monoidOf M).surj
  exists_of_eq := (Localization.monoidOf M).eq_iff_exists.mp

Localization of a Commutative Ring at a Submonoid

Informal description

The localization $R[M^{-1}]$ of a commutative ring $R$ at a submonoid $M$ satisfies the properties of being a localization. Specifically, there exists a ring homomorphism $R \to R[M^{-1}]$ such that: 1. Every element of $M$ maps to a unit in $R[M^{-1}]$; 2. Every element of $R[M^{-1}]$ can be written as $f(x) \cdot f(y)^{-1}$ for some $x \in R$ and $y \in M$; 3. The kernel of the homomorphism is characterized by $f(x) = f(y)$ if and only if there exists $c \in M$ such that $x \cdot c = y \cdot c$.

Localization.instNoZeroDivisors instance

[NoZeroDivisors R] : NoZeroDivisors (Localization M)

Full source

instance [NoZeroDivisors R] : NoZeroDivisors (Localization M) := IsLocalization.noZeroDivisors M

No Zero Divisors in Localization

Informal description

If a commutative ring $R$ has no zero divisors, then its localization $R[M^{-1}]$ at any submonoid $M$ also has no zero divisors.

Localization.toLocalizationMap_eq_monoidOf theorem

: toLocalizationMap M (Localization M) = monoidOf M

Full source

@[simp]
theorem toLocalizationMap_eq_monoidOf : toLocalizationMap M (Localization M) = monoidOf M :=
  rfl

Equality of Localization and Monoid Localization Maps

Informal description

The localization map from a commutative ring $R$ to its localization $R[M^{-1}]$ at a submonoid $M$ is equal to the monoid localization map `monoidOf M$.

Localization.monoidOf_eq_algebraMap theorem

(x) : (monoidOf M).toMap x = algebraMap R (Localization M) x

Full source

theorem monoidOf_eq_algebraMap (x) : (monoidOf M).toMap x = algebraMap R (Localization M) x :=
  rfl

Equality of Monoid Homomorphism and Algebra Map in Localization

Informal description

For any element $x$ of the commutative ring $R$, the monoid homomorphism `monoidOf M` applied to $x$ is equal to the algebra map from $R$ to the localization of $R$ at the submonoid $M$ applied to $x$.

Localization.mk_one_eq_algebraMap theorem

(x) : mk x 1 = algebraMap R (Localization M) x

Full source

theorem mk_one_eq_algebraMap (x) : mk x 1 = algebraMap R (Localization M) x :=
  rfl

Localization at Identity Equals Canonical Map: $\text{mk}(x, 1) = \text{algebraMap}_R(S)(x)$

Informal description

For any element $x$ of a commutative ring $R$, the localization of $x$ at the multiplicative identity $1$ in the submonoid $M$ is equal to the image of $x$ under the canonical algebra map from $R$ to its localization at $M$, i.e., $\text{mk}(x, 1) = \text{algebraMap}_R(S)(x)$, where $S$ is the localization of $R$ at $M$.

Localization.mk_eq_mk'_apply theorem

(x y) : mk x y = IsLocalization.mk' (Localization M) x y

Full source

theorem mk_eq_mk'_apply (x y) : mk x y = IsLocalization.mk' (Localization M) x y := by
  rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]

Equality of Localization Construction and Fraction Representation: $\text{mk}(x, y) = \text{mk'}(x, y)$

Informal description

For any element $x$ in a commutative ring $R$ and any element $y$ in a submonoid $M$ of $R$, the localization element $\text{mk}(x, y)$ in $R[M^{-1}]$ is equal to the fraction $\text{mk'}(x, y) = f(x) \cdot f(y)^{-1}$, where $f : R \to R[M^{-1}]$ is the canonical algebra map.

Localization.mk_eq_mk' theorem

: (mk : R → M → Localization M) = IsLocalization.mk' (Localization M)

Full source

theorem mk_eq_mk' : (mk : R → M → Localization M) = IsLocalization.mk' (Localization M) :=
  mk_eq_monoidOf_mk'

Localization Construction via Fractions: $\text{mk} = \text{mk'}$

Informal description

The localization map $\text{mk} : R \times M \to R[M^{-1}]$ coincides with the map $\text{mk'}$ defined by $\text{mk'}(x, y) = f(x) \cdot f(y)^{-1}$, where $f : R \to R[M^{-1}]$ is the canonical algebra map. In other words, for any $x \in R$ and $y \in M$, the fraction $\frac{x}{y}$ constructed via $\text{mk}$ is equal to $f(x) \cdot f(y)^{-1}$ in the localization $R[M^{-1}]$.

Localization.mk_algebraMap theorem

{A : Type*} [CommSemiring A] [Algebra A R] (m : A) : mk (algebraMap A R m) 1 = algebraMap A (Localization M) m

Full source

theorem mk_algebraMap {A : Type*} [CommSemiring A] [Algebra A R] (m : A) :
    mk (algebraMap A R m) 1 = algebraMap A (Localization M) m := by
  rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]; rfl

Commutativity of Localization with Algebra Map: $\text{mk}(\text{algebraMap}(m), 1) = \text{algebraMap}(m)$

Informal description

Let $A$ be a commutative semiring with an algebra structure over $R$, and let $M$ be a submonoid of $R$. For any element $m \in A$, the localization of the algebra map $\text{algebraMap}\, A\, R\, m$ at the identity element $1 \in M$ is equal to the algebra map $\text{algebraMap}\, A\, (R[M^{-1}])\, m$ in the localization $R[M^{-1}]$. In other words, the following diagram commutes: \[ \text{mk}(\text{algebraMap}\, A\, R\, m, 1) = \text{algebraMap}\, A\, (R[M^{-1}])\, m \]

Localization.neg_mk theorem

(a b) : -(mk a b : Localization M) = mk (-a) b

Full source

theorem neg_mk (a b) : -(mk a b : Localization M) = mk (-a) b := OreLocalization.neg_def _ _

Negation of Localization Fractions: $-(\frac{a}{b}) = \frac{-a}{b}$

Informal description

For any elements $a \in R$ and $b \in M$, the negation of the fraction $\frac{a}{b}$ in the localization of $R$ at $M$ is equal to the fraction $\frac{-a}{b}$.

Localization.sub_mk theorem

(a c) (b d) : (mk a b : Localization M) - mk c d = mk ((d : R) * a - b * c) (b * d)

Full source

theorem sub_mk (a c) (b d) : (mk a b : Localization M) - mk c d =
    mk ((d : R) * a - b * c) (b * d) := by
  rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]

Subtraction Formula for Localized Fractions: $\frac{a}{b} - \frac{c}{d} = \frac{da - bc}{bd}$

Informal description

Let $R$ be a commutative ring and $M$ a submonoid of $R$. For any elements $a, c \in R$ and $b, d \in M$, the difference of the fractions $\frac{a}{b}$ and $\frac{c}{d}$ in the localization $R[M^{-1}]$ is given by: \[ \frac{a}{b} - \frac{c}{d} = \frac{d \cdot a - b \cdot c}{b \cdot d} \] where $b \cdot d \in M$ since $M$ is closed under multiplication.

IsLocalization.mk'_neg theorem

(x : R) (y : M) : mk' S (-x) y = -mk' S x y

Full source

theorem mk'_neg (x : R) (y : M) :
    mk' S (-x) y = - mk' S x y := by
  rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]

Negation of Localized Fractions: $\text{mk'}_S(-x, y) = -\text{mk'}_S(x, y)$

Informal description

For any element $x$ in a commutative ring $R$ and any element $y$ in a submonoid $M$ of $R$, the localized element $\text{mk'}_S(-x, y)$ in the localization $S$ of $R$ at $M$ is equal to the negation of $\text{mk'}_S(x, y)$, i.e., \[ \text{mk'}_S(-x, y) = -\text{mk'}_S(x, y). \]

IsLocalization.mk'_sub theorem

(x₁ x₂ : R) (y₁ y₂ : M) : mk' S (x₁ * y₂ - x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Full source

theorem mk'_sub (x₁ x₂ : R) (y₁ y₂ : M) :
    mk' S (x₁ * y₂ - x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂ := by
  rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]

Subtraction Formula for Localized Fractions: $\frac{x_1}{y_1} - \frac{x_2}{y_2} = \frac{x_1 y_2 - x_2 y_1}{y_1 y_2}$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. For any elements $x_1, x_2 \in R$ and $y_1, y_2 \in M$, the difference of the localized elements $\text{mk'}_S(x_1, y_1)$ and $\text{mk'}_S(x_2, y_2)$ is equal to the localized element $\text{mk'}_S(x_1 y_2 - x_2 y_1, y_1 y_2)$. In other words: \[ \frac{x_1}{y_1} - \frac{x_2}{y_2} = \frac{x_1 y_2 - x_2 y_1}{y_1 y_2} \]

IsLocalization.injective_of_map_algebraMap_zero theorem

{T} [CommRing T] (f : S →+* T) (h : ∀ x, f (algebraMap R S x) = 0 → algebraMap R S x = 0) : Function.Injective f

Full source

lemma injective_of_map_algebraMap_zero {T} [CommRing T] (f : S →+* T)
    (h : ∀ x, f (algebraMap R S x) = 0 → algebraMap R S x = 0) :
    Function.Injective f := by
  rw [IsLocalization.injective_iff_map_algebraMap_eq M]
  refine fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩
  rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz
  apply h at hz
  rwa [map_sub, sub_eq_zero] at hz

Injectivity of Homomorphism from Localization via Zero Map Condition

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any commutative ring $T$ and ring homomorphism $f \colon S \to T$, if for all $x \in R$ the condition $f(\text{algebraMap}\, R\, S\, x) = 0$ implies $\text{algebraMap}\, R\, S\, x = 0$, then $f$ is injective.

IsLocalization.to_map_eq_zero_iff theorem

{x : R} (hM : M ≤ nonZeroDivisors R) : algebraMap R S x = 0 ↔ x = 0

Full source

theorem to_map_eq_zero_iff {x : R} (hM : M ≤ nonZeroDivisors R) : algebraMapalgebraMap R S x = 0 ↔ x = 0 := by
  rw [← (algebraMap R S).map_zero]
  constructor <;> intro h
  · obtain ⟨c, hc⟩ := (eq_iff_exists M S).mp h
    rw [mul_zero, mul_comm] at hc
    exact hM c.2 x hc
  · rw [h]

Localization Map Injects Non-Zero Divisors: $\text{algebraMap}\, R\, S\, x = 0 \leftrightarrow x = 0$

Informal description

Let $R$ be a commutative ring and $M$ a submonoid of $R$ such that $M$ is contained in the non-zero divisors of $R$. For any element $x \in R$, the image of $x$ under the localization map $\text{algebraMap}\, R\, S$ is zero if and only if $x$ is zero.

IsLocalization.injective theorem

(hM : M ≤ nonZeroDivisors R) : Injective (algebraMap R S)

Full source

protected theorem injective (hM : M ≤ nonZeroDivisors R) : Injective (algebraMap R S) := by
  rw [injective_iff_map_eq_zero (algebraMap R S)]
  intro a ha
  rwa [to_map_eq_zero_iff S hM] at ha

Injectivity of Localization Map for Non-Zero Divisor Submonoids

Informal description

Let $R$ be a commutative ring and $M$ a submonoid of $R$ such that $M$ is contained in the set of non-zero divisors of $R$. Then the canonical ring homomorphism $\text{algebraMap}\, R\, S$ from $R$ to its localization $S$ at $M$ is injective.

IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors theorem

[Nontrivial R] (hM : M ≤ nonZeroDivisors R) {x : R} (hx : x ∈ nonZeroDivisors R) : algebraMap R S x ≠ 0

Full source

protected theorem to_map_ne_zero_of_mem_nonZeroDivisors [Nontrivial R] (hM : M ≤ nonZeroDivisors R)
    {x : R} (hx : x ∈ nonZeroDivisors R) : algebraMapalgebraMap R S x ≠ 0 :=
  show (algebraMap R S).toMonoidWithZeroHom x ≠ 0 from
    map_ne_zero_of_mem_nonZeroDivisors (algebraMap R S) (IsLocalization.injective S hM) hx

Nonzero Image of Non-Zero Divisors under Localization Map

Informal description

Let $R$ be a nontrivial commutative ring and $M$ a submonoid of $R$ contained in the non-zero divisors of $R$. For any element $x \in R$ that is a non-zero divisor, the image of $x$ under the localization map $\text{algebraMap}\, R\, S$ is nonzero in $S$.

IsLocalization.sec_snd_ne_zero theorem

[Nontrivial R] (hM : M ≤ nonZeroDivisors R) (x : S) : ((sec M x).snd : R) ≠ 0

Full source

theorem sec_snd_ne_zero [Nontrivial R] (hM : M ≤ nonZeroDivisors R) (x : S) :
    ((sec M x).snd : R) ≠ 0 :=
  nonZeroDivisors.coe_ne_zero ⟨(sec M x).snd.val, hM (sec M x).snd.property⟩

Nonvanishing of Denominator in Localization Section Function

Informal description

Let $R$ be a nontrivial commutative ring and $M$ a submonoid of $R$ contained in the non-zero divisors of $R$. If $S$ is a localization of $R$ at $M$, then for any element $x \in S$, the second component of the pair obtained from the section function $\mathrm{sec}_M(x) \in R \times M$ is nonzero in $R$.

IsLocalization.isDomain_of_le_nonZeroDivisors theorem

[Algebra A S] {M : Submonoid A} [IsLocalization M S] (hM : M ≤ nonZeroDivisors A) : IsDomain S

Full source

/-- A `CommRing` `S` which is the localization of an integral domain `R` at a subset of
non-zero elements is an integral domain. -/
theorem isDomain_of_le_nonZeroDivisors [Algebra A S] {M : Submonoid A} [IsLocalization M S]
    (hM : M ≤ nonZeroDivisors A) : IsDomain S := by
  apply @NoZeroDivisors.to_isDomain _ _ (id _) (id _)
  · exact
      ⟨⟨(algebraMap A S) 0, (algebraMap A S) 1, fun h =>
          zero_ne_one (IsLocalization.injective S hM h)⟩⟩
  · exact noZeroDivisors M

Localization at Non-Zero Divisors Preserves Integral Domain Property

Informal description

Let $A$ be a commutative ring, $S$ an $A$-algebra, and $M$ a submonoid of $A$ such that $S$ is the localization of $A$ at $M$. If $M$ is contained in the set of non-zero divisors of $A$, then $S$ is an integral domain.

IsLocalization.isDomain_localization theorem

{M : Submonoid A} (hM : M ≤ nonZeroDivisors A) : IsDomain (Localization M)

Full source

/-- The localization of an integral domain to a set of non-zero elements is an integral domain. -/
theorem isDomain_localization {M : Submonoid A} (hM : M ≤ nonZeroDivisors A) :
    IsDomain (Localization M) :=
  isDomain_of_le_nonZeroDivisors _ hM

Localization at Non-Zero Divisors Yields Integral Domain

Informal description

Let $A$ be a commutative ring and $M$ a submonoid of $A$ contained in the set of non-zero divisors of $A$. Then the localization $A[M^{-1}]$ is an integral domain.

Mathlib.RingTheory.Localization.Defs

Main definitions

Main results

Implementation notes

Tags