Documentation

Mathlib.GroupTheory.MonoidLocalization

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→* N satisfying 3 properties:

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

Given such a localization map f : M →* N→* N, we can define the surjection LocalizationMap.mk' sending (x, y) : M × S× S to f x * (f y)⁻¹⁻¹, and LocalizationMap.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→* P such that g(S) ⊆ T⊆ T induces a homomorphism of localizations, LocalizationMap.map, from N to Q. We treat the special case of localizing away from an element in the sections AwayMap and Away.

We also define the quotient of M × S× S by the unique congruence relation (equivalence relation preserving a binary operation) r such that for any other congruence relation s on M × S× S satisfying '∀ y ∈ S∀ y ∈ S∈ S, (1, 1) ∼ (y, y)∼ (y, y) under s', we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by s whenever (x₁, y₁) ∼ (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.

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.toMap, as coercions don't work well for this structure.

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→ S → Localization S→ Localization S equals the surjection LocalizationMap.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_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.

Tags #

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

structure AddSubmonoid.LocalizationMap {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (N : Type u_2) [inst : AddCommMonoid N] extends AddMonoidHom :
Type (maxu_1u_2)

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

Instances For
    structure Submonoid.LocalizationMap {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (N : Type u_2) [inst : CommMonoid N] extends MonoidHom :
    Type (maxu_1u_2)

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

    Instances For
      def addLocalization.r {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
      AddCon (M × { x // x S })

      The congruence relation on M × S× S, M an AddCommMonoid 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× S such that for any other congruence relation s on M × S× S where for all y ∈ S∈ S, (0, 0) ∼ (y, y)∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by s.

      Equations
      def Localization.r {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :
      Con (M × { x // x S })

      The congruence relation on M × S× 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× S such that for any other congruence relation s on M × S× S where for all y ∈ S∈ S, (1, 1) ∼ (y, y)∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by s.

      Equations
      def addLocalization.r' {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
      AddCon (M × { x // x S })

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

      Equations
      • One or more equations did not get rendered due to their size.
      def addLocalization.r'.proof_2 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) {a : M × { x // x S }} {b : M × { x // x S }} {c : M × { x // x S }} {d : M × { x // x S }} :
      Setoid.r a bSetoid.r c dSetoid.r (a + c) (b + d)
      Equations
      def addLocalization.r'.proof_1 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
      Equivalence fun a b => c, c + (b.snd + a.fst) = c + (a.snd + b.fst)
      Equations
      • (_ : Equivalence fun a b => c, c + (b.snd + a.fst) = c + (a.snd + b.fst)) = (_ : Equivalence fun a b => c, c + (b.snd + a.fst) = c + (a.snd + b.fst))
      abbrev addLocalization.r'.match_1 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
      ∀ {x y : M × { x // x S }} (motive : (c, c + (y.snd + x.fst) = c + (x.snd + y.fst)) → Prop) (x_1 : c, c + (y.snd + x.fst) = c + (x.snd + y.fst)), (∀ (c : { x // x S }) (hc : c + (y.snd + x.fst) = c + (x.snd + y.fst)), motive (_ : c, c + (y.snd + x.fst) = c + (x.snd + y.fst))) → motive x_1
      Equations
      def Localization.r' {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :
      Con (M × { x // x S })

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

      Equations
      • One or more equations did not get rendered due to their size.
      abbrev addLocalization.r_eq_r'.match_1 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (p : M) (q : { x // x S }) (x : M) (y : { x // x S }) (motive : ↑(addLocalization.r' S) (p, q) (x, y)Prop) :
      (x : ↑(addLocalization.r' S) (p, q) (x, y)) → ((t : { x // x S }) → (ht : t + ((x, y).snd + (p, q).fst) = t + ((p, q).snd + (x, y).fst)) → motive (_ : c, c + ((x, y).snd + (p, q).fst) = c + ((p, q).snd + (x, y).fst))) → motive x
      Equations
      abbrev addLocalization.r_eq_r'.match_3 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
      (x : M × { x // x S }) → (motive : (x_1 : M × { x // x S }) → ↑(addLocalization.r' S) x_1 xProp) → ∀ (x_1 : M × { x // x S }) (x_2 : ↑(addLocalization.r' S) x_1 x), (∀ (p : M) (q : { x // x S }) (x : ↑(addLocalization.r' S) (p, q) x), motive (p, q) x) → motive x_1 x_2
      Equations
      abbrev addLocalization.r_eq_r'.match_2 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (p : M) (q : { x // x S }) (motive : (x : M × { x // x S }) → ↑(addLocalization.r' S) (p, q) xProp) :
      (x : M × { x // x S }) → (x_1 : ↑(addLocalization.r' S) (p, q) x) → ((x : M) → (y : { x // x S }) → (x_2 : ↑(addLocalization.r' S) (p, q) (x, y)) → motive (x, y) x_2) → motive x x_1
      Equations

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

      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_iff_exists {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {x : M × { x // x S }} {y : M × { x // x S }} :
      ↑(addLocalization.r S) x y c, c + (y.snd + x.fst) = c + (x.snd + y.fst)
      theorem Localization.r_iff_exists {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {x : M × { x // x S }} {y : M × { x // x S }} :
      ↑(Localization.r S) x y c, c * (y.snd * x.fst) = c * (x.snd * y.fst)
      def addLocalization {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
      Type u_1

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

      Equations
      def Localization {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :
      Type u_1

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

      Equations
      Equations
      instance Localization.inhabited {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :
      Equations

      Addition in an addLocalization 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
      def Localization.mul {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :

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

      Equations

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

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

      Equations
      def Localization.one {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :

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

      Equations

      Multiplication with a natural in an AddLocalization 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
      def Localization.npow {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :

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

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

      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      def addLocalization.mk {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (x : M) (y : { x // x S }) :

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

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

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

      Equations
      theorem addLocalization.mk_eq_mk_iff {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {a : M} {c : M} {b : { x // x S }} {d : { x // x S }} :
      theorem Localization.mk_eq_mk_iff {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {a : M} {c : M} {b : { x // x S }} {d : { x // x S }} :
      Localization.mk a b = Localization.mk c d ↑(Localization.r S) (a, b) (c, d)
      def addLocalization.rec {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SSort u} (f : (a : M) → (b : { x // x S }) → p (addLocalization.mk a b)) (H : ∀ {a c : M} {b d : { x // x S }} (h : ↑(addLocalization.r S) (a, b) (c, d)), (_ : addLocalization.mk a b = addLocalization.mk 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
      • One or more equations did not get rendered due to their size.
      def addLocalization.rec.proof_1 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {a : M} {c : M} {b : { x // x S }} {d : { x // x S }} (h : ↑(addLocalization.r S) (a, b) (c, d)) :
      Equations
      def addLocalization.rec.proof_3 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SSort u_2} (f : (a : M) → (b : { x // x S }) → p (addLocalization.mk a b)) (H : ∀ {a c : M} {b d : { x // x S }} (h : ↑(addLocalization.r S) (a, b) (c, d)), (_ : addLocalization.mk a b = addLocalization.mk c d)f a b = f c d) (y : M × { x // x S }) (z : M × { x // x S }) (h : Setoid.r y z) :
      (_ : Quot.mk Setoid.r y = Quot.mk Setoid.r z)(fun y => (_ : addLocalization.mk y.fst y.snd = addLocalization.mk y.fst y.snd)f y.fst y.snd) y = (fun y => (_ : addLocalization.mk y.fst y.snd = addLocalization.mk y.fst y.snd)f y.fst y.snd) z
      Equations
      • One or more equations did not get rendered due to their size.
      def addLocalization.rec.proof_2 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (y : M × { x // x S }) :
      addLocalization.mk y.fst y.snd = addLocalization.mk y.fst y.snd
      Equations
      def Localization.rec {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization SSort u} (f : (a : M) → (b : { x // x S }) → p (Localization.mk a b)) (H : ∀ {a c : M} {b d : { x // x S }} (h : ↑(Localization.r S) (a, b) (c, d)), (_ : Localization.mk a b = Localization.mk 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
      • One or more equations did not get rendered due to their size.
      theorem addLocalization.mk_add {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (a : M) (c : M) (b : { x // x S }) (d : { x // x S }) :
      theorem Localization.mk_mul {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (a : M) (c : M) (b : { x // x S }) (d : { x // x S }) :
      theorem Localization.mk_one {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} :
      theorem addLocalization.mk_nsmul {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (n : ) (a : M) (b : { x // x S }) :
      theorem Localization.mk_pow {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (n : ) (a : M) (b : { x // x S }) :
      Localization.mk a b ^ n = Localization.mk (a ^ n) (b ^ n)
      @[simp]
      theorem addLocalization.ndrec_mk {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SSort u} (f : (a : M) → (b : { x // x S }) → p (addLocalization.mk a b)) (H : ∀ {a c : M} {b d : { x // x S }} (h : ↑(addLocalization.r S) (a, b) (c, d)), (_ : addLocalization.mk a b = addLocalization.mk c d)f a b = f c d) (a : M) (b : { x // x S }) :
      @[simp]
      theorem Localization.ndrec_mk {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization SSort u} (f : (a : M) → (b : { x // x S }) → p (Localization.mk a b)) (H : ∀ {a c : M} {b d : { x // x S }} (h : ↑(Localization.r S) (a, b) (c, d)), (_ : Localization.mk a b = Localization.mk c d)f a b = f c d) (a : M) (b : { x // x S }) :
      def addLocalization.liftOn.proof_1 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_2} (f : M{ x // x S }p) (H : ∀ {a c : M} {b d : { x // x S }}, ↑(addLocalization.r S) (a, b) (c, d)f a b = f c d) :
      ∀ {a c : M} {b d : { x // x S }} (h : ↑(addLocalization.r S) (a, b) (c, d)), (_ : addLocalization.mk a b = addLocalization.mk c d)f a b = f c d
      Equations
      def addLocalization.liftOn {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (x : addLocalization S) (f : M{ x // x S }p) (H : ∀ {a c : M} {b d : { x // x S }}, ↑(addLocalization.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
      • One or more equations did not get rendered due to their size.
      def Localization.liftOn {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (x : Localization S) (f : M{ x // x S }p) (H : ∀ {a c : M} {b d : { x // x 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
      • One or more equations did not get rendered due to their size.
      theorem addLocalization.liftOn_mk {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (f : M{ x // x S }p) (H : ∀ {a c : M} {b d : { x // x S }}, ↑(addLocalization.r S) (a, b) (c, d)f a b = f c d) (a : M) (b : { x // x S }) :
      theorem Localization.liftOn_mk {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (f : M{ x // x S }p) (H : ∀ {a c : M} {b d : { x // x S }}, ↑(Localization.r S) (a, b) (c, d)f a b = f c d) (a : M) (b : { x // x S }) :
      theorem addLocalization.ind {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SProp} (H : (y : M × { x // x S }) → p (addLocalization.mk y.fst y.snd)) (x : addLocalization S) :
      p x
      theorem Localization.ind {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization SProp} (H : (y : M × { x // x S }) → p (Localization.mk y.fst y.snd)) (x : Localization S) :
      p x
      theorem addLocalization.induction_on {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SProp} (x : addLocalization S) (H : (y : M × { x // x S }) → p (addLocalization.mk y.fst y.snd)) :
      p x
      theorem Localization.induction_on {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization SProp} (x : Localization S) (H : (y : M × { x // x S }) → p (Localization.mk y.fst y.snd)) :
      p x
      def addLocalization.liftOn₂.proof_2 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_2} (y : addLocalization S) (f : M{ x // x S }M{ x // x S }p) (H : ∀ {a a' : M} {b b' : { x // x S }} {c c' : M} {d d' : { x // x S }}, ↑(addLocalization.r S) (a, b) (a', b')↑(addLocalization.r S) (c, d) (c', d')f a b c d = f a' b' c' d') :
      ∀ {a c : M} {b d : { x // x S }}, ↑(addLocalization.r S) (a, b) (c, d)(fun a b => addLocalization.liftOn y (f a b) fun {a_1 c} {b_1 d} hy => H a a b b a_1 c b_1 d (_ : ↑(addLocalization.r S) (a, b) (a, b)) hy) a b = (fun a b => addLocalization.liftOn y (f a b) fun {a_1 c} {b_1 d} hy => H a a b b a_1 c b_1 d (_ : ↑(addLocalization.r S) (a, b) (a, b)) hy) c d
      Equations
      • One or more equations did not get rendered due to their size.
      abbrev addLocalization.liftOn₂.match_1 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (motive : M × { x // x S }Prop) :
      (x : M × { x // x S }) → ((fst : M) → (snd : { x // x S }) → motive (fst, snd)) → motive x
      Equations
      def addLocalization.liftOn₂ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (x : addLocalization S) (y : addLocalization S) (f : M{ x // x S }M{ x // x S }p) (H : ∀ {a a' : M} {b b' : { x // x S }} {c c' : M} {d d' : { x // x S }}, ↑(addLocalization.r S) (a, b) (a', b')↑(addLocalization.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
      • One or more equations did not get rendered due to their size.
      def addLocalization.liftOn₂.proof_1 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_2} (f : M{ x // x S }M{ x // x S }p) (H : ∀ {a a' : M} {b b' : { x // x S }} {c c' : M} {d d' : { x // x S }}, ↑(addLocalization.r S) (a, b) (a', b')↑(addLocalization.r S) (c, d) (c', d')f a b c d = f a' b' c' d') (a : M) (b : { x // x S }) :
      ∀ {a c : M} {b d : { x // x S }}, ↑(addLocalization.r S) (a, b) (c, d)f a b a b = f a b c d
      Equations
      • (_ : f a b a b = f a b c d) = H a a b b a c b d (_ : ↑(addLocalization.r S) (a, b) (a, b)) hy
      def Localization.liftOn₂ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (x : Localization S) (y : Localization S) (f : M{ x // x S }M{ x // x S }p) (H : ∀ {a a' : M} {b b' : { x // x S }} {c c' : M} {d d' : { x // x 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
      • One or more equations did not get rendered due to their size.
      theorem addLocalization.liftOn₂_mk {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_1} (f : M{ x // x S }M{ x // x S }p) (H : ∀ {a a' : M} {b b' : { x // x S }} {c c' : M} {d d' : { x // x S }}, ↑(addLocalization.r S) (a, b) (a', b')↑(addLocalization.r S) (c, d) (c', d')f a b c d = f a' b' c' d') (a : M) (c : M) (b : { x // x S }) (d : { x // x S }) :
      theorem Localization.liftOn₂_mk {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u_1} (f : M{ x // x S }M{ x // x S }p) (H : ∀ {a a' : M} {b b' : { x // x S }} {c c' : M} {d d' : { x // x 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 : M) (c : M) (b : { x // x S }) (d : { x // x S }) :
      theorem addLocalization.induction_on₂ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SaddLocalization SProp} (x : addLocalization S) (y : addLocalization S) (H : (x y : M × { x // x S }) → p (addLocalization.mk x.fst x.snd) (addLocalization.mk y.fst y.snd)) :
      p x y
      theorem Localization.induction_on₂ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization SLocalization SProp} (x : Localization S) (y : Localization S) (H : (x y : M × { x // x S }) → p (Localization.mk x.fst x.snd) (Localization.mk y.fst y.snd)) :
      p x y
      theorem addLocalization.induction_on₃ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : addLocalization SaddLocalization SaddLocalization SProp} (x : addLocalization S) (y : addLocalization S) (z : addLocalization S) (H : (x y z : M × { x // x S }) → p (addLocalization.mk x.fst x.snd) (addLocalization.mk y.fst y.snd) (addLocalization.mk z.fst z.snd)) :
      p x y z
      theorem Localization.induction_on₃ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization SLocalization SLocalization SProp} (x : Localization S) (y : Localization S) (z : Localization S) (H : (x y z : M × { x // x S }) → p (Localization.mk x.fst x.snd) (Localization.mk y.fst y.snd) (Localization.mk z.fst z.snd)) :
      p x y z
      theorem addLocalization.zero_rel {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (y : { x // x S }) :
      ↑(addLocalization.r S) 0 (y, y)
      theorem Localization.one_rel {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (y : { x // x S }) :
      ↑(Localization.r S) 1 (y, y)
      theorem addLocalization.r_of_eq {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {x : M × { x // x S }} {y : M × { x // x S }} (h : y.snd + x.fst = x.snd + y.fst) :
      theorem Localization.r_of_eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {x : M × { x // x S }} {y : M × { x // x S }} (h : y.snd * x.fst = x.snd * y.fst) :
      ↑(Localization.r S) x y
      theorem addLocalization.mk_self {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (a : { x // x S }) :
      theorem Localization.mk_self {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (a : { x // x S }) :
      Localization.mk (a) a = 1
      def Localization.smul {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_2} [inst : SMul R M] [inst : IsScalarTower R M M] (c : R) (z : Localization S) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      instance Localization.instSMulLocalization {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_2} [inst : SMul R M] [inst : IsScalarTower R M M] :
      Equations
      • Localization.instSMulLocalization = { smul := Localization.smul }
      theorem Localization.smul_mk {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_1} [inst : SMul R M] [inst : IsScalarTower R M M] (c : R) (a : M) (b : { x // x S }) :
      instance Localization.instMulActionLocalization {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_2} [inst : Monoid R] [inst : MulAction R M] [inst : IsScalarTower R M M] :
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      def AddMonoidHom.toLocalizationMap.proof_1 {M : Type u_2} [inst : AddCommMonoid M] {N : Type u_1} [inst : AddCommMonoid N] (f : M →+ N) (x : M) (y : M) :
      ZeroHom.toFun (f) (x + y) = ZeroHom.toFun (f) x + ZeroHom.toFun (f) y
      Equations
      def AddMonoidHom.toLocalizationMap {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : M →+ N) (H1 : ∀ (y : { x // x S }), IsAddUnit (f y)) (H2 : ∀ (z : N), x, z + f x.snd = f x.fst) (H3 : ∀ (x y : M), f x = f y c, c + x = c + y) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      def MonoidHom.toLocalizationMap {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : M →* N) (H1 : ∀ (y : { x // x S }), IsUnit (f y)) (H2 : ∀ (z : N), x, z * f x.snd = f x.fst) (H3 : ∀ (x y : M), f x = f y c, c * x = c * y) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      abbrev AddSubmonoid.LocalizationMap.toMap {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) :
      M →+ N

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

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

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

      Equations
      theorem Submonoid.LocalizationMap.ext {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {f : Submonoid.LocalizationMap S N} {g : Submonoid.LocalizationMap S N} (h : ∀ (x : M), ↑(Submonoid.LocalizationMap.toMap f) x = ↑(Submonoid.LocalizationMap.toMap g) x) :
      f = g
      theorem AddSubmonoid.LocalizationMap.toMap_injective {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] :
      Function.Injective AddSubmonoid.LocalizationMap.toMap
      theorem Submonoid.LocalizationMap.toMap_injective {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] :
      Function.Injective Submonoid.LocalizationMap.toMap
      theorem Submonoid.LocalizationMap.map_units {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (y : { x // x S }) :
      theorem AddSubmonoid.LocalizationMap.surj {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (z : N) :
      theorem Submonoid.LocalizationMap.surj {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (z : N) :
      theorem AddSubmonoid.LocalizationMap.eq_iff_exists {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {x : M} {y : M} :
      theorem Submonoid.LocalizationMap.eq_iff_exists {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x : M} {y : M} :
      noncomputable def AddSubmonoid.LocalizationMap.sec {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (z : N) :
      M × { x // x S }

      Given a localization map f : M →+ N→+ N, a section function sending z : N to some (x, y) : M × S× S such that f x - f y = z.

      Equations
      noncomputable def Submonoid.LocalizationMap.sec {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (z : N) :
      M × { x // x S }

      Given a localization map f : M →* N→* N, a section function sending z : N to some (x, y) : M × S× S such that f x * (f y)⁻¹ = z⁻¹ = z.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      theorem AddSubmonoid.LocalizationMap.neg_unique {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {f : M →+ N} (h : ∀ (y : { x // x S }), IsAddUnit (f y)) {y : { x // x S }} {z : N} (H : f y + z = 0) :

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

      theorem Submonoid.LocalizationMap.inv_unique {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {f : M →* N} (h : ∀ (y : { x // x S }), IsUnit (f y)) {y : { x // x S }} {z : N} (H : f y * z = 1) :

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

      theorem Submonoid.LocalizationMap.map_right_cancel {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x : M} {y : M} {c : { x // x S }} (h : ↑(Submonoid.LocalizationMap.toMap f) (c * x) = ↑(Submonoid.LocalizationMap.toMap f) (c * y)) :
      theorem Submonoid.LocalizationMap.map_left_cancel {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x : M} {y : M} {c : { x // x S }} (h : ↑(Submonoid.LocalizationMap.toMap f) (x * c) = ↑(Submonoid.LocalizationMap.toMap f) (y * c)) :
      noncomputable def AddSubmonoid.LocalizationMap.mk' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :
      N

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

      Equations
      • One or more equations did not get rendered due to their size.
      noncomputable def Submonoid.LocalizationMap.mk' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :
      N

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

      Equations
      • One or more equations did not get rendered due to their size.
      theorem AddSubmonoid.LocalizationMap.mk'_add {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x₁ : M) (x₂ : M) (y₁ : { x // x S }) (y₂ : { x // x S }) :
      theorem Submonoid.LocalizationMap.mk'_mul {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x₁ : M) (x₂ : M) (y₁ : { x // x S }) (y₂ : { x // x S }) :
      @[simp]

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

      @[simp]

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

      theorem Submonoid.LocalizationMap.mk'_surjective {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (z : N) :
      theorem Submonoid.LocalizationMap.mk'_spec {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.mk'_spec' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.eq_mk'_iff_mul_eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x : M} {y : { x // x S }} {z : N} :
      theorem Submonoid.LocalizationMap.mk'_eq_iff_eq_mul {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x : M} {y : { x // x S }} {z : N} :
      theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_eq {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {x₁ : M} {x₂ : M} {y₁ : { x // x S }} {y₂ : { x // x S }} :
      theorem Submonoid.LocalizationMap.mk'_eq_iff_eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x₁ : M} {x₂ : M} {y₁ : { x // x S }} {y₂ : { x // x S }} :
      theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_eq' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {x₁ : M} {x₂ : M} {y₁ : { x // x S }} {y₂ : { x // x S }} :
      theorem Submonoid.LocalizationMap.mk'_eq_iff_eq' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {x₁ : M} {x₂ : M} {y₁ : { x // x S }} {y₂ : { x // x S }} :
      theorem AddSubmonoid.LocalizationMap.eq {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} :
      AddSubmonoid.LocalizationMap.mk' f a₁ a₂ = AddSubmonoid.LocalizationMap.mk' f b₁ b₂ c, c + (b₂ + a₁) = c + (a₂ + b₁)
      theorem Submonoid.LocalizationMap.eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} :
      Submonoid.LocalizationMap.mk' f a₁ a₂ = Submonoid.LocalizationMap.mk' f b₁ b₂ c, c * (b₂ * a₁) = c * (a₂ * b₁)
      theorem AddSubmonoid.LocalizationMap.eq' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} :
      AddSubmonoid.LocalizationMap.mk' f a₁ a₂ = AddSubmonoid.LocalizationMap.mk' f b₁ b₂ ↑(addLocalization.r S) (a₁, a₂) (b₁, b₂)
      theorem Submonoid.LocalizationMap.eq' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} :
      Submonoid.LocalizationMap.mk' f a₁ a₂ = Submonoid.LocalizationMap.mk' f b₁ b₂ ↑(Localization.r S) (a₁, a₂) (b₁, b₂)
      theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_mk'_eq {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) (g : AddSubmonoid.LocalizationMap S P) {x₁ : M} {x₂ : M} {y₁ : { x // x S }} {y₂ : { x // x S }} :
      theorem Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) (g : Submonoid.LocalizationMap S P) {x₁ : M} {x₂ : M} {y₁ : { x // x S }} {y₂ : { x // x S }} :
      theorem AddSubmonoid.LocalizationMap.exists_of_sec_mk' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :

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

      theorem Submonoid.LocalizationMap.exists_of_sec_mk' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :

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

      theorem AddSubmonoid.LocalizationMap.mk'_eq_of_eq {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} (H : a₂ + b₁ = b₂ + a₁) :
      theorem Submonoid.LocalizationMap.mk'_eq_of_eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} (H : a₂ * b₁ = b₂ * a₁) :
      theorem AddSubmonoid.LocalizationMap.mk'_eq_of_eq' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} (H : b₁ + a₂ = a₁ + b₂) :
      theorem Submonoid.LocalizationMap.mk'_eq_of_eq' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) {a₁ : M} {b₁ : M} {a₂ : { x // x S }} {b₂ : { x // x S }} (H : b₁ * a₂ = a₁ * b₂) :
      @[simp]
      theorem AddSubmonoid.LocalizationMap.mk'_self' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (y : { x // x S }) :
      @[simp]
      theorem Submonoid.LocalizationMap.mk'_self' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (y : { x // x S }) :
      @[simp]
      theorem AddSubmonoid.LocalizationMap.mk'_self {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x : M) (H : x S) :
      AddSubmonoid.LocalizationMap.mk' f x { val := x, property := H } = 0
      @[simp]
      theorem Submonoid.LocalizationMap.mk'_self {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (H : x S) :
      Submonoid.LocalizationMap.mk' f x { val := x, property := H } = 1
      theorem AddSubmonoid.LocalizationMap.add_mk'_eq_mk'_of_add {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x₁ : M) (x₂ : M) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x₁ : M) (x₂ : M) (y : { x // x S }) :
      theorem AddSubmonoid.LocalizationMap.mk'_add_eq_mk'_of_add {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x₁ : M) (x₂ : M) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.mk'_mul_eq_mk'_of_mul {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x₁ : M) (x₂ : M) (y : { x // x S }) :
      @[simp]
      @[simp]
      theorem Submonoid.LocalizationMap.mk'_mul_cancel_right {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.mk'_mul_cancel_left {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : M) (y : { x // x S }) :
      theorem AddSubmonoid.LocalizationMap.isAddUnit_comp {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) (j : N →+ P) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.isUnit_comp {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) (j : N →* P) (y : { x // x S }) :
      theorem AddSubmonoid.LocalizationMap.eq_of_eq {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) {x : M} {y : M} (h : ↑(AddSubmonoid.LocalizationMap.toMap f) x = ↑(AddSubmonoid.LocalizationMap.toMap f) y) :
      g x = g y

      Given a Localization map f : M →+ N→+ N for a Submonoid S ⊆ M⊆ M and a map of AddCommMonoids g : M →+ P→+ P such that g(S) ⊆ AddUnits P⊆ AddUnits P, f x = f y → g x = g y→ g x = g y for all x y : M.

      theorem Submonoid.LocalizationMap.eq_of_eq {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) {x : M} {y : M} (h : ↑(Submonoid.LocalizationMap.toMap f) x = ↑(Submonoid.LocalizationMap.toMap f) y) :
      g x = g y

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M and a map of CommMonoids g : M →* P→* P such that g(S) ⊆ Units P⊆ Units P, f x = f y → g x = g y→ g x = g y for all x y : M.

      theorem AddSubmonoid.LocalizationMap.comp_eq_of_eq {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_4} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} {Q : Type u_2} [inst : AddCommMonoid Q] (hg : ∀ (y : { x // x S }), g y T) (k : AddSubmonoid.LocalizationMap T Q) {x : M} {y : M} (h : ↑(AddSubmonoid.LocalizationMap.toMap f) x = ↑(AddSubmonoid.LocalizationMap.toMap f) y) :

      Given AddCommMonoids M, P, Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q for Submonoids S, T respectively, and g : M →+ P→+ P such that g(S) ⊆ T⊆ T, f x = f y implies k (g x) = k (g y).

      theorem Submonoid.LocalizationMap.comp_eq_of_eq {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_4} [inst : CommMonoid N] {P : Type u_1} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} {Q : Type u_2} [inst : CommMonoid Q] (hg : ∀ (y : { x // x S }), g y T) (k : Submonoid.LocalizationMap T Q) {x : M} {y : M} (h : ↑(Submonoid.LocalizationMap.toMap f) x = ↑(Submonoid.LocalizationMap.toMap f) y) :

      Given CommMonoids M, P, Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q for Submonoids S, T respectively, and g : M →* P→* P such that g(S) ⊆ T⊆ T, f x = f y implies k (g x) = k (g y).

      def AddSubmonoid.LocalizationMap.lift.proof_2 {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) :
      Equations
      • One or more equations did not get rendered due to their size.
      def AddSubmonoid.LocalizationMap.lift.proof_3 {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (x : N) (y : N) :
      ZeroHom.toFun { toFun := fun z => g (AddSubmonoid.LocalizationMap.sec f z).fst + ↑(-↑(IsAddUnit.liftRight (AddMonoidHom.restrict g S) hg) (AddSubmonoid.LocalizationMap.sec f z).snd), map_zero' := (_ : (fun z => g (AddSubmonoid.LocalizationMap.sec f z).fst + ↑(-↑(IsAddUnit.liftRight (AddMonoidHom.restrict g S) hg) (AddSubmonoid.LocalizationMap.sec f z).snd)) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun z => g (AddSubmonoid.LocalizationMap.sec f z).fst + ↑(-↑(IsAddUnit.liftRight (AddMonoidHom.restrict g S) hg) (AddSubmonoid.LocalizationMap.sec f z).snd), map_zero' := (_ : (fun z => g (AddSubmonoid.LocalizationMap.sec f z).fst + ↑(-↑(IsAddUnit.liftRight (AddMonoidHom.restrict g S) hg) (AddSubmonoid.LocalizationMap.sec f z).snd)) 0 = 0) } x + ZeroHom.toFun { toFun := fun z => g (AddSubmonoid.LocalizationMap.sec f z).fst + ↑(-↑(IsAddUnit.liftRight (AddMonoidHom.restrict g S) hg) (AddSubmonoid.LocalizationMap.sec f z).snd), map_zero' := (_ : (fun z => g (AddSubmonoid.LocalizationMap.sec f z).fst + ↑(-↑(IsAddUnit.liftRight (AddMonoidHom.restrict g S) hg) (AddSubmonoid.LocalizationMap.sec f z).snd)) 0 = 0) } y
      Equations
      • One or more equations did not get rendered due to their size.
      noncomputable def AddSubmonoid.LocalizationMap.lift {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {P : Type u_3} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) :
      N →+ P

      Given a localization map f : M →+ N→+ N for a submonoid S ⊆ M⊆ M and a map of AddCommMonoids g : M →+ P→+ 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× S are such that z = f x - f y.

      Equations
      • One or more equations did not get rendered due to their size.
      noncomputable def Submonoid.LocalizationMap.lift {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {P : Type u_3} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) :
      N →* P

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M and a map of CommMonoids g : M →* P→* 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× S are such that z = f x * (f y)⁻¹⁻¹.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem AddSubmonoid.LocalizationMap.lift_mk' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (x : M) (y : { x // x S }) :

      Given a Localization map f : M →+ N→+ N for a Submonoid S ⊆ M⊆ M and a map of AddCommMonoids g : M →+ P→+ 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∈ S.

      theorem Submonoid.LocalizationMap.lift_mk' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (x : M) (y : { x // x S }) :

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M and a map of CommMonoids g : M →* P→* 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∈ S.

      theorem AddSubmonoid.LocalizationMap.lift_spec {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (z : N) (v : P) :

      Given a Localization map f : M →+ N→+ N for a Submonoid S ⊆ M⊆ M, if an AddCommMonoid map g : M →+ P→+ P induces a map f.lift hg : N →+ P→+ P then for all z : N, v : P, we have f.lift hg z = v ↔ g x = g y + v↔ g x = g y + v, where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.lift_spec {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {P : Type u_1} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (z : N) (v : (fun x => P) z) :

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M, if a CommMonoid map g : M →* P→* P induces a map f.lift hg : N →* P→* P then for all z : N, v : P, we have f.lift hg z = v ↔ g x = g y * v↔ g x = g y * v, where x : M, y ∈ S∈ S are such that z * f y = f x.

      theorem AddSubmonoid.LocalizationMap.lift_spec_add {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (z : N) (w : P) (v : P) :

      Given a Localization map f : M →+ N→+ N for a Submonoid S ⊆ M⊆ M, if an AddCommMonoid map g : M →+ P→+ P induces a map f.lift hg : N →+ P→+ P then for all z : N, v w : P, we have f.lift hg z + w = v ↔ g x + w = g y + v↔ g x + w = g y + v, where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.lift_spec_mul {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {P : Type u_1} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (z : N) (w : (fun x => P) z) (v : (fun x => P) z) :

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M, if a CommMonoid map g : M →* P→* P induces a map f.lift hg : N →* P→* P then for all z : N, v w : P, we have f.lift hg z * w = v ↔ g x * w = g y * v↔ g x * w = g y * v, where x : M, y ∈ S∈ S are such that z * f y = f x.

      theorem AddSubmonoid.LocalizationMap.lift_mk'_spec {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (x : M) (v : P) (y : { x // x S }) :
      theorem Submonoid.LocalizationMap.lift_mk'_spec {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (x : M) (v : P) (y : { x // x S }) :
      ↑(Submonoid.LocalizationMap.lift f hg) (Submonoid.LocalizationMap.mk' f x y) = v g x = g y * v
      theorem AddSubmonoid.LocalizationMap.lift_add_right {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (z : N) :

      Given a Localization map f : M →+ N→+ N for a Submonoid S ⊆ M⊆ M, if an AddCommMonoid map g : M →+ P→+ P induces a map f.lift hg : N →+ P→+ P then for all z : N, we have f.lift hg z + g y = g x, where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.lift_mul_right {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_1} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (z : N) :

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M, if a CommMonoid map g : M →* P→* P induces a map f.lift hg : N →* P→* P then for all z : N, we have f.lift hg z * g y = g x, where x : M, y ∈ S∈ S are such that z * f y = f x.

      theorem AddSubmonoid.LocalizationMap.lift_add_left {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (z : N) :

      Given a Localization map f : M →+ N→+ N for a Submonoid S ⊆ M⊆ M, if an AddCommMonoid map g : M →+ P→+ P induces a map f.lift hg : N →+ P→+ P then for all z : N, we have g y + f.lift hg z = g x, where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.lift_mul_left {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_1} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (z : N) :

      Given a Localization map f : M →* N→* N for a Submonoid S ⊆ M⊆ M, if a CommMonoid map g : M →* P→* P induces a map f.lift hg : N →* P→* P then for all z : N, we have g y * f.lift hg z = g x, where x : M, y ∈ S∈ S are such that z * f y = f x.

      @[simp]
      theorem AddSubmonoid.LocalizationMap.lift_eq {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_1} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) (x : M) :
      @[simp]
      theorem Submonoid.LocalizationMap.lift_eq {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_1} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) (x : M) :
      theorem AddSubmonoid.LocalizationMap.lift_eq_iff {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) {x : M × { x // x S }} {y : M × { x // x S }} :
      ↑(AddSubmonoid.LocalizationMap.lift f hg) (AddSubmonoid.LocalizationMap.mk' f x.fst x.snd) = ↑(AddSubmonoid.LocalizationMap.lift f hg) (AddSubmonoid.LocalizationMap.mk' f y.fst y.snd) g (x.fst + y.snd) = g (y.fst + x.snd)
      theorem Submonoid.LocalizationMap.lift_eq_iff {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) {x : M × { x // x S }} {y : M × { x // x S }} :
      ↑(Submonoid.LocalizationMap.lift f hg) (Submonoid.LocalizationMap.mk' f x.fst x.snd) = ↑(Submonoid.LocalizationMap.lift f hg) (Submonoid.LocalizationMap.mk' f y.fst y.snd) g (x.fst * y.snd) = g (y.fst * x.snd)
      @[simp]
      theorem AddSubmonoid.LocalizationMap.lift_comp {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) :
      @[simp]
      theorem Submonoid.LocalizationMap.lift_comp {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) :
      @[simp]
      theorem AddSubmonoid.LocalizationMap.lift_of_comp {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) (j : N →+ P) :
      @[simp]
      theorem Submonoid.LocalizationMap.lift_of_comp {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) (j : N →* P) :
      Submonoid.LocalizationMap.lift f (_ : ∀ (y : { x // x S }), IsUnit (↑(MonoidHom.comp j (Submonoid.LocalizationMap.toMap f)) y)) = j
      theorem Submonoid.LocalizationMap.epic_of_localizationMap {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {j : N →* P} {k : N →* P} (h : ∀ (a : M), ↑(MonoidHom.comp j (Submonoid.LocalizationMap.toMap f)) a = ↑(MonoidHom.comp k (Submonoid.LocalizationMap.toMap f)) a) :
      j = k
      theorem AddSubmonoid.LocalizationMap.lift_unique {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) {j : N →+ P} (hj : ∀ (x : M), j (↑(AddSubmonoid.LocalizationMap.toMap f) x) = g x) :
      theorem Submonoid.LocalizationMap.lift_unique {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) {j : N →* P} (hj : ∀ (x : M), j (↑(Submonoid.LocalizationMap.toMap f) x) = g x) :
      @[simp]
      theorem AddSubmonoid.LocalizationMap.lift_id {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (x : N) :
      ↑(AddSubmonoid.LocalizationMap.lift f (_ : ∀ (y : { x // x S }), IsAddUnit (↑(AddSubmonoid.LocalizationMap.toMap f) y))) x = x
      @[simp]
      theorem Submonoid.LocalizationMap.lift_id {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (x : N) :
      ↑(Submonoid.LocalizationMap.lift f (_ : ∀ (y : { x // x S }), IsUnit (↑(Submonoid.LocalizationMap.toMap f) y))) x = x
      @[simp]
      theorem AddSubmonoid.LocalizationMap.lift_left_inverse {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {k : AddSubmonoid.LocalizationMap S P} (z : N) :
      ↑(AddSubmonoid.LocalizationMap.lift k (_ : ∀ (y : { x // x S }), IsAddUnit (↑(AddSubmonoid.LocalizationMap.toMap f) y))) (↑(AddSubmonoid.LocalizationMap.lift f (_ : ∀ (y : { x // x S }), IsAddUnit (↑(AddSubmonoid.LocalizationMap.toMap k) y))) z) = z

      Given two Localization maps f : M →+ N, k : M →+ P→+ N, k : M →+ P→+ P for a Submonoid S ⊆ M⊆ M, the hom from P to N induced by f is left inverse to the hom from N to P induced by k.

      @[simp]
      theorem Submonoid.LocalizationMap.lift_left_inverse {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {k : Submonoid.LocalizationMap S P} (z : N) :
      ↑(Submonoid.LocalizationMap.lift k (_ : ∀ (y : { x // x S }), IsUnit (↑(Submonoid.LocalizationMap.toMap f) y))) (↑(Submonoid.LocalizationMap.lift f (_ : ∀ (y : { x // x S }), IsUnit (↑(Submonoid.LocalizationMap.toMap k) y))) z) = z

      Given two Localization maps f : M →* N, k : M →* P→* N, k : M →* P→* P for a Submonoid S ⊆ M⊆ M, the hom from P to N induced by f is left inverse to the hom from N to P induced by k.

      theorem AddSubmonoid.LocalizationMap.lift_surjective_iff {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) :
      Function.Surjective ↑(AddSubmonoid.LocalizationMap.lift f hg) ∀ (v : P), x, v + g x.snd = g x.fst
      theorem Submonoid.LocalizationMap.lift_surjective_iff {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) :
      Function.Surjective ↑(Submonoid.LocalizationMap.lift f hg) ∀ (v : P), x, v * g x.snd = g x.fst
      theorem AddSubmonoid.LocalizationMap.lift_injective_iff {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] {P : Type u_2} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} (hg : ∀ (y : { x // x S }), IsAddUnit (g y)) :
      theorem Submonoid.LocalizationMap.lift_injective_iff {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] {P : Type u_2} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} (hg : ∀ (y : { x // x S }), IsUnit (g y)) :
      noncomputable def AddSubmonoid.LocalizationMap.map {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {P : Type u_3} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_4} [inst : AddCommMonoid Q] (k : AddSubmonoid.LocalizationMap T Q) :
      N →+ Q

      Given a AddCommMonoid homomorphism g : M →+ P→+ P where for Submonoids S ⊆ M, T ⊆ P⊆ M, T ⊆ P⊆ P we have g(S) ⊆ T⊆ T, the induced AddMonoid homomorphism from the Localization of M at S to the Localization of P at T: if f : M →+ N→+ N and k : P →+ Q→+ 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× S are such that z = f x - f y.

      Equations
      • One or more equations did not get rendered due to their size.
      def AddSubmonoid.LocalizationMap.map.proof_1 {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_3} [inst : AddCommMonoid P] {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_2} [inst : AddCommMonoid Q] (k : AddSubmonoid.LocalizationMap T Q) (y : { x // x S }) :
      IsAddUnit (↑(AddSubmonoid.LocalizationMap.toMap k) { val := g y, property := hy y })
      Equations
      noncomputable def Submonoid.LocalizationMap.map {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {P : Type u_3} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_4} [inst : CommMonoid Q] (k : Submonoid.LocalizationMap T Q) :
      N →* Q

      Given a CommMonoid homomorphism g : M →* P→* P where for Submonoids S ⊆ M, T ⊆ P⊆ M, T ⊆ P⊆ P we have g(S) ⊆ T⊆ T, the induced Monoid homomorphism from the Localization of M at S to the Localization of P at T: if f : M →* N→* N and k : P →* Q→* 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× S are such that z = f x * (f y)⁻¹⁻¹.

      Equations
      theorem AddSubmonoid.LocalizationMap.map_eq {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_4} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} (x : M) :
      theorem Submonoid.LocalizationMap.map_eq {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_4} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} (x : M) :
      @[simp]
      theorem AddSubmonoid.LocalizationMap.map_comp {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_4} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_2} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} :
      @[simp]
      theorem Submonoid.LocalizationMap.map_comp {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_4} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_2} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} :
      theorem AddSubmonoid.LocalizationMap.map_mk' {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [inst : AddCommMonoid N] {P : Type u_4} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_2} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} (x : M) (y : { x // x S }) :
      ↑(AddSubmonoid.LocalizationMap.map f hy k) (AddSubmonoid.LocalizationMap.mk' f x y) = AddSubmonoid.LocalizationMap.mk' k (g x) { val := g y, property := hy y }
      theorem Submonoid.LocalizationMap.map_mk' {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_3} [inst : CommMonoid N] {P : Type u_4} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_2} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} (x : M) (y : { x // x S }) :
      ↑(Submonoid.LocalizationMap.map f hy k) (Submonoid.LocalizationMap.mk' f x y) = Submonoid.LocalizationMap.mk' k (g x) { val := g y, property := hy y }
      theorem AddSubmonoid.LocalizationMap.map_spec {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst : AddCommMonoid N] {P : Type u_4} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} (z : N) (u : Q) :

      Given Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q for Submonoids S, T respectively, if an AddCommMonoid homomorphism g : M →+ P→+ P induces a f.map hy k : N →+ Q→+ Q, then for all z : N, u : Q, we have f.map hy k z = u ↔ k (g x) = k (g y) + u↔ k (g x) = k (g y) + u where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.map_spec {M : Type u_3} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst : CommMonoid N] {P : Type u_4} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} (z : N) (u : (fun x => Q) z) :

      Given Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q for Submonoids S, T respectively, if a CommMonoid homomorphism g : M →* P→* P induces a f.map hy k : N →* Q→* Q, then for all z : N, u : Q, we have f.map hy k z = u ↔ k (g x) = k (g y) * u↔ k (g x) = k (g y) * u where x : M, y ∈ S∈ S are such that z * f y = f x.

      theorem AddSubmonoid.LocalizationMap.map_add_right {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_4} [inst : AddCommMonoid N] {P : Type u_3} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} (z : N) :

      Given Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q for Submonoids S, T respectively, if an AddCommMonoid homomorphism g : M →+ P→+ P induces a f.map hy k : N →+ Q→+ Q, then for all z : N, we have f.map hy k z + k (g y) = k (g x) where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.map_mul_right {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_4} [inst : CommMonoid N] {P : Type u_3} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} (z : N) :

      Given Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q for Submonoids S, T respectively, if a CommMonoid homomorphism g : M →* P→* P induces a f.map hy k : N →* Q→* Q, then for all z : N, we have f.map hy k z * k (g y) = k (g x) where x : M, y ∈ S∈ S are such that z * f y = f x.

      theorem AddSubmonoid.LocalizationMap.map_add_left {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_4} [inst : AddCommMonoid N] {P : Type u_3} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} (z : N) :

      Given Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q for Submonoids S, T respectively if an AddCommMonoid homomorphism g : M →+ P→+ P induces a f.map hy k : N →+ Q→+ Q, then for all z : N, we have k (g y) + f.map hy k z = k (g x) where x : M, y ∈ S∈ S are such that z + f y = f x.

      theorem Submonoid.LocalizationMap.map_mul_left {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_4} [inst : CommMonoid N] {P : Type u_3} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_1} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} (z : N) :

      Given Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q for Submonoids S, T respectively, if a CommMonoid homomorphism g : M →* P→* P induces a f.map hy k : N →* Q→* Q, then for all z : N, we have k (g y) * f.map hy k z = k (g x) where x : M, y ∈ S∈ S are such that z * f y = f x.

      @[simp]
      theorem AddSubmonoid.LocalizationMap.map_id {M : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [inst : AddCommMonoid N] (f : AddSubmonoid.LocalizationMap S N) (z : N) :
      ↑(AddSubmonoid.LocalizationMap.map f (_ : ∀ (y : { x // x S }), ↑(AddMonoidHom.id M) y S) f) z = z
      @[simp]
      theorem Submonoid.LocalizationMap.map_id {M : Type u_2} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_1} [inst : CommMonoid N] (f : Submonoid.LocalizationMap S N) (z : N) :
      ↑(Submonoid.LocalizationMap.map f (_ : ∀ (y : { x // x S }), ↑(MonoidHom.id M) y S) f) z = z
      theorem AddSubmonoid.LocalizationMap.map_comp_map {M : Type u_6} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_4} [inst : AddCommMonoid N] {P : Type u_3} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_5} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} {A : Type u_1} [inst : AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_2} [inst : AddCommMonoid R] (j : AddSubmonoid.LocalizationMap U R) {l : P →+ A} (hl : ∀ (w : { x // x T }), l w U) :

      If AddCommMonoid homs g : M →+ P, l : P →+ A→+ P, l : P →+ A→+ A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g∘ g.

      theorem Submonoid.LocalizationMap.map_comp_map {M : Type u_6} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_4} [inst : CommMonoid N] {P : Type u_3} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_5} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} {A : Type u_1} [inst : CommMonoid A] {U : Submonoid A} {R : Type u_2} [inst : CommMonoid R] (j : Submonoid.LocalizationMap U R) {l : P →* A} (hl : ∀ (w : { x // x T }), l w U) :

      If CommMonoid homs g : M →* P, l : P →* A→* P, l : P →* A→* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g∘ g.

      theorem AddSubmonoid.LocalizationMap.map_map {M : Type u_6} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_4} [inst : AddCommMonoid N] {P : Type u_3} [inst : AddCommMonoid P] (f : AddSubmonoid.LocalizationMap S N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_5} [inst : AddCommMonoid Q] {k : AddSubmonoid.LocalizationMap T Q} {A : Type u_1} [inst : AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_2} [inst : AddCommMonoid R] (j : AddSubmonoid.LocalizationMap U R) {l : P →+ A} (hl : ∀ (w : { x // x T }), l w U) (x : N) :
      ↑(AddSubmonoid.LocalizationMap.map k hl j) (↑(AddSubmonoid.LocalizationMap.map f hy k) x) = ↑(AddSubmonoid.LocalizationMap.map f (_ : ∀ (x : { x // x S }), ↑(AddMonoidHom.comp l g) x U) j) x

      If AddCommMonoid homs g : M →+ P, l : P →+ A→+ P, l : P →+ A→+ A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g∘ g.

      theorem Submonoid.LocalizationMap.map_map {M : Type u_6} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_4} [inst : CommMonoid N] {P : Type u_3} [inst : CommMonoid P] (f : Submonoid.LocalizationMap S N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : { x // x S }), g y T) {Q : Type u_5} [inst : CommMonoid Q] {k : Submonoid.LocalizationMap T Q} {A : Type u_1} [inst : CommMonoid A] {U : Submonoid A} {R : Type u_2} [inst : CommMonoid R] (j : Submonoid.LocalizationMap U R) {l : P →* A} (hl : ∀ (w : { x // x T }), l w U) (x : N) :
      ↑(Submonoid.LocalizationMap.map k hl j) (↑(Submonoid.LocalizationMap.map f hy k) x) = ↑(Submonoid.LocalizationMap.map f (_ : ∀ (x : { x // x S }), ↑(MonoidHom.comp l g) x U) j) x

      If CommMonoid homs g : M →* P, l : P →* A→* P, l : P →* A→* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g∘ g.

      def AddSubmonoid.LocalizationMap.AwayMap {M : Type u_1} [inst : AddCommMonoid M] (x : M) (N' : Type u_2) [inst : AddCommMonoid N'] :
      Type (maxu_1u_2)

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

      Equations