mathlib3 documentation

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 #

Tags #

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

source
@[nolint]
structure add_submonoid.localization_map {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (N : Type u_2) [add_comm_monoid N] :
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
  • add_submonoid.localization_map.has_sizeof_inst
source
@[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
source
def add_localization.r {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
add_con (M × ↥S)

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
source
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
source
def add_localization.r' {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
add_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
source
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
source
theorem localization.r_eq_r' {M : Type u_1} [comm_monoid M] (S : submonoid M) :
localization.r S = localization.r' S

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').

source
theorem add_localization.r_eq_r' {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
add_localization.r S = add_localization.r' S

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').

source
theorem add_localization.r_iff_exists {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {x y : M × ↥S} :
⇑(add_localization.r S) x y ↔ ∃ (c : ↥S), ↑c + (↑(y.snd) + x.fst) = ↑c + (↑(x.snd) + y.fst)
source
theorem localization.r_iff_exists {M : Type u_1} [comm_monoid M] {S : submonoid M} {x y : M × ↥S} :
⇑(localization.r S) x y ↔ ∃ (c : ↥S), ↑c * (↑(y.snd) * x.fst) = ↑c * (↑(x.snd) * y.fst)
source
@[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
source
def add_localization {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
Type u_1

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

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

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

Equations
source
@[protected]
def add_localization.add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
add_localization S → add_localization S → add_localization S

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
source
@[protected, instance]
def localization.has_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) :
has_mul (localization S)
Equations
source
@[protected, instance]
def add_localization.has_add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
has_add (add_localization S)
Equations
source
@[protected, irreducible]
def localization.one {M : Type u_1} [comm_monoid M] (S : submonoid M) :
localization S

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

Equations
source
@[protected]
def add_localization.zero {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
add_localization S

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
source
@[protected, instance]
def add_localization.has_zero {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
has_zero (add_localization S)
Equations
source
@[protected, instance]
def localization.has_one {M : Type u_1} [comm_monoid M] (S : submonoid M) :
has_one (localization S)
Equations
source
@[protected, irreducible]
def localization.npow {M : Type u_1} [comm_monoid M] (S : submonoid M) :
ℕ → localization S → localization S

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
source
@[protected]
def add_localization.nsmul {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
ℕ → add_localization S → add_localization S

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
source
@[protected, instance]
def add_localization.add_comm_monoid {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
add_comm_monoid (add_localization S)
Equations
source
@[protected, instance]
def localization.comm_monoid {M : Type u_1} [comm_monoid M] (S : submonoid M) :
comm_monoid (localization S)
Equations
source
def localization.mk {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) (y : ↥S) :
localization 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
source
def add_localization.mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (x : M) (y : ↥S) :
add_localization 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
source
theorem add_localization.mk_eq_mk_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {a c : M} {b d : ↥S} :
add_localization.mk a b = add_localization.mk c d ↔ ⇑(add_localization.r S) (a, b) (c, d)
source
theorem localization.mk_eq_mk_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {a c : M} {b d : ↥S} :
localization.mk a b = localization.mk c d ↔ ⇑(localization.r S) (a, b) (c, d)
source
def localization.rec {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Sort u} (f : Π (a : M) (b : ↥S), p (localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(localization.r S) (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
source
def add_localization.rec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Sort u} (f : Π (a : M) (b : ↥S), p (add_localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(add_localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (x : add_localization S) :
p x

Dependent recursion principle for add_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 add_localization S.

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

Copy of quotient.rec_on_subsingleton₂ for localization

Equations
source
def add_localization.rec_on_subsingleton₂ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {r : add_localization S → add_localization S → Sort u} [h : ∀ (a c : M) (b d : ↥S), subsingleton (r (add_localization.mk a b) (add_localization.mk c d))] (x y : add_localization S) (f : Π (a c : M) (b d : ↥S), r (add_localization.mk a b) (add_localization.mk c d)) :
r x y

Copy of quotient.rec_on_subsingleton₂ for add_localization

Equations
source
theorem add_localization.mk_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (a c : M) (b d : ↥S) :
add_localization.mk a b + add_localization.mk c d = add_localization.mk (a + c) (b + d)
source
theorem localization.mk_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} (a c : M) (b d : ↥S) :
localization.mk a b * localization.mk c d = localization.mk (a * c) (b * d)
source
theorem localization.mk_one {M : Type u_1} [comm_monoid M] {S : submonoid M} :
localization.mk 1 1 = 1
source
theorem add_localization.mk_zero {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} :
add_localization.mk 0 0 = 0
source
theorem localization.mk_pow {M : Type u_1} [comm_monoid M] {S : submonoid M} (n : ℕ) (a : M) (b : ↥S) :
localization.mk a b ^ n = localization.mk (a ^ n) (b ^ n)
source
theorem add_localization.mk_nsmul {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (n : ℕ) (a : M) (b : ↥S) :
n • add_localization.mk a b = add_localization.mk (n • a) (n • b)
source
@[simp]
theorem add_localization.rec_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Sort u} (f : Π (a : M) (b : ↥S), p (add_localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(add_localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (a : M) (b : ↥S) :
add_localization.rec f H (add_localization.mk a b) = f a b
source
@[simp]
theorem localization.rec_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Sort u} (f : Π (a : M) (b : ↥S), p (localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (a : M) (b : ↥S) :
localization.rec f H (localization.mk a b) = f a b
source
def add_localization.lift_on {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (x : add_localization S) (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(add_localization.r 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
source
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}, ⇑(localization.r 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
source
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}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :
(localization.mk a b).lift_on f H = f a b
source
theorem add_localization.lift_on_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(add_localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :
(add_localization.mk a b).lift_on f H = f a b
source
theorem add_localization.ind {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Prop} (H : ∀ (y : M × ↥S), p (add_localization.mk y.fst y.snd)) (x : add_localization S) :
p x
source
theorem localization.ind {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Prop} (H : ∀ (y : M × ↥S), p (localization.mk y.fst y.snd)) (x : localization S) :
p x
source
theorem localization.induction_on {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Prop} (x : localization S) (H : ∀ (y : M × ↥S), p (localization.mk y.fst y.snd)) :
p x
source
theorem add_localization.induction_on {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Prop} (x : add_localization S) (H : ∀ (y : M × ↥S), p (add_localization.mk y.fst y.snd)) :
p x
source
def add_localization.lift_on₂ {M : Type u_1} [add_comm_monoid M] {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}, ⇑(add_localization.r S) (a, b) (a', b') → ⇑(add_localization.r S) (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
source
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}, ⇑(localization.r S) (a, b) (a', b') → ⇑(localization.r S) (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
source
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}, ⇑(localization.r S) (a, b) (a', b') → ⇑(localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :
(localization.mk a b).lift_on₂ (localization.mk c d) f H = f a b c d
source
theorem add_localization.lift_on₂_mk {M : Type u_1} [add_comm_monoid M] {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}, ⇑(add_localization.r S) (a, b) (a', b') → ⇑(add_localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :
(add_localization.mk a b).lift_on₂ (add_localization.mk c d) f H = f a b c d
source
theorem localization.induction_on₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → localization S → Prop} (x y : localization S) (H : ∀ (x y : M × ↥S), p (localization.mk x.fst x.snd) (localization.mk y.fst y.snd)) :
p x y
source
theorem add_localization.induction_on₂ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → add_localization S → Prop} (x y : add_localization S) (H : ∀ (x y : M × ↥S), p (add_localization.mk x.fst x.snd) (add_localization.mk y.fst y.snd)) :
p x y
source
theorem add_localization.induction_on₃ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → add_localization S → add_localization S → Prop} (x y z : add_localization S) (H : ∀ (x y z : M × ↥S), p (add_localization.mk x.fst x.snd) (add_localization.mk y.fst y.snd) (add_localization.mk z.fst z.snd)) :
p x y z
source
theorem localization.induction_on₃ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → localization S → localization S → Prop} (x y z : localization S) (H : ∀ (x y z : M × ↥S), p (localization.mk x.fst x.snd) (localization.mk y.fst y.snd) (localization.mk z.fst z.snd)) :
p x y z
source
theorem localization.one_rel {M : Type u_1} [comm_monoid M] {S : submonoid M} (y : ↥S) :
⇑(localization.r S) 1 (↑y, y)
source
theorem add_localization.zero_rel {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (y : ↥S) :
⇑(add_localization.r S) 0 (↑y, y)
source
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) :
⇑(localization.r S) x y
source
theorem add_localization.r_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {x y : M × ↥S} (h : ↑(y.snd) + x.fst = ↑(x.snd) + y.fst) :
⇑(add_localization.r S) x y
source
theorem add_localization.mk_self {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (a : ↥S) :
add_localization.mk ↑a a = 0
source
theorem localization.mk_self {M : Type u_1} [comm_monoid M] {S : submonoid M} (a : ↥S) :
localization.mk ↑a a = 1
source
@[protected, irreducible]
def localization.smul {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [is_scalar_tower R M M] (c : R) (z : localization S) :
localization S

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

Equations
source
@[protected, instance]
def localization.has_smul {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [is_scalar_tower R M M] :
has_smul R (localization S)
Equations
source
theorem localization.smul_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [is_scalar_tower R M M] (c : R) (a : M) (b : ↥S) :
c • localization.mk a b = localization.mk (c • a) b
source
@[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] [is_scalar_tower R₁ M M] [is_scalar_tower R₂ M M] [smul_comm_class R₁ R₂ M] :
smul_comm_class R₁ R₂ (localization S)
source
@[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] [is_scalar_tower R₁ M M] [is_scalar_tower R₂ M M] [has_smul R₁ R₂] [is_scalar_tower R₁ R₂ M] :
is_scalar_tower R₁ R₂ (localization S)
source
@[protected, instance]
def localization.smul_comm_class_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_2} [has_smul R M] [is_scalar_tower R M M] :
smul_comm_class R (localization S) (localization S)
source
@[protected, instance]
def localization.is_scalar_tower_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_2} [has_smul R M] [is_scalar_tower R M M] :
is_scalar_tower R (localization S) (localization S)
source
@[protected, instance]
def localization.is_central_scalar {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [has_smul Rᵐᵒᵖ M] [is_scalar_tower R M M] [is_scalar_tower Rᵐᵒᵖ M M] [is_central_scalar R M] :
is_central_scalar R (localization S)
source
@[protected, instance]
def localization.mul_action {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [monoid R] [mul_action R M] [is_scalar_tower R M M] :
mul_action R (localization S)
Equations
source
@[protected, instance]
def localization.mul_distrib_mul_action {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [monoid R] [mul_distrib_mul_action R M] [is_scalar_tower R M M] :
mul_distrib_mul_action R (localization S)
Equations
source
def add_monoid_hom.to_localization_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (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) :
S.localization_map N

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

Equations
source
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) :
S.localization_map N

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

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

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

source
@[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.

source
@[ext]
theorem add_submonoid.localization_map.ext {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f g : S.localization_map N} (h : ∀ (x : M), ⇑(f.to_map) x = ⇑(g.to_map) x) :
f = g
source
@[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
source
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
source
theorem add_submonoid.localization_map.ext_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f g : S.localization_map N} :
f = g ↔ ∀ (x : M), ⇑(f.to_map) x = ⇑(g.to_map) x
source
theorem add_submonoid.localization_map.to_map_injective {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] :
function.injective add_submonoid.localization_map.to_map
source
theorem submonoid.localization_map.to_map_injective {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] :
function.injective submonoid.localization_map.to_map
source
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) :
is_unit (⇑(f.to_map) ↑y)
source
theorem add_submonoid.localization_map.map_add_units {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (y : ↥S) :
is_add_unit (⇑(f.to_map) ↑y)
source
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
source
theorem add_submonoid.localization_map.surj {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :
∃ (x : M × ↥S), z + ⇑(f.to_map) ↑(x.snd) = ⇑(f.to_map) x.fst
source
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
source
theorem add_submonoid.localization_map.eq_iff_exists {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
noncomputable def add_submonoid.localization_map.sec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
theorem add_submonoid.localization_map.sec_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
theorem add_submonoid.localization_map.sec_spec' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
theorem add_submonoid.localization_map.add_neg_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) (y : ↥S) (w z : N) :
w + ↑-⇑(is_add_unit.lift_right (f.restrict S) 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.

source
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) :
w * ↑(⇑(is_unit.lift_right (f.restrict S) h) y)⁻¹ = z ↔ w = ⇑f ↑y * z

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.

source
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) :
z = w * ↑(⇑(is_unit.lift_right (f.restrict S) h) y)⁻¹ ↔ z * ⇑f ↑y = w

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.

source
theorem add_submonoid.localization_map.add_neg_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) (y : ↥S) (w z : N) :
z = w + ↑-⇑(is_add_unit.lift_right (f.restrict S) 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.

source
@[simp]
theorem add_submonoid.localization_map.add_neg {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S} :
⇑f x₁ + ↑-⇑(is_add_unit.lift_right (f.restrict S) h) y₁ = ⇑f x₂ + ↑-⇑(is_add_unit.lift_right (f.restrict S) 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₁).

source
@[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₁).

source
theorem add_submonoid.localization_map.neg_inj {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (hf : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) {y z : ↥S} (h : -⇑(is_add_unit.lift_right (f.restrict S) hf) y = -⇑(is_add_unit.lift_right (f.restrict S) hf) z) :
⇑f ↑y = ⇑f ↑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.

source
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)⁻¹) :
⇑f ↑y = ⇑f ↑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.

source
theorem add_submonoid.localization_map.neg_unique {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) {y : ↥S} {z : N} (H : ⇑f ↑y + z = 0) :
↑-⇑(is_add_unit.lift_right (f.restrict S) 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.

source
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) :
↑(⇑(is_unit.lift_right (f.restrict S) h) y)⁻¹ = z

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

source
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
source
theorem add_submonoid.localization_map.map_right_cancel {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
theorem add_submonoid.localization_map.map_left_cancel {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
noncomputable def add_submonoid.localization_map.mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
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₂
source
theorem add_submonoid.localization_map.mk'_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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₂
source
theorem add_submonoid.localization_map.mk'_zero {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) :
f.mk' x 0 = ⇑(f.to_map) x
source
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
source
@[simp]
theorem add_submonoid.localization_map.mk'_sec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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.

source
@[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.

source
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
source
theorem add_submonoid.localization_map.mk'_surjective {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :
∃ (x : M) (y : ↥S), f.mk' x y = z
source
theorem add_submonoid.localization_map.mk'_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :
f.mk' x y + ⇑(f.to_map) ↑y = ⇑(f.to_map) x
source
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
source
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
source
theorem add_submonoid.localization_map.mk'_spec' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :
⇑(f.to_map) ↑y + f.mk' x y = ⇑(f.to_map) x
source
theorem add_submonoid.localization_map.eq_mk'_iff_add_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
theorem add_submonoid.localization_map.mk'_eq_iff_eq_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
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₂)
source
theorem add_submonoid.localization_map.mk'_eq_iff_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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₂)
source
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₁)
source
theorem add_submonoid.localization_map.mk'_eq_iff_eq' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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₁)
source
@[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₁)
source
@[protected]
theorem add_submonoid.localization_map.eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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₁)
source
@[protected]
theorem add_submonoid.localization_map.eq' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} :
f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ⇑(add_localization.r S) (a₁, a₂) (b₁, b₂)
source
@[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₂ ↔ ⇑(localization.r S) (a₁, a₂) (b₁, b₂)
source
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
source
theorem add_submonoid.localization_map.eq_iff_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_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
source
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₂
source
theorem add_submonoid.localization_map.mk'_eq_iff_mk'_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_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₂
source
theorem add_submonoid.localization_map.exists_of_sec_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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.

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

source
theorem add_submonoid.localization_map.mk'_eq_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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₂
source
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₂
source
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₂
source
theorem add_submonoid.localization_map.mk'_eq_of_eq' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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₂
source
@[simp]
theorem add_submonoid.localization_map.mk'_self' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (y : ↥S) :
f.mk' ↑y y = 0
source
@[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
source
@[simp]
theorem add_submonoid.localization_map.mk'_self {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (H : x ∈ S) :
f.mk' x ⟨x, H⟩ = 0
source
@[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
source
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
source
theorem add_submonoid.localization_map.add_mk'_eq_mk'_of_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
theorem add_submonoid.localization_map.mk'_add_eq_mk'_of_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_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
source
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
source
theorem add_submonoid.localization_map.add_mk'_zero_eq_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :
⇑(f.to_map) x + f.mk' 0 y = f.mk' x y
source
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
source
@[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
source
@[simp]
theorem add_submonoid.localization_map.mk'_add_cancel_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :
f.mk' (x + ↑y) y = ⇑(f.to_map) x
source
theorem add_submonoid.localization_map.mk'_add_cancel_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :
f.mk' (↑y + x) y = ⇑(f.to_map) x
source
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
source
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) :
is_unit (⇑(j.comp f.to_map) ↑y)
source
theorem add_submonoid.localization_map.is_add_unit_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (j : N →+ P) (y : ↥S) :
is_add_unit (⇑(j.comp f.to_map) ↑y)
source
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_monoids g : M →* P such that g(S) ⊆ units P, f x = f y → g x = g y for all x y : M.

source
theorem add_submonoid.localization_map.eq_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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_monoids g : M →+ P such that g(S) ⊆ add_units P, f x = f y → g x = g y for all x y : M.

source
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_monoids 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).

source
theorem add_submonoid.localization_map.comp_eq_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} {Q : Type u_4} [add_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 add_comm_monoids 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).

source
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_monoids 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
source
noncomputable def add_submonoid.localization_map.lift {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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_monoids 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
source
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_monoids 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.

source
theorem add_submonoid.localization_map.lift_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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 + ↑-⇑(is_add_unit.lift_right (g.restrict S) hg) y

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

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

source
theorem add_submonoid.localization_map.lift_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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.

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

source
theorem add_submonoid.localization_map.lift_spec_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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.

source
theorem add_submonoid.localization_map.lift_mk'_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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
source
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
source
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.

source
theorem add_submonoid.localization_map.lift_add_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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.

source
theorem add_submonoid.localization_map.lift_add_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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.

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

source
@[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
source
@[simp]
theorem add_submonoid.localization_map.lift_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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
source
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))
source
theorem add_submonoid.localization_map.lift_eq_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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))
source
@[simp]
theorem add_submonoid.localization_map.lift_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) :
(f.lift hg).comp f.to_map = g
source
@[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
source
@[simp]
theorem add_submonoid.localization_map.lift_of_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (j : N →+ P) :
f.lift _ = j
source
@[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
source
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
source
theorem add_submonoid.localization_map.epic_of_localization_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_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
source
theorem add_submonoid.localization_map.lift_unique {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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
source
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
source
@[simp]
theorem add_submonoid.localization_map.lift_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : N) :
⇑(f.lift _) x = x
source
@[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
source
@[simp]
theorem add_submonoid.localization_map.lift_left_inverse {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_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.

source
@[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.

source
theorem add_submonoid.localization_map.lift_surjective_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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
source
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
source
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
source
theorem add_submonoid.localization_map.lift_injective_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (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
source
noncomputable def add_submonoid.localization_map.map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] (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
source
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
source
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)
source
theorem add_submonoid.localization_map.map_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} (x : M) :
⇑(f.map hy k) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑g x)
source
@[simp]
theorem add_submonoid.localization_map.map_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} :
(f.map hy k).comp f.to_map = k.to_map.comp g
source
@[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
source
theorem add_submonoid.localization_map.map_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_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, _⟩
source
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, _⟩
source
theorem add_submonoid.localization_map.map_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_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 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.

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

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

source
theorem add_submonoid.localization_map.map_add_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_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 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.

source
theorem add_submonoid.localization_map.map_add_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_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 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.

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

source
@[simp]
theorem add_submonoid.localization_map.map_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :
⇑(f.map _ f) z = z
source
@[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
source
theorem add_submonoid.localization_map.map_comp_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [add_comm_monoid A] {U : add_submonoid A} {R : Type u_6} [add_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 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.

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

source
theorem add_submonoid.localization_map.map_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [add_comm_monoid A] {U : add_submonoid A} {R : Type u_6} [add_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 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.

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

source
@[reducible]
def submonoid.localization_map.away_map {M : Type u_1} [comm_monoid M] (x : M) (N' : Type u_2) [comm_monoid N'] :
Type (max u_1 u_2)

Given x : M, the type of comm_monoid homomorphisms f : M →* N such that N is isomorphic to the localization of M at the submonoid generated by x.

Equations
source
@[reducible]
def add_submonoid.localization_map.away_map {M : Type u_1} [add_comm_monoid M] (x : M) (N' : Type u_2) [add_comm_monoid N'] :
Type (max u_1 u_2)

Given x : M, the type of add_comm_monoid homomorphisms f : M →+ N such that N is isomorphic to the localization of M at the submonoid generated by x.

Equations
source
noncomputable def submonoid.localization_map.away_map.inv_self {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] (x : M) (F : submonoid.localization_map.away_map x N) :
N

Given x : M and a localization map F : M →* N away from x, inv_self is (F x)⁻¹.

Equations
source
noncomputable def submonoid.localization_map.away_map.lift {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] {g : M →* P} (x : M) (F : submonoid.localization_map.away_map x N) (hg : is_unit (⇑g x)) :
N →* P

Given x : M, a localization map F : M →* N away from x, and a map of comm_monoids g : M →* P such that g x is invertible, the homomorphism induced from N to P sending z : N to g y * (g x)⁻ⁿ, where y : M, n : ℕ are such that z = F y * (F x)⁻ⁿ.

Equations
source
@[simp]
theorem submonoid.localization_map.away_map.lift_eq {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] {g : M →* P} (x : M) (F : submonoid.localization_map.away_map x N) (hg : is_unit (⇑g x)) (a : M) :
⇑(submonoid.localization_map.away_map.lift x F hg) (⇑(submonoid.localization_map.to_map F) a) = ⇑g a
source
@[simp]
theorem submonoid.localization_map.away_map.lift_comp {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] {g : M →* P} (x : M) (F : submonoid.localization_map.away_map x N) (hg : is_unit (⇑g x)) :
(submonoid.localization_map.away_map.lift x F hg).comp (submonoid.localization_map.to_map F) = g
source
noncomputable def submonoid.localization_map.away_to_away_right {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (x : M) (F : submonoid.localization_map.away_map x N) (y : M) (G : submonoid.localization_map.away_map (x * y) P) :
N →* P

Given x y : M and localization maps F : M →* N, G : M →* P away from x and x * y respectively, the homomorphism induced from N to P.

Equations
source
noncomputable def add_submonoid.localization_map.away_map.neg_self {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) :
B

Given x : A and a localization map F : A →+ B away from x, neg_self is - (F x).

Equations
source
noncomputable def add_submonoid.localization_map.away_map.lift {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] {g : A →+ C} (hg : is_add_unit (⇑g x)) :
B →+ C

Given x : A, a localization map F : A →+ B away from x, and a map of add_comm_monoids g : A →+ C such that g x is invertible, the homomorphism induced from B to C sending z : B to g y - n • g x, where y : A, n : ℕ are such that z = F y - n • F x.

Equations
source
@[simp]
theorem add_submonoid.localization_map.away_map.lift_eq {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] {g : A →+ C} (hg : is_add_unit (⇑g x)) (a : A) :
⇑(add_submonoid.localization_map.away_map.lift x F hg) (⇑(add_submonoid.localization_map.to_map F) a) = ⇑g a
source
@[simp]
theorem add_submonoid.localization_map.away_map.lift_comp {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] {g : A →+ C} (hg : is_add_unit (⇑g x)) :
(add_submonoid.localization_map.away_map.lift x F hg).comp (add_submonoid.localization_map.to_map F) = g
source
noncomputable def add_submonoid.localization_map.away_to_away_right {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] (y : A) (G : add_submonoid.localization_map.away_map (x + y) C) :
B →+ C

Given x y : A and localization maps F : A →+ B, G : A →+ C away from x and x + y respectively, the homomorphism induced from B to C.

Equations
source
noncomputable def add_submonoid.localization_map.add_equiv_of_localizations {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : S.localization_map P) :
N ≃+ P

If f : M →+ N and k : M →+ R are localization maps for a submonoid S, we get an isomorphism of N and R.

Equations
source
noncomputable def submonoid.localization_map.mul_equiv_of_localizations {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) :
N ≃* P

If f : M →* N and k : M →* P are localization maps for a submonoid S, we get an isomorphism of N and P.

Equations
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_localizations_apply {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} {x : N} :
⇑(f.mul_equiv_of_localizations k) x = ⇑(f.lift _) x
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_localizations_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : N} :
⇑(f.add_equiv_of_localizations k) x = ⇑(f.lift _) x
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_localizations_symm_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : P} :
⇑((f.add_equiv_of_localizations k).symm) x = ⇑(k.lift _) x
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_localizations_symm_apply {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} {x : P} :
⇑((f.mul_equiv_of_localizations k).symm) x = ⇑(k.lift _) x
source
theorem add_submonoid.localization_map.add_equiv_of_localizations_symm_eq_add_equiv_of_localizations {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} :
(k.add_equiv_of_localizations f).symm = f.add_equiv_of_localizations k
source
theorem submonoid.localization_map.mul_equiv_of_localizations_symm_eq_mul_equiv_of_localizations {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} :
(k.mul_equiv_of_localizations f).symm = f.mul_equiv_of_localizations k
source
def add_submonoid.localization_map.of_add_equiv_of_localizations {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : N ≃+ P) :
S.localization_map P

If f : M →+ N is a localization map for a submonoid S and k : N ≃+ P is an isomorphism of add_comm_monoids, k ∘ f is a localization map for M at S.

Equations
source
def submonoid.localization_map.of_mul_equiv_of_localizations {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 : N ≃* P) :
S.localization_map P

If f : M →* N is a localization map for a submonoid S and k : N ≃* P is an isomorphism of comm_monoids, k ∘ f is a localization map for M at S.

Equations
source
@[simp]
theorem add_submonoid.localization_map.of_add_equiv_of_localizations_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} (x : M) :
⇑((f.of_add_equiv_of_localizations k).to_map) x = ⇑k (⇑(f.to_map) x)
source
@[simp]
theorem submonoid.localization_map.of_mul_equiv_of_localizations_apply {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 : N ≃* P} (x : M) :
⇑((f.of_mul_equiv_of_localizations k).to_map) x = ⇑k (⇑(f.to_map) x)
source
theorem add_submonoid.localization_map.of_add_equiv_of_localizations_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} :
(f.of_add_equiv_of_localizations k).to_map = k.to_add_monoid_hom.comp f.to_map
source
theorem submonoid.localization_map.of_mul_equiv_of_localizations_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) {k : N ≃* P} :
(f.of_mul_equiv_of_localizations k).to_map = k.to_monoid_hom.comp f.to_map
source
theorem submonoid.localization_map.symm_comp_of_mul_equiv_of_localizations_apply {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 : N ≃* P} (x : M) :
⇑(k.symm) (⇑((f.of_mul_equiv_of_localizations k).to_map) x) = ⇑(f.to_map) x
source
theorem add_submonoid.localization_map.symm_comp_of_add_equiv_of_localizations_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} (x : M) :
⇑(k.symm) (⇑((f.of_add_equiv_of_localizations k).to_map) x) = ⇑(f.to_map) x
source
theorem add_submonoid.localization_map.symm_comp_of_add_equiv_of_localizations_apply' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : P ≃+ N} (x : M) :
⇑k (⇑((f.of_add_equiv_of_localizations k.symm).to_map) x) = ⇑(f.to_map) x
source
theorem submonoid.localization_map.symm_comp_of_mul_equiv_of_localizations_apply' {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 : P ≃* N} (x : M) :
⇑k (⇑((f.of_mul_equiv_of_localizations k.symm).to_map) x) = ⇑(f.to_map) x
source
theorem add_submonoid.localization_map.of_add_equiv_of_localizations_eq_iff_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} {x : M} {y : P} :
⇑((f.of_add_equiv_of_localizations k).to_map) x = y ↔ ⇑(f.to_map) x = ⇑(k.symm) y
source
theorem submonoid.localization_map.of_mul_equiv_of_localizations_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) {k : N ≃* P} {x : M} {y : P} :
⇑((f.of_mul_equiv_of_localizations k).to_map) x = y ↔ ⇑(f.to_map) x = ⇑(k.symm) y
source
theorem submonoid.localization_map.mul_equiv_of_localizations_right_inv {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) :
f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k) = k
source
theorem add_submonoid.localization_map.add_equiv_of_localizations_right_inv {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : S.localization_map P) :
f.of_add_equiv_of_localizations (f.add_equiv_of_localizations k) = k
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_localizations_right_inv_apply {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} {x : M} :
⇑((f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k)).to_map) x = ⇑(k.to_map) x
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_localizations_right_inv_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : M} :
⇑((f.of_add_equiv_of_localizations (f.add_equiv_of_localizations k)).to_map) x = ⇑(k.to_map) x
source
theorem submonoid.localization_map.mul_equiv_of_localizations_left_inv {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 : N ≃* P) :
f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k) = k
source
theorem add_submonoid.localization_map.add_equiv_of_localizations_left_neg {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : N ≃+ P) :
f.add_equiv_of_localizations (f.of_add_equiv_of_localizations k) = k
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_localizations_left_inv_apply {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 : N ≃* P} (x : N) :
⇑(f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k)) x = ⇑k x
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_localizations_left_neg_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} (x : N) :
⇑(f.add_equiv_of_localizations (f.of_add_equiv_of_localizations k)) x = ⇑k x
source
@[simp]
theorem add_submonoid.localization_map.of_add_equiv_of_localizations_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :
f.of_add_equiv_of_localizations (add_equiv.refl N) = f
source
@[simp]
theorem submonoid.localization_map.of_mul_equiv_of_localizations_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :
f.of_mul_equiv_of_localizations (mul_equiv.refl N) = f
source
theorem submonoid.localization_map.of_mul_equiv_of_localizations_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) {Q : Type u_4} [comm_monoid Q] {k : N ≃* P} {j : P ≃* Q} :
(f.of_mul_equiv_of_localizations (k.trans j)).to_map = j.to_monoid_hom.comp (f.of_mul_equiv_of_localizations k).to_map
source
theorem add_submonoid.localization_map.of_add_equiv_of_localizations_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {Q : Type u_4} [add_comm_monoid Q] {k : N ≃+ P} {j : P ≃+ Q} :
(f.of_add_equiv_of_localizations (k.trans j)).to_map = j.to_add_monoid_hom.comp (f.of_add_equiv_of_localizations k).to_map
source
def add_submonoid.localization_map.of_add_equiv_of_dom {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) :
T.localization_map N

Given comm_monoids 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 comm_monoids such that k(T) = S, f ∘ k is a localization map for T.

Equations
source
def submonoid.localization_map.of_mul_equiv_of_dom {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) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) :
T.localization_map N

Given comm_monoids 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 comm_monoids such that k(T) = S, f ∘ k is a localization map for T.

Equations
source
@[simp]
theorem add_submonoid.localization_map.of_add_equiv_of_dom_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) (x : P) :
⇑((f.of_add_equiv_of_dom H).to_map) x = ⇑(f.to_map) (⇑k x)
source
@[simp]
theorem submonoid.localization_map.of_mul_equiv_of_dom_apply {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) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) (x : P) :
⇑((f.of_mul_equiv_of_dom H).to_map) x = ⇑(f.to_map) (⇑k x)
source
theorem submonoid.localization_map.of_mul_equiv_of_dom_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) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) :
(f.of_mul_equiv_of_dom H).to_map = f.to_map.comp k.to_monoid_hom
source
theorem add_submonoid.localization_map.of_add_equiv_of_dom_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) :
(f.of_add_equiv_of_dom H).to_map = f.to_map.comp k.to_add_monoid_hom
source
theorem add_submonoid.localization_map.of_add_equiv_of_dom_comp_symm {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) (x : M) :
⇑((f.of_add_equiv_of_dom H).to_map) (⇑(k.symm) x) = ⇑(f.to_map) x
source
theorem submonoid.localization_map.of_mul_equiv_of_dom_comp_symm {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) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) (x : M) :
⇑((f.of_mul_equiv_of_dom H).to_map) (⇑(k.symm) x) = ⇑(f.to_map) x
source
theorem add_submonoid.localization_map.of_add_equiv_of_dom_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : M ≃+ P} (H : add_submonoid.map k.symm.to_add_monoid_hom T = S) (x : M) :
⇑((f.of_add_equiv_of_dom H).to_map) (⇑k x) = ⇑(f.to_map) x
source
theorem submonoid.localization_map.of_mul_equiv_of_dom_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) {T : submonoid P} {k : M ≃* P} (H : submonoid.map k.symm.to_monoid_hom T = S) (x : M) :
⇑((f.of_mul_equiv_of_dom H).to_map) (⇑k x) = ⇑(f.to_map) x
source
@[simp]
theorem submonoid.localization_map.of_mul_equiv_of_dom_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :
f.of_mul_equiv_of_dom _ = f

A special case of f ∘ id = f, f a localization map.

source
@[simp]
theorem add_submonoid.localization_map.of_add_equiv_of_dom_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :
f.of_add_equiv_of_dom _ = f

A special case of f ∘ id = f, f a localization map.

source
noncomputable def submonoid.localization_map.mul_equiv_of_mul_equiv {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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] (k : T.localization_map Q) {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) :
N ≃* Q

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.

Equations
source
noncomputable def add_submonoid.localization_map.add_equiv_of_add_equiv {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] (k : T.localization_map Q) {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) :
N ≃+ Q

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.

Equations
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_add_equiv_eq_map_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : N) :
⇑(f.add_equiv_of_add_equiv k H) x = ⇑(f.map _ k) x
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_mul_equiv_eq_map_apply {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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : N) :
⇑(f.mul_equiv_of_mul_equiv k H) x = ⇑(f.map _ k) x
source
theorem add_submonoid.localization_map.add_equiv_of_add_equiv_eq_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) :
(f.add_equiv_of_add_equiv k H).to_add_monoid_hom = f.map _ k
source
theorem submonoid.localization_map.mul_equiv_of_mul_equiv_eq_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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) :
(f.mul_equiv_of_mul_equiv k H).to_monoid_hom = f.map _ k
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_add_equiv_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : M) :
⇑(f.add_equiv_of_add_equiv k H) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑j x)
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_mul_equiv_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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : M) :
⇑(f.mul_equiv_of_mul_equiv k H) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑j x)
source
@[simp]
theorem add_submonoid.localization_map.add_equiv_of_add_equiv_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : M) (y : ↥S) :
⇑(f.add_equiv_of_add_equiv k H) (f.mk' x y) = k.mk' (⇑j x) ⟨⇑j ↑y, _⟩
source
@[simp]
theorem submonoid.localization_map.mul_equiv_of_mul_equiv_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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : M) (y : ↥S) :
⇑(f.mul_equiv_of_mul_equiv k H) (f.mk' x y) = k.mk' (⇑j x) ⟨⇑j ↑y, _⟩
source
@[simp]
theorem add_submonoid.localization_map.of_add_equiv_of_add_equiv_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : M) :
⇑((f.of_add_equiv_of_localizations (f.add_equiv_of_add_equiv k H)).to_map) x = ⇑(k.to_map) (⇑j x)
source
@[simp]
theorem submonoid.localization_map.of_mul_equiv_of_mul_equiv_apply {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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : M) :
⇑((f.of_mul_equiv_of_localizations (f.mul_equiv_of_mul_equiv k H)).to_map) x = ⇑(k.to_map) (⇑j x)
source
theorem submonoid.localization_map.of_mul_equiv_of_mul_equiv {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) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) :
(f.of_mul_equiv_of_localizations (f.mul_equiv_of_mul_equiv k H)).to_map = k.to_map.comp j.to_monoid_hom
source
theorem add_submonoid.localization_map.of_add_equiv_of_add_equiv {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) :
(f.of_add_equiv_of_localizations (f.add_equiv_of_add_equiv k H)).to_map = k.to_map.comp j.to_add_monoid_hom
source
def localization.monoid_of {M : Type u_1} [comm_monoid M] (S : submonoid M) :
S.localization_map (localization S)

Natural hom sending x : M, M a comm_monoid, to the equivalence class of (x, 1) in the localization of M at a submonoid.

Equations
source
def add_localization.add_monoid_of {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :
S.localization_map (add_localization S)

Natural homomorphism sending x : M, M an add_comm_monoid, to the equivalence class of (x, 0) in the localization of M at a submonoid.

Equations
source
theorem add_localization.mk_zero_eq_add_monoid_of_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (x : M) :
add_localization.mk x 0 = ⇑((add_localization.add_monoid_of S).to_map) x
source
theorem localization.mk_one_eq_monoid_of_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) :
localization.mk x 1 = ⇑((localization.monoid_of S).to_map) x
source
theorem localization.mk_eq_monoid_of_mk'_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) (y : ↥S) :
localization.mk x y = (localization.monoid_of S).mk' x y
source
theorem add_localization.mk_eq_add_monoid_of_mk'_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (x : M) (y : ↥S) :
add_localization.mk x y = (add_localization.add_monoid_of S).mk' x y
source
@[simp]
theorem localization.mk_eq_monoid_of_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} :
localization.mk = (localization.monoid_of S).mk'
source
@[simp]
theorem add_localization.mk_eq_add_monoid_of_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} :
add_localization.mk = (add_localization.add_monoid_of S).mk'
source
@[simp]
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}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :
((localization.monoid_of S).mk' a b).lift_on f H = f a b
source
@[simp]
theorem add_localization.lift_on_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(add_localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :
((add_localization.add_monoid_of S).mk' a b).lift_on f H = f a b
source
@[simp]
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}, ⇑(localization.r S) (a, b) (a', b') → ⇑(localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :
((localization.monoid_of S).mk' a b).lift_on₂ ((localization.monoid_of S).mk' c d) f H = f a b c d
source
@[simp]
theorem add_localization.lift_on₂_mk' {M : Type u_1} [add_comm_monoid M] {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}, ⇑(add_localization.r S) (a, b) (a', b') → ⇑(add_localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :
((add_localization.add_monoid_of S).mk' a b).lift_on₂ ((add_localization.add_monoid_of S).mk' c d) f H = f a b c d
source
noncomputable def add_localization.add_equiv_of_quotient {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :
add_localization S ≃+ N

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.

Equations
source
noncomputable def localization.mul_equiv_of_quotient {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :
localization S ≃* N

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.

Equations
source
@[simp]
theorem localization.mul_equiv_of_quotient_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : localization S) :
⇑(localization.mul_equiv_of_quotient f) x = ⇑((localization.monoid_of S).lift _) x
source
@[simp]
theorem add_localization.add_equiv_of_quotient_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : add_localization S) :
⇑(add_localization.add_equiv_of_quotient f) x = ⇑((add_localization.add_monoid_of S).lift _) x
source
@[simp]
theorem add_localization.add_equiv_of_quotient_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :
⇑(add_localization.add_equiv_of_quotient f) ((add_localization.add_monoid_of S).mk' x y) = f.mk' x y
source
@[simp]
theorem localization.mul_equiv_of_quotient_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) :
⇑(localization.mul_equiv_of_quotient f) ((localization.monoid_of S).mk' x y) = f.mk' x y
source
theorem add_localization.add_equiv_of_quotient_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :
⇑(add_localization.add_equiv_of_quotient f) (add_localization.mk x y) = f.mk' x y
source
theorem localization.mul_equiv_of_quotient_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) :
⇑(localization.mul_equiv_of_quotient f) (localization.mk x y) = f.mk' x y
source
@[simp]
theorem add_localization.add_equiv_of_quotient_add_monoid_of {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) :
⇑(add_localization.add_equiv_of_quotient f) (⇑((add_localization.add_monoid_of S).to_map) x) = ⇑(f.to_map) x
source
@[simp]
theorem localization.mul_equiv_of_quotient_monoid_of {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) :
⇑(localization.mul_equiv_of_quotient f) (⇑((localization.monoid_of S).to_map) x) = ⇑(f.to_map) x
source
@[simp]
theorem add_localization.add_equiv_of_quotient_symm_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :
⇑((add_localization.add_equiv_of_quotient f).symm) (f.mk' x y) = (add_localization.add_monoid_of S).mk' x y
source
@[simp]
theorem localization.mul_equiv_of_quotient_symm_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) :
⇑((localization.mul_equiv_of_quotient f).symm) (f.mk' x y) = (localization.monoid_of S).mk' x y
source
theorem localization.mul_equiv_of_quotient_symm_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) :
⇑((localization.mul_equiv_of_quotient f).symm) (f.mk' x y) = localization.mk x y
source
theorem add_localization.add_equiv_of_quotient_symm_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :
⇑((add_localization.add_equiv_of_quotient f).symm) (f.mk' x y) = add_localization.mk x y
source
@[simp]
theorem localization.mul_equiv_of_quotient_symm_monoid_of {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) :
⇑((localization.mul_equiv_of_quotient f).symm) (⇑(f.to_map) x) = ⇑((localization.monoid_of S).to_map) x
source
@[simp]
theorem add_localization.add_equiv_of_quotient_symm_add_monoid_of {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) :
⇑((add_localization.add_equiv_of_quotient f).symm) (⇑(f.to_map) x) = ⇑((add_localization.add_monoid_of S).to_map) x
source
@[reducible]
def add_localization.away {M : Type u_1} [add_comm_monoid M] (x : M) :
Type u_1

Given x : M, the localization of M at the submonoid generated by x, as a quotient.

Equations
source
@[reducible]
def localization.away {M : Type u_1} [comm_monoid M] (x : M) :
Type u_1

Given x : M, the localization of M at the submonoid generated by x, as a quotient.

Equations
source
def localization.away.inv_self {M : Type u_1} [comm_monoid M] (x : M) :
localization.away x

Given x : M, inv_self is x⁻¹ in the localization (as a quotient type) of M at the submonoid generated by x.

Equations
source
def add_localization.away.neg_self {M : Type u_1} [add_comm_monoid M] (x : M) :
add_localization.away x

Given x : M, neg_self is -x in the localization (as a quotient type) of M at the submonoid generated by x.

Equations
source
@[reducible]
def localization.away.monoid_of {M : Type u_1} [comm_monoid M] (x : M) :
submonoid.localization_map.away_map x (localization.away x)

Given x : M, the natural hom sending y : M, M a comm_monoid, to the equivalence class of (y, 1) in the localization of M at the submonoid generated by x.

Equations
source
@[reducible]
def add_localization.away.add_monoid_of {M : Type u_1} [add_comm_monoid M] (x : M) :
add_submonoid.localization_map.away_map x (add_localization.away x)

Given x : M, the natural hom sending y : M, M an add_comm_monoid, to the equivalence class of (y, 0) in the localization of M at the submonoid generated by x.

Equations
source
@[simp]
theorem add_localization.away.mk_eq_add_monoid_of_mk' {M : Type u_1} [add_comm_monoid M] (x : M) :
add_localization.mk = add_submonoid.localization_map.mk' (add_localization.away.add_monoid_of x)
source
@[simp]
theorem localization.away.mk_eq_monoid_of_mk' {M : Type u_1} [comm_monoid M] (x : M) :
localization.mk = submonoid.localization_map.mk' (localization.away.monoid_of x)
source
noncomputable def localization.away.mul_equiv_of_quotient {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] (x : M) (f : submonoid.localization_map.away_map x N) :
localization.away x ≃* N

Given x : M and a localization map f : M →* N away from x, we get an isomorphism between the localization of M at the submonoid generated by x as a quotient type and N.

Equations
source
noncomputable def add_localization.away.add_equiv_of_quotient {M : Type u_1} [add_comm_monoid M] {N : Type u_2} [add_comm_monoid N] (x : M) (f : add_submonoid.localization_map.away_map x N) :
add_localization.away x ≃+ N

Given x : M and a localization map f : M →+ N away from x, we get an isomorphism between the localization of M at the submonoid generated by x as a quotient type and N.

Equations
source
@[nolint]
structure submonoid.localization_with_zero_map {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) (N : Type u_2) [comm_monoid_with_zero N] :
Type (max u_1 u_2)

The type of homomorphisms between monoids with zero 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_with_zero_map
  • submonoid.localization_with_zero_map.has_sizeof_inst
source
def submonoid.localization_with_zero_map.to_monoid_with_zero_hom {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {N : Type u_2} [comm_monoid_with_zero N] (f : S.localization_with_zero_map N) :
M →*₀ N

The monoid with zero hom underlying a localization_map.

Equations
source
@[protected, irreducible]
def localization.zero {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) :
localization S

The zero element in a localization is defined as (0, 1).

Should not be confused with add_localization.zero which is (0, 0).

Equations
source
@[protected, instance]
def localization.has_zero {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) :
has_zero (localization S)
Equations
source
@[protected, instance]
def localization.comm_monoid_with_zero {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) :
comm_monoid_with_zero (localization S)
Equations
source
theorem localization.mk_zero {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} (x : ↥S) :
localization.mk 0 x = 0
source
theorem localization.lift_on_zero {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {p : Type u_2} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) :
0.lift_on f H = f 0 1
source
@[simp]
theorem submonoid.localization_map.sec_zero_fst {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {N : Type u_2} [comm_monoid_with_zero N] {f : S.localization_map N} :
⇑(f.to_map) (f.sec 0).fst = 0
source
noncomputable def submonoid.localization_with_zero_map.lift {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {N : Type u_2} [comm_monoid_with_zero N] {P : Type u_3} [comm_monoid_with_zero P] (f : S.localization_with_zero_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_with_zeros 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
source
theorem localization.mk_left_injective {α : Type u_1} [cancel_comm_monoid α] {s : submonoid α} (b : ↥s) :
function.injective (λ (a : α), localization.mk a b)
source
theorem add_localization.mk_left_injective {α : Type u_1} [add_cancel_comm_monoid α] {s : add_submonoid α} (b : ↥s) :
function.injective (λ (a : α), add_localization.mk a b)
source
theorem localization.mk_eq_mk_iff' {α : Type u_1} [cancel_comm_monoid α] {s : submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
localization.mk a₁ a₂ = localization.mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
source
theorem add_localization.mk_eq_mk_iff' {α : Type u_1} [add_cancel_comm_monoid α] {s : add_submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
add_localization.mk a₁ a₂ = add_localization.mk b₁ b₂ ↔ ↑b₂ + a₁ = ↑a₂ + b₁
source
@[protected, instance]
def localization.decidable_eq {α : Type u_1} [cancel_comm_monoid α] {s : submonoid α} [decidable_eq α] :
decidable_eq (localization s)
Equations
source
@[protected, instance]
def add_localization.decidable_eq {α : Type u_1} [add_cancel_comm_monoid α] {s : add_submonoid α} [decidable_eq α] :
decidable_eq (add_localization s)
Equations

Order #

source
@[protected, instance]
def localization.has_le {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :
has_le (localization s)
Equations
source
@[protected, instance]
def add_localization.has_le {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :
has_le (add_localization s)
Equations
source
@[protected, instance]
def add_localization.has_lt {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :
has_lt (add_localization s)
Equations
source
@[protected, instance]
def localization.has_lt {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :
has_lt (localization s)
Equations
source
theorem localization.mk_le_mk {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
localization.mk a₁ a₂ ≤ localization.mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁
source
theorem add_localization.mk_le_mk {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
add_localization.mk a₁ a₂ ≤ add_localization.mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁
source
theorem add_localization.mk_lt_mk {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
add_localization.mk a₁ a₂ < add_localization.mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁
source
theorem localization.mk_lt_mk {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
localization.mk a₁ a₂ < localization.mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁
source
@[protected, instance]
def add_localization.partial_order {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :
partial_order (add_localization s)
Equations
source
@[protected, instance]
def localization.partial_order {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :
partial_order (localization s)
Equations
source
@[protected, instance]
def localization.ordered_cancel_comm_monoid {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :
ordered_cancel_comm_monoid (localization s)
Equations
source
@[protected, instance]
def add_localization.ordered_cancel_add_comm_monoid {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :
ordered_cancel_add_comm_monoid (add_localization s)
Equations
source
@[protected, instance]
def add_localization.decidable_le {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} [decidable_rel has_le.le] :
decidable_rel has_le.le
Equations
source
@[protected, instance]
def localization.decidable_le {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} [decidable_rel has_le.le] :
decidable_rel has_le.le
Equations
source
@[protected, instance]
def add_localization.decidable_lt {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} [decidable_rel has_lt.lt] :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
def localization.decidable_lt {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} [decidable_rel has_lt.lt] :
decidable_rel has_lt.lt
Equations
source
def localization.mk_order_embedding {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} (b : ↥s) :
α ↪o localization s

An ordered cancellative monoid injects into its localization by sending a to a / b.

Equations
source
def add_localization.mk_order_embedding {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} (b : ↥s) :
α ↪o add_localization s

An ordered cancellative monoid injects into its localization by sending a to a - b.

Equations
source
@[simp]
theorem add_localization.mk_order_embedding_apply {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} (b : ↥s) (a : α) :
⇑(add_localization.mk_order_embedding b) a = add_localization.mk a b
source
@[simp]
theorem localization.mk_order_embedding_apply {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} (b : ↥s) (a : α) :
⇑(localization.mk_order_embedding b) a = localization.mk a b
source
@[protected, instance]
def add_localization.linear_ordered_cancel_add_comm_monoid {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :
linear_ordered_cancel_add_comm_monoid (add_localization s)
Equations
source
@[protected, instance]
def localization.linear_ordered_cancel_comm_monoid {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s : submonoid α} :
linear_ordered_cancel_comm_monoid (localization s)
Equations