# mathlib3documentation

group_theory.monoid_localization

# Localizations of commutative monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Localizing a commutative ring at one of its submonoids does not rely on the ring's addition, so we can generalize localizations to commutative monoids.

We characterize the localization of a commutative monoid `M` at a submonoid `S` up to isomorphism; that is, a commutative monoid `N` is the localization of `M` at `S` iff we can find a monoid homomorphism `f : M →* N` satisfying 3 properties:

1. For all `y ∈ S`, `f y` is a unit;
2. For all `z : N`, there exists `(x, y) : M × S` such that `z * f y = f x`;
3. For all `x, y : M`, `f x = f y` iff there exists `c ∈ S` such that `x * c = y * c`.

Given such a localization map `f : M →* N`, we can define the surjection `localization_map.mk'` sending `(x, y) : M × S` to `f x * (f y)⁻¹`, and `localization_map.lift`, the homomorphism from `N` induced by a homomorphism from `M` which maps elements of `S` to invertible elements of the codomain. Similarly, given commutative monoids `P, Q`, a submonoid `T` of `P` and a localization map for `T` from `P` to `Q`, then a homomorphism `g : M →* P` such that `g(S) ⊆ T` induces a homomorphism of localizations, `localization_map.map`, from `N` to `Q`. We treat the special case of localizing away from an element in the sections `away_map` and `away`.

We also define the quotient of `M × S` by the unique congruence relation (equivalence relation preserving a binary operation) `r` such that for any other congruence relation `s` on `M × S` satisfying '`∀ y ∈ S`, `(1, 1) ∼ (y, y)` under `s`', we have that `(x₁, y₁) ∼ (x₂, y₂)` by `s` whenever `(x₁, y₁) ∼ (x₂, y₂)` by `r`. We show this relation is equivalent to the standard localization relation. This defines the localization as a quotient type, `localization`, but the majority of subsequent lemmas in the file are given in terms of localizations up to isomorphism, using maps which satisfy the characteristic predicate.

The Grothendieck group construction corresponds to localizing at the top submonoid, namely making every element invertible.

## Implementation notes #

In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally `rewrite` one structure with an isomorphic one; one way around this is to isolate a predicate characterizing a structure up to isomorphism, and reason about things that satisfy the predicate.

The infimum form of the localization congruence relation is chosen as 'canonical' here, since it shortens some proofs.

To apply a localization map `f` as a function, we use `f.to_map`, as coercions don't work well for this structure.

To reason about the localization as a quotient type, use `mk_eq_monoid_of_mk'` and associated lemmas. These show the quotient map `mk : M → S → localization S` equals the surjection `localization_map.mk'` induced by the map `monoid_of : localization_map S (localization S)` (where `of` establishes the localization as a quotient type satisfies the characteristic predicate). The lemma `mk_eq_monoid_of_mk'` hence gives you access to the results in the rest of the file, which are about the `localization_map.mk'` induced by any localization map.

## TODO #

• Show that the localization at the top monoid is a group.
• Generalise to (nonempty) subsemigroups.
• If we acquire more bundlings, we can make `localization.mk_order_embedding` be an ordered monoid embedding.

## Tags #

localization, monoid localization, quotient monoid, congruence relation, characteristic predicate, commutative monoid, grothendieck group

@[nolint]
structure add_submonoid.localization_map {M : Type u_1} (S : add_submonoid M) (N : Type u_2)  :
Type (max u_1 u_2)

The type of add_monoid homomorphisms satisfying the characteristic predicate: if `f : M →+ N` satisfies this predicate, then `N` is isomorphic to the localization of `M` at `S`.

Instances for `add_submonoid.localization_map`
@[nolint]
structure submonoid.localization_map {M : Type u_1} [comm_monoid M] (S : submonoid M) (N : Type u_2) [comm_monoid N] :
Type (max u_1 u_2)

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`.

Instances for `submonoid.localization_map`
• submonoid.localization_map.has_sizeof_inst

The congruence relation on `M × S`, `M` an `add_comm_monoid` and `S` an `add_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`, `(0, 0) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies `(x₁, y₁) ∼ (x₂, y₂)` by `s`.

Equations
def localization.r {M : Type u_1} [comm_monoid M] (S : submonoid M) :
con (M × S)

The congruence relation on `M × S`, `M` a `comm_monoid` 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`.

Equations

An alternate form of the congruence relation on `M × S`, `M` a `comm_monoid` and `S` a submonoid of `M`, whose quotient is the localization of `M` at `S`.

Equations
def localization.r' {M : Type u_1} [comm_monoid M] (S : submonoid M) :
con (M × S)

An alternate form of the congruence relation on `M × S`, `M` a `comm_monoid` and `S` a submonoid of `M`, whose quotient is the localization of `M` at `S`.

Equations
theorem localization.r_eq_r' {M : Type u_1} [comm_monoid M] (S : submonoid M) :

The congruence relation used to localize a `comm_monoid` at a submonoid can be expressed equivalently as an infimum (see `localization.r`) or explicitly (see `localization.r'`).

The additive congruence relation used to localize an `add_comm_monoid` at a submonoid can be expressed equivalently as an infimum (see `add_localization.r`) or explicitly (see `add_localization.r'`).

theorem add_localization.r_iff_exists {M : Type u_1} {S : add_submonoid M} {x y : M × S} :
x y (c : S), c + ((y.snd) + x.fst) = c + ((x.snd) + y.fst)
theorem localization.r_iff_exists {M : Type u_1} [comm_monoid M] {S : submonoid M} {x y : M × S} :
x y (c : S), c * ((y.snd) * x.fst) = c * ((x.snd) * y.fst)
@[irreducible]
def localization {M : Type u_1} [comm_monoid M] (S : submonoid M) :
Type u_1

The localization of a `comm_monoid` at one of its submonoids (as a quotient type).

Equations
Instances for `localization`
Type u_1

The localization of an `add_comm_monoid` at one of its submonoids (as a quotient type).

Equations
Instances for `add_localization`
@[protected, instance]
def localization.inhabited {M : Type u_1} [comm_monoid M] (S : submonoid M) :
Equations
@[protected, instance]
Equations
@[protected, irreducible]
def localization.mul {M : Type u_1} [comm_monoid M] (S : submonoid M) :

Multiplication in a localization is defined as `⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c, b * d⟩`.

Equations
@[protected]

Addition in an `add_localization` is defined as `⟨a, b⟩ + ⟨c, d⟩ = ⟨a + c, b + d⟩`.

Should not be confused with the ring localization counterpart `localization.add`, which maps `⟨a, b⟩ + ⟨c, d⟩` to `⟨d * a + b * c, b * d⟩`.

Equations
@[protected, instance]
def localization.has_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) :
Equations
@[protected, instance]
Equations
@[protected, irreducible]
def localization.one {M : Type u_1} [comm_monoid M] (S : submonoid M) :

The identity element of a localization is defined as `⟨1, 1⟩`.

Equations
@[protected]

The identity element of an `add_localization` is defined as `⟨0, 0⟩`.

Should not be confused with the ring localization counterpart `localization.zero`, which is defined as `⟨0, 1⟩`.

Equations
@[protected, instance]
Equations
@[protected, instance]
def localization.has_one {M : Type u_1} [comm_monoid M] (S : submonoid M) :
Equations
@[protected, irreducible]
def localization.npow {M : Type u_1} [comm_monoid M] (S : submonoid M) :

Exponentiation in a localization is defined as `⟨a, b⟩ ^ n = ⟨a ^ n, b ^ n⟩`.

This is a separate `irreducible` def to ensure the elaborator doesn't waste its time trying to unify some huge recursive definition with itself, but unfolded one step less.

Equations
@[protected]

Multiplication with a natural in an `add_localization` is defined as `n • ⟨a, b⟩ = ⟨n • a, n • b⟩`.

This is a separate `irreducible` def to ensure the elaborator doesn't waste its time trying to unify some huge recursive definition with itself, but unfolded one step less.

Equations
@[protected, instance]
Equations
@[protected, instance]
def localization.comm_monoid {M : Type u_1} [comm_monoid M] (S : submonoid M) :
Equations
def localization.mk {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) (y : S) :

Given a `comm_monoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to the equivalence class of `(x, y)` in the localization of `M` at `S`.

Equations
def add_localization.mk {M : Type u_1} {S : add_submonoid M} (x : M) (y : S) :

Given an `add_comm_monoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to the equivalence class of `(x, y)` in the localization of `M` at `S`.

Equations
theorem add_localization.mk_eq_mk_iff {M : Type u_1} {S : add_submonoid M} {a c : M} {b d : S} :
(a, b) (c, d)
theorem localization.mk_eq_mk_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {a c : M} {b d : S} :
= (a, b) (c, d)
def localization.rec {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (f : Π (a : M) (b : S), p b)) (H : {a c : M} {b d : S} (h : (a, b) (c, d)), eq.rec (f a b) _ = f c d) (x : localization S) :
p x

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`.

Equations
def add_localization.rec {M : Type u_1} {S : add_submonoid M} {p : Sort u} (f : Π (a : M) (b : S), p b)) (H : {a c : M} {b d : S} (h : (a, b) (c, d)), eq.rec (f a b) _ = f c d) (x : add_localization S) :
p x

Dependent recursion principle for `add_localization`s: 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 `add_localization S`.

Equations
def localization.rec_on_subsingleton₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {r : } [h : (a c : M) (b d : S), subsingleton (r b) d))] (x y : localization S) (f : Π (a c : M) (b d : S), r b) d)) :
r x y

Copy of `quotient.rec_on_subsingleton₂` for `localization`

Equations
• f = (prod.rec (λ (_x : M) (_x_1 : S), prod.rec (λ (_x_2 : M) (_x_3 : S), f _x _x_2 _x_1 _x_3)))
def add_localization.rec_on_subsingleton₂ {M : Type u_1} {S : add_submonoid M} {r : } [h : (a c : M) (b d : S), subsingleton (r b) d))] (x y : add_localization S) (f : Π (a c : M) (b d : S), r b) d)) :
r x y

Copy of `quotient.rec_on_subsingleton₂` for `add_localization`

Equations
• f = (prod.rec (λ (_x : M) (_x_1 : S), prod.rec (λ (_x_2 : M) (_x_3 : S), f _x _x_2 _x_1 _x_3)))
theorem add_localization.mk_add {M : Type u_1} {S : add_submonoid M} (a c : M) (b d : S) :
= add_localization.mk (a + c) (b + d)
theorem localization.mk_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} (a c : M) (b d : S) :
* = localization.mk (a * c) (b * d)
theorem localization.mk_one {M : Type u_1} [comm_monoid M] {S : submonoid M} :
= 1
= 0
theorem localization.mk_pow {M : Type u_1} [comm_monoid M] {S : submonoid M} (n : ) (a : M) (b : S) :
^ n = localization.mk (a ^ n) (b ^ n)
theorem add_localization.mk_nsmul {M : Type u_1} {S : add_submonoid M} (n : ) (a : M) (b : S) :
@[simp]
theorem add_localization.rec_mk {M : Type u_1} {S : add_submonoid M} {p : Sort u} (f : Π (a : M) (b : S), p b)) (H : {a c : M} {b d : S} (h : (a, b) (c, d)), eq.rec (f a b) _ = f c d) (a : M) (b : S) :
b) = f a b
@[simp]
theorem localization.rec_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (f : Π (a : M) (b : S), p b)) (H : {a c : M} {b d : S} (h : (a, b) (c, d)), eq.rec (f a b) _ = f c d) (a : M) (b : S) :
b) = f a b
def add_localization.lift_on {M : Type u_1} {S : add_submonoid M} {p : Sort u} (x : add_localization S) (f : M S p) (H : {a c : M} {b d : S}, (a, b) (c, d) f a b = f c d) :
p

Non-dependent recursion principle for `add_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`.

Equations
def localization.lift_on {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (x : localization S) (f : M S p) (H : {a c : M} {b d : S}, (a, b) (c, d) f a b = f c d) :
p

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`.

Equations
theorem localization.lift_on_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (f : M S p) (H : {a c : M} {b d : S}, (a, b) (c, d) f a b = f c d) (a : M) (b : S) :
b).lift_on f H = f a b
theorem add_localization.lift_on_mk {M : Type u_1} {S : add_submonoid M} {p : Sort u} (f : M S p) (H : {a c : M} {b d : S}, (a, b) (c, d) f a b = f c d) (a : M) (b : S) :
b).lift_on f H = f a b
theorem add_localization.ind {M : Type u_1} {S : add_submonoid M} {p : Prop} (H : (y : M × S), p y.snd)) (x : add_localization S) :
p x
theorem localization.ind {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Prop} (H : (y : M × S), p y.snd)) (x : localization S) :
p x
theorem localization.induction_on {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Prop} (x : localization S) (H : (y : M × S), p y.snd)) :
p x
theorem add_localization.induction_on {M : Type u_1} {S : add_submonoid M} {p : Prop} (x : add_localization S) (H : (y : M × S), p y.snd)) :
p x
def add_localization.lift_on₂ {M : Type u_1} {S : add_submonoid M} {p : Sort u} (x y : add_localization S) (f : M S M S p) (H : {a a' : M} {b b' : S} {c c' : M} {d d' : S}, (a, b) (a', b') (c, d) (c', d') f a b c d = f a' b' c' d') :
p

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`.

Equations
def localization.lift_on₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (x y : localization S) (f : M S M S p) (H : {a a' : M} {b b' : S} {c c' : M} {d d' : S}, (a, b) (a', b') (c, d) (c', d') f a b c d = f a' b' c' d') :
p

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`.

Equations
theorem localization.lift_on₂_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u_2} (f : M S M S p) (H : {a a' : M} {b b' : S} {c c' : M} {d d' : S}, (a, b) (a', b') (c, d) (c', d') f a b c d = f a' b' c' d') (a c : M) (b d : S) :
b).lift_on₂ d) f H = f a b c d
theorem add_localization.lift_on₂_mk {M : Type u_1} {S : add_submonoid M} {p : Sort u_2} (f : M S M S p) (H : {a a' : M} {b b' : S} {c c' : M} {d d' : S}, (a, b) (a', b') (c, d) (c', d') f a b c d = f a' b' c' d') (a c : M) (b d : S) :
b).lift_on₂ d) f H = f a b c d
theorem localization.induction_on₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Prop} (x y : localization S) (H : (x y : M × S), p x.snd) y.snd)) :
p x y
theorem add_localization.induction_on₂ {M : Type u_1} {S : add_submonoid M} {p : Prop} (x y : add_localization S) (H : (x y : M × S), p x.snd) y.snd)) :
p x y
theorem add_localization.induction_on₃ {M : Type u_1} {S : add_submonoid M} {p : Prop} (x y z : add_localization S) (H : (x y z : M × S), p x.snd) y.snd) z.snd)) :
p x y z
theorem localization.induction_on₃ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Prop} (x y z : localization S) (H : (x y z : M × S), p x.snd) y.snd) z.snd)) :
p x y z
theorem localization.one_rel {M : Type u_1} [comm_monoid M] {S : submonoid M} (y : S) :
1 (y, y)
theorem add_localization.zero_rel {M : Type u_1} {S : add_submonoid M} (y : S) :
0 (y, y)
theorem localization.r_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {x y : M × S} (h : (y.snd) * x.fst = (x.snd) * y.fst) :
x y
theorem add_localization.r_of_eq {M : Type u_1} {S : add_submonoid M} {x y : M × S} (h : (y.snd) + x.fst = (x.snd) + y.fst) :
x y
theorem add_localization.mk_self {M : Type u_1} {S : add_submonoid M} (a : S) :
theorem localization.mk_self {M : Type u_1} [comm_monoid M] {S : submonoid M} (a : S) :
= 1
@[protected, irreducible]
def localization.smul {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [ M] [ M] (c : R) (z : localization S) :

Scalar multiplication in a monoid localization is defined as `c • ⟨a, b⟩ = ⟨c • a, b⟩`.

Equations
@[protected, instance]
def localization.has_smul {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [ M] [ M] :
Equations
theorem localization.smul_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [ M] [ M] (c : R) (a : M) (b : S) :
@[protected, instance]
def localization.smul_comm_class {M : Type u_1} [comm_monoid M] {S : submonoid M} {R₁ : Type u_5} {R₂ : Type u_6} [has_smul R₁ M] [has_smul R₂ M] [ M M] [ M M] [ R₂ M] :
R₂ (localization S)
@[protected, instance]
def localization.is_scalar_tower {M : Type u_1} [comm_monoid M] {S : submonoid M} {R₁ : Type u_5} {R₂ : Type u_6} [has_smul R₁ M] [has_smul R₂ M] [ M M] [ M M] [has_smul R₁ R₂] [ R₂ M] :
R₂ (localization S)
@[protected, instance]
def localization.smul_comm_class_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_2} [ M] [ M] :
@[protected, instance]
def localization.is_scalar_tower_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_2} [ M] [ M] :
@[protected, instance]
def localization.is_central_scalar {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [ M] [ M] [ M] [ M] [ M] :
@[protected, instance]
def localization.mul_action {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [monoid R] [ M] [ M] :
Equations
@[protected, instance]
def localization.mul_distrib_mul_action {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [monoid R] [ M] :
Equations
def add_monoid_hom.to_localization_map {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : M →+ N) (H1 : (y : S), is_add_unit (f y)) (H2 : (z : N), (x : M × S), z + f (x.snd) = f x.fst) (H3 : (x y : M), f x = f y (c : S), c + x = c + y) :

Makes a localization map from an `add_comm_monoid` hom satisfying the characteristic predicate.

Equations
def monoid_hom.to_localization_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : M →* N) (H1 : (y : S), is_unit (f y)) (H2 : (z : N), (x : M × S), z * f (x.snd) = f x.fst) (H3 : (x y : M), f x = f y (c : S), c * x = c * y) :

Makes a localization map from a `comm_monoid` hom satisfying the characteristic predicate.

Equations
@[reducible]
def add_submonoid.localization_map.to_map {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) :
M →+ N

Short for `to_add_monoid_hom`; used to apply a localization map as a function.

@[reducible]
def submonoid.localization_map.to_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :
M →* N

Short for `to_monoid_hom`; used to apply a localization map as a function.

@[ext]
theorem add_submonoid.localization_map.ext {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f g : S.localization_map N} (h : (x : M), (f.to_map) x = (g.to_map) x) :
f = g
@[ext]
theorem submonoid.localization_map.ext {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f g : S.localization_map N} (h : (x : M), (f.to_map) x = (g.to_map) x) :
f = g
theorem submonoid.localization_map.ext_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f g : S.localization_map N} :
f = g (x : M), (f.to_map) x = (g.to_map) x
theorem add_submonoid.localization_map.ext_iff {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f g : S.localization_map N} :
f = g (x : M), (f.to_map) x = (g.to_map) x
theorem submonoid.localization_map.map_units {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (y : S) :
theorem submonoid.localization_map.surj {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :
(x : M × S), z * (f.to_map) (x.snd) = (f.to_map) x.fst
theorem add_submonoid.localization_map.surj {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (z : N) :
(x : M × S), z + (f.to_map) (x.snd) = (f.to_map) x.fst
theorem submonoid.localization_map.eq_iff_exists {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x y : M} :
(f.to_map) x = (f.to_map) y (c : S), c * x = c * y
theorem add_submonoid.localization_map.eq_iff_exists {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x y : M} :
(f.to_map) x = (f.to_map) y (c : S), c + x = c + y
noncomputable def submonoid.localization_map.sec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :
M × S

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`.

Equations
noncomputable def add_submonoid.localization_map.sec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (z : N) :
M × S

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`.

Equations
theorem submonoid.localization_map.sec_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (z : N) :
z * (f.to_map) ((f.sec z).snd) = (f.to_map) (f.sec z).fst
theorem add_submonoid.localization_map.sec_spec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : S.localization_map N} (z : N) :
z + (f.to_map) ((f.sec z).snd) = (f.to_map) (f.sec z).fst
theorem submonoid.localization_map.sec_spec' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (z : N) :
(f.to_map) (f.sec z).fst = (f.to_map) ((f.sec z).snd) * z
theorem add_submonoid.localization_map.sec_spec' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : S.localization_map N} (z : N) :
(f.to_map) (f.sec z).fst = (f.to_map) ((f.sec z).snd) + z
theorem add_submonoid.localization_map.add_neg_left {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : M →+ N} (h : (y : S), is_add_unit (f y)) (y : S) (w z : N) :
w + - h) y = z w = f y + z

Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that `f(S) ⊆ add_units N`, for all `w : M, z : N` and `y ∈ S`, we have `w - f y = z ↔ w = f y + z`.

theorem submonoid.localization_map.mul_inv_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : (y : S), is_unit (f y)) (y : S) (w z : N) :

Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all `w : M, z : N` and `y ∈ S`, we have `w * (f y)⁻¹ = z ↔ w = f y * z`.

theorem submonoid.localization_map.mul_inv_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : (y : S), is_unit (f y)) (y : S) (w z : N) :

Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all `w : M, z : N` and `y ∈ S`, we have `z = w * (f y)⁻¹ ↔ z * f y = w`.

theorem add_submonoid.localization_map.add_neg_right {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : M →+ N} (h : (y : S), is_add_unit (f y)) (y : S) (w z : N) :
z = w + - h) y z + f y = w

Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that `f(S) ⊆ add_units N`, for all `w : M, z : N` and `y ∈ S`, we have `z = w - f y ↔ z + f y = w`.

@[simp]
theorem add_submonoid.localization_map.add_neg {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : M →+ N} (h : (y : S), is_add_unit (f y)) {x₁ x₂ : M} {y₁ y₂ : S} :
f x₁ + - h) y₁ = f x₂ + - h) y₂ f (x₁ + y₂) = f (x₂ + y₁)

Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that `f(S) ⊆ add_units 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₁)`.

@[simp]
theorem submonoid.localization_map.mul_inv {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : (y : S), is_unit (f y)) {x₁ x₂ : M} {y₁ y₂ : S} :
f x₁ * ((is_unit.lift_right (f.restrict S) h) y₁)⁻¹ = f x₂ * ((is_unit.lift_right (f.restrict S) h) y₂)⁻¹ f (x₁ * y₂) = f (x₂ * y₁)

Given a monoid hom `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₁)`.

theorem add_submonoid.localization_map.neg_inj {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : M →+ N} (hf : (y : S), is_add_unit (f y)) {y z : S} (h : - hf) y = - hf) z) :

Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that `f(S) ⊆ add_units N`, for all `y, z ∈ S`, we have `- (f y) = - (f z) → f y = f z`.

theorem submonoid.localization_map.inv_inj {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (hf : (y : S), is_unit (f y)) {y z : S} (h : ((is_unit.lift_right (f.restrict S) hf) y)⁻¹ = ((is_unit.lift_right (f.restrict S) hf) z)⁻¹) :

Given a monoid hom `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`.

theorem add_submonoid.localization_map.neg_unique {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {f : M →+ N} (h : (y : S), is_add_unit (f y)) {y : S} {z : N} (H : f y + z = 0) :
- h) y = z

Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that `f(S) ⊆ add_units N`, for all `y ∈ S`, `- (f y)` is unique.

theorem submonoid.localization_map.inv_unique {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : (y : S), is_unit (f y)) {y : S} {z : N} (H : f y * z = 1) :

Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all `y ∈ S`, `(f y)⁻¹` is unique.

theorem submonoid.localization_map.map_right_cancel {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x y : M} {c : S} (h : (f.to_map) (c * x) = (f.to_map) (c * y)) :
(f.to_map) x = (f.to_map) y
theorem add_submonoid.localization_map.map_right_cancel {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x y : M} {c : S} (h : (f.to_map) (c + x) = (f.to_map) (c + y)) :
(f.to_map) x = (f.to_map) y
theorem submonoid.localization_map.map_left_cancel {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x y : M} {c : S} (h : (f.to_map) (x * c) = (f.to_map) (y * c)) :
(f.to_map) x = (f.to_map) y
theorem add_submonoid.localization_map.map_left_cancel {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x y : M} {c : S} (h : (f.to_map) (x + c) = (f.to_map) (y + c)) :
(f.to_map) x = (f.to_map) y
noncomputable def add_submonoid.localization_map.mk' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
N

Given a localization map `f : M →+ N`, the surjection sending `(x, y) : M × S` to `f x - f y`.

Equations
noncomputable def submonoid.localization_map.mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
N

Given a localization map `f : M →* N`, the surjection sending `(x, y) : M × S` to `f x * (f y)⁻¹`.

Equations
theorem submonoid.localization_map.mk'_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y₁ y₂ : S) :
f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂
theorem add_submonoid.localization_map.mk'_add {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x₁ x₂ : M) (y₁ y₂ : S) :
f.mk' (x₁ + x₂) (y₁ + y₂) = f.mk' x₁ y₁ + f.mk' x₂ y₂
theorem add_submonoid.localization_map.mk'_zero {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) :
f.mk' x 0 = (f.to_map) x
theorem submonoid.localization_map.mk'_one {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) :
f.mk' x 1 = (f.to_map) x
@[simp]
theorem add_submonoid.localization_map.mk'_sec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (z : N) :
f.mk' (f.sec z).fst (f.sec z).snd = z

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`.

@[simp]
theorem submonoid.localization_map.mk'_sec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :
f.mk' (f.sec z).fst (f.sec z).snd = z

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 submonoid.localization_map.mk'_surjective {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :
(x : M) (y : S), f.mk' x y = z
theorem add_submonoid.localization_map.mk'_surjective {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (z : N) :
(x : M) (y : S), f.mk' x y = z
theorem add_submonoid.localization_map.mk'_spec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
f.mk' x y + (f.to_map) y = (f.to_map) x
theorem submonoid.localization_map.mk'_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
f.mk' x y * (f.to_map) y = (f.to_map) x
theorem submonoid.localization_map.mk'_spec' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
(f.to_map) y * f.mk' x y = (f.to_map) x
theorem add_submonoid.localization_map.mk'_spec' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
(f.to_map) y + f.mk' x y = (f.to_map) x
theorem add_submonoid.localization_map.eq_mk'_iff_add_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x : M} {y : S} {z : N} :
z = f.mk' x y z + (f.to_map) y = (f.to_map) x
theorem submonoid.localization_map.eq_mk'_iff_mul_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x : M} {y : S} {z : N} :
z = f.mk' x y z * (f.to_map) y = (f.to_map) x
theorem add_submonoid.localization_map.mk'_eq_iff_eq_add {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x : M} {y : S} {z : N} :
f.mk' x y = z (f.to_map) x = z + (f.to_map) y
theorem submonoid.localization_map.mk'_eq_iff_eq_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x : M} {y : S} {z : N} :
f.mk' x y = z (f.to_map) x = z * (f.to_map) y
theorem submonoid.localization_map.mk'_eq_iff_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : S} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ (f.to_map) (y₂ * x₁) = (f.to_map) (y₁ * x₂)
theorem add_submonoid.localization_map.mk'_eq_iff_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : S} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ (f.to_map) (y₂ + x₁) = (f.to_map) (y₁ + x₂)
theorem submonoid.localization_map.mk'_eq_iff_eq' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : S} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ (f.to_map) (x₁ * y₂) = (f.to_map) (x₂ * y₁)
theorem add_submonoid.localization_map.mk'_eq_iff_eq' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : S} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ (f.to_map) (x₁ + y₂) = (f.to_map) (x₂ + y₁)
@[protected]
theorem submonoid.localization_map.eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} :
f.mk' a₁ a₂ = f.mk' b₁ b₂ (c : S), c * (b₂ * a₁) = c * (a₂ * b₁)
@[protected]
theorem add_submonoid.localization_map.eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} :
f.mk' a₁ a₂ = f.mk' b₁ b₂ (c : S), c + (b₂ + a₁) = c + (a₂ + b₁)
@[protected]
theorem add_submonoid.localization_map.eq' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} :
f.mk' a₁ a₂ = f.mk' b₁ b₂ (a₁, a₂) (b₁, b₂)
@[protected]
theorem submonoid.localization_map.eq' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} :
f.mk' a₁ a₂ = f.mk' b₁ b₂ (a₁, a₂) (b₁, b₂)
theorem submonoid.localization_map.eq_iff_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (g : S.localization_map P) {x y : M} :
(f.to_map) x = (f.to_map) y (g.to_map) x = (g.to_map) y
theorem add_submonoid.localization_map.eq_iff_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) (g : S.localization_map P) {x y : M} :
(f.to_map) x = (f.to_map) y (g.to_map) x = (g.to_map) y
theorem submonoid.localization_map.mk'_eq_iff_mk'_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (g : S.localization_map P) {x₁ x₂ : M} {y₁ y₂ : S} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ g.mk' x₁ y₁ = g.mk' x₂ y₂
theorem add_submonoid.localization_map.mk'_eq_iff_mk'_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) (g : S.localization_map P) {x₁ x₂ : M} {y₁ y₂ : S} :
f.mk' x₁ y₁ = f.mk' x₂ y₂ g.mk' x₁ y₁ = g.mk' x₂ y₂
theorem add_submonoid.localization_map.exists_of_sec_mk' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
(c : S), c + (((f.sec (f.mk' x y)).snd) + x) = c + (y + (f.sec (f.mk' x y)).fst)

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 submonoid.localization_map.exists_of_sec_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
(c : S), c * (((f.sec (f.mk' x y)).snd) * x) = c * (y * (f.sec (f.mk' x y)).fst)

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 add_submonoid.localization_map.mk'_eq_of_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} (H : a₂ + b₁ = b₂ + a₁) :
f.mk' a₁ a₂ = f.mk' b₁ b₂
theorem submonoid.localization_map.mk'_eq_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} (H : a₂ * b₁ = b₂ * a₁) :
f.mk' a₁ a₂ = f.mk' b₁ b₂
theorem submonoid.localization_map.mk'_eq_of_eq' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} (H : b₁ * a₂ = a₁ * b₂) :
f.mk' a₁ a₂ = f.mk' b₁ b₂
theorem add_submonoid.localization_map.mk'_eq_of_eq' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : S} (H : b₁ + a₂ = a₁ + b₂) :
f.mk' a₁ a₂ = f.mk' b₁ b₂
@[simp]
theorem add_submonoid.localization_map.mk'_self' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (y : S) :
f.mk' y y = 0
@[simp]
theorem submonoid.localization_map.mk'_self' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (y : S) :
f.mk' y y = 1
@[simp]
theorem add_submonoid.localization_map.mk'_self {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (H : x S) :
f.mk' x x, H⟩ = 0
@[simp]
theorem submonoid.localization_map.mk'_self {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (H : x S) :
f.mk' x x, H⟩ = 1
theorem submonoid.localization_map.mul_mk'_eq_mk'_of_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y : S) :
(f.to_map) x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y
theorem add_submonoid.localization_map.add_mk'_eq_mk'_of_add {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x₁ x₂ : M) (y : S) :
(f.to_map) x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y
theorem add_submonoid.localization_map.mk'_add_eq_mk'_of_add {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x₁ x₂ : M) (y : S) :
f.mk' x₂ y + (f.to_map) x₁ = f.mk' (x₁ + x₂) y
theorem submonoid.localization_map.mk'_mul_eq_mk'_of_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y : S) :
f.mk' x₂ y * (f.to_map) x₁ = f.mk' (x₁ * x₂) y
theorem add_submonoid.localization_map.add_mk'_zero_eq_mk' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
(f.to_map) x + f.mk' 0 y = f.mk' x y
theorem submonoid.localization_map.mul_mk'_one_eq_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
(f.to_map) x * f.mk' 1 y = f.mk' x y
@[simp]
theorem submonoid.localization_map.mk'_mul_cancel_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
f.mk' (x * y) y = (f.to_map) x
@[simp]
theorem add_submonoid.localization_map.mk'_add_cancel_right {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
f.mk' (x + y) y = (f.to_map) x
theorem add_submonoid.localization_map.mk'_add_cancel_left {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : M) (y : S) :
f.mk' (y + x) y = (f.to_map) x
theorem submonoid.localization_map.mk'_mul_cancel_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : S) :
f.mk' (y * x) y = (f.to_map) x
theorem submonoid.localization_map.is_unit_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (j : N →* P) (y : S) :
theorem add_submonoid.localization_map.is_add_unit_comp {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) (j : N →+ P) (y : S) :
theorem submonoid.localization_map.eq_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) {x y : M} (h : (f.to_map) x = (f.to_map) y) :
g x = g y

Given a localization map `f : M →* N` for a submonoid `S ⊆ M` and a map of `comm_monoid`s `g : M →* P` such that `g(S) ⊆ units P`, `f x = f y → g x = g y` for all `x y : M`.

theorem add_submonoid.localization_map.eq_of_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) {x y : M} (h : (f.to_map) x = (f.to_map) y) :
g x = g y

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M` and a map of `add_comm_monoid`s `g : M →+ P` such that `g(S) ⊆ add_units P`, `f x = f y → g x = g y` for all `x y : M`.

theorem submonoid.localization_map.comp_eq_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} {Q : Type u_4} [comm_monoid Q] (hg : (y : S), g y T) (k : T.localization_map Q) {x y : M} (h : (f.to_map) x = (f.to_map) y) :
(k.to_map) (g x) = (k.to_map) (g y)

Given `comm_monoid`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 add_submonoid.localization_map.comp_eq_of_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} {Q : Type u_4} (hg : (y : S), g y T) (k : T.localization_map Q) {x y : M} (h : (f.to_map) x = (f.to_map) y) :
(k.to_map) (g x) = (k.to_map) (g y)

Given `add_comm_monoid`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)`.

noncomputable def submonoid.localization_map.lift {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) :
N →* P

Given a localization map `f : M →* N` for a submonoid `S ⊆ M` and a map of `comm_monoid`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)⁻¹`.

Equations
noncomputable def add_submonoid.localization_map.lift {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) :
N →+ P

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M` and a map of `add_comm_monoid`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`.

Equations
theorem submonoid.localization_map.lift_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (x : M) (y : S) :
(f.lift hg) (f.mk' x y) = g x * ((is_unit.lift_right (g.restrict S) hg) y)⁻¹

Given a localization map `f : M →* N` for a submonoid `S ⊆ M` and a map of `comm_monoid`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 add_submonoid.localization_map.lift_mk' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (x : M) (y : S) :
(f.lift hg) (f.mk' x y) = g x + - hg) y

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M` and a map of `add_comm_monoid`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 submonoid.localization_map.lift_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (z : N) (v : P) :
(f.lift hg) z = v g (f.sec z).fst = g ((f.sec z).snd) * v

Given a localization map `f : M →* N` for a submonoid `S ⊆ M`, if a `comm_monoid` 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 add_submonoid.localization_map.lift_spec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (z : N) (v : P) :
(f.lift hg) z = v g (f.sec z).fst = g ((f.sec z).snd) + v

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M`, if an `add_comm_monoid` 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 submonoid.localization_map.lift_spec_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (z : N) (w v : P) :
(f.lift hg) z * w = v g (f.sec z).fst * w = g ((f.sec z).snd) * v

Given a localization map `f : M →* N` for a submonoid `S ⊆ M`, if a `comm_monoid` 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 add_submonoid.localization_map.lift_spec_add {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (z : N) (w v : P) :
(f.lift hg) z + w = v g (f.sec z).fst + w = g ((f.sec z).snd) + v

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M`, if an `add_comm_monoid` 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 add_submonoid.localization_map.lift_mk'_spec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (x : M) (v : P) (y : S) :
(f.lift hg) (f.mk' x y) = v g x = g y + v
theorem submonoid.localization_map.lift_mk'_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (x : M) (v : P) (y : S) :
(f.lift hg) (f.mk' x y) = v g x = g y * v
theorem submonoid.localization_map.lift_mul_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (z : N) :
(f.lift hg) z * g ((f.sec z).snd) = g (f.sec z).fst

Given a localization map `f : M →* N` for a submonoid `S ⊆ M`, if a `comm_monoid` 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 add_submonoid.localization_map.lift_add_right {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (z : N) :
(f.lift hg) z + g ((f.sec z).snd) = g (f.sec z).fst

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M`, if an `add_comm_monoid` 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 add_submonoid.localization_map.lift_add_left {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (z : N) :
g ((f.sec z).snd) + (f.lift hg) z = g (f.sec z).fst

Given a localization map `f : M →+ N` for a submonoid `S ⊆ M`, if an `add_comm_monoid` 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 submonoid.localization_map.lift_mul_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (z : N) :
g ((f.sec z).snd) * (f.lift hg) z = g (f.sec z).fst

Given a localization map `f : M →* N` for a submonoid `S ⊆ M`, if a `comm_monoid` 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`.

@[simp]
theorem submonoid.localization_map.lift_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) (x : M) :
(f.lift hg) ((f.to_map) x) = g x
@[simp]
theorem add_submonoid.localization_map.lift_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) (x : M) :
(f.lift hg) ((f.to_map) x) = g x
theorem submonoid.localization_map.lift_eq_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) {x y : M × S} :
(f.lift hg) (f.mk' x.fst x.snd) = (f.lift hg) (f.mk' y.fst y.snd) g (x.fst * (y.snd)) = g (y.fst * (x.snd))
theorem add_submonoid.localization_map.lift_eq_iff {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) {x y : M × S} :
(f.lift hg) (f.mk' x.fst x.snd) = (f.lift hg) (f.mk' y.fst y.snd) g (x.fst + (y.snd)) = g (y.fst + (x.snd))
@[simp]
theorem add_submonoid.localization_map.lift_comp {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) :
(f.lift hg).comp f.to_map = g
@[simp]
theorem submonoid.localization_map.lift_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) :
(f.lift hg).comp f.to_map = g
@[simp]
theorem add_submonoid.localization_map.lift_of_comp {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) (j : N →+ P) :
f.lift _ = j
@[simp]
theorem submonoid.localization_map.lift_of_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (j : N →* P) :
f.lift _ = j
theorem submonoid.localization_map.epic_of_localization_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {j k : N →* P} (h : (a : M), (j.comp f.to_map) a = (k.comp f.to_map) a) :
j = k
theorem add_submonoid.localization_map.epic_of_localization_map {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {j k : N →+ P} (h : (a : M), (j.comp f.to_map) a = (k.comp f.to_map) a) :
j = k
theorem add_submonoid.localization_map.lift_unique {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) {j : N →+ P} (hj : (x : M), j ((f.to_map) x) = g x) :
f.lift hg = j
theorem submonoid.localization_map.lift_unique {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) {j : N →* P} (hj : (x : M), j ((f.to_map) x) = g x) :
f.lift hg = j
@[simp]
theorem add_submonoid.localization_map.lift_id {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (x : N) :
(f.lift _) x = x
@[simp]
theorem submonoid.localization_map.lift_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : N) :
(f.lift _) x = x
@[simp]
theorem add_submonoid.localization_map.lift_left_inverse {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {k : S.localization_map P} (z : N) :
(k.lift _) ((f.lift _) z) = z

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`.

@[simp]
theorem submonoid.localization_map.lift_left_inverse {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} (z : N) :
(k.lift _) ((f.lift _) z) = z

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 add_submonoid.localization_map.lift_surjective_iff {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) :
function.surjective (f.lift hg) (v : P), (x : M × S), v + g (x.snd) = g x.fst
theorem submonoid.localization_map.lift_surjective_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) :
function.surjective (f.lift hg) (v : P), (x : M × S), v * g (x.snd) = g x.fst
theorem submonoid.localization_map.lift_injective_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : (y : S), is_unit (g y)) :
function.injective (f.lift hg) (x y : M), (f.to_map) x = (f.to_map) y g x = g y
theorem add_submonoid.localization_map.lift_injective_iff {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} (hg : (y : S), is_add_unit (g y)) :
function.injective (f.lift hg) (x y : M), (f.to_map) x = (f.to_map) y g x = g y
noncomputable def add_submonoid.localization_map.map {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} (k : T.localization_map Q) :
N →+ Q

Given a `add_comm_monoid` homomorphism `g : M →+ P` where for submonoids `S ⊆ M, T ⊆ P` we have `g(S) ⊆ T`, the induced add_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`.

Equations
noncomputable def submonoid.localization_map.map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] (k : T.localization_map Q) :
N →* Q

Given a `comm_monoid` 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)⁻¹`.

Equations
theorem submonoid.localization_map.map_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (x : M) :
(f.map hy k) ((f.to_map) x) = (k.to_map) (g x)
theorem add_submonoid.localization_map.map_eq {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} (x : M) :
(f.map hy k) ((f.to_map) x) = (k.to_map) (g x)
@[simp]
theorem add_submonoid.localization_map.map_comp {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} :
(f.map hy k).comp f.to_map = k.to_map.comp g
@[simp]
theorem submonoid.localization_map.map_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} :
(f.map hy k).comp f.to_map = k.to_map.comp g
theorem add_submonoid.localization_map.map_mk' {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} (x : M) (y : S) :
(f.map hy k) (f.mk' x y) = k.mk' (g x) g y, _⟩
theorem submonoid.localization_map.map_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (x : M) (y : S) :
(f.map hy k) (f.mk' x y) = k.mk' (g x) g y, _⟩
theorem add_submonoid.localization_map.map_spec {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} (z : N) (u : Q) :
(f.map hy k) z = u (k.to_map) (g (f.sec z).fst) = (k.to_map) (g ((f.sec z).snd)) + u

Given localization maps `f : M →+ N, k : P →+ Q` for submonoids `S, T` respectively, if an `add_comm_monoid` 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 submonoid.localization_map.map_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (z : N) (u : Q) :
(f.map hy k) z = u (k.to_map) (g (f.sec z).fst) = (k.to_map) (g ((f.sec z).snd)) * u

Given localization maps `f : M →* N, k : P →* Q` for submonoids `S, T` respectively, if a `comm_monoid` 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 submonoid.localization_map.map_mul_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (z : N) :
(f.map hy k) z * (k.to_map) (g ((f.sec z).snd)) = (k.to_map) (g (f.sec z).fst)

Given localization maps `f : M →* N, k : P →* Q` for submonoids `S, T` respectively, if a `comm_monoid` 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 add_submonoid.localization_map.map_add_right {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} (z : N) :
(f.map hy k) z + (k.to_map) (g ((f.sec z).snd)) = (k.to_map) (g (f.sec z).fst)

Given localization maps `f : M →+ N, k : P →+ Q` for submonoids `S, T` respectively, if an `add_comm_monoid` 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 add_submonoid.localization_map.map_add_left {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} (z : N) :
(k.to_map) (g ((f.sec z).snd)) + (f.map hy k) z = (k.to_map) (g (f.sec z).fst)

Given localization maps `f : M →+ N, k : P →+ Q` for submonoids `S, T` respectively, if an `add_comm_monoid` 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 submonoid.localization_map.map_mul_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (z : N) :
(k.to_map) (g ((f.sec z).snd)) * (f.map hy k) z = (k.to_map) (g (f.sec z).fst)

Given localization maps `f : M →* N, k : P →* Q` for submonoids `S, T` respectively, if a `comm_monoid` 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`.

@[simp]
theorem add_submonoid.localization_map.map_id {M : Type u_1} {S : add_submonoid M} {N : Type u_2} (f : S.localization_map N) (z : N) :
(f.map _ f) z = z
@[simp]
theorem submonoid.localization_map.map_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :
(f.map _ f) z = z
theorem add_submonoid.localization_map.map_comp_map {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} {A : Type u_5} {U : add_submonoid A} {R : Type u_6} (j : U.localization_map R) {l : P →+ A} (hl : (w : T), l w U) :
(k.map hl j).comp (f.map hy k) = f.map _ j

If `add_comm_monoid` 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 submonoid.localization_map.map_comp_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [comm_monoid A] {U : submonoid A} {R : Type u_6} [comm_monoid R] (j : U.localization_map R) {l : P →* A} (hl : (w : T), l w U) :
(k.map hl j).comp (f.map hy k) = f.map _ j

If `comm_monoid` 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 add_submonoid.localization_map.map_map {M : Type u_1} {S : add_submonoid M} {N : Type u_2} {P : Type u_3} (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : (y : S), g y T) {Q : Type u_4} {k : T.localization_map Q} {A : Type u_5} {U : add_submonoid A} {R : Type u_6} (j : U.localization_map R) {l : P →+ A} (hl : (w : T), l w U) (x : N) :
(k.map hl j) ((f.map hy k) x) = (f.map _ j) x

If `add_comm_monoid` 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 submonoid.localization_map.map_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : (y : S), g y T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [comm_monoid A] {U : submonoid A} {R : Type u_6} [comm_monoid R] (j : U.localization_map R) {l : P →* A} (hl : (w : T), l w U) (x : N) :
(k.map hl j) ((f.map hy k) x) = (f.map _ j) x

If `comm_monoid` 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`.

@[reducible]
def