Mathlib.GroupTheory.MonoidLocalization.Basic

AddSubmonoid.LocalizationMap structure

extends AddMonoidHom M N

Full source

/-- The type of AddMonoid homomorphisms satisfying the characteristic predicate: if `f : M →+ N`
satisfies this predicate, then `N` is isomorphic to the localization of `M` at `S`. -/
structure LocalizationMap extends AddMonoidHom M N where
  map_add_units' : ∀ y : S, IsAddUnit (toFun y)
  surj' : ∀ z : N, ∃ x : M × S, z + toFun x.2 = toFun x.1
  exists_of_eq : ∀ x y, toFun x = toFun y → ∃ c : S, ↑c + x = ↑c + y

Localization map for additive commutative monoids

Informal description

The structure representing a localization map for an additive commutative monoid $ M $ at a submonoid $ S $. A map $ f: M \to N $ is a localization map if it satisfies the following properties: 1. For all $ y \in S $, $ f(y) $ is invertible in $ N $; 2. For all $ z \in N $, there exists $ (x, y) \in M \times S $ such that $ z + f(y) = f(x) $; 3. For all $ x, y \in M $, if $ f(x) = f(y) $, then there exists $ c \in S $ such that $ x + c = y + c $. This structure extends an additive monoid homomorphism $ M \to N $.

Submonoid.LocalizationMap structure

extends MonoidHom M N

Full source

/-- The type of monoid homomorphisms satisfying the characteristic predicate: if `f : M →* N`
satisfies this predicate, then `N` is isomorphic to the localization of `M` at `S`. -/
structure LocalizationMap extends MonoidHom M N where
  map_units' : ∀ y : S, IsUnit (toFun y)
  surj' : ∀ z : N, ∃ x : M × S, z * toFun x.2 = toFun x.1
  exists_of_eq : ∀ x y, toFun x = toFun y → ∃ c : S, ↑c * x = c * y

Localization map for commutative monoids

Informal description

The structure representing a localization map for a commutative monoid $M$ at a submonoid $S$, which is a monoid homomorphism $f \colon M \to N$ satisfying the following properties: 1. For every $y \in S$, the image $f(y)$ is a unit in $N$; 2. For every $z \in N$, there exists $(x, y) \in M \times S$ such that $z \cdot f(y) = f(x)$; 3. For any $x, y \in M$ such that $f(x) = f(y)$, there exists $c \in S$ such that $x \cdot c = y \cdot c$. Such a map characterizes $N$ up to isomorphism as the localization of $M$ at $S$.

Localization.r definition

(S : Submonoid M) : Con (M × S)

Full source

/-- The congruence relation on `M × S`, `M` a `CommMonoid` and `S` a submonoid of `M`, whose
quotient is the localization of `M` at `S`, defined as the unique congruence relation on
`M × S` such that for any other congruence relation `s` on `M × S` where for all `y ∈ S`,
`(1, 1) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies
`(x₁, y₁) ∼ (x₂, y₂)` by `s`. -/
@[to_additive AddLocalization.r
    "The congruence relation on `M × S`, `M` an `AddCommMonoid` and `S` an `AddSubmonoid` of `M`,
whose quotient is the localization of `M` at `S`, defined as the unique congruence relation on
`M × S` such that for any other congruence relation `s` on `M × S` where for all `y ∈ S`,
`(0, 0) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies
`(x₁, y₁) ∼ (x₂, y₂)` by `s`."]
def r (S : Submonoid M) : Con (M × S) :=
  sInf { c | ∀ y : S, c 1 (y, y) }

Localization congruence relation

Informal description

The congruence relation $\sim$ on $M \times S$, where $M$ is a commutative monoid and $S$ is a submonoid of $M$, is defined as the infimum of all congruence relations $c$ on $M \times S$ such that $(1, 1) \sim (y, y)$ under $c$ for every $y \in S$. This relation characterizes the localization of $M$ at $S$ as the quotient of $M \times S$ by $\sim$.

Localization.r' definition

: Con (M × S)

Full source

/-- An alternate form of the congruence relation on `M × S`, `M` a `CommMonoid` and `S` a
submonoid of `M`, whose quotient is the localization of `M` at `S`. -/
@[to_additive AddLocalization.r'
    "An alternate form of the congruence relation on `M × S`, `M` a `CommMonoid` and `S` a
submonoid of `M`, whose quotient is the localization of `M` at `S`."]
def r' : Con (M × S) := by
  -- note we multiply by `c` on the left so that we can later generalize to `•`
  refine
    { r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
      iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
      mul' := ?_ }
  · rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
    use t₂ * t₁ * b.2
    simp only [Submonoid.coe_mul]
    calc
      (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
      _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl
  · rintro a b c d ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
    use t₂ * t₁
    calc
      (t₂ * t₁ : M) * (b.2 * d.2 * (a.1 * c.1)) = t₂ * (d.2 * c.1) * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = (t₂ * t₁ : M) * (a.2 * c.2 * (b.1 * d.1)) := by rw [ht₁, ht₂]; ac_rfl

Localization congruence relation (alternate form)

Informal description

The congruence relation `r'` on the product `M × S`, where `M` is a commutative monoid and `S` is a submonoid of `M`, is defined such that two pairs `(x₁, y₁)` and `(x₂, y₂)` are related if there exists an element `c ∈ S` satisfying the equation $c \cdot (y₂ \cdot x₁) = c \cdot (y₁ \cdot x₂)$. This relation is used to construct the localization of `M` at `S` as a quotient of `M × S`.

Localization.r_eq_r' theorem

: r S = r' S

Full source

/-- The congruence relation used to localize a `CommMonoid` at a submonoid can be expressed
equivalently as an infimum (see `Localization.r`) or explicitly
(see `Localization.r'`). -/
@[to_additive AddLocalization.r_eq_r'
    "The additive congruence relation used to localize an `AddCommMonoid` at a submonoid can be
expressed equivalently as an infimum (see `AddLocalization.r`) or explicitly
(see `AddLocalization.r'`)."]
theorem r_eq_r' : r S = r' S :=
  le_antisymm (sInf_le fun _ ↦ ⟨1, by simp⟩) <|
    le_sInf fun b H ⟨p, q⟩ ⟨x, y⟩ ⟨t, ht⟩ ↦ by
      rw [← one_mul (p, q), ← one_mul (x, y)]
      refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_
      convert b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1
      dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢
      simp_rw [mul_assoc, ht, mul_comm y q]

Equivalence of Localization Congruence Relations: $r = r'$

Informal description

For a commutative monoid $M$ and a submonoid $S \subseteq M$, the congruence relation $r$ used to localize $M$ at $S$ (defined as the infimum of all congruence relations making $(1,1) \sim (y,y)$ for all $y \in S$) is equal to the explicit congruence relation $r'$ defined by $(x_1, y_1) \sim (x_2, y_2)$ if there exists $c \in S$ such that $c \cdot (y_2 \cdot x_1) = c \cdot (y_1 \cdot x_2)$.

Localization.r_iff_exists theorem

{x y : M × S} : r S x y ↔ ∃ c : S, ↑c * (↑y.2 * x.1) = c * (x.2 * y.1)

Full source

@[to_additive AddLocalization.r_iff_exists]
theorem r_iff_exists {x y : M × S} : rr S x y ↔ ∃ c : S, ↑c * (↑y.2 * x.1) = c * (x.2 * y.1) := by
  rw [r_eq_r' S]; rfl

Characterization of Localization Congruence Relation: $r(x,y) \leftrightarrow \exists c \in S, c(y_2x_1) = c(x_2y_1)$

Informal description

For a commutative monoid $M$ with a submonoid $S$, and for any pairs $(x_1, y_1), (x_2, y_2) \in M \times S$, the elements are related under the localization congruence relation $r$ if and only if there exists an element $c \in S$ such that $c \cdot (y_2 \cdot x_1) = c \cdot (x_2 \cdot y_1)$.

Localization.r_iff_oreEqv_r theorem

{x y : M × S} : r S x y ↔ (OreLocalization.oreEqv S M).r x y

Full source

@[to_additive AddLocalization.r_iff_oreEqv_r]
theorem r_iff_oreEqv_r {x y : M × S} : rr S x y ↔ (OreLocalization.oreEqv S M).r x y := by
  simp only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv, smul_eq_mul,
    Submonoid.mk_smul]
  constructor
  · rintro ⟨u, hu, e⟩
    exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩
  · rintro ⟨u, hu, v, e₁, e₂⟩
    exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩

Equivalence of Localization and Ore Relations: $r \leftrightarrow \text{oreEqv}$

Informal description

For any commutative monoid $M$ with a submonoid $S$, and for any pairs $(x_1, y_1), (x_2, y_2) \in M \times S$, the elements are related under the localization congruence relation $r$ if and only if they are related under the Ore equivalence relation $\text{oreEqv}$ for the localization of $M$ at $S$.

Localization abbrev

Full source

/-- The localization of a `CommMonoid` at one of its submonoids (as a quotient type). -/
@[to_additive AddLocalization
    "The localization of an `AddCommMonoid` at one of its submonoids (as a quotient type)."]
abbrev Localization := OreLocalization S M

Localization of a Commutative Monoid at a Submonoid

Informal description

The localization of a commutative monoid $M$ at a submonoid $S$ is the quotient type obtained by identifying pairs $(x_1, y_1)$ and $(x_2, y_2)$ in $M \times S$ if there exists an element $c \in S$ such that $c \cdot (y_2 \cdot x_1) = c \cdot (x_2 \cdot y_1)$. This construction allows for the formal inversion of elements in $S$ within the monoid $M$.

Localization.mk definition

(x : M) (y : S) : Localization S

Full source

/-- Given a `CommMonoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to the equivalence
class of `(x, y)` in the localization of `M` at `S`. -/
@[to_additive
    "Given an `AddCommMonoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to
the equivalence class of `(x, y)` in the localization of `M` at `S`."]
def mk (x : M) (y : S) : Localization S := x /ₒ y

Canonical map to localization at a submonoid

Informal description

Given a commutative monoid $ M $ and a submonoid $ S \subseteq M $, the function $\text{mk}$ sends an element $ x \in M $ and $ y \in S $ to the equivalence class of the pair $(x, y)$ in the localization of $ M $ at $ S $, denoted $ M[S^{-1}] $. This equivalence class represents the formal fraction $ \frac{x}{y} $ in the localized monoid.

Localization.mk_eq_mk_iff theorem

{a c : M} {b d : S} : mk a b = mk c d ↔ r S ⟨a, b⟩ ⟨c, d⟩

Full source

@[to_additive]
theorem mk_eq_mk_iff {a c : M} {b d : S} : mkmk a b = mk c d ↔ r S ⟨a, b⟩ ⟨c, d⟩ := by
  rw [mk, mk, OreLocalization.oreDiv_eq_iff, r_iff_oreEqv_r]; rfl

Equality of Localization Elements via Congruence Relation

Informal description

For any elements $a, c \in M$ and $b, d \in S$, the equivalence classes $\text{mk}(a, b)$ and $\text{mk}(c, d)$ in the localization $M[S^{-1}]$ are equal if and only if the pairs $(a, b)$ and $(c, d)$ are related under the localization congruence relation $r$.

Localization.rec definition

 {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b))
  (H : ∀ {a c : M} {b d : S} (h : r S (a, b) (c, d)), (Eq.ndrec (f a b) (mk_eq_mk_iff.mpr h) : p (mk c d)) = f c d)
  (x) : p x

Full source

/-- Dependent recursion principle for `Localizations`: given elements `f a b : p (mk a b)`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d` (with the correct coercions),
then `f` is defined on the whole `Localization S`. -/
@[to_additive (attr := elab_as_elim)
    "Dependent recursion principle for `AddLocalizations`: given elements `f a b : p (mk a b)`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d` (with the correct coercions),
then `f` is defined on the whole `AddLocalization S`."]
def rec {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b))
    (H : ∀ {a c : M} {b d : S} (h : r S (a, b) (c, d)),
      (Eq.ndrec (f a b) (mk_eq_mk_iff.mpr h) : p (mk c d)) = f c d) (x) : p x :=
  Quot.rec (fun y ↦ Eq.ndrec (f y.1 y.2) (by rfl))
    (fun y z h ↦ by cases y; cases z; exact H (r_iff_oreEqv_r.mpr h)) x

Dependent recursion principle for localizations

Informal description

Given a commutative monoid $ M $ with a submonoid $ S \subseteq M $, and a dependent type family $ p $ on the localization $ M[S^{-1}] $, the dependent recursion principle `Localization.rec` constructs a function $ p(x) $ for any $ x \in M[S^{-1}] $ by providing: 1. A function $ f $ that defines $ p $ on representatives, i.e., for any $ a \in M $ and $ b \in S $, $ f $ gives a value $ p(\text{mk}(a, b)) $, where $\text{mk}(a, b)$ is the equivalence class of $(a, b)$ in $ M[S^{-1}] $. 2. A proof $ H $ that $ f $ respects the localization congruence relation $ r $, meaning that if $(a, b) \sim (c, d)$ under $ r $, then the value $ f(a, b) $ (transported along the equality $\text{mk}(a, b) = \text{mk}(c, d)$) equals $ f(c, d) $. This allows defining functions on $ M[S^{-1}] $ by specifying their behavior on representatives and verifying compatibility with the equivalence relation.

Localization.recOnSubsingleton₂ definition

 {r : Localization S → Localization S → Sort u} [h : ∀ (a c : M) (b d : S), Subsingleton (r (mk a b) (mk c d))]
  (x y : Localization S) (f : ∀ (a c : M) (b d : S), r (mk a b) (mk c d)) : r x y

Full source

/-- Copy of `Quotient.recOnSubsingleton₂` for `Localization` -/
@[to_additive (attr := elab_as_elim) "Copy of `Quotient.recOnSubsingleton₂` for `AddLocalization`"]
def recOnSubsingleton₂ {r : Localization S → Localization S → Sort u}
    [h : ∀ (a c : M) (b d : S), Subsingleton (r (mk a b) (mk c d))] (x y : Localization S)
    (f : ∀ (a c : M) (b d : S), r (mk a b) (mk c d)) : r x y :=
  @Quotient.recOnSubsingleton₂' _ _ _ _ r (Prod.rec fun _ _ => Prod.rec fun _ _ => h _ _ _ _) x y
    (Prod.rec fun _ _ => Prod.rec fun _ _ => f _ _ _ _)

Dependent recursion on pairs of localized elements with subsingleton condition

Informal description

Given a commutative monoid $M$ with a submonoid $S \subseteq M$, and a dependent type family $r$ on pairs of elements in the localization $M[S^{-1}]$ such that for any $a, c \in M$ and $b, d \in S$, the type $r(\text{mk}(a, b), \text{mk}(c, d))$ is a subsingleton, the function $\text{recOnSubsingleton₂}$ allows defining a value of type $r(x, y)$ for any $x, y \in M[S^{-1}]$ by providing a function $f$ that defines $r$ on representatives. Here, $\text{mk}(a, b)$ denotes the equivalence class of the pair $(a, b)$ in the localization $M[S^{-1}]$.

Localization.mk_mul theorem

(a c : M) (b d : S) : mk a b * mk c d = mk (a * c) (b * d)

Full source

@[to_additive]
theorem mk_mul (a c : M) (b d : S) : mk a b * mk c d = mk (a * c) (b * d) :=
  mul_comm b d ▸ OreLocalization.oreDiv_mul_oreDiv

Multiplication Rule in Localization: $\frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}$

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any elements $a, c \in M$ and $b, d \in S$, the product of the equivalence classes $\frac{a}{b}$ and $\frac{c}{d}$ in the localization $M[S^{-1}]$ equals the equivalence class $\frac{a \cdot c}{b \cdot d}$. In symbols: $$\frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}$$

Localization.mk_one theorem

: mk 1 (1 : S) = 1

Full source

@[to_additive]
theorem mk_one : mk 1 (1 : S) = 1 := OreLocalization.one_def

Identity Element in Localization: $\frac{1}{1} = 1$

Informal description

In the localization of a commutative monoid $M$ at a submonoid $S$, the equivalence class of the pair $(1, 1)$ is equal to the multiplicative identity element of the localized monoid. That is, $\frac{1}{1} = 1$ in $M[S^{-1}]$.

Localization.mk_pow theorem

(n : ℕ) (a : M) (b : S) : mk a b ^ n = mk (a ^ n) (b ^ n)

Full source

@[to_additive]
theorem mk_pow (n : ℕ) (a : M) (b : S) : mk a b ^ n = mk (a ^ n) (b ^ n) := by
  induction n <;> simp [pow_succ, *, ← mk_mul, ← mk_one]

Power Rule in Localization: $\left(\frac{a}{b}\right)^n = \frac{a^n}{b^n}$

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any natural number $n$, element $a \in M$, and $b \in S$, the $n$-th power of the equivalence class $\frac{a}{b}$ in the localization $M[S^{-1}]$ equals the equivalence class $\frac{a^n}{b^n}$. In symbols: $$\left(\frac{a}{b}\right)^n = \frac{a^n}{b^n}$$

Localization.mk_prod theorem

 {ι} (t : Finset ι) (f : ι → M) (s : ι → S) : ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

Full source

@[to_additive]
theorem mk_prod {ι} (t : Finset ι) (f : ι → M) (s : ι → S) :
    ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i) := by
  classical
  induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]

Product Rule in Localization: $\prod \frac{f(i)}{s(i)} = \frac{\prod f(i)}{\prod s(i)}$

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given a finite index set $\iota$, a finite subset $t \subseteq \iota$, and functions $f \colon \iota \to M$ and $s \colon \iota \to S$, the product of the equivalence classes $\frac{f(i)}{s(i)}$ for $i \in t$ in the localization $M[S^{-1}]$ equals the equivalence class of the pair consisting of the product $\prod_{i \in t} f(i)$ in $M$ and the product $\prod_{i \in t} s(i)$ in $S$. In symbols: $$\prod_{i \in t} \frac{f(i)}{s(i)} = \frac{\prod_{i \in t} f(i)}{\prod_{i \in t} s(i)}$$

Localization.ndrec_mk theorem

 {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b)) (H) (a : M) (b : S) :
  (rec f H (mk a b) : p (mk a b)) = f a b

Full source

@[to_additive (attr := simp)]
theorem ndrec_mk {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b)) (H) (a : M)
    (b : S) : (rec f H (mk a b) : p (mk a b)) = f a b := rfl

Dependent Recursor Computes Canonically on Localization Representatives

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given a dependent type family $p$ on the localization $M[S^{-1}]$ and a function $f \colon M \times S \to p(\text{mk}(a, b))$ that respects the localization congruence relation, the value of the dependent recursor $\text{rec}(f, H)$ applied to the equivalence class $\text{mk}(a, b)$ equals $f(a, b)$. In symbols: $$\text{rec}(f, H)(\text{mk}(a, b)) = f(a, b)$$

Localization.liftOn definition

 {p : Sort u} (x : Localization S) (f : M → S → p) (H : ∀ {a c : M} {b d : S}, r S (a, b) (c, d) → f a b = f c d) : p

Full source

/-- Non-dependent recursion principle for localizations: given elements `f a b : p`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d`,
then `f` is defined on the whole `Localization S`. -/
@[to_additive
    "Non-dependent recursion principle for `AddLocalization`s: given elements `f a b : p`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d`,
then `f` is defined on the whole `Localization S`."]
def liftOn {p : Sort u} (x : Localization S) (f : M → S → p)
    (H : ∀ {a c : M} {b d : S}, r S (a, b) (c, d) → f a b = f c d) : p :=
  rec f (fun h ↦ (by simpa only [eq_rec_constant] using H h)) x

Function definition on localization via representatives

Informal description

Given a commutative monoid $ M $ with a submonoid $ S \subseteq M $, the function `Localization.liftOn` allows defining a function on the localization $ M[S^{-1}] $ by specifying its behavior on representatives and verifying compatibility with the localization congruence relation. Specifically, for any type $ p $, any element $ x \in M[S^{-1}] $, a function $ f : M \to S \to p $, and a proof $ H $ that $ f $ respects the relation $ r $ (i.e., $ f(a, b) = f(c, d) $ whenever $ (a, b) \sim (c, d) $ under $ r $), the function `liftOn` returns a value in $ p $ by applying $ f $ to a representative of $ x $.

Localization.liftOn_mk theorem

{p : Sort u} (f : M → S → p) (H) (a : M) (b : S) : liftOn (mk a b) f H = f a b

Full source

@[to_additive]
theorem liftOn_mk {p : Sort u} (f : M → S → p) (H) (a : M) (b : S) :
    liftOn (mk a b) f H = f a b := rfl

Lift Function Computes Canonically on Localization Representatives

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any type $p$, any function $f : M \times S \to p$ that respects the localization congruence relation (i.e., $f(a,b) = f(c,d)$ whenever $(a,b) \sim (c,d)$ under the relation $r$), and any elements $a \in M$, $b \in S$, we have that applying the lift function to the equivalence class $\text{mk}(a,b)$ yields $f(a,b)$. In symbols: $$\text{liftOn}(\text{mk}(a,b), f, H) = f(a,b)$$

Localization.ind theorem

{p : Localization S → Prop} (H : ∀ y : M × S, p (mk y.1 y.2)) (x) : p x

Full source

@[to_additive (attr := elab_as_elim, induction_eliminator, cases_eliminator)]
theorem ind {p : Localization S → Prop} (H : ∀ y : M × S, p (mk y.1 y.2)) (x) : p x :=
  rec (fun a b ↦ H (a, b)) (fun _ ↦ rfl) x

Induction Principle for Localization of a Commutative Monoid

Informal description

For any predicate $p$ on the localization $M[S^{-1}]$ of a commutative monoid $M$ at a submonoid $S$, if $p$ holds for all elements of the form $\text{mk}(x, y)$ where $x \in M$ and $y \in S$, then $p$ holds for all elements of $M[S^{-1}]$.

Localization.induction_on theorem

{p : Localization S → Prop} (x) (H : ∀ y : M × S, p (mk y.1 y.2)) : p x

Full source

@[to_additive (attr := elab_as_elim)]
theorem induction_on {p : Localization S → Prop} (x) (H : ∀ y : M × S, p (mk y.1 y.2)) : p x :=
  ind H x

Induction Principle for Localization of Commutative Monoids

Informal description

For any predicate $p$ on the localization $M[S^{-1}]$ of a commutative monoid $M$ at a submonoid $S$, if $p$ holds for all elements of the form $\frac{x}{y}$ where $x \in M$ and $y \in S$, then $p$ holds for all elements of $M[S^{-1}]$.

Localization.liftOn₂ definition

 {p : Sort u} (x y : Localization S) (f : M → S → M → S → p)
  (H : ∀ {a a' b b' c c' d d'}, r S (a, b) (a', b') → r S (c, d) (c', d') → f a b c d = f a' b' c' d') : p

Full source

/-- Non-dependent recursion principle for localizations: given elements `f x y : p`
for all `x` and `y`, such that `r S x x'` and `r S y y'` implies `f x y = f x' y'`,
then `f` is defined on the whole `Localization S`. -/
@[to_additive
    "Non-dependent recursion principle for localizations: given elements `f x y : p`
for all `x` and `y`, such that `r S x x'` and `r S y y'` implies `f x y = f x' y'`,
then `f` is defined on the whole `Localization S`."]
def liftOn₂ {p : Sort u} (x y : Localization S) (f : M → S → M → S → p)
    (H : ∀ {a a' b b' c c' d d'}, r S (a, b) (a', b') → r S (c, d) (c', d') →
      f a b c d = f a' b' c' d') : p :=
  liftOn x (fun a b ↦ liftOn y (f a b) fun hy ↦ H ((r S).refl _) hy) fun hx ↦
    induction_on y fun ⟨_, _⟩ ↦ H hx ((r S).refl _)

Binary function definition on localization via representatives

Informal description

Given a commutative monoid $ M $ with a submonoid $ S \subseteq M $, the function `Localization.liftOn₂` allows defining a binary function on the localization $ M[S^{-1}] $ by specifying its behavior on pairs of representatives and verifying compatibility with the localization congruence relation. Specifically, for any type $ p $, any elements $ x, y \in M[S^{-1}] $, a function $ f : M \to S \to M \to S \to p $, and a proof $ H $ that $ f $ respects the relation $ r $ (i.e., $ f(a, b, c, d) = f(a', b', c', d') $ whenever $ (a, b) \sim (a', b') $ and $ (c, d) \sim (c', d') $ under $ r $), the function `liftOn₂` returns a value in $ p $ by applying $ f $ to representatives of $ x $ and $ y $.

Localization.liftOn₂_mk theorem

{p : Sort*} (f : M → S → M → S → p) (H) (a c : M) (b d : S) : liftOn₂ (mk a b) (mk c d) f H = f a b c d

Full source

@[to_additive]
theorem liftOn₂_mk {p : Sort*} (f : M → S → M → S → p) (H) (a c : M) (b d : S) :
    liftOn₂ (mk a b) (mk c d) f H = f a b c d := rfl

Lifted Binary Function on Localization Representatives

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any type $p$, any function $f \colon M \times S \times M \times S \to p$ that respects the localization congruence relation $r$ (i.e., $f(a,b,c,d) = f(a',b',c',d')$ whenever $(a,b) \sim (a',b')$ and $(c,d) \sim (c',d')$ under $r$), and any elements $a, c \in M$, $b, d \in S$, we have that applying the lifted function to the canonical representatives $\frac{a}{b}$ and $\frac{c}{d}$ equals the direct application of $f$ to these representatives, i.e., \[ \text{liftOn}_2\left(\frac{a}{b}, \frac{c}{d}, f, H\right) = f(a, b, c, d). \]

Localization.induction_on₂ theorem

{p : Localization S → Localization S → Prop} (x y) (H : ∀ x y : M × S, p (mk x.1 x.2) (mk y.1 y.2)) : p x y

Full source

@[to_additive (attr := elab_as_elim)]
theorem induction_on₂ {p : Localization S → Localization S → Prop} (x y)
    (H : ∀ x y : M × S, p (mk x.1 x.2) (mk y.1 y.2)) : p x y :=
  induction_on x fun x ↦ induction_on y <| H x

Double Induction Principle for Localization of Commutative Monoids

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any predicate $p$ on pairs of elements in the localization $M[S^{-1}]$, if $p$ holds for all pairs of the form $(\frac{x_1}{y_1}, \frac{x_2}{y_2})$ where $x_1, x_2 \in M$ and $y_1, y_2 \in S$, then $p$ holds for all pairs of elements in $M[S^{-1}]$.

Localization.induction_on₃ theorem

 {p : Localization S → Localization S → Localization S → Prop} (x y z)
  (H : ∀ x y z : M × S, p (mk x.1 x.2) (mk y.1 y.2) (mk z.1 z.2)) : p x y z

Full source

@[to_additive (attr := elab_as_elim)]
theorem induction_on₃ {p : Localization S → Localization S → Localization S → Prop} (x y z)
    (H : ∀ x y z : M × S, p (mk x.1 x.2) (mk y.1 y.2) (mk z.1 z.2)) : p x y z :=
  induction_on₂ x y fun x y ↦ induction_on z <| H x y

Triple Induction Principle for Localization of Commutative Monoids

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any predicate $p$ on triples of elements in the localization $M[S^{-1}]$, if $p$ holds for all triples of the form $(\frac{x_1}{y_1}, \frac{x_2}{y_2}, \frac{x_3}{y_3})$ where $x_1, x_2, x_3 \in M$ and $y_1, y_2, y_3 \in S$, then $p$ holds for all triples of elements in $M[S^{-1}]$.

Localization.one_rel theorem

(y : S) : r S 1 (y, y)

Full source

@[to_additive]
theorem one_rel (y : S) : r S 1 (y, y) := fun _ hb ↦ hb y

Identity Relation in Localization Congruence

Informal description

For any element $y$ in the submonoid $S$ of a commutative monoid $M$, the congruence relation $r$ on $M \times S$ satisfies $1 \sim (y, y)$.

Localization.r_of_eq theorem

{x y : M × S} (h : ↑y.2 * x.1 = ↑x.2 * y.1) : r S x y

Full source

@[to_additive]
theorem r_of_eq {x y : M × S} (h : ↑y.2 * x.1 = ↑x.2 * y.1) : r S x y :=
  r_iff_exists.2 ⟨1, by rw [h]⟩

Localization Congruence Relation Induced by Cross-Multiplication Equality

Informal description

For any pairs $(x_1, y_1), (x_2, y_2) \in M \times S$ where $M$ is a commutative monoid and $S$ is a submonoid of $M$, if $y_2 \cdot x_1 = x_2 \cdot y_1$ holds in $M$, then $(x_1, y_1) \sim (x_2, y_2)$ under the localization congruence relation $r$.

Localization.mk_self theorem

(a : S) : mk (a : M) a = 1

Full source

@[to_additive]
theorem mk_self (a : S) : mk (a : M) a = 1 := by
  symm
  rw [← mk_one, mk_eq_mk_iff]
  exact one_rel a

Localization Identity: $\frac{a}{a} = 1$ in $M[S^{-1}]$

Informal description

For any element $a$ in the submonoid $S$ of a commutative monoid $M$, the equivalence class of the pair $(a, a)$ in the localization $M[S^{-1}]$ is equal to the multiplicative identity element, i.e., $\frac{a}{a} = 1$.

Localization.smul_mk theorem

[SMul R M] [IsScalarTower R M M] (c : R) (a b) : c • (mk a b : Localization S) = mk (c • a) b

Full source

theorem smul_mk [SMul R M] [IsScalarTower R M M] (c : R) (a b) :
    c • (mk a b : Localization S) = mk (c • a) b := by
  rw [mk, mk, ← OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv]
  show (c • 1) • a /ₒ (b * 1) = _
  rw [smul_assoc, one_smul, mul_one]

Scalar Multiplication Commutes with Localization: $c \cdot \frac{a}{b} = \frac{c \cdot a}{b}$

Informal description

Let $M$ be a commutative monoid with a scalar multiplication action by a type $R$ satisfying the scalar tower condition (i.e., $r \cdot (m \cdot n) = (r \cdot m) \cdot n$ for all $r \in R$ and $m, n \in M$). For any $c \in R$, $a \in M$, and $b \in S$ (where $S$ is a submonoid of $M$), the scalar multiplication in the localization satisfies $c \cdot \left(\frac{a}{b}\right) = \frac{c \cdot a}{b}$, where $\frac{a}{b}$ denotes the equivalence class of $(a,b)$ in the localization $M[S^{-1}]$.

Localization.instSMulCommClassOfIsScalarTower instance

{R M : Type*} [CommMonoid M] [SMul R M] [IsScalarTower R M M] : SMulCommClass R M M

Full source

instance {R M : Type*} [CommMonoid M] [SMul R M] [IsScalarTower R M M] : SMulCommClass R M M where
  smul_comm r s x := by
    rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]

Commutativity of Scalar Actions in Localization

Informal description

For any commutative monoid $M$ with a scalar multiplication action by $R$ that satisfies the scalar tower condition (i.e., $r \cdot (m \cdot n) = (r \cdot m) \cdot n$ for all $r \in R$ and $m, n \in M$), the actions of $R$ and $M$ on the localization of $M$ at a submonoid $S$ commute. That is, for any $r \in R$, $m \in M$, and $s \in S$, we have $r \cdot (m \cdot s) = m \cdot (r \cdot s)$ in the localization.

MonoidHom.toLocalizationMap definition

 (f : M →* N) (H1 : ∀ y : S, IsUnit (f y)) (H2 : ∀ z, ∃ x : M × S, z * f x.2 = f x.1)
  (H3 : ∀ x y, f x = f y → ∃ c : S, ↑c * x = ↑c * y) : Submonoid.LocalizationMap S N

Full source

/-- Makes a localization map from a `CommMonoid` hom satisfying the characteristic predicate. -/
@[to_additive
    "Makes a localization map from an `AddCommMonoid` hom satisfying the characteristic predicate."]
def toLocalizationMap (f : M →* N) (H1 : ∀ y : S, IsUnit (f y))
    (H2 : ∀ z, ∃ x : M × S, z * f x.2 = f x.1) (H3 : ∀ x y, f x = f y → ∃ c : S, ↑c * x = ↑c * y) :
    Submonoid.LocalizationMap S N :=
  { f with
    map_units' := H1
    surj' := H2
    exists_of_eq := H3 }

Localization map from a monoid homomorphism satisfying characteristic properties

Informal description

Given a monoid homomorphism $ f \colon M \to N $ between commutative monoids, and a submonoid $ S $ of $ M $, the function `MonoidHom.toLocalizationMap` constructs a localization map for $ M $ at $ S $ with codomain $ N $, provided the following conditions hold: 1. For every $ y \in S $, the image $ f(y) $ is a unit in $ N $; 2. For every $ z \in N $, there exists a pair $ (x, y) \in M \times S $ such that $ z \cdot f(y) = f(x) $; 3. For any $ x, y \in M $ such that $ f(x) = f(y) $, there exists $ c \in S $ such that $ c \cdot x = c \cdot y $. This localization map characterizes $ N $ as the localization of $ M $ at $ S $ up to isomorphism.

Submonoid.LocalizationMap.toMap abbrev

(f : LocalizationMap S N)

Full source

/-- Short for `toMonoidHom`; used to apply a localization map as a function. -/
@[to_additive "Short for `toAddMonoidHom`; used to apply a localization map as a function."]
abbrev toMap (f : LocalizationMap S N) := f.toMonoidHom

Underlying homomorphism of a localization map

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, the function `toMap` represents the underlying monoid homomorphism $f$ itself, allowing it to be applied as a function.

Submonoid.LocalizationMap.ext theorem

{f g : LocalizationMap S N} (h : ∀ x, f.toMap x = g.toMap x) : f = g

Full source

@[to_additive (attr := ext)]
theorem ext {f g : LocalizationMap S N} (h : ∀ x, f.toMap x = g.toMap x) : f = g := by
  rcases f with ⟨⟨⟩⟩
  rcases g with ⟨⟨⟩⟩
  simp only [mk.injEq, MonoidHom.mk.injEq]
  exact OneHom.ext h

Extensionality of Localization Maps

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $N$ a commutative monoid. For any two localization maps $f, g \colon M \to N$ of $M$ at $S$, if $f(x) = g(x)$ for all $x \in M$, then $f = g$.

Submonoid.LocalizationMap.toMap_injective theorem

: Function.Injective (@LocalizationMap.toMap _ _ S N _)

Full source

@[to_additive]
theorem toMap_injective : Function.Injective (@LocalizationMap.toMap _ _ S N _) :=
  fun _ _ h ↦ ext <| DFunLike.ext_iff.1 h

Injectivity of the Underlying Homomorphism in Localization Maps

Informal description

The function `toMap` from localization maps $f \colon M \to N$ of a commutative monoid $M$ at a submonoid $S$ to their underlying monoid homomorphisms is injective. That is, if two localization maps have equal underlying homomorphisms, then they are equal as localization maps.

Submonoid.LocalizationMap.map_units theorem

(f : LocalizationMap S N) (y : S) : IsUnit (f.toMap y)

Full source

@[to_additive]
theorem map_units (f : LocalizationMap S N) (y : S) : IsUnit (f.toMap y) :=
  f.2 y

Localization maps send submonoid elements to units

Informal description

For any localization map $f \colon M \to N$ of a commutative monoid $M$ at a submonoid $S$, and for any element $y \in S$, the image $f(y)$ is a unit in $N$.

Submonoid.LocalizationMap.surj theorem

(f : LocalizationMap S N) (z : N) : ∃ x : M × S, z * f.toMap x.2 = f.toMap x.1

Full source

@[to_additive]
theorem surj (f : LocalizationMap S N) (z : N) : ∃ x : M × S, z * f.toMap x.2 = f.toMap x.1 :=
  f.3 z

Surjectivity of Localization Map: $z \cdot f(y) = f(x)$ for some $(x,y) \in M \times S$

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given a localization map $f \colon M \to N$ for $S$, for every element $z \in N$ there exists a pair $(x, y) \in M \times S$ such that $z \cdot f(y) = f(x)$.

Submonoid.LocalizationMap.surj₂ theorem

 (f : LocalizationMap S N) (z w : N) : ∃ z' w' : M, ∃ d : S, (z * f.toMap d = f.toMap z') ∧ (w * f.toMap d = f.toMap w')

Full source

/-- Given a localization map `f : M →* N`, and `z w : N`, there exist `z' w' : M` and `d : S`
such that `f z' / f d = z` and `f w' / f d = w`. -/
@[to_additive
    "Given a localization map `f : M →+ N`, and `z w : N`, there exist `z' w' : M` and `d : S`
such that `f z' - f d = z` and `f w' - f d = w`."]
theorem surj₂ (f : LocalizationMap S N) (z w : N) : ∃ z' w' : M, ∃ d : S,
    (z * f.toMap d = f.toMap z') ∧  (w * f.toMap d = f.toMap w') := by
  let ⟨a, ha⟩ := surj f z
  let ⟨b, hb⟩ := surj f w
  refine ⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩
  · simp_rw [mul_def, map_mul, ← ha]
    exact (mul_assoc z _ _).symm
  · simp_rw [mul_def, map_mul, ← hb]
    exact mul_left_comm w _ _

Common Denominator Property for Localization Maps

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given a localization map $f \colon M \to N$ for $S$, for any two elements $z, w \in N$, there exist elements $z', w' \in M$ and $d \in S$ such that: \[ z \cdot f(d) = f(z') \quad \text{and} \quad w \cdot f(d) = f(w'). \]

Submonoid.LocalizationMap.sec definition

(f : LocalizationMap S N) (z : N) : M × S

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`. -/
@[to_additive
    "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 (f : LocalizationMap S N) (z : N) : M × S := Classical.choose <| f.surj z

Section of a localization map

Informal description

Given a localization map $ f \colon M \to N $ for a commutative monoid $ M $ at a submonoid $ S $, the function $ \text{sec} $ assigns to each $ z \in N $ a pair $ (x, y) \in M \times S $ such that $ f(x) = z \cdot f(y) $. This provides a section of the localization process, ensuring that every element of $ N $ can be expressed in terms of elements of $ M $ and $ S $.

Submonoid.LocalizationMap.sec_spec theorem

{f : LocalizationMap S N} (z : N) : z * f.toMap (f.sec z).2 = f.toMap (f.sec z).1

Full source

@[to_additive]
theorem sec_spec {f : LocalizationMap S N} (z : N) :
    z * f.toMap (f.sec z).2 = f.toMap (f.sec z).1 := Classical.choose_spec <| f.surj z

Section Property of Localization Maps: $z \cdot f(y) = f(x)$ for $(x,y) = \mathrm{sec}(z)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. For any element $z \in N$, if $(x, y) \in M \times S$ is the pair obtained from the section $\mathrm{sec}(z)$, then $z \cdot f(y) = f(x)$.

Submonoid.LocalizationMap.sec_spec' theorem

{f : LocalizationMap S N} (z : N) : f.toMap (f.sec z).1 = f.toMap (f.sec z).2 * z

Full source

@[to_additive]
theorem sec_spec' {f : LocalizationMap S N} (z : N) :
    f.toMap (f.sec z).1 = f.toMap (f.sec z).2 * z := by rw [mul_comm, sec_spec]

Alternative Section Property of Localization Maps: $f(x) = f(y) \cdot z$ for $(x,y) = \mathrm{sec}(z)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. For any element $z \in N$, if $(x, y) \in M \times S$ is the pair obtained from the section $\mathrm{sec}(z)$, then $f(x) = f(y) \cdot z$.

Submonoid.LocalizationMap.mul_inv_left theorem

 {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
  w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z ↔ w = f y * z

Full source

/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`w, z : N` and `y ∈ S`, we have `w * (f y)⁻¹ = z ↔ w = f y * z`. -/
@[to_additive
    "Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `w, z : N` and `y ∈ S`, we have `w - f y = z ↔ w = f y + z`."]
theorem mul_inv_left {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
    w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z ↔ w = f y * z := by
  rw [mul_comm]
  exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)

Equivalence of Left Multiplication by Inverse in Localization

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism such that $f(y)$ is a unit in $N$ for every $y \in S$. Then for any $w, z \in N$ and $y \in S$, we have the equivalence: \[ w \cdot (f(y))^{-1} = z \quad \leftrightarrow \quad w = f(y) \cdot z. \]

Submonoid.LocalizationMap.mul_inv_right theorem

 {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
  z = w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ ↔ z * f y = w

Full source

/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`w, z : N` and `y ∈ S`, we have `z = w * (f y)⁻¹ ↔ z * f y = w`. -/
@[to_additive
    "Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `w, z : N` and `y ∈ S`, we have `z = w - f y ↔ z + f y = w`."]
theorem mul_inv_right {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
    z = w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ ↔ z * f y = w := by
  rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]

Equivalence of Right Multiplication by Inverse in Localization

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism such that $f(y)$ is a unit in $N$ for every $y \in S$. Then for any $w, z \in N$ and $y \in S$, we have the equivalence: \[ z = w \cdot (f(y))^{-1} \quad \leftrightarrow \quad z \cdot f(y) = w. \]

Submonoid.LocalizationMap.mul_inv theorem

 {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {x₁ x₂} {y₁ y₂ : S} :
  f x₁ * (IsUnit.liftRight (f.restrict S) h y₁)⁻¹ = f x₂ * (IsUnit.liftRight (f.restrict S) h y₂)⁻¹ ↔
    f (x₁ * y₂) = f (x₂ * y₁)

Full source

/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ Nˣ`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
`f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁)`. -/
@[to_additive (attr := simp)
    "Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
`f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁)`."]
theorem mul_inv {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {x₁ x₂} {y₁ y₂ : S} :
    f x₁ * (IsUnit.liftRight (f.restrict S) h y₁)⁻¹ =
        f x₂ * (IsUnit.liftRight (f.restrict S) h y₂)⁻¹ ↔
      f (x₁ * y₂) = f (x₂ * y₁) := by
  rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
    f.map_mul, f.map_mul]

Equivalence of Fraction Equality in Localization: $f(x_1)/f(y_1) = f(x_2)/f(y_2) \leftrightarrow f(x_1y_2) = f(x_2y_1)$

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism such that $f(y)$ is a unit in $N$ for every $y \in S$. Then for any $x_1, x_2 \in M$ and $y_1, y_2 \in S$, we have the equivalence: \[ f(x_1) \cdot (f(y_1))^{-1} = f(x_2) \cdot (f(y_2))^{-1} \quad \leftrightarrow \quad f(x_1 \cdot y_2) = f(x_2 \cdot y_1). \]

Submonoid.LocalizationMap.inv_inj theorem

 {f : M →* N} (hf : ∀ y : S, IsUnit (f y)) {y z : S}
  (h : (IsUnit.liftRight (f.restrict S) hf y)⁻¹ = (IsUnit.liftRight (f.restrict S) hf z)⁻¹) : f y = f z

Full source

/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`y, z ∈ S`, we have `(f y)⁻¹ = (f z)⁻¹ → f y = f z`. -/
@[to_additive
    "Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `y, z ∈ S`, we have `- (f y) = - (f z) → f y = f z`."]
theorem inv_inj {f : M →* N} (hf : ∀ y : S, IsUnit (f y)) {y z : S}
    (h : (IsUnit.liftRight (f.restrict S) hf y)⁻¹ = (IsUnit.liftRight (f.restrict S) hf z)⁻¹) :
      f y = f z := by
  rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]
  exact Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹

Injectivity of Unit Images via Equality of Inverses in Localization

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism such that $f(y)$ is a unit in $N$ for every $y \in S$. Then for any $y, z \in S$, if the inverses of $f(y)$ and $f(z)$ are equal, then $f(y) = f(z)$.

Submonoid.LocalizationMap.inv_unique theorem

 {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {y : S} {z : N} (H : f y * z = 1) :
  (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z

Full source

/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`y ∈ S`, `(f y)⁻¹` is unique. -/
@[to_additive
    "Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `y ∈ S`, `- (f y)` is unique."]
theorem inv_unique {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {y : S} {z : N} (H : f y * z = 1) :
    (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z := by
  rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]
  exact H.symm

Uniqueness of Inverse in Localization of Commutative Monoids

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism such that $f(y)$ is a unit in $N$ for every $y \in S$. For any $y \in S$ and $z \in N$ satisfying $f(y) \cdot z = 1$, the inverse of $f(y)$ in $N$ equals $z$, i.e., $(f(y))^{-1} = z$.

Submonoid.LocalizationMap.map_right_cancel theorem

{x y} {c : S} (h : f.toMap (c * x) = f.toMap (c * y)) : f.toMap x = f.toMap y

Full source

@[to_additive]
theorem map_right_cancel {x y} {c : S} (h : f.toMap (c * x) = f.toMap (c * y)) :
    f.toMap x = f.toMap y := by
  rw [f.toMap.map_mul, f.toMap.map_mul] at h
  let ⟨u, hu⟩ := f.map_units c
  rw [← hu] at h
  exact (Units.mul_right_inj u).1 h

Right Cancellation Property for Localization Maps

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $x, y \in M$ and $c \in S$, if $f(c \cdot x) = f(c \cdot y)$, then $f(x) = f(y)$.

Submonoid.LocalizationMap.map_left_cancel theorem

{x y} {c : S} (h : f.toMap (x * c) = f.toMap (y * c)) : f.toMap x = f.toMap y

Full source

@[to_additive]
theorem map_left_cancel {x y} {c : S} (h : f.toMap (x * c) = f.toMap (y * c)) :
    f.toMap x = f.toMap y :=
  f.map_right_cancel (c := c) <| by rw [mul_comm _ x, mul_comm _ y, h]

Left Cancellation Property for Localization Maps

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $x, y \in M$ and $c \in S$, if $f(x \cdot c) = f(y \cdot c)$, then $f(x) = f(y)$.

Submonoid.LocalizationMap.mk' definition

(f : LocalizationMap S N) (x : M) (y : S) : N

Full source

/-- Given a localization map `f : M →* N`, the surjection sending `(x, y) : M × S` to
`f x * (f y)⁻¹`. -/
@[to_additive
      "Given a localization map `f : M →+ N`, the surjection sending `(x, y) : M × S`
to `f x - f y`."]
noncomputable def mk' (f : LocalizationMap S N) (x : M) (y : S) : N :=
  f.toMap x * ↑(IsUnit.liftRight (f.toMap.restrict S) f.map_units y)⁻¹

Localization map surjection

Informal description

Given a localization map $ f \colon M \to N $ for a commutative monoid $ M $ at a submonoid $ S $, the function $ \text{mk}' $ sends a pair $(x, y) \in M \times S$ to the element $ f(x) \cdot (f(y))^{-1} $ in $ N $, where $ (f(y))^{-1} $ is the inverse of $ f(y) $ in the group of units of $ N $.

Submonoid.LocalizationMap.mk'_mul theorem

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

Full source

@[to_additive]
theorem mk'_mul (x₁ x₂ : M) (y₁ y₂ : S) : f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂ :=
  (mul_inv_left f.map_units _ _ _).2 <|
    show _ = _ * (_ * _ * (_ * _)) by
      rw [← mul_assoc, ← mul_assoc, mul_inv_right f.map_units, mul_assoc, mul_assoc,
          mul_comm _ (f.toMap x₂), ← mul_assoc, ← mul_assoc, mul_inv_right f.map_units,
          Submonoid.coe_mul, f.toMap.map_mul, f.toMap.map_mul]
      ac_rfl

Multiplicativity of Localization Map Construction: $f.\text{mk}'(x_1x_2, y_1y_2) = f.\text{mk}'(x_1,y_1) \cdot f.\text{mk}'(x_2,y_2)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Then for any elements $x_1, x_2 \in M$ and $y_1, y_2 \in S$, the following equality holds: \[ f.\text{mk}'(x_1 \cdot x_2, y_1 \cdot y_2) = f.\text{mk}'(x_1, y_1) \cdot f.\text{mk}'(x_2, y_2), \] where $f.\text{mk}'(x,y) = f(x) \cdot (f(y))^{-1}$ is the canonical map sending $(x,y) \in M \times S$ to its localized form in $N$.

Submonoid.LocalizationMap.mk'_one theorem

(x) : f.mk' x (1 : S) = f.toMap x

Full source

@[to_additive]
theorem mk'_one (x) : f.mk' x (1 : S) = f.toMap x := by
  rw [mk', MonoidHom.map_one]
  exact mul_one _

Localization at Identity Element Equals Original Map

Informal description

For any localization map $ f \colon M \to N $ of a commutative monoid $ M $ at a submonoid $ S $, and for any element $ x \in M $, the localization of $ x $ with respect to the identity element $ 1 \in S $ satisfies $ f.\text{mk}'(x, 1) = f(x) $.

Submonoid.LocalizationMap.mk'_sec theorem

(z : N) : f.mk' (f.sec z).1 (f.sec z).2 = z

Full source

/-- Given a localization map `f : M →* N` for a submonoid `S ⊆ M`, for all `z : N` we have that if
`x : M, y ∈ S` are such that `z * f y = f x`, then `f x * (f y)⁻¹ = z`. -/
@[to_additive (attr := simp)
    "Given a localization map `f : M →+ N` for a Submonoid `S ⊆ M`, for all `z : N`
we have that if `x : M, y ∈ S` are such that `z + f y = f x`, then `f x - f y = z`."]
theorem mk'_sec (z : N) : f.mk' (f.sec z).1 (f.sec z).2 = z :=
  show _ * _ = _ by rw [← sec_spec, mul_inv_left, mul_comm]

Localization of Section Elements Equals Original Element

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. For any element $z \in N$, if $(x, y) \in M \times S$ is the pair obtained from the section $\mathrm{sec}(z)$, then the localization of $x$ at $y$ equals $z$, i.e., \[ f(x) \cdot (f(y))^{-1} = z. \]

Submonoid.LocalizationMap.mk'_surjective theorem

(z : N) : ∃ (x : _) (y : S), f.mk' x y = z

Full source

@[to_additive]
theorem mk'_surjective (z : N) : ∃ (x : _) (y : S), f.mk' x y = z :=
  ⟨(f.sec z).1, (f.sec z).2, f.mk'_sec z⟩

Surjectivity of the Localization Map $ \text{mk}' $

Informal description

Given a localization map $ f \colon M \to N $ for a commutative monoid $ M $ at a submonoid $ S $, the function $ \text{mk}' $ is surjective. That is, for every element $ z \in N $, there exists a pair $ (x, y) \in M \times S $ such that $ f(x) \cdot (f(y))^{-1} = z $.

Submonoid.LocalizationMap.mk'_spec theorem

(x) (y : S) : f.mk' x y * f.toMap y = f.toMap x

Full source

@[to_additive]
theorem mk'_spec (x) (y : S) : f.mk' x y * f.toMap y = f.toMap x :=
  show _ * _ * _ = _ by rw [mul_assoc, mul_comm _ (f.toMap y), ← mul_assoc, mul_inv_left, mul_comm]

Localization relation: $f.mk'(x,y) \cdot f(y) = f(x)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $N$ a commutative monoid equipped with a localization map $f \colon M \to N$. For any $x \in M$ and $y \in S$, the element $f.mk'(x,y) \cdot f(y)$ equals $f(x)$, where $f.mk'(x,y) := f(x) \cdot (f(y))^{-1}$ is the localization of $x$ at $y$.

Submonoid.LocalizationMap.mk'_spec' theorem

(x) (y : S) : f.toMap y * f.mk' x y = f.toMap x

Full source

@[to_additive]
theorem mk'_spec' (x) (y : S) : f.toMap y * f.mk' x y = f.toMap x := by rw [mul_comm, mk'_spec]

Localization relation: $f(y) \cdot f.mk'(x,y) = f(x)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $N$ a commutative monoid equipped with a localization map $f \colon M \to N$. For any $x \in M$ and $y \in S$, the element $f(y) \cdot f.mk'(x,y)$ equals $f(x)$, where $f.mk'(x,y) := f(x) \cdot (f(y))^{-1}$ is the localization of $x$ at $y$.

Submonoid.LocalizationMap.mk'_eq_iff_eq_mul theorem

{x} {y : S} {z} : f.mk' x y = z ↔ f.toMap x = z * f.toMap y

Full source

@[to_additive]
theorem mk'_eq_iff_eq_mul {x} {y : S} {z} : f.mk' x y = z ↔ f.toMap x = z * f.toMap y := by
  rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]

Equivalence of Localization Expression and Product Form

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, and elements $x \in M$, $y \in S$, and $z \in N$, the equality $f(x) \cdot (f(y))^{-1} = z$ holds if and only if $f(x) = z \cdot f(y)$.

Submonoid.LocalizationMap.mk'_eq_iff_eq theorem

{x₁ x₂} {y₁ y₂ : S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (y₂ * x₁) = f.toMap (y₁ * x₂)

Full source

@[to_additive]
theorem mk'_eq_iff_eq {x₁ x₂} {y₁ y₂ : S} :
    f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (y₂ * x₁) = f.toMap (y₁ * x₂) :=
  ⟨fun H ↦ by
    rw [f.toMap.map_mul, f.toMap.map_mul, f.mk'_eq_iff_eq_mul.1 H,← mul_assoc, mk'_spec',
      mul_comm ((toMap f) x₂) _],
    fun H ↦ by
    rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f.toMap y₁), ← mul_assoc, ←
      f.toMap.map_mul, mul_comm x₂, ← H, ← mul_comm x₁, f.toMap.map_mul,
      mul_inv_right f.map_units]⟩

Equivalence of Localized Elements: $f(x₁)/f(y₁) = f(x₂)/f(y₂) \leftrightarrow f(y₂x₁) = f(y₁x₂)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $x₁, x₂ \in M$ and $y₁, y₂ \in S$, the equality \[ f(x₁) \cdot (f(y₁))^{-1} = f(x₂) \cdot (f(y₂))^{-1} \] holds if and only if \[ f(y₂ \cdot x₁) = f(y₁ \cdot x₂). \]

Submonoid.LocalizationMap.mk'_eq_iff_eq' theorem

{x₁ x₂} {y₁ y₂ : S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * y₂) = f.toMap (x₂ * y₁)

Full source

@[to_additive]
theorem mk'_eq_iff_eq' {x₁ x₂} {y₁ y₂ : S} :
    f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * y₂) = f.toMap (x₂ * y₁) := by
  simp only [f.mk'_eq_iff_eq, mul_comm]

Equivalence of Localized Elements via Commutative Product: $f(x₁)/f(y₁) = f(x₂)/f(y₂) \leftrightarrow f(x₁y₂) = f(x₂y₁)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $x₁, x₂ \in M$ and $y₁, y₂ \in S$, the equality \[ f(x₁) \cdot (f(y₁))^{-1} = f(x₂) \cdot (f(y₂))^{-1} \] holds if and only if \[ f(x₁ \cdot y₂) = f(x₂ \cdot y₁). \]

Submonoid.LocalizationMap.eq theorem

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

Full source

@[to_additive]
protected theorem eq {a₁ b₁} {a₂ b₂ : S} :
    f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ c : S, ↑c * (↑b₂ * a₁) = c * (a₂ * b₁) :=
  f.mk'_eq_iff_eq.trans <| f.eq_iff_exists

Equality of Localized Elements via Common Denominator

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $a₁, b₁ \in M$ and $a₂, b₂ \in S$, the equality \[ f(a₁) \cdot (f(a₂))^{-1} = f(b₁) \cdot (f(b₂))^{-1} \] holds if and only if there exists $c \in S$ such that \[ c \cdot (b₂ \cdot a₁) = c \cdot (a₂ \cdot b₁). \]

Submonoid.LocalizationMap.eq' theorem

{a₁ b₁} {a₂ b₂ : S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ Localization.r S (a₁, a₂) (b₁, b₂)

Full source

@[to_additive]
protected theorem eq' {a₁ b₁} {a₂ b₂ : S} :
    f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ Localization.r S (a₁, a₂) (b₁, b₂) := by
  rw [f.eq, Localization.r_iff_exists]

Equality of Localized Elements via Congruence Relation: $f(a₁)/f(a₂) = f(b₁)/f(b₂) \leftrightarrow (a₁,a₂) \sim (b₁,b₂)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $a₁, b₁ \in M$ and $a₂, b₂ \in S$, the equality \[ f(a₁) \cdot (f(a₂))^{-1} = f(b₁) \cdot (f(b₂))^{-1} \] holds if and only if the pairs $(a₁, a₂)$ and $(b₁, b₂)$ are related under the localization congruence relation $r$ on $M \times S$.

Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq theorem

 (g : LocalizationMap S P) {x₁ x₂} {y₁ y₂ : S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

Full source

@[to_additive]
theorem mk'_eq_iff_mk'_eq (g : LocalizationMap S P) {x₁ x₂} {y₁ y₂ : S} :
    f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂ :=
  f.eq'.trans g.eq'.symm

Equivalence of Localized Elements Across Different Localization Maps

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any two localization maps $f \colon M \to N$ and $g \colon M \to P$ at $S$, and for any elements $x₁, x₂ \in M$ and $y₁, y₂ \in S$, the equality \[ f(x₁) \cdot (f(y₁))^{-1} = f(x₂) \cdot (f(y₂))^{-1} \] holds in $N$ if and only if the equality \[ g(x₁) \cdot (g(y₁))^{-1} = g(x₂) \cdot (g(y₂))^{-1} \] holds in $P$.

Submonoid.LocalizationMap.exists_of_sec_mk' theorem

(x) (y : S) : ∃ c : S, ↑c * (↑(f.sec <| f.mk' x y).2 * x) = c * (y * (f.sec <| f.mk' x y).1)

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, for all `x₁ : M` and `y₁ ∈ S`,
if `x₂ : M, y₂ ∈ S` are such that `f x₁ * (f y₁)⁻¹ * f y₂ = f x₂`, then there exists `c ∈ S`
such that `x₁ * y₂ * c = x₂ * y₁ * c`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, for all `x₁ : M`
and `y₁ ∈ S`, if `x₂ : M, y₂ ∈ S` are such that `(f x₁ - f y₁) + f y₂ = f x₂`, then there exists
`c ∈ S` such that `x₁ + y₂ + c = x₂ + y₁ + c`."]
theorem exists_of_sec_mk' (x) (y : S) :
    ∃ c : S, ↑c * (↑(f.sec <| f.mk' x y).2 * x) = c * (y * (f.sec <| f.mk' x y).1) :=
  f.eq_iff_exists.1 <| f.mk'_eq_iff_eq.1 <| (mk'_sec _ _).symm

Existence of Cancellation Element for Localized Sections

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. For any $x \in M$ and $y \in S$, there exists an element $c \in S$ such that \[ c \cdot (f^{-1}(f(x)/f(y))_2 \cdot x) = c \cdot (y \cdot f^{-1}(f(x)/f(y))_1), \] where $(f^{-1}(f(x)/f(y))_1, f^{-1}(f(x)/f(y))_2) \in M \times S$ is the section of $f(x)/f(y)$ under $f$.

Submonoid.LocalizationMap.mk'_eq_of_eq theorem

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

Full source

@[to_additive]
theorem mk'_eq_of_eq {a₁ b₁ : M} {a₂ b₂ : S} (H : ↑a₂ * b₁ = ↑b₂ * a₁) :
    f.mk' a₁ a₂ = f.mk' b₁ b₂ :=
  f.mk'_eq_iff_eq.2 <| H ▸ rfl

Equality of Localized Elements via Cross-Multiplication

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $a₁, b₁ \in M$ and $a₂, b₂ \in S$, if $a₂ \cdot b₁ = b₂ \cdot a₁$ holds in $M$, then the localized elements satisfy $f(a₁) \cdot (f(a₂))^{-1} = f(b₁) \cdot (f(b₂))^{-1}$ in $N$.

Submonoid.LocalizationMap.mk'_eq_of_eq' theorem

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

Full source

@[to_additive]
theorem mk'_eq_of_eq' {a₁ b₁ : M} {a₂ b₂ : S} (H : b₁ * ↑a₂ = a₁ * ↑b₂) :
    f.mk' a₁ a₂ = f.mk' b₁ b₂ :=
  f.mk'_eq_of_eq <| by simpa only [mul_comm] using H

Equality of Localized Elements via Cross-Multiplication (Alternate Form)

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map. For any elements $a₁, b₁ \in M$ and $a₂, b₂ \in S$, if $b₁ \cdot a₂ = a₁ \cdot b₂$ holds in $M$, then the localized elements satisfy $f(a₁) \cdot (f(a₂))^{-1} = f(b₁) \cdot (f(b₂))^{-1}$ in $N$.

Submonoid.LocalizationMap.mk'_cancel theorem

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

Full source

@[to_additive]
theorem mk'_cancel (a : M) (b c : S) :
    f.mk' (a * c) (b * c) = f.mk' a b :=
  mk'_eq_of_eq' f (by rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc])

Cancellation Property in Localization: $f(a \cdot c)/f(b \cdot c) = f(a)/f(b)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. For any element $a \in M$ and elements $b, c \in S$, the localized elements satisfy: \[ f(a \cdot c) \cdot (f(b \cdot c))^{-1} = f(a) \cdot (f(b))^{-1} \]

Submonoid.LocalizationMap.mk'_eq_of_same theorem

{a b} {d : S} : f.mk' a d = f.mk' b d ↔ ∃ c : S, c * a = c * b

Full source

@[to_additive]
theorem mk'_eq_of_same {a b} {d : S} :
    f.mk' a d = f.mk' b d ↔ ∃ c : S, c * a = c * b := by
  rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]
  exact (map_units f d).mul_left_inj

Equality of Localized Elements via Common Multiplier: $f(a)/f(d) = f(b)/f(d) \leftrightarrow \exists c \in S, c \cdot a = c \cdot b$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. For any elements $a, b \in M$ and $d \in S$, the equality \[ f(a) \cdot (f(d))^{-1} = f(b) \cdot (f(d))^{-1} \] holds if and only if there exists $c \in S$ such that $c \cdot a = c \cdot b$ in $M$.

Submonoid.LocalizationMap.mk'_self' theorem

(y : S) : f.mk' (y : M) y = 1

Full source

@[to_additive (attr := simp)]
theorem mk'_self' (y : S) : f.mk' (y : M) y = 1 :=
  show _ * _ = _ by rw [mul_inv_left, mul_one]

Localization of a submonoid element with itself yields identity

Informal description

For any element $y$ in the submonoid $S$ of a commutative monoid $M$, and for any localization map $f \colon M \to N$ at $S$, the element $f(y) \cdot (f(y))^{-1}$ equals the multiplicative identity $1$ in $N$.

Submonoid.LocalizationMap.mk'_self theorem

(x) (H : x ∈ S) : f.mk' x ⟨x, H⟩ = 1

Full source

@[to_additive (attr := simp)]
theorem mk'_self (x) (H : x ∈ S) : f.mk' x ⟨x, H⟩ = 1 := mk'_self' f ⟨x, H⟩

Localization of a submonoid element with itself yields identity

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given a localization map $f \colon M \to N$ at $S$, for any element $x \in S$ (with proof $H$ that $x \in S$), we have $f(x) \cdot (f(x))^{-1} = 1$ in $N$.

Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul theorem

(x₁ x₂) (y : S) : f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

Full source

@[to_additive]
theorem mul_mk'_eq_mk'_of_mul (x₁ x₂) (y : S) : f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y := by
  rw [← mk'_one, ← mk'_mul, one_mul]

Compatibility of localization map with multiplication: $f(x₁) \cdot f.\text{mk}'(x₂,y) = f.\text{mk}'(x₁x₂,y)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Then for any elements $x₁, x₂ \in M$ and $y \in S$, the following equality holds in $N$: \[ f(x₁) \cdot f.\text{mk}'(x₂, y) = f.\text{mk}'(x₁ \cdot x₂, y), \] where $f.\text{mk}'(x,y) = f(x) \cdot (f(y))^{-1}$ is the canonical localization map.

Submonoid.LocalizationMap.mk'_mul_eq_mk'_of_mul theorem

(x₁ x₂) (y : S) : f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * x₂) y

Full source

@[to_additive]
theorem mk'_mul_eq_mk'_of_mul (x₁ x₂) (y : S) : f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * x₂) y := by
  rw [mul_comm, mul_mk'_eq_mk'_of_mul]

Compatibility of localization map with multiplication: $f.\text{mk}'(x₂,y) \cdot f(x₁) = f.\text{mk}'(x₁x₂,y)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Then for any elements $x₁, x₂ \in M$ and $y \in S$, the following equality holds in $N$: \[ f.\text{mk}'(x₂, y) \cdot f(x₁) = f.\text{mk}'(x₁ \cdot x₂, y), \] where $f.\text{mk}'(x,y) = f(x) \cdot (f(y))^{-1}$ is the canonical localization map.

Submonoid.LocalizationMap.mul_mk'_one_eq_mk' theorem

(x) (y : S) : f.toMap x * f.mk' 1 y = f.mk' x y

Full source

@[to_additive]
theorem mul_mk'_one_eq_mk' (x) (y : S) : f.toMap x * f.mk' 1 y = f.mk' x y := by
  rw [mul_mk'_eq_mk'_of_mul, mul_one]

Localization identity: $f(x) \cdot f(1,y)^{-1} = f(x,y)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Then for any element $x \in M$ and $y \in S$, the following equality holds in $N$: \[ f(x) \cdot f.\text{mk}'(1, y) = f.\text{mk}'(x, y), \] where $f.\text{mk}'(x,y) = f(x) \cdot (f(y))^{-1}$ is the canonical localization map.

Submonoid.LocalizationMap.mk'_mul_cancel_right theorem

(x : M) (y : S) : f.mk' (x * y) y = f.toMap x

Full source

@[to_additive (attr := simp)]
theorem mk'_mul_cancel_right (x : M) (y : S) : f.mk' (x * y) y = f.toMap x := by
  rw [← mul_mk'_one_eq_mk', f.toMap.map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]

Right cancellation property in localization: $f(xy,y) = f(x)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Then for any element $x \in M$ and $y \in S$, the following equality holds in $N$: \[ f.\text{mk}'(x \cdot y, y) = f(x), \] where $f.\text{mk}'(x,y) = f(x) \cdot (f(y))^{-1}$ is the canonical localization map.

Submonoid.LocalizationMap.mk'_mul_cancel_left theorem

(x) (y : S) : f.mk' ((y : M) * x) y = f.toMap x

Full source

@[to_additive]
theorem mk'_mul_cancel_left (x) (y : S) : f.mk' ((y : M) * x) y = f.toMap x := by
  rw [mul_comm, mk'_mul_cancel_right]

Left cancellation property in localization: $f(yx,y) = f(x)$

Informal description

Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Then for any element $x \in M$ and $y \in S$, the following equality holds in $N$: \[ f.\text{mk}'(y \cdot x, y) = f(x), \] where $f.\text{mk}'(x,y) = f(x) \cdot (f(y))^{-1}$ is the canonical localization map.

Submonoid.LocalizationMap.isUnit_comp theorem

(j : N →* P) (y : S) : IsUnit (j.comp f.toMap y)

Full source

@[to_additive]
theorem isUnit_comp (j : N →* P) (y : S) : IsUnit (j.comp f.toMap y) :=
  ⟨Units.map j <| IsUnit.liftRight (f.toMap.restrict S) f.map_units y,
    show j _ = j _ from congr_arg j <| IsUnit.coe_liftRight (f.toMap.restrict S) f.map_units _⟩

Composition of Localization Map Preserves Units

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map at $S$. For any monoid homomorphism $j \colon N \to P$ and any element $y \in S$, the composition $j \circ f$ maps $y$ to a unit in $P$. In other words, $j(f(y))$ is a unit in $P$.

Submonoid.LocalizationMap.comp_eq_of_eq theorem

 {T : Submonoid P} {Q : Type*} [CommMonoid Q] (hg : ∀ y : S, g y ∈ T) (k : LocalizationMap T Q) {x y}
  (h : f.toMap x = f.toMap y) : k.toMap (g x) = k.toMap (g y)

Full source

/-- Given `CommMonoid`s `M, P`, Localization maps `f : M →* N, k : P →* Q` for Submonoids
`S, T` respectively, and `g : M →* P` such that `g(S) ⊆ T`, `f x = f y` implies
`k (g x) = k (g y)`. -/
@[to_additive
    "Given `AddCommMonoid`s `M, P`, Localization maps `f : M →+ N, k : P →+ Q` for Submonoids
`S, T` respectively, and `g : M →+ P` such that `g(S) ⊆ T`, `f x = f y`
implies `k (g x) = k (g y)`."]
theorem comp_eq_of_eq {T : Submonoid P} {Q : Type*} [CommMonoid Q] (hg : ∀ y : S, g y ∈ T)
    (k : LocalizationMap T Q) {x y} (h : f.toMap x = f.toMap y) : k.toMap (g x) = k.toMap (g y) :=
  f.eq_of_eq (fun y : S ↦ show IsUnit (k.toMap.comp g y) from k.map_units ⟨g y, hg y⟩) h

Localization Maps Preserve Equality under Compatible Homomorphisms

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively. Given localization maps $f \colon M \to N$ for $S$ and $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, if $f(x) = f(y)$ for some $x, y \in M$, then $k(g(x)) = k(g(y))$.

Submonoid.LocalizationMap.lift definition

: N →* P

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g y` is invertible for all `y : S`, the homomorphism induced from
`N` to `P` sending `z : N` to `g x * (g y)⁻¹`, where `(x, y) : M × S` are such that
`z = f x * (f y)⁻¹`. -/
@[to_additive
    "Given a localization map `f : M →+ N` for a submonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
induced from `N` to `P` sending `z : N` to `g x - g y`, where `(x, y) : M × S` are such that
`z = f x - f y`."]
noncomputable def lift : N →* P where
  toFun z := g (f.sec z).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec z).2)⁻¹
  map_one' := by rw [mul_inv_left, mul_one]; exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])
  map_mul' x y := by
    rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ←
      mul_assoc, ← mul_assoc, mul_inv_right hg]
    repeat rw [← g.map_mul]
    exact f.eq_of_eq hg (by simp_rw [f.toMap.map_mul, sec_spec']; ac_rfl)

Induced homomorphism from localization

Informal description

Given a localization map $ f \colon M \to N $ for a commutative monoid $ M $ at a submonoid $ S $, and a monoid homomorphism $ g \colon M \to P $ such that $ g(y) $ is a unit in $ P $ for every $ y \in S $, the function $ \text{lift} $ is the induced homomorphism from $ N $ to $ P $ defined by sending $ z \in N $ to $ g(x) \cdot (g(y))^{-1} $, where $ (x, y) \in M \times S $ is any pair such that $ z = f(x) \cdot (f(y))^{-1} $.

Submonoid.LocalizationMap.lift_apply theorem

(z) : f.lift hg z = g (f.sec z).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec z).2)⁻¹

Full source

@[to_additive]
lemma lift_apply (z) :
    f.lift hg z = g (f.sec z).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec z).2)⁻¹ :=
  rfl

Explicit Formula for the Induced Homomorphism from Localization

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, the induced homomorphism $\text{lift}(f, g) \colon N \to P$ satisfies \[ \text{lift}(f, g)(z) = g(x) \cdot (g(y))^{-1}, \] where $(x, y) = \text{sec}(f)(z)$ is the section of $f$ at $z \in N$.

Submonoid.LocalizationMap.lift_mk' theorem

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

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g y` is invertible for all `y : S`, the homomorphism induced from
`N` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : M, y ∈ S`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`."]
theorem lift_mk' (x y) : f.lift hg (f.mk' x y) = g x * (IsUnit.liftRight (g.restrict S) hg y)⁻¹ :=
  (mul_inv hg).2 <|
    f.eq_of_eq hg <| by
      simp_rw [f.toMap.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]

Induced homomorphism on localization satisfies $\text{lift}(f(x)/f(y)) = g(x)/g(y)$

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, the induced homomorphism $\text{lift}(f, g) \colon N \to P$ satisfies \[ \text{lift}(f, g)(f(x) \cdot (f(y))^{-1}) = g(x) \cdot (g(y))^{-1} \] for all $x \in M$ and $y \in S$.

Submonoid.LocalizationMap.lift_localizationMap_mk' theorem

(g : S.LocalizationMap P) (x y) : f.lift g.map_units (f.mk' x y) = g.mk' x y

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a localization map
`g : M →* P` for the same submonoid, the homomorphism induced from
`N` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : M, y ∈ S`. -/
@[to_additive (attr := simp)
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M` and a localization map
`g : M →+ P` for the same submonoid, the homomorphism
induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`."]
theorem lift_localizationMap_mk' (g : S.LocalizationMap P) (x y) :
    f.lift g.map_units (f.mk' x y) = g.mk' x y :=
  f.lift_mk' _ _ _

Induced homomorphism preserves localization fractions: $\text{lift}(f(x)/f(y)) = g(x)/g(y)$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ and $g \colon M \to P$ be localization maps for $S$. For any $x \in M$ and $y \in S$, the induced homomorphism $\text{lift}(f, g) \colon N \to P$ satisfies \[ \text{lift}(f, g)(f(x) \cdot (f(y))^{-1}) = g(x) \cdot (g(y))^{-1}. \]

Submonoid.LocalizationMap.lift_spec theorem

(z v) : f.lift hg z = v ↔ g (f.sec z).1 = g (f.sec z).2 * v

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N, v : P`, we have
`f.lift hg z = v ↔ g x = g y * v`, where `x : M, y ∈ S` are such that `z * f y = f x`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, if an
`AddCommMonoid` map `g : M →+ P` induces a map `f.lift hg : N →+ P` then for all
`z : N, v : P`, we have `f.lift hg z = v ↔ g x = g y + v`, where `x : M, y ∈ S` are such that
`z + f y = f x`."]
theorem lift_spec (z v) : f.lift hg z = v ↔ g (f.sec z).1 = g (f.sec z).2 * v :=
  mul_inv_left hg _ _ v

Characterization of the lift of a localization map via section elements

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, and the induced homomorphism $f.lift\ hg \colon N \to P$, then for any $z \in N$ and $v \in P$, we have: \[ f.lift\ hg\ z = v \quad \leftrightarrow \quad g(x) = g(y) \cdot v \] where $(x, y) = f.sec\ z$ is the section of $z$ under $f$.

Submonoid.LocalizationMap.lift_spec_mul theorem

(z w v) : f.lift hg z * w = v ↔ g (f.sec z).1 * w = g (f.sec z).2 * v

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N, v w : P`, we have
`f.lift hg z * w = v ↔ g x * w = g y * v`, where `x : M, y ∈ S` are such that
`z * f y = f x`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, if an `AddCommMonoid` map
`g : M →+ P` induces a map `f.lift hg : N →+ P` then for all
`z : N, v w : P`, we have `f.lift hg z + w = v ↔ g x + w = g y + v`, where `x : M, y ∈ S` are such
that `z + f y = f x`."]
theorem lift_spec_mul (z w v) : f.lift hg z * w = v ↔ g (f.sec z).1 * w = g (f.sec z).2 * v := by
  rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]

Characterization of the lift of a localization map via multiplication with section elements

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $z \in N$ and $v, w \in P$, we have the equivalence: \[ f.lift\ hg\ z \cdot w = v \quad \leftrightarrow \quad g(x) \cdot w = g(y) \cdot v, \] where $(x, y) = f.sec\ z$ is the section of $z$ under $f$.

Submonoid.LocalizationMap.lift_mk'_spec theorem

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

Full source

@[to_additive]
theorem lift_mk'_spec (x v) (y : S) : f.lift hg (f.mk' x y) = v ↔ g x = g y * v := by
  rw [f.lift_mk' hg]; exact mul_inv_left hg _ _ _

Characterization of the lift of a localization map on fractions: $f.lift\,hg\,(x/y) = v \leftrightarrow g(x) = g(y) \cdot v$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $x \in M$, $y \in S$, and $v \in P$, we have the equivalence: \[ f.lift\,hg\,(f(x) \cdot (f(y))^{-1}) = v \quad \leftrightarrow \quad g(x) = g(y) \cdot v. \]

Submonoid.LocalizationMap.lift_mul_right theorem

(z) : f.lift hg z * g (f.sec z).2 = g (f.sec z).1

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N`, we have
`f.lift hg z * g y = g x`, where `x : M, y ∈ S` are such that `z * f y = f x`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, if an `AddCommMonoid`
map `g : M →+ P` induces a map `f.lift hg : N →+ P` then for all `z : N`, we have
`f.lift hg z + g y = g x`, where `x : M, y ∈ S` are such that `z + f y = f x`."]
theorem lift_mul_right (z) : f.lift hg z * g (f.sec z).2 = g (f.sec z).1 := by
  rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, mul_one]

Right multiplication property of localization lift: $f.lift\,hg\,z \cdot g(y) = g(x)$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $z \in N$ we have \[ f.lift\,hg\,z \cdot g(y) = g(x), \] where $(x, y) = f.sec\,z$ is the section of $f$ at $z$ (so $x \in M$ and $y \in S$ satisfy $z \cdot f(y) = f(x)$).

Submonoid.LocalizationMap.lift_mul_left theorem

(z) : g (f.sec z).2 * f.lift hg z = g (f.sec z).1

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N`, we have
`g y * f.lift hg z = g x`, where `x : M, y ∈ S` are such that `z * f y = f x`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, if an `AddCommMonoid` map
`g : M →+ P` induces a map `f.lift hg : N →+ P` then for all `z : N`, we have
`g y + f.lift hg z = g x`, where `x : M, y ∈ S` are such that `z + f y = f x`."]
theorem lift_mul_left (z) : g (f.sec z).2 * f.lift hg z = g (f.sec z).1 := by
  rw [mul_comm, lift_mul_right]

Left multiplication property of localization lift: $g(y) \cdot f.lift\,hg\,z = g(x)$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $z \in N$ we have \[ g(y) \cdot f.lift\,hg\,z = g(x), \] where $(x, y) = f.sec\,z$ is the section of $f$ at $z$ (so $x \in M$ and $y \in S$ satisfy $z \cdot f(y) = f(x)$).

Submonoid.LocalizationMap.lift_eq theorem

(x : M) : f.lift hg (f.toMap x) = g x

Full source

@[to_additive (attr := simp)]
theorem lift_eq (x : M) : f.lift hg (f.toMap x) = g x := by
  rw [lift_spec, ← g.map_mul]; exact f.eq_of_eq hg (by rw [sec_spec', f.toMap.map_mul])

Lift of Localization Map Evaluates as Original Homomorphism: $f.lift\ hg \circ f = g$

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $x \in M$, the induced homomorphism $f.lift\ hg$ satisfies: \[ f.lift\ hg\ (f(x)) = g(x) \]

Submonoid.LocalizationMap.lift_eq_iff theorem

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

Full source

@[to_additive]
theorem lift_eq_iff {x y : M × S} :
    f.lift hg (f.mk' x.1 x.2) = f.lift hg (f.mk' y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2) := by
  rw [lift_mk', lift_mk', mul_inv hg]

Equivalence of Fraction Equality under Localization Lift: $\text{lift}(f(x_1)/f(y_1)) = \text{lift}(f(x_2)/f(y_2)) \leftrightarrow g(x_1y_2) = g(x_2y_1)$

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $(x_1, y_1), (x_2, y_2) \in M \times S$, the induced homomorphism $\text{lift}(f, g) \colon N \to P$ satisfies \[ \text{lift}(f, g)(f(x_1) \cdot (f(y_1))^{-1}) = \text{lift}(f, g)(f(x_2) \cdot (f(y_2))^{-1}) \quad \leftrightarrow \quad g(x_1 \cdot y_2) = g(x_2 \cdot y_1). \]

Submonoid.LocalizationMap.lift_comp theorem

: (f.lift hg).comp f.toMap = g

Full source

@[to_additive (attr := simp)]
theorem lift_comp : (f.lift hg).comp f.toMap = g := by ext; exact f.lift_eq hg _

Composition of Localization Lift with Original Map Equals Given Homomorphism: $(f.lift\ hg) \circ f = g$

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, the composition of the induced homomorphism $f.lift\ hg \colon N \to P$ with $f$ equals $g$, i.e., \[ (f.lift\ hg) \circ f = g. \]

Submonoid.LocalizationMap.lift_of_comp theorem

(j : N →* P) : f.lift (f.isUnit_comp j) = j

Full source

@[to_additive (attr := simp)]
theorem lift_of_comp (j : N →* P) : f.lift (f.isUnit_comp j) = j := by
  ext
  simp_rw [lift_spec, MonoidHom.comp_apply, ← j.map_mul, sec_spec']

Uniqueness of the Induced Homomorphism from Localization: $\mathrm{lift}(f, hg) = j$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map at $S$. For any monoid homomorphism $j \colon N \to P$, the induced homomorphism $\mathrm{lift}(f, hg)$ (where $hg$ is the proof that $j \circ f$ maps elements of $S$ to units in $P$) is equal to $j$.

Submonoid.LocalizationMap.epic_of_localizationMap theorem

{j k : N →* P} (h : ∀ a, j.comp f.toMap a = k.comp f.toMap a) : j = k

Full source

@[to_additive]
theorem epic_of_localizationMap {j k : N →* P} (h : ∀ a, j.comp f.toMap a = k.comp f.toMap a) :
    j = k := by
  rw [← f.lift_of_comp j, ← f.lift_of_comp k]
  congr 1 with x; exact h x

Epic Property of Localization Maps: $j \circ f = k \circ f$ implies $j = k$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map at $S$. For any two monoid homomorphisms $j, k \colon N \to P$, if $j \circ f = k \circ f$ (i.e., $j(f(a)) = k(f(a))$ for all $a \in M$), then $j = k$.

Submonoid.LocalizationMap.lift_unique theorem

{j : N →* P} (hj : ∀ x, j (f.toMap x) = g x) : f.lift hg = j

Full source

@[to_additive]
theorem lift_unique {j : N →* P} (hj : ∀ x, j (f.toMap x) = g x) : f.lift hg = j := by
  ext
  rw [lift_spec, ← hj, ← hj, ← j.map_mul]
  apply congr_arg
  rw [← sec_spec']

Uniqueness of the Lift from Localization: $f.lift\ hg = j$ when $j \circ f = g$

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, and a monoid homomorphism $j \colon N \to P$ satisfying $j(f(x)) = g(x)$ for all $x \in M$, then the induced homomorphism $f.lift\ hg$ equals $j$.

Submonoid.LocalizationMap.lift_id theorem

(x) : f.lift f.map_units x = x

Full source

@[to_additive (attr := simp)]
theorem lift_id (x) : f.lift f.map_units x = x :=
  DFunLike.ext_iff.1 (f.lift_of_comp <| MonoidHom.id N) x

Identity Property of the Induced Homomorphism from Localization: $\mathrm{lift}(f, f.\mathrm{map\_units}) = \mathrm{id}_N$

Informal description

For any localization map $f \colon M \to N$ of a commutative monoid $M$ at a submonoid $S$, the induced homomorphism $\mathrm{lift}(f, f.\mathrm{map\_units})$ is the identity map on $N$, i.e., $\mathrm{lift}(f, f.\mathrm{map\_units})(x) = x$ for all $x \in N$.

Submonoid.LocalizationMap.lift_comp_lift theorem

 {T : Submonoid M} (hST : S ≤ T) {Q : Type*} [CommMonoid Q] (k : LocalizationMap T Q) {A : Type*} [CommMonoid A]
  {l : M →* A} (hl : ∀ w : T, IsUnit (l w)) :
  (k.lift hl).comp (f.lift (map_units k ⟨_, hST ·.2⟩)) = f.lift (hl ⟨_, hST ·.2⟩)

Full source

/-- Given Localization maps `f : M →* N` for a Submonoid `S ⊆ M` and
`k : M →* Q` for a Submonoid `T ⊆ M`, such that `S ≤ T`, and we have
`l : M →* A`, the composition of the induced map `f.lift` for `k` with
the induced map `k.lift` for `l` is equal to the induced map `f.lift` for `l`. -/
@[to_additive
    "Given Localization maps `f : M →+ N` for a Submonoid `S ⊆ M` and
`k : M →+ Q` for a Submonoid `T ⊆ M`, such that `S ≤ T`, and we have
`l : M →+ A`, the composition of the induced map `f.lift` for `k` with
the induced map `k.lift` for `l` is equal to the induced map `f.lift` for `l`"]
theorem lift_comp_lift {T : Submonoid M} (hST : S ≤ T) {Q : Type*} [CommMonoid Q]
    (k : LocalizationMap T Q) {A : Type*} [CommMonoid A] {l : M →* A}
    (hl : ∀ w : T, IsUnit (l w)) :
    (k.lift hl).comp (f.lift (map_units k ⟨_, hST ·.2⟩)) =
    f.lift (hl ⟨_, hST ·.2⟩) := .symm <|
  lift_unique _ _ fun x ↦ by rw [← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]

Composition of Localization Lifts Commutes: $(k.\mathrm{lift}\, hl) \circ (f.\mathrm{lift}\, k.\mathrm{map\_units}) = f.\mathrm{lift}\, hl$

Informal description

Let $M$ be a commutative monoid with submonoids $S \subseteq T \subseteq M$, and let $f \colon M \to N$ and $k \colon M \to Q$ be localization maps for $S$ and $T$ respectively. Given a commutative monoid $A$ and a monoid homomorphism $l \colon M \to A$ such that $l(w)$ is a unit in $A$ for every $w \in T$, the composition of the induced homomorphism $k.\mathrm{lift}(hl)$ with the induced homomorphism $f.\mathrm{lift}(k.\mathrm{map\_units})$ equals the induced homomorphism $f.\mathrm{lift}(hl)$. In other words, the following diagram commutes: \[ \begin{tikzcd} M \arrow[r, "f"] \arrow[d, "k"] & N \arrow[d, "f.\mathrm{lift}(k.\mathrm{map\_units})"] \\ Q \arrow[r, "k.\mathrm{lift}(hl)"] & A \end{tikzcd} \] where $hl$ denotes the condition that $l(w)$ is a unit for all $w \in T$.

Submonoid.LocalizationMap.lift_comp_lift_eq theorem

 {Q : Type*} [CommMonoid Q] (k : LocalizationMap S Q) {A : Type*} [CommMonoid A] {l : M →* A}
  (hl : ∀ w : S, IsUnit (l w)) : (k.lift hl).comp (f.lift k.map_units) = f.lift hl

Full source

@[to_additive]
theorem lift_comp_lift_eq {Q : Type*} [CommMonoid Q] (k : LocalizationMap S Q)
    {A : Type*} [CommMonoid A] {l : M →* A} (hl : ∀ w : S, IsUnit (l w)) :
    (k.lift hl).comp (f.lift k.map_units) = f.lift hl :=
  lift_comp_lift f le_rfl k hl

Commutativity of Localization Lifts: $(k.\mathrm{lift}\, hl) \circ (f.\mathrm{lift}\, k.\mathrm{map\_units}) = f.\mathrm{lift}\, hl$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ and $k \colon M \to Q$ be localization maps for $S$. Given a commutative monoid $A$ and a monoid homomorphism $l \colon M \to A$ such that $l(w)$ is a unit in $A$ for every $w \in S$, the composition of the induced homomorphism $k.\mathrm{lift}(hl)$ with the induced homomorphism $f.\mathrm{lift}(k.\mathrm{map\_units})$ equals the induced homomorphism $f.\mathrm{lift}(hl)$. In other words, the following diagram commutes: \[ \begin{tikzcd} M \arrow[r, "f"] \arrow[d, "k"] & N \arrow[d, "f.\mathrm{lift}(k.\mathrm{map\_units})"] \\ Q \arrow[r, "k.\mathrm{lift}(hl)"] & A \end{tikzcd} \] where $hl$ denotes the condition that $l(w)$ is a unit for all $w \in S$.

Submonoid.LocalizationMap.lift_left_inverse theorem

{k : LocalizationMap S P} (z : N) : k.lift f.map_units (f.lift k.map_units z) = z

Full source

/-- Given two Localization maps `f : M →* N, k : M →* P` for a Submonoid `S ⊆ M`, the hom
from `P` to `N` induced by `f` is left inverse to the hom from `N` to `P` induced by `k`. -/
@[to_additive (attr := simp)
    "Given two Localization maps `f : M →+ N, k : M →+ P` for a Submonoid `S ⊆ M`, the hom
from `P` to `N` induced by `f` is left inverse to the hom from `N` to `P` induced by `k`."]
theorem lift_left_inverse {k : LocalizationMap S P} (z : N) :
    k.lift f.map_units (f.lift k.map_units z) = z :=
  (DFunLike.congr_fun (lift_comp_lift_eq f k f.map_units) z).trans (lift_id f z)

Left Inverse Property of Localization-Induced Homomorphisms: $k.\mathrm{lift}(f.\mathrm{map\_units}) \circ f.\mathrm{lift}(k.\mathrm{map\_units}) = \mathrm{id}_N$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ and $k \colon M \to P$ be localization maps for $S$. Then for any $z \in N$, the composition of the induced homomorphisms satisfies \[ k.\mathrm{lift}(f.\mathrm{map\_units}) \left( f.\mathrm{lift}(k.\mathrm{map\_units})(z) \right) = z. \] In other words, the homomorphism induced by $f$ is a left inverse to the homomorphism induced by $k$.

Submonoid.LocalizationMap.lift_surjective_iff theorem

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

Full source

@[to_additive]
theorem lift_surjective_iff :
    Function.SurjectiveFunction.Surjective (f.lift hg) ↔ ∀ v : P, ∃ x : M × S, v * g x.2 = g x.1 := by
  constructor
  · intro H v
    obtain ⟨z, hz⟩ := H v
    obtain ⟨x, hx⟩ := f.surj z
    use x
    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
  · intro H v
    obtain ⟨x, hx⟩ := H v
    use f.mk' x.1 x.2
    rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

Surjectivity Criterion for Induced Homomorphism on Localization: $\text{lift}(f, g)$ is surjective iff $v \cdot g(y) = g(x)$ for some $(x, y) \in M \times S$

Informal description

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

Submonoid.LocalizationMap.lift_injective_iff theorem

: Function.Injective (f.lift hg) ↔ ∀ x y, f.toMap x = f.toMap y ↔ g x = g y

Full source

@[to_additive]
theorem lift_injective_iff :
    Function.InjectiveFunction.Injective (f.lift hg) ↔ ∀ x y, f.toMap x = f.toMap y ↔ g x = g y := by
  constructor
  · intro H x y
    constructor
    · exact f.eq_of_eq hg
    · intro h
      rw [← f.lift_eq hg, ← f.lift_eq hg] at h
      exact H h
  · intro H z w h
    obtain ⟨_, _⟩ := f.surj z
    obtain ⟨_, _⟩ := f.surj w
    rw [← f.mk'_sec z, ← f.mk'_sec w]
    exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

Injectivity Criterion for Localization Lift: $f.lift\ hg$ injective $\leftrightarrow$ ($f(x)=f(y) \leftrightarrow g(x)=g(y)$)

Informal description

Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Given a monoid homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, the induced homomorphism $f.lift\ hg \colon N \to P$ is injective if and only if for all $x, y \in M$, the equality $f(x) = f(y)$ holds if and only if $g(x) = g(y)$.

Submonoid.LocalizationMap.map definition

: N →* Q

Full source

/-- Given a `CommMonoid` homomorphism `g : M →* P` where for Submonoids `S ⊆ M, T ⊆ P` we have
`g(S) ⊆ T`, the induced Monoid homomorphism from the Localization of `M` at `S` to the
Localization of `P` at `T`: if `f : M →* N` and `k : P →* Q` are Localization maps for `S` and
`T` respectively, we send `z : N` to `k (g x) * (k (g y))⁻¹`, where `(x, y) : M × S` are such
that `z = f x * (f y)⁻¹`. -/
@[to_additive
    "Given an `AddCommMonoid` homomorphism `g : M →+ P` where for Submonoids `S ⊆ M, T ⊆ P` we have
`g(S) ⊆ T`, the induced AddMonoid homomorphism from the Localization of `M` at `S` to the
Localization of `P` at `T`: if `f : M →+ N` and `k : P →+ Q` are Localization maps for `S` and
`T` respectively, we send `z : N` to `k (g x) - k (g y)`, where `(x, y) : M × S` are such
that `z = f x - f y`."]
noncomputable def map : N →* Q :=
  @lift _ _ _ _ _ _ _ f (k.toMap.comp g) fun y ↦ k.map_units ⟨g y, hy y⟩

Induced homomorphism between localizations

Informal description

Given a commutative monoid $M$ with a submonoid $S$, a localization map $f \colon M \to N$ for $S$, a commutative monoid $P$ with a submonoid $T$, a localization map $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, the induced homomorphism $\text{map} \colon N \to Q$ is defined by sending $z \in N$ to $k(g(x)) \cdot (k(g(y)))^{-1}$, where $(x, y) \in M \times S$ is any pair such that $z = f(x) \cdot (f(y))^{-1}$.

Submonoid.LocalizationMap.map_eq theorem

(x) : f.map hy k (f.toMap x) = k.toMap (g x)

Full source

@[to_additive (attr := simp)]
theorem map_eq (x) : f.map hy k (f.toMap x) = k.toMap (g x) :=
  f.lift_eq (fun y ↦ k.map_units ⟨g y, hy y⟩) x

Localization Homomorphism Evaluation: $\text{map}(f(x)) = k(g(x))$

Informal description

Let $M$ and $N$ be commutative monoids with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. Given commutative monoids $P$ and $Q$ with a submonoid $T \subseteq P$, a localization map $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, then for any $x \in M$, the induced homomorphism $\text{map} \colon N \to Q$ satisfies: \[ \text{map}(f(x)) = k(g(x)) \]

Submonoid.LocalizationMap.map_comp theorem

: (f.map hy k).comp f.toMap = k.toMap.comp g

Full source

@[to_additive (attr := simp)]
theorem map_comp : (f.map hy k).comp f.toMap = k.toMap.comp g :=
  f.lift_comp fun y ↦ k.map_units ⟨g y, hy y⟩

Composition of Localization Maps: $(f.map\ hy\ k) \circ f = k \circ g$

Informal description

Given commutative monoids $M$ and $N$ with a submonoid $S \subseteq M$, a localization map $f \colon M \to N$ for $S$, commutative monoids $P$ and $Q$ with a submonoid $T \subseteq P$, a localization map $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, the composition of the induced homomorphism $f.map\ hy\ k \colon N \to Q$ with $f$ equals the composition of $k$ with $g$, i.e., \[ (f.map\ hy\ k) \circ f = k \circ g. \]

Submonoid.LocalizationMap.map_mk' theorem

(x) (y : S) : f.map hy k (f.mk' x y) = k.mk' (g x) ⟨g y, hy y⟩

Full source

@[to_additive (attr := simp)]
theorem map_mk' (x) (y : S) : f.map hy k (f.mk' x y) = k.mk' (g x) ⟨g y, hy y⟩ := by
  rw [map, lift_mk', mul_inv_left]
  show k.toMap (g x) = k.toMap (g y) * _
  rw [mul_mk'_eq_mk'_of_mul]
  exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm

Localization Homomorphism Preserves Fraction Representation: $\text{map}(f(x)/f(y)) = k(g(x))/k(g(y))$

Informal description

Let $M$ and $N$ be commutative monoids with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. Given commutative monoids $P$ and $Q$ with a submonoid $T \subseteq P$, a localization map $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, then for any $x \in M$ and $y \in S$, the induced homomorphism $\text{map} \colon N \to Q$ satisfies: \[ \text{map}(f(x) \cdot (f(y))^{-1}) = k(g(x)) \cdot (k(g(y)))^{-1}. \]

Submonoid.LocalizationMap.map_spec theorem

(z u) : f.map hy k z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g (f.sec z).2) * u

Full source

/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
`u : Q`, we have `f.map hy k z = u ↔ k (g x) = k (g y) * u` where `x : M, y ∈ S` are such that
`z * f y = f x`. -/
@[to_additive
    "Given Localization maps `f : M →+ N, k : P →+ Q` for Submonoids `S, T` respectively, if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
`u : Q`, we have `f.map hy k z = u ↔ k (g x) = k (g y) + u` where `x : M, y ∈ S` are such that
`z + f y = f x`."]
theorem map_spec (z u) : f.map hy k z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g (f.sec z).2) * u :=
  f.lift_spec (fun y ↦ k.map_units ⟨g y, hy y⟩) _ _

Characterization of the induced localization map via section elements

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively. Given localization maps $f \colon M \to N$ for $S$ and $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, then for any $z \in N$ and $u \in Q$, the induced map $f.map\ hy\ k$ satisfies: \[ f.map\ hy\ k\ z = u \quad \leftrightarrow \quad k(g(x)) = k(g(y)) \cdot u \] where $(x, y) = f.sec\ z$ is the section of $z$ under $f$.

Submonoid.LocalizationMap.map_mul_right theorem

(z) : f.map hy k z * k.toMap (g (f.sec z).2) = k.toMap (g (f.sec z).1)

Full source

/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
we have `f.map hy k z * k (g y) = k (g x)` where `x : M, y ∈ S` are such that
`z * f y = f x`. -/
@[to_additive
    "Given Localization maps `f : M →+ N, k : P →+ Q` for Submonoids `S, T` respectively, if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
we have `f.map hy k z + k (g y) = k (g x)` where `x : M, y ∈ S` are such that
`z + f y = f x`."]
theorem map_mul_right (z) : f.map hy k z * k.toMap (g (f.sec z).2) = k.toMap (g (f.sec z).1) :=
  f.lift_mul_right (fun y ↦ k.map_units ⟨g y, hy y⟩) _

Right multiplication property of induced localization maps: $f.map\,hy\,k\,z \cdot k(g(y)) = k(g(x))$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively. Given localization maps $f \colon M \to N$ for $S$ and $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, then for any $z \in N$, the induced map $f.map\,hy\,k$ satisfies: \[ f.map\,hy\,k\,z \cdot k(g(y)) = k(g(x)), \] where $(x, y) = f.sec\,z$ is the section of $z$ under $f$ (i.e., $x \in M$ and $y \in S$ satisfy $z \cdot f(y) = f(x)$).

Submonoid.LocalizationMap.map_mul_left theorem

(z) : k.toMap (g (f.sec z).2) * f.map hy k z = k.toMap (g (f.sec z).1)

Full source

/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
we have `k (g y) * f.map hy k z = k (g x)` where `x : M, y ∈ S` are such that
`z * f y = f x`. -/
@[to_additive
    "Given Localization maps `f : M →+ N, k : P →+ Q` for Submonoids `S, T` respectively if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
we have `k (g y) + f.map hy k z = k (g x)` where `x : M, y ∈ S` are such that
`z + f y = f x`."]
theorem map_mul_left (z) : k.toMap (g (f.sec z).2) * f.map hy k z = k.toMap (g (f.sec z).1) := by
  rw [mul_comm, f.map_mul_right]

Left multiplication property of induced localization maps: $k(g(y)) \cdot f.\text{map}\,hy\,k\,z = k(g(x))$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively. Given localization maps $f \colon M \to N$ for $S$ and $k \colon P \to Q$ for $T$, and a monoid homomorphism $g \colon M \to P$ such that $g(S) \subseteq T$, then for any $z \in N$, the induced map $f.\text{map}\,hy\,k$ satisfies: \[ k(g(y)) \cdot f.\text{map}\,hy\,k\,z = k(g(x)), \] where $(x, y) = f.\text{sec}\,z$ is the section of $z$ under $f$ (i.e., $x \in M$ and $y \in S$ satisfy $z \cdot f(y) = f(x)$).

Submonoid.LocalizationMap.map_id theorem

(z : N) : f.map (fun y ↦ show MonoidHom.id M y ∈ S from y.2) f z = z

Full source

@[to_additive (attr := simp)]
theorem map_id (z : N) : f.map (fun y ↦ show MonoidHom.idMonoidHom.id M y ∈ S from y.2) f z = z :=
  f.lift_id z

Identity Property of Induced Localization Map: $f.\mathrm{map}\,(\lambda y, y.2)\,f = \mathrm{id}_N$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Then the induced homomorphism $f.\mathrm{map}$ obtained by taking $g = \mathrm{id}_M$ and $k = f$ is the identity map on $N$, i.e., for all $z \in N$, we have $f.\mathrm{map}\,(\lambda y, y.2)\,f\,z = z$.

Submonoid.LocalizationMap.map_comp_map theorem

 {A : Type*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R] (j : LocalizationMap U R) {l : P →* A}
  (hl : ∀ w : T, l w ∈ U) : (k.map hl j).comp (f.map hy k) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j

Full source

/-- If `CommMonoid` homs `g : M →* P, l : P →* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
@[to_additive
    "If `AddCommMonoid` homs `g : M →+ 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*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R]
    (j : LocalizationMap U R) {l : P →* A} (hl : ∀ w : T, l w ∈ U) :
    (k.map hl j).comp (f.map hy k) =
    f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j := by
  ext z
  show j.toMap _ * _ = j.toMap (l _) * _
  rw [mul_inv_left, ← mul_assoc, mul_inv_right]
  show j.toMap _ * j.toMap (l (g _)) = j.toMap (l _) * _
  rw [← j.toMap.map_mul, ← j.toMap.map_mul, ← l.map_mul, ← l.map_mul]
  exact
    k.comp_eq_of_eq hl j
      (by rw [k.toMap.map_mul, k.toMap.map_mul, sec_spec', mul_assoc, map_mul_right])

Composition of Induced Localization Maps Equals Induced Map of Composition

Informal description

Let $M$, $P$, and $A$ be commutative monoids with submonoids $S \subseteq M$, $T \subseteq P$, and $U \subseteq A$ respectively. Given localization maps $f \colon M \to N$ for $S$, $k \colon P \to Q$ for $T$, and $j \colon A \to R$ for $U$, and monoid homomorphisms $g \colon M \to P$ and $l \colon P \to A$ such that $g(S) \subseteq T$ and $l(T) \subseteq U$, the composition of the induced maps $(k.map\,hl\,j) \circ (f.map\,hy\,k)$ equals the map $f.map\,(\lambda x, hl \langle g x, hy x \rangle)\,j$ induced by the composition $l \circ g \colon M \to A$.

Submonoid.LocalizationMap.map_map theorem

 {A : Type*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R] (j : LocalizationMap U R) {l : P →* A}
  (hl : ∀ w : T, l w ∈ U) (x) : k.map hl j (f.map hy k x) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j x

Full source

/-- If `CommMonoid` homs `g : M →* P, l : P →* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`. -/
@[to_additive
    "If `AddCommMonoid` homs `g : M →+ 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*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R]
    (j : LocalizationMap U R) {l : P →* A} (hl : ∀ w : T, l w ∈ U) (x) :
    k.map hl j (f.map hy k x) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j x := by
  -- Porting note: need to specify `k` explicitly
  rw [← f.map_comp_map (k := k) hy j hl]
  simp only [MonoidHom.coe_comp, comp_apply]

Compatibility of Induced Localization Maps with Composition

Informal description

Let $M$, $P$, and $A$ be commutative monoids with submonoids $S \subseteq M$, $T \subseteq P$, and $U \subseteq A$ respectively. Given localization maps $f \colon M \to N$ for $S$, $k \colon P \to Q$ for $T$, and $j \colon A \to R$ for $U$, and monoid homomorphisms $g \colon M \to P$ and $l \colon P \to A$ such that $g(S) \subseteq T$ and $l(T) \subseteq U$, then for any $x \in N$, the following equality holds: \[ k.\text{map}(hl, j)(f.\text{map}(hy, k)(x)) = f.\text{map}(\lambda x, hl \langle g x, hy x \rangle, j)(x). \]

Submonoid.LocalizationMap.map_injective_of_injective theorem

(hg : Injective g) (k : LocalizationMap (S.map g) Q) : Injective (map f (apply_coe_mem_map g S) k)

Full source

/-- Given an injective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
the induced monoid homomorphism from the localization of `M` at `S` to the
localization of `P` at `g S`, is injective.
-/
@[to_additive "Given an injective `AddCommMonoid` homomorphism `g : M →+ P`, and a
submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
to the localization of `P` at `g S`, is injective. "]
theorem map_injective_of_injective (hg : Injective g) (k : LocalizationMap (S.map g) Q) :
    Injective (map f (apply_coe_mem_map g S) k) := fun z w hizw ↦ by
  set i := map f (apply_coe_mem_map g S) k
  have ifkg (a : M) : i (f.toMap a) = k.toMap (g a) := map_eq f (apply_coe_mem_map g S) a
  let ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w
  have : k.toMap (g z') = k.toMap (g w') := by
    rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
  obtain ⟨⟨_, c, hc, rfl⟩, eq⟩ := k.exists_of_eq _ _ this
  simp_rw [← map_mul, hg.eq_iff] at eq
  rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]
  exact ⟨⟨c, hc⟩, eq⟩

Injectivity of Induced Localization Homomorphism from Injective Base Homomorphism

Informal description

Let $M$ and $P$ be commutative monoids, $S$ a submonoid of $M$, and $g \colon M \to P$ an injective monoid homomorphism. Let $f \colon M \to N$ be a localization map for $S$ and $k \colon P \to Q$ a localization map for the image submonoid $g(S)$. Then the induced homomorphism $\text{map} \colon N \to Q$ is injective.

Submonoid.LocalizationMap.map_surjective_of_surjective theorem

(hg : Surjective g) (k : LocalizationMap (S.map g) Q) : Surjective (map f (apply_coe_mem_map g S) k)

Full source

/-- Given a surjective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
the induced monoid homomorphism from the localization of `M` at `S` to the
localization of `P` at `g S`, is surjective.
-/
@[to_additive "Given a surjective `AddCommMonoid` homomorphism `g : M →+ P`, and a
submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
to the localization of `P` at `g S`, is surjective. "]
theorem map_surjective_of_surjective (hg : Surjective g) (k : LocalizationMap (S.map g) Q) :
    Surjective (map f (apply_coe_mem_map g S) k) := fun z ↦ by
  obtain ⟨y, ⟨y', s, hs, rfl⟩, rfl⟩ := k.mk'_surjective z
  obtain ⟨x, rfl⟩ := hg y
  use f.mk' x ⟨s, hs⟩
  rw [map_mk']

Surjectivity of Localization Homomorphism Induced by Surjective Base Homomorphism

Informal description

Let $M$ and $P$ be commutative monoids, $S$ a submonoid of $M$, and $g \colon M \to P$ a surjective monoid homomorphism. Let $f \colon M \to N$ be a localization map for $S$ and $k \colon P \to Q$ a localization map for the image submonoid $g(S)$. Then the induced homomorphism $\text{map} \colon N \to Q$ is surjective.

Submonoid.LocalizationMap.mulEquivOfLocalizations definition

(k : LocalizationMap S P) : N ≃* P

Full source

/-- If `f : M →* N` and `k : M →* P` are Localization maps for a Submonoid `S`, we get an
isomorphism of `N` and `P`. -/
@[to_additive
    "If `f : M →+ N` and `k : M →+ R` are Localization maps for an AddSubmonoid `S`, we get an
isomorphism of `N` and `R`."]
noncomputable def mulEquivOfLocalizations (k : LocalizationMap S P) : N ≃* P :=
{ toFun := f.lift k.map_units
  invFun := k.lift f.map_units
  left_inv := f.lift_left_inverse
  right_inv := k.lift_left_inverse
  map_mul' := MonoidHom.map_mul _ }

Isomorphism between localizations of a commutative monoid

Informal description

Given two localization maps $ f \colon M \to N $ and $ k \colon M \to P $ for a commutative monoid $ M $ at a submonoid $ S $, the function `mulEquivOfLocalizations` defines a multiplicative isomorphism $ N \simeq^* P $ between the localizations $ N $ and $ P $. This isomorphism is constructed by lifting the localization maps $ f $ and $ k $ to each other's codomains, ensuring that the resulting maps are mutual inverses and preserve multiplication.

Submonoid.LocalizationMap.mulEquivOfLocalizations_apply theorem

{k : LocalizationMap S P} {x} : f.mulEquivOfLocalizations k x = f.lift k.map_units x

Full source

@[to_additive (attr := simp)]
theorem mulEquivOfLocalizations_apply {k : LocalizationMap S P} {x} :
    f.mulEquivOfLocalizations k x = f.lift k.map_units x := rfl

Application of Localization Isomorphism via Lifting

Informal description

Given two localization maps $ f \colon M \to N $ and $ k \colon M \to P $ for a commutative monoid $ M $ at a submonoid $ S $, the multiplicative isomorphism $ \varphi \colon N \simeq^* P $ defined by `mulEquivOfLocalizations` satisfies $ \varphi(x) = \text{lift}_f(k)(x) $ for all $ x \in N $, where $ \text{lift}_f(k) $ is the homomorphism induced by $ k $ via the universal property of localization.

Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_apply theorem

{k : LocalizationMap S P} {x} : (f.mulEquivOfLocalizations k).symm x = k.lift f.map_units x

Full source

@[to_additive (attr := simp)]
theorem mulEquivOfLocalizations_symm_apply {k : LocalizationMap S P} {x} :
    (f.mulEquivOfLocalizations k).symm x = k.lift f.map_units x := rfl

Inverse of Localization Isomorphism via Lifting

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given two localization maps $f \colon M \to N$ and $k \colon M \to P$ for $M$ at $S$, the inverse of the multiplicative isomorphism $\varphi \colon N \simeq^* P$ induced by these localizations satisfies $\varphi^{-1}(x) = k.\text{lift}(f.\text{map\_units})(x)$ for all $x \in P$. Here, $k.\text{lift}(f.\text{map\_units})$ denotes the homomorphism from $P$ to $N$ induced by the universal property of the localization $k$.

Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations theorem

{k : LocalizationMap S P} : (k.mulEquivOfLocalizations f).symm = f.mulEquivOfLocalizations k

Full source

@[to_additive]
theorem mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations {k : LocalizationMap S P} :
    (k.mulEquivOfLocalizations f).symm = f.mulEquivOfLocalizations k := rfl

Inverse of Localization Isomorphism Equals Swapped Isomorphism

Informal description

Given two localization maps $f \colon M \to N$ and $k \colon M \to P$ for a commutative monoid $M$ at a submonoid $S$, the inverse of the multiplicative isomorphism $k.\text{mulEquivOfLocalizations}\ f$ is equal to $f.\text{mulEquivOfLocalizations}\ k$.

Submonoid.LocalizationMap.ofMulEquivOfLocalizations definition

(k : N ≃* P) : LocalizationMap S P

Full source

/-- If `f : M →* N` is a Localization map for a Submonoid `S` and `k : N ≃* P` is an isomorphism
of `CommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`. -/
@[to_additive
    "If `f : M →+ N` is a Localization map for a Submonoid `S` and `k : N ≃+ P` is an isomorphism
of `AddCommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`."]
def ofMulEquivOfLocalizations (k : N ≃* P) : LocalizationMap S P :=
  (k.toMonoidHom.comp f.toMap).toLocalizationMap (fun y ↦ isUnit_comp f k.toMonoidHom y)
    (fun v ↦
      let ⟨z, hz⟩ := k.surjective v
      let ⟨x, hx⟩ := f.surj z
      ⟨x, show v * k _ = k _ by rw [← hx, map_mul, ← hz]⟩)
    fun x y ↦ (k.apply_eq_iff_eq.trans f.eq_iff_exists).1

Localization map via composition with multiplicative isomorphism

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, and a multiplicative isomorphism $k \colon N \simeq^* P$, the composition $k \circ f$ is a localization map for $M$ at $S$ with codomain $P$. Specifically, the map $k \circ f$ satisfies the following properties: 1. For every $y \in S$, the image $(k \circ f)(y)$ is a unit in $P$; 2. For every $v \in P$, there exists $(x, y) \in M \times S$ such that $v \cdot (k \circ f)(y) = (k \circ f)(x)$; 3. For any $x, y \in M$ such that $(k \circ f)(x) = (k \circ f)(y)$, there exists $c \in S$ such that $x \cdot c = y \cdot c$. This construction allows the localization to be transported along an isomorphism of codomains.

Submonoid.LocalizationMap.ofMulEquivOfLocalizations_apply theorem

{k : N ≃* P} (x) : (f.ofMulEquivOfLocalizations k).toMap x = k (f.toMap x)

Full source

@[to_additive (attr := simp)]
theorem ofMulEquivOfLocalizations_apply {k : N ≃* P} (x) :
    (f.ofMulEquivOfLocalizations k).toMap x = k (f.toMap x) := rfl

Localization Map Composition with Multiplicative Isomorphism Preserves Evaluation

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given a multiplicative isomorphism $k \colon N \simeq^* P$ and any element $x \in M$, the localization map $(f.\text{ofMulEquivOfLocalizations}\ k)$ evaluated at $x$ equals $k$ applied to $f(x)$. In other words, $(f.\text{ofMulEquivOfLocalizations}\ k)(x) = k(f(x))$.

Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq theorem

{k : N ≃* P} : (f.ofMulEquivOfLocalizations k).toMap = k.toMonoidHom.comp f.toMap

Full source

@[to_additive]
theorem ofMulEquivOfLocalizations_eq {k : N ≃* P} :
    (f.ofMulEquivOfLocalizations k).toMap = k.toMonoidHom.comp f.toMap := rfl

Composition of Localization Map with Multiplicative Isomorphism Equals Homomorphism Composition

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, and a multiplicative isomorphism $k \colon N \simeq^* P$, the underlying homomorphism of the composed localization map $f \circ k$ is equal to the composition of $k$ as a monoid homomorphism with $f$. That is, $(f \circ k).toMap = k.toMonoidHom \circ f.toMap$.

Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply theorem

{k : N ≃* P} (x) : k.symm ((f.ofMulEquivOfLocalizations k).toMap x) = f.toMap x

Full source

@[to_additive]
theorem symm_comp_ofMulEquivOfLocalizations_apply {k : N ≃* P} (x) :
    k.symm ((f.ofMulEquivOfLocalizations k).toMap x) = f.toMap x := k.symm_apply_apply (f.toMap x)

Inverse Isomorphism Recovers Original Localization Map

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$, with $f \colon M \to N$ a localization map for $S$. For any multiplicative isomorphism $k \colon N \simeq^* P$ and any element $x \in M$, the composition of the inverse isomorphism $k^{-1}$ with the localization map $(k \circ f)$ recovers the original localization map, i.e., $$ k^{-1}\big((k \circ f)(x)\big) = f(x). $$

Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply' theorem

{k : P ≃* N} (x) : k ((f.ofMulEquivOfLocalizations k.symm).toMap x) = f.toMap x

Full source

@[to_additive]
theorem symm_comp_ofMulEquivOfLocalizations_apply' {k : P ≃* N} (x) :
    k ((f.ofMulEquivOfLocalizations k.symm).toMap x) = f.toMap x := k.apply_symm_apply (f.toMap x)

Inverse Composition with Localization Map via Multiplicative Isomorphism

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$, with $f \colon M \to N$ a localization map at $S$. For any multiplicative isomorphism $k \colon P \simeq^* N$ and any $x \in M$, we have: \[ k\left((f \circ k^{-1}).toMap(x)\right) = f(x) \] where $(f \circ k^{-1}).toMap$ denotes the underlying homomorphism of the localization map obtained by composing $f$ with the inverse isomorphism $k^{-1}$.

Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq_iff_eq theorem

{k : N ≃* P} {x y} : (f.ofMulEquivOfLocalizations k).toMap x = y ↔ f.toMap x = k.symm y

Full source

@[to_additive]
theorem ofMulEquivOfLocalizations_eq_iff_eq {k : N ≃* P} {x y} :
    (f.ofMulEquivOfLocalizations k).toMap x = y ↔ f.toMap x = k.symm y :=
  k.toEquiv.eq_symm_apply.symm

Equivalence of Localization Maps via Multiplicative Isomorphism

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given a localization map $f \colon M \to N$ for $S$, a multiplicative isomorphism $k \colon N \simeq^* P$, and elements $x \in M$, $y \in P$, the following are equivalent: 1. The image of $x$ under the composed localization map $k \circ f$ equals $y$; 2. The image of $x$ under $f$ equals the image of $y$ under the inverse isomorphism $k^{-1}$. In other words, $(k \circ f)(x) = y$ if and only if $f(x) = k^{-1}(y)$.

Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv theorem

(k : LocalizationMap S P) : f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k

Full source

@[to_additive addEquivOfLocalizations_right_inv]
theorem mulEquivOfLocalizations_right_inv (k : LocalizationMap S P) :
    f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k :=
  toMap_injective <| f.lift_comp k.map_units

Right Inverse Property of Localization Isomorphism: $ f \circ (f \simeq k) = k $

Informal description

Given two localization maps $ f \colon M \to N $ and $ k \colon M \to P $ for a commutative monoid $ M $ at a submonoid $ S $, the composition of the isomorphism $ f.mulEquivOfLocalizations\ k \colon N \simeq^* P $ with the original localization map $ f $ yields the localization map $ k $. In other words, \[ f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations\ k) = k. \]

Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv_apply theorem

{k : LocalizationMap S P} {x} : (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)).toMap x = k.toMap x

Full source

@[to_additive addEquivOfLocalizations_right_inv_apply]
theorem mulEquivOfLocalizations_right_inv_apply {k : LocalizationMap S P} {x} :
    (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)).toMap x = k.toMap x := by simp

Right Inverse Property of Localization Isomorphism

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. Given localization maps $f \colon M \to N$ and $k \colon M \to P$ for $S$, and an element $x \in M$, the image of $x$ under the composition of $f$ with the isomorphism $\text{mulEquivOfLocalizations}\ f\ k$ equals its image under $k$. That is, \[ (f.\text{ofMulEquivOfLocalizations}\ (f.\text{mulEquivOfLocalizations}\ k)).\text{toMap}\ x = k.\text{toMap}\ x \]

Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv theorem

(k : N ≃* P) : f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k

Full source

@[to_additive]
theorem mulEquivOfLocalizations_left_inv (k : N ≃* P) :
    f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k :=
  DFunLike.ext _ _ fun x ↦ DFunLike.ext_iff.1 (f.lift_of_comp k.toMonoidHom) x

Inverse Property of Localization Isomorphism Construction

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, and a multiplicative isomorphism $k \colon N \simeq^* P$, the composition of the isomorphism $\mathrm{mulEquivOfLocalizations}$ with the localization map $\mathrm{ofMulEquivOfLocalizations}$ yields back the original isomorphism $k$. That is, $\mathrm{mulEquivOfLocalizations}(f, \mathrm{ofMulEquivOfLocalizations}(f, k)) = k$.

Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv_apply theorem

{k : N ≃* P} (x) : f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) x = k x

Full source

@[to_additive]
theorem mulEquivOfLocalizations_left_inv_apply {k : N ≃* P} (x) :
    f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) x = k x := by simp

Inverse Property of Localization-Induced Isomorphism: $(\mathrm{mulEquivOfLocalizations} \circ \mathrm{ofMulEquivOfLocalizations})(k)(x) = k(x)$

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map at $S$. For any multiplicative isomorphism $k \colon N \simeq^* P$ and any element $x \in N$, the composition of the isomorphism induced by localization with its inverse evaluation at $x$ satisfies: $$f.\mathrm{mulEquivOfLocalizations}(f.\mathrm{ofMulEquivOfLocalizations}(k))(x) = k(x)$$

Submonoid.LocalizationMap.ofMulEquivOfLocalizations_id theorem

: f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

Full source

@[to_additive (attr := simp)]
theorem ofMulEquivOfLocalizations_id : f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f := by
  ext; rfl

Localization Map Invariance under Identity Isomorphism

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, the composition of $f$ with the identity multiplicative isomorphism $\mathrm{id}_N \colon N \simeq^* N$ yields $f$ itself. That is, $f \circ \mathrm{id}_N = f$.

Submonoid.LocalizationMap.ofMulEquivOfLocalizations_comp theorem

 {k : N ≃* P} {j : P ≃* Q} :
  (f.ofMulEquivOfLocalizations (k.trans j)).toMap = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap

Full source

@[to_additive]
theorem ofMulEquivOfLocalizations_comp {k : N ≃* P} {j : P ≃* Q} :
    (f.ofMulEquivOfLocalizations (k.trans j)).toMap =
      j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap := by
  ext; rfl

Composition Property of Localization Maps via Multiplicative Isomorphisms

Informal description

Let $M$ be a commutative monoid with a submonoid $S$, and let $f \colon M \to N$ be a localization map for $S$. Given multiplicative isomorphisms $k \colon N \simeq^* P$ and $j \colon P \simeq^* Q$, the composition of localization maps satisfies: $$(f \circ (k \circ j)) = j \circ (f \circ k)$$ where $f \circ (k \circ j)$ denotes the localization map obtained by first composing $f$ with the isomorphism $k \circ j \colon N \simeq^* Q$, and $j \circ (f \circ k)$ denotes the composition of the localization map $f \circ k$ with the isomorphism $j$.

Submonoid.LocalizationMap.ofMulEquivOfDom definition

{k : P ≃* M} (H : T.map k.toMonoidHom = S) : LocalizationMap T N

Full source

/-- Given `CommMonoid`s `M, P` and Submonoids `S ⊆ M, T ⊆ P`, if `f : M →* N` is a Localization
map for `S` and `k : P ≃* M` is an isomorphism of `CommMonoid`s such that `k(T) = S`, `f ∘ k`
is a Localization map for `T`. -/
@[to_additive
    "Given `AddCommMonoid`s `M, P` and `AddSubmonoid`s `S ⊆ M, T ⊆ P`, if `f : M →* N` is a
    Localization map for `S` and `k : P ≃+ M` is an isomorphism of `AddCommMonoid`s such that
    `k(T) = S`, `f ∘ k` is a Localization map for `T`."]
def ofMulEquivOfDom {k : P ≃* M} (H : T.map k.toMonoidHom = S) : LocalizationMap T N :=
  let H' : S.comap k.toMonoidHom = T :=
    H ▸ (SetLike.coe_injective <| T.1.1.preimage_image_eq k.toEquiv.injective)
  (f.toMap.comp k.toMonoidHom).toLocalizationMap
    (fun y ↦
      let ⟨z, hz⟩ := f.map_units ⟨k y, H ▸ Set.mem_image_of_mem k y.2⟩
      ⟨z, hz⟩)
    (fun z ↦
      let ⟨x, hx⟩ := f.surj z
      let ⟨v, hv⟩ := k.surjective x.1
      let ⟨w, hw⟩ := k.surjective x.2
      ⟨(v, ⟨w, H' ▸ show k w ∈ S from hw.symm ▸ x.2.2⟩), by
        simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, hw, hx]⟩)
    fun x y ↦ by
      rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
        MonoidHom.coe_coe, f.eq_iff_exists]
      rintro ⟨c, hc⟩
      let ⟨d, hd⟩ := k.surjective c
      refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
      rw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.injective hc

Localization map induced by a multiplicative isomorphism of domains

Informal description

Given commutative monoids $M$, $P$ and submonoids $S \subseteq M$, $T \subseteq P$, if $f \colon M \to N$ is a localization map for $S$ and $k \colon P \simeq^* M$ is a multiplicative isomorphism such that $k(T) = S$, then the composition $f \circ k$ is a localization map for $T$. More precisely, for any multiplicative isomorphism $k \colon P \simeq^* M$ satisfying $k(T) = S$, the map $f \circ k \colon P \to N$ satisfies the characteristic properties of a localization map for $T$: 1. For every $y \in T$, $(f \circ k)(y)$ is a unit in $N$; 2. For every $z \in N$, there exists $(x, y) \in P \times T$ such that $z \cdot (f \circ k)(y) = (f \circ k)(x)$; 3. For any $x, y \in P$ with $(f \circ k)(x) = (f \circ k)(y)$, there exists $c \in T$ such that $x \cdot c = y \cdot c$.

Submonoid.LocalizationMap.ofMulEquivOfDom_apply theorem

{k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) : (f.ofMulEquivOfDom H).toMap x = f.toMap (k x)

Full source

@[to_additive (attr := simp)]
theorem ofMulEquivOfDom_apply {k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) :
    (f.ofMulEquivOfDom H).toMap x = f.toMap (k x) := rfl

Application of Localization Map via Multiplicative Isomorphism

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively. Given a localization map $f \colon M \to N$ for $S$ and a multiplicative isomorphism $k \colon P \simeq^* M$ such that $k(T) = S$, then for any $x \in P$, the localization map $(f \circ k) \colon P \to N$ satisfies $(f \circ k)(x) = f(k(x))$.

Submonoid.LocalizationMap.ofMulEquivOfDom_eq theorem

{k : P ≃* M} (H : T.map k.toMonoidHom = S) : (f.ofMulEquivOfDom H).toMap = f.toMap.comp k.toMonoidHom

Full source

@[to_additive]
theorem ofMulEquivOfDom_eq {k : P ≃* M} (H : T.map k.toMonoidHom = S) :
    (f.ofMulEquivOfDom H).toMap = f.toMap.comp k.toMonoidHom := rfl

Equality of Localization Maps via Domain Isomorphism

Informal description

Given commutative monoids $M$, $P$ with submonoids $S \subseteq M$ and $T \subseteq P$, and a multiplicative isomorphism $k \colon P \simeq^* M$ such that $k(T) = S$, the localization map $f \circ k \colon P \to N$ for $T$ is equal to the composition of the localization map $f \colon M \to N$ for $S$ with the monoid homomorphism $k \colon P \to M$. In other words, $(f \circ k)(x) = f(k(x))$ for all $x \in P$.

Submonoid.LocalizationMap.ofMulEquivOfDom_comp_symm theorem

{k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) : (f.ofMulEquivOfDom H).toMap (k.symm x) = f.toMap x

Full source

@[to_additive]
theorem ofMulEquivOfDom_comp_symm {k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) :
    (f.ofMulEquivOfDom H).toMap (k.symm x) = f.toMap x :=
  congr_arg f.toMap <| k.apply_symm_apply x

Localization Map Composition with Inverse Isomorphism: $(f \circ k)(k^{-1}(x)) = f(x)$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$, and let $f \colon M \to N$ be a localization map for $S$. Given a multiplicative isomorphism $k \colon P \simeq^* M$ such that $k(T) = S$, then for any $x \in M$, the localization map $(f \circ k) \colon P \to N$ satisfies $(f \circ k)(k^{-1}(x)) = f(x)$.

Submonoid.LocalizationMap.ofMulEquivOfDom_comp theorem

{k : M ≃* P} (H : T.map k.symm.toMonoidHom = S) (x) : (f.ofMulEquivOfDom H).toMap (k x) = f.toMap x

Full source

@[to_additive]
theorem ofMulEquivOfDom_comp {k : M ≃* P} (H : T.map k.symm.toMonoidHom = S) (x) :
    (f.ofMulEquivOfDom H).toMap (k x) = f.toMap x := congr_arg f.toMap <| k.symm_apply_apply x

Compatibility of Localization with Multiplicative Isomorphism: $(f \circ k^{-1})(k(x)) = f(x)$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$, and let $f \colon M \to N$ be a localization map for $S$. Given a multiplicative isomorphism $k \colon M \simeq^* P$ such that the image of $S$ under $k^{-1}$ is $T$ (i.e., $T = k^{-1}(S)$), then for any $x \in M$, the localization map $(f \circ k^{-1})$ for $T$ satisfies $(f \circ k^{-1})(k(x)) = f(x)$.

Submonoid.LocalizationMap.ofMulEquivOfDom_id theorem

 :
  f.ofMulEquivOfDom
      (show S.map (MulEquiv.refl M).toMonoidHom = S from
        Submonoid.ext fun x ↦ ⟨fun ⟨_, hy, h⟩ ↦ h ▸ hy, fun h ↦ ⟨x, h, rfl⟩⟩) =
    f

Full source

/-- A special case of `f ∘ id = f`, `f` a Localization map. -/
@[to_additive (attr := simp) "A special case of `f ∘ id = f`, `f` a Localization map."]
theorem ofMulEquivOfDom_id :
    f.ofMulEquivOfDom
        (show S.map (MulEquiv.refl M).toMonoidHom = S from
          Submonoid.ext fun x ↦ ⟨fun ⟨_, hy, h⟩ ↦ h ▸ hy, fun h ↦ ⟨x, h, rfl⟩⟩) = f := by
  ext; rfl

Identity Isomorphism Preserves Localization Map: $f \circ \mathrm{id} = f$

Informal description

Given a localization map $f \colon M \to N$ for a commutative monoid $M$ at a submonoid $S$, the localization map obtained by composing $f$ with the identity multiplicative isomorphism $\mathrm{id} \colon M \simeq^* M$ is equal to $f$ itself. More precisely, if we consider the identity isomorphism $\mathrm{id} \colon M \simeq^* M$ and note that $\mathrm{id}(S) = S$, then the induced localization map $f \circ \mathrm{id}$ is identical to $f$.

Submonoid.LocalizationMap.mulEquivOfMulEquiv definition

(k : LocalizationMap T Q) {j : M ≃* P} (H : S.map j.toMonoidHom = T) : N ≃* Q

Full source

/-- Given Localization maps `f : M →* N, k : P →* U` for Submonoids `S, T` respectively, an
isomorphism `j : M ≃* P` such that `j(S) = T` induces an isomorphism of localizations `N ≃* U`. -/
@[to_additive
    "Given Localization maps `f : M →+ N, k : P →+ U` for Submonoids `S, T` respectively, an
isomorphism `j : M ≃+ P` such that `j(S) = T` induces an isomorphism of localizations `N ≃+ U`."]
noncomputable def mulEquivOfMulEquiv (k : LocalizationMap T Q) {j : M ≃* P}
    (H : S.map j.toMonoidHom = T) : N ≃* Q :=
  f.mulEquivOfLocalizations <| k.ofMulEquivOfDom H

Isomorphism of localizations induced by a multiplicative isomorphism of monoids

Informal description

Given localization maps $ f \colon M \to N $ for a submonoid $ S \subseteq M $ and $ k \colon P \to Q $ for a submonoid $ T \subseteq P $, and a multiplicative isomorphism $ j \colon M \simeq^* P $ such that $ j(S) = T $, there exists a multiplicative isomorphism $ N \simeq^* Q $ between the localizations $ N $ and $ Q $. This isomorphism is constructed by first using $ j $ to induce a localization map $ k \circ j \colon M \to Q $ for $ S $, and then applying the universal property of localizations to obtain an isomorphism between $ N $ and $ Q $.

Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map_apply theorem

 {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x) :
  f.mulEquivOfMulEquiv k H x = f.map (fun y : S ↦ show j.toMonoidHom y ∈ T from H ▸ Set.mem_image_of_mem j y.2) k x

Full source

@[to_additive (attr := simp)]
theorem mulEquivOfMulEquiv_eq_map_apply {k : LocalizationMap T Q} {j : M ≃* P}
    (H : S.map j.toMonoidHom = T) (x) :
    f.mulEquivOfMulEquiv k H x =
      f.map (fun y : S ↦ show j.toMonoidHom y ∈ T from H ▸ Set.mem_image_of_mem j y.2) k x := rfl

Isomorphism of Localizations via Induced Map: $\text{mulEquivOfMulEquiv} = \text{map}(k \circ j|_S)$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively. Given localization maps $f \colon M \to N$ for $S$ and $k \colon P \to Q$ for $T$, and a multiplicative isomorphism $j \colon M \simeq^* P$ such that $j(S) = T$, then for any $x \in N$, the isomorphism $\text{mulEquivOfMulEquiv}$ between $N$ and $Q$ satisfies: \[ \text{mulEquivOfMulEquiv}(x) = \text{map}(k \circ j|_S)(x) \] where $\text{map}(k \circ j|_S)$ is the induced homomorphism from $N$ to $Q$ via the restriction of $j$ to $S$.

Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map theorem

 {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) :
  (f.mulEquivOfMulEquiv k H).toMonoidHom =
    f.map (fun y : S ↦ show j.toMonoidHom y ∈ T from H ▸ Set.mem_image_of_mem j y.2) k

Full source

@[to_additive]
theorem mulEquivOfMulEquiv_eq_map {k : LocalizationMap T Q} {j : M ≃* P}
    (H : S.map j.toMonoidHom = T) :
    (f.mulEquivOfMulEquiv k H).toMonoidHom =
      f.map (fun y : S ↦ show j.toMonoidHom y ∈ T from H ▸ Set.mem_image_of_mem j y.2) k := rfl

Equality of Induced Homomorphisms in Localization via Multiplicative Isomorphism

Informal description

Given localization maps $ f \colon M \to N $ for a submonoid $ S \subseteq M $ and $ k \colon P \to Q $ for a submonoid $ T \subseteq P $, and a multiplicative isomorphism $ j \colon M \simeq^* P $ such that $ j(S) = T $, the monoid homomorphism induced by the multiplicative isomorphism $ N \simeq^* Q $ equals the induced homomorphism between localizations $ f.map \, k $.

Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq theorem

 {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x) :
  f.mulEquivOfMulEquiv k H (f.toMap x) = k.toMap (j x)

Full source

@[to_additive]
theorem mulEquivOfMulEquiv_eq {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T)
    (x) :
    f.mulEquivOfMulEquiv k H (f.toMap x) = k.toMap (j x) :=
  f.map_eq (fun y : S ↦ H ▸ Set.mem_image_of_mem j y.2) _

Localization Isomorphism Preserves Images: $\varphi(f(x)) = k(j(x))$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$ respectively, and let $f \colon M \to N$ and $k \colon P \to Q$ be localization maps for $S$ and $T$. Given a multiplicative isomorphism $j \colon M \simeq^* P$ such that $j(S) = T$, then for any $x \in M$, the induced isomorphism $\varphi \colon N \simeq^* Q$ satisfies: \[ \varphi(f(x)) = k(j(x)) \]

Submonoid.LocalizationMap.mulEquivOfMulEquiv_mk' theorem

 {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x y) :
  f.mulEquivOfMulEquiv k H (f.mk' x y) = k.mk' (j x) ⟨j y, H ▸ Set.mem_image_of_mem j y.2⟩

Full source

@[to_additive]
theorem mulEquivOfMulEquiv_mk' {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T)
    (x y) :
    f.mulEquivOfMulEquiv k H (f.mk' x y) = k.mk' (j x) ⟨j y, H ▸ Set.mem_image_of_mem j y.2⟩ :=
  f.map_mk' (fun y : S ↦ H ▸ Set.mem_image_of_mem j y.2) _ _

Localization isomorphism preserves fraction representation: $\varphi(f(x)/f(y)) = k(j(x))/k(j(y))$

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$, and let $f \colon M \to N$ and $k \colon P \to Q$ be localization maps for $S$ and $T$ respectively. Given a multiplicative isomorphism $j \colon M \simeq^* P$ such that $j(S) = T$, then for any $x \in M$ and $y \in S$, the induced isomorphism $\varphi \colon N \simeq^* Q$ satisfies: \[ \varphi(f(x) \cdot (f(y))^{-1}) = k(j(x)) \cdot (k(j(y)))^{-1}. \] Here, $(f(y))^{-1}$ and $(k(j(y)))^{-1}$ denote the inverses in the respective localizations.

Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_apply theorem

 {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x) :
  (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap x = k.toMap (j x)

Full source

@[to_additive]
theorem of_mulEquivOfMulEquiv_apply {k : LocalizationMap T Q} {j : M ≃* P}
    (H : S.map j.toMonoidHom = T) (x) :
    (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap x = k.toMap (j x) :=
  Submonoid.LocalizationMap.ext_iff.1 (f.mulEquivOfLocalizations_right_inv (k.ofMulEquivOfDom H)) x

Compatibility of Localization Maps with Monoid Isomorphism

Informal description

Let $M$ and $P$ be commutative monoids with submonoids $S \subseteq M$ and $T \subseteq P$, and let $f \colon M \to N$ and $k \colon P \to Q$ be localization maps for $S$ and $T$ respectively. Given a multiplicative isomorphism $j \colon M \simeq^* P$ such that $j(S) = T$, then for any $x \in M$, the composition of localization maps satisfies: \[ (f \circ (f.mulEquivOfMulEquiv\ k\ H)).toMap\ x = k(j(x)) \] where $H$ is the proof that $j(S) = T$.

Submonoid.LocalizationMap.of_mulEquivOfMulEquiv theorem

 {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) :
  (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap = k.toMap.comp j.toMonoidHom

Full source

@[to_additive]
theorem of_mulEquivOfMulEquiv {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) :
    (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap = k.toMap.comp j.toMonoidHom :=
  MonoidHom.ext <| f.of_mulEquivOfMulEquiv_apply H

Compatibility of Localization Maps with Monoid Isomorphism via Composition

Informal description

Given commutative monoids $M$ and $P$ with submonoids $S \subseteq M$ and $T \subseteq P$, let $f \colon M \to N$ be a localization map for $S$ and $k \colon P \to Q$ be a localization map for $T$. If $j \colon M \simeq^* P$ is a multiplicative isomorphism such that $j(S) = T$, then the composition of localization maps satisfies: \[ (f \circ \varphi).toMap = k \circ j \] where $\varphi \colon N \simeq^* Q$ is the isomorphism induced by $j$, and $(f \circ \varphi).toMap$ denotes the underlying homomorphism of the composed localization map.

Localization.monoidOf definition

: Submonoid.LocalizationMap S (Localization S)

Full source

/-- Natural homomorphism sending `x : M`, `M` a `CommMonoid`, to the equivalence class of
`(x, 1)` in the Localization of `M` at a Submonoid. -/
@[to_additive
    "Natural homomorphism sending `x : M`, `M` an `AddCommMonoid`, to the equivalence class of
`(x, 0)` in the Localization of `M` at a Submonoid."]
def monoidOf : Submonoid.LocalizationMap S (Localization S) :=
  { (r S).mk'.comp <| MonoidHom.inl M
        S with
    toFun := fun x ↦ mk x 1
    map_one' := mk_one
    map_mul' := fun x y ↦ by rw [mk_mul, mul_one]
    map_units' := fun y ↦
      isUnit_iff_exists_inv.2 ⟨mk 1 y, by rw [mk_mul, mul_one, one_mul, mk_self]⟩
    surj' := fun z ↦ induction_on z fun x ↦
      ⟨x, by rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]⟩
    exists_of_eq := fun x y ↦ Iff.mp <|
      mk_eq_mk_iff.trans <|
        r_iff_exists.trans <|
          show (∃ c : S, ↑c * (1 * x) = c * (1 * y)) ↔ _ by rw [one_mul, one_mul] }

Localization homomorphism of a commutative monoid at a submonoid

Informal description

The natural homomorphism from a commutative monoid $ M $ to its localization at a submonoid $ S $, denoted $ M[S^{-1}] $, which sends each element $ x \in M $ to the equivalence class of the pair $ (x, 1) $ in the localization. This homomorphism satisfies the universal property of localization, mapping elements of $ S $ to units in $ M[S^{-1}] $.

Localization.mk_one_eq_monoidOf_mk theorem

(x) : mk x 1 = (monoidOf S).toMap x

Full source

@[to_additive]
theorem mk_one_eq_monoidOf_mk (x) : mk x 1 = (monoidOf S).toMap x := rfl

Equality of Localization Map and Canonical Construction at Identity

Informal description

For any element $x$ of a commutative monoid $M$ with submonoid $S$, the equivalence class of the pair $(x, 1)$ in the localization $M[S^{-1}]$ is equal to the image of $x$ under the natural localization homomorphism from $M$ to $M[S^{-1}]$.

Localization.mk_eq_monoidOf_mk'_apply theorem

(x y) : mk x y = (monoidOf S).mk' x y

Full source

@[to_additive]
theorem mk_eq_monoidOf_mk'_apply (x y) : mk x y = (monoidOf S).mk' x y :=
  show _ = _ * _ from
    (Submonoid.LocalizationMap.mul_inv_right (monoidOf S).map_units _ _ _).2 <| by
      rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]
      conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
      exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

Equality of Localization Construction and Canonical Map: $\frac{x}{y} = \text{mk}'(x, y)$

Informal description

For any elements $x \in M$ and $y \in S$, the equivalence class $\frac{x}{y}$ in the localization $M[S^{-1}]$ is equal to the image of $(x, y)$ under the canonical localization map $\text{mk}'$ associated with the natural localization homomorphism.

Localization.mk_eq_monoidOf_mk' theorem

: mk = (monoidOf S).mk'

Full source

@[to_additive]
theorem mk_eq_monoidOf_mk' : mk = (monoidOf S).mk' :=
  funext fun _ ↦ funext fun _ ↦ mk_eq_monoidOf_mk'_apply _ _

Equality of Localization Construction and Canonical Map: $\text{mk} = \text{mk}'$

Informal description

The canonical map $\text{mk} \colon M \times S \to M[S^{-1}]$ that sends $(x, y)$ to the equivalence class $\frac{x}{y}$ in the localization of $M$ at $S$ is equal to the localization map $\text{mk}'$ induced by the natural localization homomorphism $\text{monoidOf} \ S \colon M \to M[S^{-1}]$.

Localization.liftOn_mk' theorem

{p : Sort u} (f : M → S → p) (H) (a : M) (b : S) : liftOn ((monoidOf S).mk' a b) f H = f a b

Full source

@[to_additive (attr := simp)]
theorem liftOn_mk' {p : Sort u} (f : M → S → p) (H) (a : M) (b : S) :
    liftOn ((monoidOf S).mk' a b) f H = f a b := by rw [← mk_eq_monoidOf_mk', liftOn_mk]

Lift Function Computes Canonically on Localization Map Elements

Informal description

For any commutative monoid $M$ with a submonoid $S \subseteq M$, any type $p$, any function $f \colon M \times S \to p$ that respects the localization congruence relation, and any elements $a \in M$, $b \in S$, the lift function applied to the canonical localization element $\text{mk}'(a,b)$ yields $f(a,b)$. In symbols: $$\text{liftOn}(\text{mk}'(a,b), f, H) = f(a,b)$$

Localization.liftOn₂_mk' theorem

 {p : Sort*} (f : M → S → M → S → p) (H) (a c : M) (b d : S) :
  liftOn₂ ((monoidOf S).mk' a b) ((monoidOf S).mk' c d) f H = f a b c d

Full source

@[to_additive (attr := simp)]
theorem liftOn₂_mk' {p : Sort*} (f : M → S → M → S → p) (H) (a c : M) (b d : S) :
    liftOn₂ ((monoidOf S).mk' a b) ((monoidOf S).mk' c d) f H = f a b c d := by
  rw [← mk_eq_monoidOf_mk', liftOn₂_mk]

Lifted Binary Function on Localization Elements Equals Function on Representatives

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$. For any type $p$, any function $f \colon M \times S \times M \times S \to p$ that respects the localization congruence relation (i.e., $f(a,b,c,d) = f(a',b',c',d')$ whenever $(a,b) \sim (a',b')$ and $(c,d) \sim (c',d')$ under the localization relation), and any elements $a, c \in M$, $b, d \in S$, we have: \[ \text{liftOn}_2\left(\frac{a}{b}, \frac{c}{d}, f, H\right) = f(a, b, c, d), \] where $\frac{a}{b}$ and $\frac{c}{d}$ denote the images of $(a,b)$ and $(c,d)$ under the canonical localization map.

Localization.mulEquivOfQuotient definition

(f : Submonoid.LocalizationMap S N) : Localization S ≃* N

Full source

/-- Given a Localization map `f : M →* N` for a Submonoid `S`, we get an isomorphism between
the Localization of `M` at `S` as a quotient type and `N`. -/
@[to_additive
    "Given a Localization map `f : M →+ N` for a Submonoid `S`, we get an isomorphism between
the Localization of `M` at `S` as a quotient type and `N`."]
noncomputable def mulEquivOfQuotient (f : Submonoid.LocalizationMap S N) : LocalizationLocalization S ≃* N :=
  (monoidOf S).mulEquivOfLocalizations f

Isomorphism between quotient localization and target monoid

Informal description

Given a commutative monoid $ M $ with a submonoid $ S \subseteq M $ and a localization map $ f \colon M \to N $ for $ S $, the function `mulEquivOfQuotient` defines a multiplicative isomorphism between the quotient type `Localization S` (the localization of $ M $ at $ S $) and $ N $. This isomorphism is constructed by lifting the localization map $ f $ to the quotient type, ensuring that the equivalence relation used to define `Localization S` is respected. Specifically, for any elements $ x, y \in M \times S $, the isomorphism maps the equivalence class of $ (x, y) $ in `Localization S` to $ f(x) \cdot (f(y))^{-1} $ in $ N $.

Localization.mulEquivOfQuotient_apply theorem

(x) : mulEquivOfQuotient f x = (monoidOf S).lift f.map_units x

Full source

@[to_additive (attr := simp)]
theorem mulEquivOfQuotient_apply (x) : mulEquivOfQuotient f x = (monoidOf S).lift f.map_units x :=
  rfl

Isomorphism Application: $\text{mulEquivOfQuotient}(f)(x) = \text{lift}(f)(x)$

Informal description

For any element $x$ in the localization of a commutative monoid $M$ at a submonoid $S$, the multiplicative isomorphism $\text{mulEquivOfQuotient}(f)$ maps $x$ to the element obtained by lifting the localization map $f$ (which sends elements of $S$ to units) via the universal property of localization. That is, \[ \text{mulEquivOfQuotient}(f)(x) = \text{lift}(f)(x), \] where $\text{lift}(f)$ is the unique homomorphism induced by $f$ from the localization to the target monoid $N$.

Localization.mulEquivOfQuotient_mk' theorem

(x y) : mulEquivOfQuotient f ((monoidOf S).mk' x y) = f.mk' x y

Full source

@[to_additive]
theorem mulEquivOfQuotient_mk' (x y) : mulEquivOfQuotient f ((monoidOf S).mk' x y) = f.mk' x y :=
  (monoidOf S).lift_mk' _ _ _

Isomorphism maps localization equivalence class to $f(x)/f(y)$

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. For any $x \in M$ and $y \in S$, the multiplicative isomorphism $\text{mulEquivOfQuotient}(f)$ maps the equivalence class of $(x, y)$ in the localization $M[S^{-1}]$ to $f(x) \cdot (f(y))^{-1}$ in $N$.

Localization.mulEquivOfQuotient_mk theorem

(x y) : mulEquivOfQuotient f (mk x y) = f.mk' x y

Full source

@[to_additive]
theorem mulEquivOfQuotient_mk (x y) : mulEquivOfQuotient f (mk x y) = f.mk' x y := by
  rw [mk_eq_monoidOf_mk'_apply]; exact mulEquivOfQuotient_mk' _ _

Isomorphism maps localization equivalence class $\frac{x}{y}$ to $f(x)/f(y)$

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. For any $x \in M$ and $y \in S$, the multiplicative isomorphism $\text{mulEquivOfQuotient}(f)$ maps the equivalence class $\frac{x}{y}$ in the localization $M[S^{-1}]$ to $f(x) \cdot (f(y))^{-1}$ in $N$.

Localization.mulEquivOfQuotient_monoidOf theorem

(x) : mulEquivOfQuotient f ((monoidOf S).toMap x) = f.toMap x

Full source

@[to_additive]
theorem mulEquivOfQuotient_monoidOf (x) :
    mulEquivOfQuotient f ((monoidOf S).toMap x) = f.toMap x := by simp

Compatibility of Localization Isomorphism with Canonical Homomorphism: $\text{mulEquivOfQuotient}\, f \circ \text{monoidOf}\, S = f$

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. Then, for any $x \in M$, the multiplicative isomorphism $\text{mulEquivOfQuotient}\, f$ between the localization $\text{Localization}\, S$ and $N$ satisfies: \[ \text{mulEquivOfQuotient}\, f \left( (\text{monoidOf}\, S)(x) \right) = f(x), \] where $\text{monoidOf}\, S \colon M \to \text{Localization}\, S$ is the canonical localization homomorphism.

Localization.mulEquivOfQuotient_symm_mk' theorem

(x y) : (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y

Full source

@[to_additive (attr := simp)]
theorem mulEquivOfQuotient_symm_mk' (x y) :
    (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y :=
  f.lift_mk' (monoidOf S).map_units _ _

Inverse Localization Isomorphism Maps Fractions to Fractions

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. Then for any $x \in M$ and $y \in S$, the inverse of the multiplicative isomorphism $\text{mulEquivOfQuotient}\, f$ between $N$ and $\text{Localization}\, S$ satisfies: \[ (\text{mulEquivOfQuotient}\, f)^{-1}\left(f(x) \cdot (f(y))^{-1}\right) = \text{monoidOf}\, S(x) \cdot (\text{monoidOf}\, S(y))^{-1}, \] where $\text{monoidOf}\, S \colon M \to \text{Localization}\, S$ is the canonical localization homomorphism.

Localization.mulEquivOfQuotient_symm_mk theorem

(x y) : (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y

Full source

@[to_additive]
theorem mulEquivOfQuotient_symm_mk (x y) : (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y := by
  rw [mk_eq_monoidOf_mk'_apply]; exact mulEquivOfQuotient_symm_mk' _ _

Inverse Localization Isomorphism Maps Fractions to Their Canonical Form

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. Then for any $x \in M$ and $y \in S$, the inverse of the multiplicative isomorphism $\text{mulEquivOfQuotient}\, f$ between $N$ and the localization $\text{Localization}\, S$ satisfies: \[ (\text{mulEquivOfQuotient}\, f)^{-1}\left(f(x) \cdot (f(y))^{-1}\right) = \frac{x}{y}, \] where $\frac{x}{y}$ denotes the equivalence class of $(x, y)$ in $\text{Localization}\, S$.

Localization.mulEquivOfQuotient_symm_monoidOf theorem

(x) : (mulEquivOfQuotient f).symm (f.toMap x) = (monoidOf S).toMap x

Full source

@[to_additive (attr := simp)]
theorem mulEquivOfQuotient_symm_monoidOf (x) :
    (mulEquivOfQuotient f).symm (f.toMap x) = (monoidOf S).toMap x :=
  f.lift_eq (monoidOf S).map_units _

Inverse Localization Isomorphism Preserves Natural Map: $(\text{mulEquivOfQuotient}\, f)^{-1} \circ f = \text{monoidOf}\, S$

Informal description

Let $M$ be a commutative monoid with a submonoid $S \subseteq M$, and let $f \colon M \to N$ be a localization map for $S$. For any element $x \in M$, the inverse of the multiplicative isomorphism $\text{mulEquivOfQuotient}\, f$ applied to $f(x)$ equals the image of $x$ under the natural homomorphism $\text{monoidOf}\, S \colon M \to \text{Localization}\, S$. In other words: \[ (\text{mulEquivOfQuotient}\, f)^{-1}(f(x)) = (\text{monoidOf}\, S)(x) \]

Localization.mk_left_injective theorem

(b : s) : Injective fun a => mk a b

Full source

@[to_additive]
theorem mk_left_injective (b : s) : Injective fun a => mk a b := fun c d h => by
  simpa [mk_eq_mk_iff, r_iff_exists] using h

Injectivity of Localization Map with Fixed Denominator

Informal description

For any element $b$ in the submonoid $S$ of a commutative monoid $M$, the function $a \mapsto \frac{a}{b}$ from $M$ to the localization $M[S^{-1}]$ is injective. In other words, if $\frac{a_1}{b} = \frac{a_2}{b}$ in $M[S^{-1}]$, then $a_1 = a_2$ in $M$.

Localization.mk_eq_mk_iff' theorem

: mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = a₂ * b₁

Full source

@[to_additive]
theorem mk_eq_mk_iff' : mkmk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = a₂ * b₁ := by
  simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]

Equality Criterion for Localization Elements: $\frac{a₁}{a₂} = \frac{b₁}{b₂} \leftrightarrow b₂ \cdot a₁ = a₂ \cdot b₁$

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any elements $a₁, b₁ \in M$ and $a₂, b₂ \in S$, the equivalence classes $\text{mk}(a₁, a₂)$ and $\text{mk}(b₁, b₂)$ in the localization $M[S^{-1}]$ are equal if and only if $b₂ \cdot a₁ = a₂ \cdot b₁$ in $M$.

Localization.decidableEq instance

[DecidableEq α] : DecidableEq (Localization s)

Full source

@[to_additive]
instance decidableEq [DecidableEq α] : DecidableEq (Localization s) := fun a b =>
  Localization.recOnSubsingleton₂ a b fun _ _ _ _ => decidable_of_iff' _ mk_eq_mk_iff'

Decidability of Equality in Localization of Commutative Monoids

Informal description

For any commutative monoid $\alpha$ with a submonoid $s$ and a decidable equality on $\alpha$, the localization $\text{Localization}\,s$ also has decidable equality.

OreLocalization.localizationMap definition

: S.LocalizationMap R[S⁻¹]

Full source

/-- The morphism `numeratorHom` is a monoid localization map in the case of commutative `R`. -/
protected def localizationMap : S.LocalizationMap R[S⁻¹] := Localization.monoidOf S

Localization map for Ore localization of a commutative monoid

Informal description

The natural localization map from a commutative monoid $ R $ to its Ore localization $ R[S^{-1}] $ at a submonoid $ S $, which sends each element $ x \in R $ to the equivalence class of the pair $ (x, 1) $ in the Ore localization. This map satisfies the universal property of localization, mapping elements of $ S $ to units in $ R[S^{-1}] $.

OreLocalization.equivMonoidLocalization definition

: Localization S ≃* R[S⁻¹]

Full source

/-- If `R` is commutative, Ore localization and monoid localization are isomorphic. -/
protected noncomputable def equivMonoidLocalization : LocalizationLocalization S ≃* R[S⁻¹] := MulEquiv.refl _

Isomorphism between Ore localization and monoid localization

Informal description

The multiplicative isomorphism between the Ore localization $R[S^{-1}]$ and the monoid localization $\text{Localization}\,S$ of a commutative monoid $R$ at a submonoid $S$.

Mathlib.GroupTheory.MonoidLocalization.Basic

Implementation notes

TODO

Tags