Localizations of commutative monoids

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 such that f x = f y, there exists c ∈ S such that x * c = y * c. (The converse is a consequence of 1.)

Given such a localization map f : M →* N, we can define the surjection Submonoid.LocalizationMap.mk' sending (x, y) : M × S to f x * (f y)⁻¹. Mapping properties of the localization (e.g. extending a map from M → P to N if the image of S is contained in the units) are treated in a later file Mathlib.GroupTheory.MonoidLocalization.Maps.

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 reason about the localization as a quotient type, use mk_eq_monoidOf_mk' and associated lemmas. These show the quotient map mk : M → S → Localization S equals the surjection LocalizationMap.mk' induced by the map Localization.monoidOf : Submonoid.LocalizationMap S (Localization S) (where of establishes the localization as a quotient type satisfies the characteristic predicate). The lemma mk_eq_monoidOf_mk' hence gives you access to the results in the rest of the file, which are about the LocalizationMap.mk' induced by any localization map.

TODO

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

Tags

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

structure AddSubmonoid.IsLocalizationMap {M : Type u_1} [AddCommMonoid M] {N : Type u_2} [AddCommMonoid N] (S : AddSubmonoid M) (f : M → N) : Prop

A predicate characterizing homomorphisms between additive monoids M and N that form a commutative triangle with the canonical map from M to its localization at S and some isomorphism between N and the localization.

• map_addUnits (y : ↥S) : IsAddUnit (f ↑y)
• surj (z : N) : ∃ (x : M × ↥S), z + f ↑x.2 = f x.1
• exists_of_eq {x y : M} : f x = f y → ∃ (c : ↥S), ↑c + x = ↑c + y

structure AddSubmonoid.LocalizationMap {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (N : Type u_2) [AddCommMonoid N] extends M →ₙ+ N : Type (max u_1 u_2)

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

• toFun : M → N
• map_add' (x y : M) : self.toFun (x + y) = self.toFun x + self.toFun y
• isLocalizationMap : S.IsLocalizationMap self.toFun

structure Submonoid.IsLocalizationMap {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] (S : Submonoid M) (f : M → N) : Prop

A predicate characterizing homomorphisms between monoids M and N that form a commutative triangle with the canonical map from M to its localization at S and some isomorphism between N and the localization.

• map_units (y : ↥S) : IsUnit (f ↑y)
• surj (z : N) : ∃ (x : M × ↥S), z * f ↑x.2 = f x.1
• exists_of_eq {x y : M} : f x = f y → ∃ (c : ↥S), ↑c * x = ↑c * y

theorem Submonoid.isLocalizationMap_iff {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] (S : Submonoid M) (f : M → N) : S.IsLocalizationMap f ↔ (∀ (y : ↥S), IsUnit (f ↑y)) ∧ (∀ (z : N), ∃ (x : M × ↥S), z * f ↑x.2 = f x.1) ∧ ∀ {x y : M}, f x = f y → ∃ (c : ↥S), ↑c * x = ↑c * y

theorem AddSubmonoid.isLocalizationMap_iff {M : Type u_1} [AddCommMonoid M] {N : Type u_2} [AddCommMonoid N] (S : AddSubmonoid M) (f : M → N) : S.IsLocalizationMap f ↔ (∀ (y : ↥S), IsAddUnit (f ↑y)) ∧ (∀ (z : N), ∃ (x : M × ↥S), z + f ↑x.2 = f x.1) ∧ ∀ {x y : M}, f x = f y → ∃ (c : ↥S), ↑c + x = ↑c + y

structure Submonoid.LocalizationMap {M : Type u_1} [CommMonoid M] (S : Submonoid M) (N : Type u_2) [CommMonoid N] extends M →ₙ* 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.

• toFun : M → N
• map_mul' (x y : M) : self.toFun (x * y) = self.toFun x * self.toFun y
• isLocalizationMap : S.IsLocalizationMap self.toFun

def Localization.r {M : Type u_1} [CommMonoid M] (S : Submonoid M) : Con (M × ↥S)

The congruence relation on M × S, M a CommMonoid and S a submonoid of M, whose quotient is the localization of M at S, defined as the unique congruence relation on M × S such that for any other congruence relation s on M × S where for all y ∈ S, (1, 1) ∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂) by s.

Equations

• Localization.r S = sInf {c : Con (M × ↥S) | ∀ (y : ↥S), c 1 (↑y, y)}

def AddLocalization.r {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : AddCon (M × ↥S)

The congruence relation on M × S, M an AddCommMonoid and S an AddSubmonoid of M, whose quotient is the localization of M at S, defined as the unique congruence relation on M × S such that for any other congruence relation s on M × S where for all y ∈ S, (0, 0) ∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂) by s.

Equations

• AddLocalization.r S = sInf {c : AddCon (M × ↥S) | ∀ (y : ↥S), c 0 (↑y, y)}

def Localization.r' {M : Type u_1} [CommMonoid M] (S : Submonoid M) : Con (M × ↥S)

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

Equations

• Localization.r' S = { r := fun (a b : M × ↥S) => ∃ (c : ↥S), ↑c * (↑b.2 * a.1) = ↑c * (↑a.2 * b.1), iseqv := ⋯, mul' := ⋯ }

def AddLocalization.r' {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : AddCon (M × ↥S)

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

Equations

• AddLocalization.r' S = { r := fun (a b : M × ↥S) => ∃ (c : ↥S), ↑c + (↑b.2 + a.1) = ↑c + (↑a.2 + b.1), iseqv := ⋯, add' := ⋯ }

theorem Localization.r_eq_r' {M : Type u_1} [CommMonoid M] (S : Submonoid M) : r S = r' S

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

theorem AddLocalization.r_eq_r' {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : r S = r' S

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

theorem Localization.r_iff_exists {M : Type u_1} [CommMonoid M] {S : Submonoid M} {x y : M × ↥S} : (r S) x y ↔ ∃ (c : ↥S), ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

theorem AddLocalization.r_iff_exists {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S} : (r S) x y ↔ ∃ (c : ↥S), ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)

theorem Localization.r_iff_oreEqv_r {M : Type u_1} [CommMonoid M] {S : Submonoid M} {x y : M × ↥S} : (r S) x y ↔ (OreLocalization.oreEqv S M) x y

theorem AddLocalization.r_iff_oreEqv_r {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S} : (r S) x y ↔ (AddOreLocalization.oreEqv S M) x y

@[reducible, inline]

abbrev Localization {M : Type u_1} [CommMonoid M] (S : Submonoid M) : Type u_1

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

Equations

• Localization S = OreLocalization S M

@[reducible, inline]

abbrev AddLocalization {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : Type u_1

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

Equations

• AddLocalization S = AddOreLocalization S M

def Localization.mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} (x : M) (y : ↥S) : Localization S

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

Equations

• Localization.mk x y = x /ₒ y

def AddLocalization.mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (x : M) (y : ↥S) : AddLocalization S

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

Equations

• AddLocalization.mk x y = x -ₒ y

theorem Localization.mk_eq_mk_iff {M : Type u_1} [CommMonoid M] {S : Submonoid M} {a c : M} {b d : ↥S} : mk a b = mk c d ↔ (r S) (a, b) (c, d)

theorem AddLocalization.mk_eq_mk_iff {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {a c : M} {b d : ↥S} : mk a b = mk c d ↔ (r S) (a, b) (c, d)

def Localization.rec {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Sort u} (f : (a : M) → (b : ↥S) → p (mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ 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

• Localization.rec f H x = Quot.rec (fun (y : M × ↥S) => ⋯ ▸ f y.1 y.2) ⋯ x

def AddLocalization.rec {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Sort u} (f : (a : M) → (b : ↥S) → p (mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (x : AddLocalization S) : p x

Dependent recursion principle for AddLocalizations: given elements f a b : p (mk a b) for all a b, such that r S (a, b) (c, d) implies f a b = f c d (with the correct coercions), then f is defined on the whole AddLocalization S.

Equations

• AddLocalization.rec f H x = Quot.rec (fun (y : M × ↥S) => ⋯ ▸ f y.1 y.2) ⋯ x

def Localization.recOnSubsingleton₂ {M : Type u_1} [CommMonoid M] {S : Submonoid M} {r : Localization S → Localization S → Sort u} [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (mk a b) (mk c d))] (x y : Localization S) (f : (a c : M) → (b d : ↥S) → r (mk a b) (mk c d)) : r x y

Copy of Quotient.recOnSubsingleton₂ for Localization

Equations

• One or more equations did not get rendered due to their size.

def AddLocalization.recOnSubsingleton₂ {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {r : AddLocalization S → AddLocalization S → Sort u} [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (mk a b) (mk c d))] (x y : AddLocalization S) (f : (a c : M) → (b d : ↥S) → r (mk a b) (mk c d)) : r x y

Copy of Quotient.recOnSubsingleton₂ for AddLocalization

Equations

• One or more equations did not get rendered due to their size.

theorem Localization.mk_mul {M : Type u_1} [CommMonoid M] {S : Submonoid M} (a c : M) (b d : ↥S) : mk a b * mk c d = mk (a * c) (b * d)

theorem AddLocalization.mk_add {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (a c : M) (b d : ↥S) : mk a b + mk c d = mk (a + c) (b + d)

theorem Localization.mk_one {M : Type u_1} [CommMonoid M] {S : Submonoid M} : mk 1 1 = 1

theorem AddLocalization.mk_zero {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} : mk 0 0 = 0

theorem Localization.mk_pow {M : Type u_1} [CommMonoid M] {S : Submonoid M} (n : ℕ) (a : M) (b : ↥S) : mk a b ^ n = mk (a ^ n) (b ^ n)

theorem AddLocalization.mk_nsmul {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (n : ℕ) (a : M) (b : ↥S) : n • mk a b = mk (n • a) (n • b)

theorem Localization.mk_prod {M : Type u_1} [CommMonoid M] {S : Submonoid M} {ι : Type u_4} (t : Finset ι) (f : ι → M) (s : ι → ↥S) : ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

theorem AddLocalization.mk_sum {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {ι : Type u_4} (t : Finset ι) (f : ι → M) (s : ι → ↥S) : ∑ i ∈ t, mk (f i) (s i) = mk (∑ i ∈ t, f i) (∑ i ∈ t, s i)

@[simp]

theorem Localization.ndrec_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Sort u} (f : (a : M) → (b : ↥S) → p (mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (a : M) (b : ↥S) : rec f H (mk a b) = f a b

@[simp]

theorem AddLocalization.ndrec_mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Sort u} (f : (a : M) → (b : ↥S) → p (mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (a : M) (b : ↥S) : rec f H (mk a b) = f a b

def Localization.liftOn {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Sort u} (x : Localization S) (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) : p

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

• x.liftOn f H = Localization.rec f ⋯ x

def AddLocalization.liftOn {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (x : AddLocalization S) (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) : p

Non-dependent recursion principle for AddLocalizations: 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

• x.liftOn f H = AddLocalization.rec f ⋯ x

theorem Localization.liftOn_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : (mk a b).liftOn f H = f a b

theorem AddLocalization.liftOn_mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : (mk a b).liftOn f H = f a b

theorem Localization.ind {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Prop} (H : ∀ (y : M × ↥S), p (mk y.1 y.2)) (x : Localization S) : p x

theorem AddLocalization.ind {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Prop} (H : ∀ (y : M × ↥S), p (mk y.1 y.2)) (x : AddLocalization S) : p x

theorem Localization.induction_on {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Prop} (x : Localization S) (H : ∀ (y : M × ↥S), p (mk y.1 y.2)) : p x

theorem AddLocalization.induction_on {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Prop} (x : AddLocalization S) (H : ∀ (y : M × ↥S), p (mk y.1 y.2)) : p x

def Localization.liftOn₂ {M : Type u_1} [CommMonoid 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}, (r S) (a, b) (a', b') → (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

• x.liftOn₂ y f H = x.liftOn (fun (a : M) (b : ↥S) => y.liftOn (f a b) ⋯) ⋯

def AddLocalization.liftOn₂ {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (x y : AddLocalization S) (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (r S) (a, b) (a', b') → (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

• x.liftOn₂ y f H = x.liftOn (fun (a : M) (b : ↥S) => y.liftOn (f a b) ⋯) ⋯

theorem Localization.liftOn₂_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) : (mk a b).liftOn₂ (mk c d) f H = f a b c d

theorem AddLocalization.liftOn₂_mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) : (mk a b).liftOn₂ (mk c d) f H = f a b c d

theorem Localization.induction_on₂ {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Localization S → Prop} (x y : Localization S) (H : ∀ (x y : M × ↥S), p (mk x.1 x.2) (mk y.1 y.2)) : p x y

theorem AddLocalization.induction_on₂ {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → AddLocalization S → Prop} (x y : AddLocalization S) (H : ∀ (x y : M × ↥S), p (mk x.1 x.2) (mk y.1 y.2)) : p x y

theorem Localization.induction_on₃ {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Localization S → Localization S → Prop} (x y z : Localization S) (H : ∀ (x y z : M × ↥S), p (mk x.1 x.2) (mk y.1 y.2) (mk z.1 z.2)) : p x y z

theorem AddLocalization.induction_on₃ {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → AddLocalization S → AddLocalization S → Prop} (x y z : AddLocalization S) (H : ∀ (x y z : M × ↥S), p (mk x.1 x.2) (mk y.1 y.2) (mk z.1 z.2)) : p x y z

theorem Localization.one_rel {M : Type u_1} [CommMonoid M] {S : Submonoid M} (y : ↥S) : (r S) 1 (↑y, y)

theorem AddLocalization.zero_rel {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (y : ↥S) : (r S) 0 (↑y, y)

theorem Localization.r_of_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {x y : M × ↥S} (h : ↑y.2 * x.1 = ↑x.2 * y.1) : (r S) x y

theorem AddLocalization.r_of_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S} (h : ↑y.2 + x.1 = ↑x.2 + y.1) : (r S) x y

theorem Localization.mk_self {M : Type u_1} [CommMonoid M] {S : Submonoid M} (a : ↥S) : mk (↑a) a = 1

theorem AddLocalization.mk_self {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (a : ↥S) : mk (↑a) a = 0

@[simp]

theorem Localization.mk_self_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} (a : M) (haS : a ∈ S) : mk a ⟨a, haS⟩ = 1

@[simp]

theorem AddLocalization.mk_self_mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (a : M) (haS : a ∈ S) : mk a ⟨a, haS⟩ = 0

def Localization.mkHom {M : Type u_1} [CommMonoid M] {S : Submonoid M} : M × ↥S →* Localization S

Localization.mk as a monoid hom.

Equations

• Localization.mkHom = { toFun := fun (x : M × ↥S) => Localization.mk x.1 x.2, map_one' := ⋯, map_mul' := ⋯ }

def AddLocalization.mkHom {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} : M × ↥S →+ AddLocalization S

Localization.mk as a monoid hom.

Equations

• AddLocalization.mkHom = { toFun := fun (x : M × ↥S) => AddLocalization.mk x.1 x.2, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Localization.mkHom_apply {M : Type u_1} [CommMonoid M] {S : Submonoid M} (x : M × ↥S) : mkHom x = mk x.1 x.2

@[simp]

theorem AddLocalization.mkHom_apply {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (x : M × ↥S) : mkHom x = mk x.1 x.2

theorem Localization.mkHom_surjective {M : Type u_1} [CommMonoid M] {S : Submonoid M} : Function.Surjective ⇑mkHom

theorem AddLocalization.mkHom_surjective {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} : Function.Surjective ⇑mkHom

theorem Localization.smul_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_4} [SMul R M] [IsScalarTower R M M] (c : R) (a : M) (b : ↥S) : c • mk a b = mk (c • a) b

instance Localization.instSMulCommClassOfIsScalarTower {R : Type u_7} {M : Type u_8} [CommMonoid M] [SMul R M] [IsScalarTower R M M] : SMulCommClass R M M

def MonoidHom.toLocalizationMap {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : M →* N) (H1 : ∀ (y : ↥S), IsUnit (f ↑y)) (H2 : ∀ (z : N), ∃ (x : M × ↥S), z * f ↑x.2 = f x.1) (H3 : ∀ (x y : M), f x = f y → ∃ (c : ↥S), ↑c * x = ↑c * y) : S.LocalizationMap N

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

Equations

• f.toLocalizationMap H1 H2 H3 = { toFun := (↑f).toFun, map_mul' := ⋯, isLocalizationMap := ⋯ }

def AddMonoidHom.toLocalizationMap {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : M →+ N) (H1 : ∀ (y : ↥S), IsAddUnit (f ↑y)) (H2 : ∀ (z : N), ∃ (x : M × ↥S), z + f ↑x.2 = f x.1) (H3 : ∀ (x y : M), f x = f y → ∃ (c : ↥S), ↑c + x = ↑c + y) : S.LocalizationMap N

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

Equations

• f.toLocalizationMap H1 H2 H3 = { toFun := (↑f).toFun, map_add' := ⋯, isLocalizationMap := ⋯ }

theorem Submonoid.IsLocalizationMap.map_one {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {F : Type u_4} [FunLike F M N] [MulHomClass F M N] {f : F} (hf : S.IsLocalizationMap ⇑f) : f 1 = 1

theorem AddSubmonoid.IsLocalizationMap.map_zero {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {F : Type u_4} [FunLike F M N] [AddHomClass F M N] {f : F} (hf : S.IsLocalizationMap ⇑f) : f 0 = 0

theorem Submonoid.IsLocalizationMap.mulEquiv_comp {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {f : M → N} (hf : S.IsLocalizationMap f) {E : Type u_4} [EquivLike E N P] [MulEquivClass E N P] (e : E) : S.IsLocalizationMap (⇑e ∘ f)

theorem AddSubmonoid.IsLocalizationMap.addEquiv_comp {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] {f : M → N} (hf : S.IsLocalizationMap f) {E : Type u_4} [EquivLike E N P] [AddEquivClass E N P] (e : E) : S.IsLocalizationMap (⇑e ∘ f)

@[reducible, inline]

abbrev Submonoid.LocalizationMap.toMonoidHom {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) : M →* N

A localization map between monoids automatically preserves 1 and therefore is a monoid homomorphism.

Equations

• f.toMonoidHom = { toFun := f.toFun, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

abbrev AddSubmonoid.LocalizationMap.toAddMonoidHom {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) : M →+ N

A localization map between additive monoids automatically preserves 0 and therefore is an additive monoid homomorphism.

Equations

• f.toAddMonoidHom = { toFun := f.toFun, map_zero' := ⋯, map_add' := ⋯ }

@[reducible, inline, deprecated Submonoid.LocalizationMap.toMonoidHom (since := "2025-08-13")]

abbrev Submonoid.LocalizationMap.toMap {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) : M →* N

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

Equations

• f.toMap = f.toMonoidHom

@[reducible, inline, deprecated AddSubmonoid.LocalizationMap.toAddMonoidHom (since := "2025-08-13")]

abbrev AddSubmonoid.LocalizationMap.toMap {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) : M →+ N

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

Equations

• f.toMap = f.toAddMonoidHom

theorem Submonoid.LocalizationMap.toMonoidHom_injective {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] : Function.Injective toMonoidHom

theorem AddSubmonoid.LocalizationMap.toAddMonoidHom_injective {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] : Function.Injective toAddMonoidHom

@[deprecated Submonoid.LocalizationMap.toMonoidHom_injective (since := "2025-08-13")]

theorem Submonoid.LocalizationMap.toMap_injective {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] : Function.Injective toMonoidHom

Alias of Submonoid.LocalizationMap.toMonoidHom_injective.

instance Submonoid.LocalizationMap.instFunLike {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] : FunLike (S.LocalizationMap N) M N

Equations

• Submonoid.LocalizationMap.instFunLike = { coe := fun (f : S.LocalizationMap N) => ⇑f.toMonoidHom, coe_injective' := ⋯ }

instance AddSubmonoid.LocalizationMap.instFunLike {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] : FunLike (S.LocalizationMap N) M N

Equations

• AddSubmonoid.LocalizationMap.instFunLike = { coe := fun (f : S.LocalizationMap N) => ⇑f.toAddMonoidHom, coe_injective' := ⋯ }

instance Submonoid.LocalizationMap.instMonoidHomClass {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] : MonoidHomClass (S.LocalizationMap N) M N

instance AddSubmonoid.LocalizationMap.instAddMonoidHomClass {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] : AddMonoidHomClass (S.LocalizationMap N) M N

@[simp]

theorem Submonoid.LocalizationMap.toMonoidHom_apply {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) : f.toMonoidHom x = f x

@[simp]

theorem AddSubmonoid.LocalizationMap.toAddMonoidHom_apply {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) : f.toAddMonoidHom x = f x

theorem Submonoid.LocalizationMap.ext {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f g : S.LocalizationMap N} (h : ∀ (x : M), f x = g x) : f = g

theorem AddSubmonoid.LocalizationMap.ext {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f g : S.LocalizationMap N} (h : ∀ (x : M), f x = g x) : f = g

theorem Submonoid.LocalizationMap.ext_iff {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f g : S.LocalizationMap N} : f = g ↔ ∀ (x : M), f x = g x

theorem AddSubmonoid.LocalizationMap.ext_iff {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f g : S.LocalizationMap N} : f = g ↔ ∀ (x : M), f x = g x

theorem Submonoid.LocalizationMap.map_units {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (y : ↥S) : IsUnit (f ↑y)

theorem AddSubmonoid.LocalizationMap.map_addUnits {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (y : ↥S) : IsAddUnit (f ↑y)

theorem Submonoid.LocalizationMap.surj {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (z : N) : ∃ (x : M × ↥S), z * f ↑x.2 = f x.1

theorem AddSubmonoid.LocalizationMap.surj {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) : ∃ (x : M × ↥S), z + f ↑x.2 = f x.1

theorem Submonoid.LocalizationMap.exists_of_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x y : M} : f x = f y → ∃ (c : ↥S), ↑c * x = ↑c * y

theorem AddSubmonoid.LocalizationMap.exists_of_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x y : M} : f x = f y → ∃ (c : ↥S), ↑c + x = ↑c + y

theorem Submonoid.LocalizationMap.surj₂ {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (z w : N) : ∃ (z' : M) (w' : M) (d : ↥S), z * f ↑d = f z' ∧ w * f ↑d = f w'

Given a localization map f : M →* N, and z w : N, there exist z' w' : M and d : S such that f z' / f d = z and f w' / f d = w.

theorem AddSubmonoid.LocalizationMap.surj₂ {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z w : N) : ∃ (z' : M) (w' : M) (d : ↥S), z + f ↑d = f z' ∧ w + f ↑d = f w'

Given a localization map f : M →+ N, and z w : N, there exist z' w' : M and d : S such that f z' - f d = z and f w' - f d = w.

theorem Submonoid.LocalizationMap.eq_iff_exists {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x y : M} : f x = f y ↔ ∃ (c : ↥S), ↑c * x = ↑c * y

theorem AddSubmonoid.LocalizationMap.eq_iff_exists {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x y : M} : f x = f y ↔ ∃ (c : ↥S), ↑c + x = ↑c + y

noncomputable def Submonoid.LocalizationMap.sec {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap 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

• f.sec z = Classical.choose ⋯

noncomputable def AddSubmonoid.LocalizationMap.sec {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap 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

• f.sec z = Classical.choose ⋯

theorem Submonoid.LocalizationMap.sec_spec {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (z : N) : z * f ↑(f.sec z).2 = f (f.sec z).1

theorem AddSubmonoid.LocalizationMap.sec_spec {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (z : N) : z + f ↑(f.sec z).2 = f (f.sec z).1

theorem Submonoid.LocalizationMap.sec_spec' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (z : N) : f (f.sec z).1 = f ↑(f.sec z).2 * z

theorem AddSubmonoid.LocalizationMap.sec_spec' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (z : N) : f (f.sec z).1 = f ↑(f.sec z).2 + z

theorem Submonoid.LocalizationMap.mul_inv_left {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : M →* N} (h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N) : w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z ↔ w = f ↑y * z

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

theorem AddSubmonoid.LocalizationMap.add_neg_left {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) (y : ↥S) (w z : N) : w + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) = z ↔ w = f ↑y + z

Given an AddMonoidHom f : M →+ N and Submonoid S ⊆ M such that f(S) ⊆ AddUnits N, for all w, z : N and y ∈ S, we have w - f y = z ↔ w = f y + z.

theorem Submonoid.LocalizationMap.mul_inv_right {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : M →* N} (h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N) : z = w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ ↔ z * f ↑y = w

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

theorem AddSubmonoid.LocalizationMap.add_neg_right {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) (y : ↥S) (w z : N) : z = w + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) ↔ z + f ↑y = w

Given an AddMonoidHom f : M →+ N and Submonoid S ⊆ M such that f(S) ⊆ AddUnits N, for all w, z : N and y ∈ S, we have z = w - f y ↔ z + f y = w.

@[simp]

theorem Submonoid.LocalizationMap.mul_inv {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : M →* N} (h : ∀ (y : ↥S), IsUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f x₁ * ↑((IsUnit.liftRight (f.restrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.restrict S) h) y₂)⁻¹ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Given a MonoidHom f : M →* N and Submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all x₁ x₂ : M and y₁, y₂ ∈ S, we have f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁).

@[simp]

theorem AddSubmonoid.LocalizationMap.add_neg {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f x₁ + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y₁) = f x₂ + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y₂) ↔ f (x₁ + ↑y₂) = f (x₂ + ↑y₁)

Given an AddMonoidHom f : M →+ N and Submonoid S ⊆ M such that f(S) ⊆ AddUnits N, for all x₁ x₂ : M and y₁, y₂ ∈ S, we have f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁).

theorem Submonoid.LocalizationMap.inv_inj {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : M →* N} (hf : ∀ (y : ↥S), IsUnit (f ↑y)) {y z : ↥S} (h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹) : f ↑y = f ↑z

Given a MonoidHom f : M →* N and Submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all y, z ∈ S, we have (f y)⁻¹ = (f z)⁻¹ → f y = f z.

theorem AddSubmonoid.LocalizationMap.neg_inj {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : M →+ N} (hf : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y z : ↥S} (h : -(IsAddUnit.liftRight (f.restrict S) hf) y = -(IsAddUnit.liftRight (f.restrict S) hf) z) : f ↑y = f ↑z

Given an AddMonoidHom f : M →+ N and Submonoid S ⊆ M such that f(S) ⊆ AddUnits N, for all y, z ∈ S, we have - (f y) = - (f z) → f y = f z.

theorem Submonoid.LocalizationMap.inv_unique {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : M →* N} (h : ∀ (y : ↥S), IsUnit (f ↑y)) {y : ↥S} {z : N} (H : f ↑y * z = 1) : ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z

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

theorem AddSubmonoid.LocalizationMap.neg_unique {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y : ↥S} {z : N} (H : f ↑y + z = 0) : ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) = z

Given an AddMonoidHom f : M →+ N and Submonoid S ⊆ M such that f(S) ⊆ AddUnits N, for all y ∈ S, - (f y) is unique.

theorem Submonoid.LocalizationMap.map_right_cancel {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x y : M} {c : ↥S} (h : f (↑c * x) = f (↑c * y)) : f x = f y

theorem AddSubmonoid.LocalizationMap.map_right_cancel {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x y : M} {c : ↥S} (h : f (↑c + x) = f (↑c + y)) : f x = f y

theorem Submonoid.LocalizationMap.map_left_cancel {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x y : M} {c : ↥S} (h : f (x * ↑c) = f (y * ↑c)) : f x = f y

theorem AddSubmonoid.LocalizationMap.map_left_cancel {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x y : M} {c : ↥S} (h : f (x + ↑c) = f (y + ↑c)) : f x = f y

noncomputable def Submonoid.LocalizationMap.mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap 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

• f.mk' x y = f x * ↑((IsUnit.liftRight (f.toMonoidHom.restrict S) ⋯) y)⁻¹

noncomputable def AddSubmonoid.LocalizationMap.mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap 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

• f.mk' x y = f x + ↑(-(IsAddUnit.liftRight (f.toAddMonoidHom.restrict S) ⋯) y)

theorem Submonoid.LocalizationMap.mk'_mul {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x₁ x₂ : M) (y₁ y₂ : ↥S) : f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

theorem AddSubmonoid.LocalizationMap.mk'_add {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x₁ x₂ : M) (y₁ y₂ : ↥S) : f.mk' (x₁ + x₂) (y₁ + y₂) = f.mk' x₁ y₁ + f.mk' x₂ y₂

theorem Submonoid.LocalizationMap.mk'_one {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) : f.mk' x 1 = f x

theorem AddSubmonoid.LocalizationMap.mk'_zero {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) : f.mk' x 0 = f x

@[simp]

theorem Submonoid.LocalizationMap.mk'_sec {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (z : N) : f.mk' (f.sec z).1 (f.sec z).2 = z

Given a localization map f : M →* N for a submonoid S ⊆ M, for all z : N we have that if x : M, y ∈ S are such that z * f y = f x, then f x * (f y)⁻¹ = z.

@[simp]

theorem AddSubmonoid.LocalizationMap.mk'_sec {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) : f.mk' (f.sec z).1 (f.sec z).2 = z

Given a localization map f : M →+ N for an AddSubmonoid S ⊆ M, for all z : N we have that if x : M, y ∈ S are such that z + f y = f x, then f x - f y = z.

theorem Submonoid.LocalizationMap.mk'_surjective {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (z : N) : ∃ (x : M) (y : ↥S), f.mk' x y = z

theorem AddSubmonoid.LocalizationMap.mk'_surjective {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) : ∃ (x : M) (y : ↥S), f.mk' x y = z

theorem Submonoid.LocalizationMap.mk'_spec {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f.mk' x y * f ↑y = f x

theorem AddSubmonoid.LocalizationMap.mk'_spec {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f.mk' x y + f ↑y = f x

theorem Submonoid.LocalizationMap.mk'_spec' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f ↑y * f.mk' x y = f x

theorem AddSubmonoid.LocalizationMap.mk'_spec' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f ↑y + f.mk' x y = f x

theorem Submonoid.LocalizationMap.eq_mk'_iff_mul_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N} : z = f.mk' x y ↔ z * f ↑y = f x

theorem AddSubmonoid.LocalizationMap.eq_mk'_iff_add_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N} : z = f.mk' x y ↔ z + f ↑y = f x

theorem Submonoid.LocalizationMap.mk'_eq_iff_eq_mul {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N} : f.mk' x y = z ↔ f x = z * f ↑y

theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_eq_add {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N} : f.mk' x y = z ↔ f x = z + f ↑y

theorem Submonoid.LocalizationMap.mk'_eq_iff_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (↑y₂ * x₁) = f (↑y₁ * x₂)

theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (↑y₂ + x₁) = f (↑y₁ + x₂)

theorem Submonoid.LocalizationMap.mk'_eq_iff_eq' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_eq' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (x₁ + ↑y₂) = f (x₂ + ↑y₁)

theorem Submonoid.LocalizationMap.eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ (c : ↥S), ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)

theorem AddSubmonoid.LocalizationMap.eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ (c : ↥S), ↑c + (↑b₂ + a₁) = ↑c + (↑a₂ + b₁)

theorem Submonoid.LocalizationMap.eq' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)

theorem AddSubmonoid.LocalizationMap.eq' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (AddLocalization.r S) (a₁, a₂) (b₁, b₂)

theorem Submonoid.LocalizationMap.eq_iff_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x y : M} : f x = f y ↔ g x = g y

theorem AddSubmonoid.LocalizationMap.eq_iff_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x y : M} : f x = f y ↔ g x = g y

theorem Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_mk'_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x₁ x₂ : M} {y₁ y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

theorem Submonoid.LocalizationMap.exists_of_sec_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : ∃ (c : ↥S), ↑c * (↑(f.sec (f.mk' x y)).2 * x) = ↑c * (↑y * (f.sec (f.mk' x y)).1)

Given a Localization map f : M →* N for a Submonoid S ⊆ M, for all x₁ : M and y₁ ∈ S, if x₂ : M, y₂ ∈ S are such that f x₁ * (f y₁)⁻¹ * f y₂ = f x₂, then there exists c ∈ S such that x₁ * y₂ * c = x₂ * y₁ * c.

theorem AddSubmonoid.LocalizationMap.exists_of_sec_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : ∃ (c : ↥S), ↑c + (↑(f.sec (f.mk' x y)).2 + x) = ↑c + (↑y + (f.sec (f.mk' x y)).1)

Given a Localization map f : M →+ N for a Submonoid S ⊆ M, for all x₁ : M and y₁ ∈ S, if x₂ : M, y₂ ∈ S are such that (f x₁ - f y₁) + f y₂ = f x₂, then there exists c ∈ S such that x₁ + y₂ + c = x₂ + y₁ + c.

theorem Submonoid.LocalizationMap.mk'_eq_of_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : ↑a₂ * b₁ = ↑b₂ * a₁) : f.mk' a₁ a₂ = f.mk' b₁ b₂

theorem AddSubmonoid.LocalizationMap.mk'_eq_of_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : ↑a₂ + b₁ = ↑b₂ + a₁) : f.mk' a₁ a₂ = f.mk' b₁ b₂

theorem Submonoid.LocalizationMap.mk'_eq_of_eq' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : b₁ * ↑a₂ = a₁ * ↑b₂) : f.mk' a₁ a₂ = f.mk' b₁ b₂

theorem AddSubmonoid.LocalizationMap.mk'_eq_of_eq' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : b₁ + ↑a₂ = a₁ + ↑b₂) : f.mk' a₁ a₂ = f.mk' b₁ b₂

theorem Submonoid.LocalizationMap.mk'_cancel {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (a : M) (b c : ↥S) : f.mk' (a * ↑c) (b * c) = f.mk' a b

theorem AddSubmonoid.LocalizationMap.mk'_cancel {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (a : M) (b c : ↥S) : f.mk' (a + ↑c) (b + c) = f.mk' a b

theorem Submonoid.LocalizationMap.mk'_eq_of_same {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {a b : M} {d : ↥S} : f.mk' a d = f.mk' b d ↔ ∃ (c : ↥S), ↑c * a = ↑c * b

theorem AddSubmonoid.LocalizationMap.mk'_eq_of_same {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a b : M} {d : ↥S} : f.mk' a d = f.mk' b d ↔ ∃ (c : ↥S), ↑c + a = ↑c + b

@[simp]

theorem Submonoid.LocalizationMap.mk'_self' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (y : ↥S) : f.mk' (↑y) y = 1

@[simp]

theorem AddSubmonoid.LocalizationMap.mk'_self' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (y : ↥S) : f.mk' (↑y) y = 0

@[simp]

theorem Submonoid.LocalizationMap.mk'_self {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (H : x ∈ S) : f.mk' x ⟨x, H⟩ = 1

@[simp]

theorem AddSubmonoid.LocalizationMap.mk'_self {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (H : x ∈ S) : f.mk' x ⟨x, H⟩ = 0

theorem Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S) : f x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

theorem AddSubmonoid.LocalizationMap.add_mk'_eq_mk'_of_add {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S) : f x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y

theorem Submonoid.LocalizationMap.mk'_mul_eq_mk'_of_mul {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S) : f.mk' x₂ y * f x₁ = f.mk' (x₁ * x₂) y

theorem AddSubmonoid.LocalizationMap.mk'_add_eq_mk'_of_add {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S) : f.mk' x₂ y + f x₁ = f.mk' (x₁ + x₂) y

theorem Submonoid.LocalizationMap.mul_mk'_one_eq_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f x * f.mk' 1 y = f.mk' x y

theorem AddSubmonoid.LocalizationMap.add_mk'_zero_eq_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f x + f.mk' 0 y = f.mk' x y

@[simp]

theorem Submonoid.LocalizationMap.mk'_mul_cancel_right {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f.mk' (x * ↑y) y = f x

@[simp]

theorem AddSubmonoid.LocalizationMap.mk'_add_cancel_right {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f.mk' (x + ↑y) y = f x

theorem Submonoid.LocalizationMap.mk'_mul_cancel_left {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f.mk' (↑y * x) y = f x

theorem AddSubmonoid.LocalizationMap.mk'_add_cancel_left {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (x : M) (y : ↥S) : f.mk' (↑y + x) y = f x

theorem Submonoid.LocalizationMap.isUnit_comp {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] (f : S.LocalizationMap N) (j : N →* P) (y : ↥S) : IsUnit ((j.comp f.toMonoidHom) ↑y)

theorem AddSubmonoid.LocalizationMap.isAddUnit_comp {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) (j : N →+ P) (y : ↥S) : IsAddUnit ((j.comp f.toAddMonoidHom) ↑y)

theorem Submonoid.LocalizationMap.epic_of_localizationMap {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {P : Type u_4} [Monoid P] {j k : N →* P} (h : j.comp f.toMonoidHom = k.comp f.toMonoidHom) : j = k

theorem AddSubmonoid.LocalizationMap.epic_of_localizationMap {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {P : Type u_4} [AddMonoid P] {j k : N →+ P} (h : j.comp f.toAddMonoidHom = k.comp f.toAddMonoidHom) : j = k

def Localization.monoidOf {M : Type u_1} [CommMonoid M] (S : Submonoid M) : S.LocalizationMap (Localization S)

Natural homomorphism sending x : M, M a CommMonoid, to the equivalence class of (x, 1) in the Localization of M at a Submonoid.

Equations

• Localization.monoidOf S = { toFun := fun (x : M) => Localization.mk x 1, map_mul' := ⋯, isLocalizationMap := ⋯ }

def AddLocalization.addMonoidOf {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : S.LocalizationMap (AddLocalization S)

Natural homomorphism sending x : M, M an AddCommMonoid, to the equivalence class of (x, 0) in the Localization of M at a Submonoid.

Equations

• AddLocalization.addMonoidOf S = { toFun := fun (x : M) => AddLocalization.mk x 0, map_add' := ⋯, isLocalizationMap := ⋯ }

theorem Localization.mk_one_eq_monoidOf_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} (x : M) : mk x 1 = (monoidOf S) x

theorem AddLocalization.mk_zero_eq_addMonoidOf_mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (x : M) : mk x 0 = (addMonoidOf S) x

theorem Localization.mk_eq_monoidOf_mk'_apply {M : Type u_1} [CommMonoid M] {S : Submonoid M} (x : M) (y : ↥S) : mk x y = (monoidOf S).mk' x y

theorem AddLocalization.mk_eq_addMonoidOf_mk'_apply {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (x : M) (y : ↥S) : mk x y = (addMonoidOf S).mk' x y

theorem Localization.mk_eq_monoidOf_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} : mk = (monoidOf S).mk'

theorem AddLocalization.mk_eq_addMonoidOf_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} : mk = (addMonoidOf S).mk'

@[simp]

theorem Localization.liftOn_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : ((monoidOf S).mk' a b).liftOn f H = f a b

@[simp]

theorem AddLocalization.liftOn_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : ((addMonoidOf S).mk' a b).liftOn f H = f a b

@[simp]

theorem Localization.liftOn₂_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) : ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f H = f a b c d

@[simp]

theorem AddLocalization.liftOn₂_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) : ((addMonoidOf S).mk' a b).liftOn₂ ((addMonoidOf S).mk' c d) f H = f a b c d

instance Localization.instIsMulTorsionFree {M : Type u_1} [CommMonoid M] {S : Submonoid M} [IsMulTorsionFree M] : IsMulTorsionFree (Localization S)

The localization of a torsion-free monoid is torsion-free.

instance AddLocalization.instIsAddTorsionFree {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} [IsAddTorsionFree M] : IsAddTorsionFree (AddLocalization S)

The localization of a torsion-free monoid is torsion-free.

theorem Localization.mk_left_injective {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s : Submonoid α} (b : ↥s) : Function.Injective fun (a : α) => mk a b

theorem AddLocalization.mk_left_injective {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s : AddSubmonoid α} (b : ↥s) : Function.Injective fun (a : α) => mk a b

theorem Localization.mk_eq_mk_iff' {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁

theorem AddLocalization.mk_eq_mk_iff' {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} : mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ + a₁ = ↑a₂ + b₁

instance Localization.decidableEq {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s : Submonoid α} [DecidableEq α] : DecidableEq (Localization s)

Equations

• a.decidableEq b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 * x = ↑x_2 * x_1) ⋯

instance AddLocalization.decidableEq {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s : AddSubmonoid α} [DecidableEq α] : DecidableEq (AddLocalization s)

Equations

• a.decidableEq b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 + x = ↑x_2 + x_1) ⋯

def OreLocalization.localizationMap (R : Type u_1) [CommMonoid R] (S : Submonoid R) : S.LocalizationMap (OreLocalization S R)

The morphism numeratorHom is a monoid localization map in the case of commutative R.

Equations

• OreLocalization.localizationMap R S = Localization.monoidOf S

noncomputable def OreLocalization.equivMonoidLocalization (R : Type u_1) [CommMonoid R] (S : Submonoid R) : Localization S ≃* OreLocalization S R

If R is commutative, Ore localization and monoid localization are isomorphic.

Equations

• OreLocalization.equivMonoidLocalization R S = MulEquiv.refl (Localization S)

theorem Submonoid.isLocalizationMap_iff_bijective {M : Type u_1} {G : Type u_2} {F : Type u_3} [CommMonoid M] [CommGroup G] {S : Submonoid G} [FunLike F G M] [MulHomClass F G M] {f : F} : S.IsLocalizationMap ⇑f ↔ Function.Bijective ⇑f

theorem AddSubmonoid.isLocalizationMap_iff_bijective {M : Type u_1} {G : Type u_2} {F : Type u_3} [AddCommMonoid M] [AddCommGroup G] {S : AddSubmonoid G} [FunLike F G M] [AddHomClass F G M] {f : F} : S.IsLocalizationMap ⇑f ↔ Function.Bijective ⇑f

theorem Submonoid.isLocalizationMap_id {G : Type u_2} [CommGroup G] (S : Submonoid G) : S.IsLocalizationMap id

theorem AddSubmonoid.isLocalizationMap_id {G : Type u_2} [AddCommGroup G] (S : AddSubmonoid G) : S.IsLocalizationMap id

theorem Submonoid.isLocalizationMap_of_group {M : Type u_1} {G : Type u_2} [CommMonoid M] [CommGroup G] {S : Submonoid M} {f : M → G} (hf : Function.Injective f) (surj : ∀ (g : G), ∃ (x : M), ∃ y ∈ S, g = f x / f y) : S.IsLocalizationMap f

theorem AddSubmonoid.isLocalizationMap_of_addGroup {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {S : AddSubmonoid M} {f : M → G} (hf : Function.Injective f) (surj : ∀ (g : G), ∃ (x : M), ∃ y ∈ S, g = f x - f y) : S.IsLocalizationMap f

theorem AddSubmonoid.isLocalizationMap_nat_int (S : AddSubmonoid ℕ) (hS : S ≠ ⊥) : S.IsLocalizationMap Nat.cast

theorem AddSubmonoid.isLocalizationMap_top_nat_int : ⊤.IsLocalizationMap Nat.cast

theorem Submonoid.LocalizationMap.injective_iff {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) : Function.Injective ⇑f ↔ ∀ ⦃x : M⦄, x ∈ S → IsRegular x

theorem AddSubmonoid.LocalizationMap.injective_iff {M : Type u_1} {N : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} [AddCommMonoid N] (f : S.LocalizationMap N) : Function.Injective ⇑f ↔ ∀ ⦃x : M⦄, x ∈ S → IsAddRegular x

theorem Submonoid.LocalizationMap.top_injective_iff {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] (f : ⊤.LocalizationMap N) : Function.Injective ⇑f ↔ IsCancelMul M

theorem AddSubmonoid.LocalizationMap.top_injective_iff {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] (f : ⊤.LocalizationMap N) : Function.Injective ⇑f ↔ IsCancelAdd M

theorem Submonoid.LocalizationMap.map_isRegular {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) {m : M} (hm : IsRegular m) : IsRegular (f m)

theorem AddSubmonoid.LocalizationMap.map_isAddRegular {M : Type u_1} {N : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} [AddCommMonoid N] (f : S.LocalizationMap N) {m : M} (hm : IsAddRegular m) : IsAddRegular (f m)

theorem Submonoid.LocalizationMap.isCancelMul {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) [IsCancelMul M] : IsCancelMul N

theorem AddSubmonoid.LocalizationMap.isCancelAdd {M : Type u_1} {N : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} [AddCommMonoid N] (f : S.LocalizationMap N) [IsCancelAdd M] : IsCancelAdd N

instance Submonoid.LocalizationMap.instIsCancelMulLocalization {M : Type u_1} [CommMonoid M] {S : Submonoid M} [IsCancelMul M] : IsCancelMul (Localization S)

instance AddSubmonoid.LocalizationMap.instIsCancelAddLocalization {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} [IsCancelAdd M] : IsCancelAdd (AddLocalization S)

instance Submonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelMul {M : Type u_1} [CommMonoid M] {S : Submonoid M} [IsCancelMul M] [Nontrivial M] : Nontrivial (Localization S)

instance AddSubmonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelAdd {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} [IsCancelAdd M] [Nontrivial M] : Nontrivial (AddLocalization S)

theorem Submonoid.LocalizationMap.subsingleton_of_subsingleton {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) [Subsingleton M] : Subsingleton N

theorem AddSubmonoid.LocalizationMap.subsingleton_of_subsingleton {M : Type u_1} {N : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} [AddCommMonoid N] (f : S.LocalizationMap N) [Subsingleton M] : Subsingleton N

instance Submonoid.LocalizationMap.instSubsingletonLocalization {M : Type u_1} [CommMonoid M] {S : Submonoid M} [Subsingleton M] : Subsingleton (Localization S)