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)⁻¹, and Submonoid.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 such that g(S) ⊆ 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 by the unique congruence relation (equivalence relation preserving a binary operation) r such that for any other congruence relation s on M × S satisfying '∀ y ∈ S, (1, 1) ∼ (y, y) under s', we have that (x₁, y₁) ∼ (x₂, y₂) by s whenever (x₁, y₁) ∼ (x₂, y₂) by r. We show this relation is equivalent to the standard localization relation. This defines the localization as a quotient type, Localization, but the majority of subsequent lemmas in the file are given in terms of localizations up to isomorphism, using maps which satisfy the characteristic predicate.

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

Implementation notes

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

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

To apply a localization map f as a function, we use f.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 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.LocalizationMap {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (N : Type u_2) [AddCommMonoid N] extends AddMonoidHom : 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_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' : ∀ (x y : M), (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• map_add_units' : ∀ (y : ↥S), IsAddUnit ((↑self.toAddMonoidHom).toFun ↑y)
• surj' : ∀ (z : N), ∃ (x : M × ↥S), z + (↑self.toAddMonoidHom).toFun ↑x.2 = (↑self.toAddMonoidHom).toFun x.1
• exists_of_eq : ∀ (x y : M), (↑self.toAddMonoidHom).toFun x = (↑self.toAddMonoidHom).toFun y → ∃ (c : ↥S), ↑c + x = ↑c + y

theorem AddSubmonoid.LocalizationMap.map_add_units' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (self : S.LocalizationMap N) (y : ↥S) : IsAddUnit ((↑self.toAddMonoidHom).toFun ↑y)

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

theorem AddSubmonoid.LocalizationMap.exists_of_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (self : S.LocalizationMap N) (x : M) (y : M) : (↑self.toAddMonoidHom).toFun x = (↑self.toAddMonoidHom).toFun 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 MonoidHom : 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_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' : ∀ (x y : M), (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• map_units' : ∀ (y : ↥S), IsUnit ((↑self.toMonoidHom).toFun ↑y)
• surj' : ∀ (z : N), ∃ (x : M × ↥S), z * (↑self.toMonoidHom).toFun ↑x.2 = (↑self.toMonoidHom).toFun x.1
• exists_of_eq : ∀ (x y : M), (↑self.toMonoidHom).toFun x = (↑self.toMonoidHom).toFun y → ∃ (c : ↥S), ↑c * x = ↑c * y

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

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

theorem Submonoid.LocalizationMap.exists_of_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (self : S.LocalizationMap N) (x : M) (y : M) : (↑self.toMonoidHom).toFun x = (↑self.toMonoidHom).toFun y → ∃ (c : ↥S), ↑c * x = ↑c * 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)

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)

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 AddLocalization.r'.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : Equivalence fun (a b : M × ↥S) => ∃ (c : ↥S), ↑c + (↑b.2 + a.1) = ↑c + (↑a.2 + b.1)

abbrev AddLocalization.r'.match_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ {x y : M × ↥S} (motive : (∃ (c : ↥S), ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)) → Prop) (x_1 : ∃ (c : ↥S), ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)), (∀ (c : ↥S) (hc : ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem AddLocalization.r'.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) {a : M × ↥S} {b : M × ↥S} {c : M × ↥S} {d : M × ↥S} : Setoid.r a b → Setoid.r c d → Setoid.r (a + c) (b + d)

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' := ⋯ }

abbrev AddLocalization.r_eq_r'.match_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (p : M) (q : ↥S) (x : M) (y : ↥S) (motive : (AddLocalization.r' S) (p, q) (x, y) → Prop) : ∀ (x_1 : (AddLocalization.r' S) (p, q) (x, y)), (∀ (t : ↥S) (ht : ↑t + (↑(x, y).2 + (p, q).1) = ↑t + (↑(p, q).2 + (x, y).1)), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

abbrev AddLocalization.r_eq_r'.match_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : M × ↥S) (motive : (x_1 : M × ↥S) → (AddLocalization.r' S) x_1 x → Prop) (x_1 : M × ↥S) (x_2 : (AddLocalization.r' S) x_1 x), (∀ (p : M) (q : ↥S) (x : (AddLocalization.r' S) (p, q) x), motive (p, q) x) → motive x_1 x_2

Equations

• ⋯ = ⋯

theorem AddLocalization.r_eq_r' {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : AddLocalization.r S = AddLocalization.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').

abbrev AddLocalization.r_eq_r'.match_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (p : M) (q : ↥S) (motive : (x : M × ↥S) → (AddLocalization.r' S) (p, q) x → Prop) : ∀ (x : M × ↥S) (x_1 : (AddLocalization.r' S) (p, q) x), (∀ (x : M) (y : ↥S) (x_2 : (AddLocalization.r' S) (p, q) (x, y)), motive (x, y) x_2) → motive x x_1

Equations

• ⋯ = ⋯

theorem Localization.r_eq_r' {M : Type u_1} [CommMonoid M] (S : Submonoid M) : Localization.r S = Localization.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_iff_exists {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {x : M × ↥S} {y : M × ↥S} : (AddLocalization.r S) x y ↔ ∃ (c : ↥S), ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)

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

def 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 = (AddLocalization.r S).Quotient

def 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 = (Localization.r S).Quotient

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

Equations

• AddLocalization.inhabited S = AddCon.Quotient.inhabited

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

Equations

• Localization.inhabited S = Con.Quotient.inhabited

@[irreducible]

def Localization.mul {M : Type u_4} [CommMonoid M] (S : Submonoid M) : Localization S → Localization S → Localization S

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

Equations

• @Localization.mul = Localization.wrapped✝.1

theorem Localization.mul_def {M : Type u_4} [CommMonoid M] (S : Submonoid M) : Localization.mul S = Mul.mul

def AddLocalization.add {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) : AddLocalization S → AddLocalization S → AddLocalization S

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

• @AddLocalization.add = Localization.wrapped✝.1

theorem AddLocalization.add_def {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) : AddLocalization.add S = Add.add

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

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

Equations

• AddLocalization.instAdd S = { add := AddLocalization.add S }

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

Equations

• Localization.instMul S = { mul := Localization.mul S }

@[irreducible]

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

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

Equations

• @Localization.one = Localization.wrapped✝.1

theorem Localization.one_def {M : Type u_4} [CommMonoid M] (S : Submonoid M) : Localization.one S = One.one

theorem AddLocalization.zero_def {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) : AddLocalization.zero S = Zero.zero

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

def AddLocalization.zero {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) : AddLocalization S

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

• @AddLocalization.zero = Localization.wrapped✝.1

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

Equations

• AddLocalization.instZero S = { zero := AddLocalization.zero S }

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

Equations

• Localization.instOne S = { one := Localization.one S }

theorem Localization.npow_def {M : Type u_4} [CommMonoid M] (S : Submonoid M) : Localization.npow S = Monoid.npow

@[irreducible]

def Localization.npow {M : Type u_4} [CommMonoid M] (S : Submonoid M) : ℕ → Localization S → Localization S

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

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

Equations

• @Localization.npow = Localization.wrapped✝.1

def AddLocalization.nsmul {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) : ℕ → AddLocalization S → AddLocalization S

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

• @AddLocalization.nsmul = Localization.wrapped✝.1

theorem AddLocalization.nsmul_def {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) : AddLocalization.nsmul S = AddMonoid.nsmul

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.

theorem AddLocalization.addCommMonoid.proof_6 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : AddLocalization S) (y : AddLocalization S) : AddLocalization.add S x y = AddLocalization.add S y x

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

Equations

• AddLocalization.addCommMonoid S = AddCommMonoid.mk ⋯

theorem AddLocalization.addCommMonoid.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : AddLocalization S) : AddLocalization.add S x (AddLocalization.zero S) = x

theorem AddLocalization.addCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : AddLocalization S) : AddLocalization.nsmul S 0 x = AddLocalization.zero S

theorem AddLocalization.addCommMonoid.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : AddLocalization S) : AddLocalization.add S (AddLocalization.zero S) x = x

theorem AddLocalization.addCommMonoid.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : AddLocalization S) (y : AddLocalization S) (z : AddLocalization S) : AddLocalization.add S (AddLocalization.add S x y) z = AddLocalization.add S x (AddLocalization.add S y z)

theorem AddLocalization.addCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (n : ℕ) (x : AddLocalization S) : AddLocalization.nsmul S n.succ x = AddLocalization.add S (AddLocalization.nsmul S n x) x

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

Equations

• Localization.commMonoid S = CommMonoid.mk ⋯

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 = (AddLocalization.r S).mk' (x, y)

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 = (Localization.r S).mk' (x, y)

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

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

theorem AddLocalization.rec.proof_2 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (y : M × ↥S) : AddLocalization.mk y.1 y.2 = AddLocalization.mk y.1 y.2

def AddLocalization.rec {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Sort u} (f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.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

theorem AddLocalization.rec.proof_3 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Sort u_2} (f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (y : M × ↥S) (z : M × ↥S) (h : Setoid.r y z) : ⋯ ▸ (fun (y : M × ↥S) => ⋯ ▸ f y.1 y.2) y = (fun (y : M × ↥S) => ⋯ ▸ f y.1 y.2) z

theorem AddLocalization.rec.proof_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {a : M} {c : M} {b : ↥S} {d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)) : AddLocalization.mk a b = AddLocalization.mk 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 (Localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (Localization.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.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 (AddLocalization.mk a b) (AddLocalization.mk c d))] (x : AddLocalization S) (y : AddLocalization S) (f : (a c : M) → (b d : ↥S) → r (AddLocalization.mk a b) (AddLocalization.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 AddLocalization.recOnSubsingleton₂.proof_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {r : AddLocalization S → AddLocalization S → Sort u_2} [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (AddLocalization.mk a b) (AddLocalization.mk c d))] (t : M × ↥S) (b : M × ↥S) : Subsingleton (r ⟦t⟧ ⟦b⟧)

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 (Localization.mk a b) (Localization.mk c d))] (x : Localization S) (y : Localization S) (f : (a c : M) → (b d : ↥S) → r (Localization.mk a b) (Localization.mk c d)) : r x y

Copy of Quotient.recOnSubsingleton₂ for Localization

Equations

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

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

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

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

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

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

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

@[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 (AddLocalization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (a : M) (b : ↥S) : AddLocalization.rec f H (AddLocalization.mk a b) = f a b

@[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 (Localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : (Localization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (a : M) (b : ↥S) : Localization.rec f H (Localization.mk a b) = f a b

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}, (AddLocalization.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 AddLocalization.liftOn.proof_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_2} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d) : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d

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}, (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

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

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}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : (AddLocalization.mk a b).liftOn f H = f a b

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}, (Localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : (Localization.mk a b).liftOn f H = f a b

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

theorem Localization.ind {M : Type u_1} [CommMonoid M] {S : Submonoid M} {p : Localization S → Prop} (H : ∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) (x : Localization S) : 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 (AddLocalization.mk y.1 y.2)) : 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 (Localization.mk y.1 y.2)) : p x

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

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

abbrev AddLocalization.liftOn₂.match_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (motive : M × ↥S → Prop) : ∀ (x : M × ↥S), (∀ (fst : M) (snd : ↥S), motive (fst, snd)) → motive x

Equations

• ⋯ = ⋯

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

theorem AddLocalization.liftOn₂.proof_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_2} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥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 : ↥S) : ∀ {a_1 c : M} {b_1 d : ↥S}, (AddLocalization.r S) (a_1, b_1) (c, d) → f a b a_1 b_1 = f a b c d

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

Non-dependent recursion principle for localizations: given elements f x y : p for all x and y, such that r S x x' and r S y y' implies f x y = f x' y', then f is defined on the whole Localization S.

Equations

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

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}, (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 : ↥S) (d : ↥S) : (AddLocalization.mk a b).liftOn₂ (AddLocalization.mk c d) f H = f a b c d

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}, (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 : ↥S) (d : ↥S) : (Localization.mk a b).liftOn₂ (Localization.mk c d) f H = f a b c d

theorem AddLocalization.induction_on₂ {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → AddLocalization S → Prop} (x : AddLocalization S) (y : AddLocalization S) (H : ∀ (x y : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.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 → Prop} (x : Localization S) (y : Localization S) (H : ∀ (x y : M × ↥S), p (Localization.mk x.1 x.2) (Localization.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 → AddLocalization S → Prop} (x : AddLocalization S) (y : AddLocalization S) (z : AddLocalization S) (H : ∀ (x y z : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.mk y.1 y.2) (AddLocalization.mk z.1 z.2)) : p x y z

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

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

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

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

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

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

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

theorem Localization.smul_def {M : Type u_7} [CommMonoid M] {S : Submonoid M} {R : Type u_8} [SMul R M] [IsScalarTower R M M] (c : R) (z : Localization S) : Localization.smul c z = z.liftOn (fun (a : M) (b : ↥S) => Localization.mk (c • a) b) ⋯

@[irreducible]

def Localization.smul {M : Type u_7} [CommMonoid M] {S : Submonoid M} {R : Type u_8} [SMul R M] [IsScalarTower R M M] (c : R) (z : Localization S) : Localization S

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

Equations

• @Localization.smul = Localization.wrapped✝.1

instance Localization.instSMulLocalization {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_4} [SMul R M] [IsScalarTower R M M] : SMul R (Localization S)

Equations

• Localization.instSMulLocalization = { smul := Localization.smul }

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 • Localization.mk a b = Localization.mk (c • a) b

instance Localization.instSMulCommClass {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R₁ : Type u_5} {R₂ : Type u_6} [SMul R₁ M] [SMul R₂ M] [IsScalarTower R₁ M M] [IsScalarTower R₂ M M] [SMulCommClass R₁ R₂ M] : SMulCommClass R₁ R₂ (Localization S)

Equations

• ⋯ = ⋯

instance Localization.instIsScalarTower {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R₁ : Type u_5} {R₂ : Type u_6} [SMul R₁ M] [SMul R₂ M] [IsScalarTower R₁ M M] [IsScalarTower R₂ M M] [SMul R₁ R₂] [IsScalarTower R₁ R₂ M] : IsScalarTower R₁ R₂ (Localization S)

Equations

• ⋯ = ⋯

instance Localization.smulCommClass_right {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_7} [SMul R M] [IsScalarTower R M M] : SMulCommClass R (Localization S) (Localization S)

Equations

• ⋯ = ⋯

instance Localization.isScalarTower_right {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_7} [SMul R M] [IsScalarTower R M M] : IsScalarTower R (Localization S) (Localization S)

Equations

• ⋯ = ⋯

instance Localization.instIsCentralScalar {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_4} [SMul R M] [SMul Rᵐᵒᵖ M] [IsScalarTower R M M] [IsScalarTower Rᵐᵒᵖ M M] [IsCentralScalar R M] : IsCentralScalar R (Localization S)

Equations

• ⋯ = ⋯

instance Localization.instMulActionOfIsScalarTower {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_4} [Monoid R] [MulAction R M] [IsScalarTower R M M] : MulAction R (Localization S)

Equations

• Localization.instMulActionOfIsScalarTower = MulAction.mk ⋯ ⋯

instance Localization.instMulDistribMulActionOfIsScalarTower {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_4} [Monoid R] [MulDistribMulAction R M] [IsScalarTower R M M] : MulDistribMulAction R (Localization S)

Equations

• Localization.instMulDistribMulActionOfIsScalarTower = MulDistribMulAction.mk ⋯ ⋯

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 = { toAddMonoidHom := f, map_add_units' := H1, surj' := H2, exists_of_eq := H3 }

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 = { toMonoidHom := f, map_units' := H1, surj' := H2, exists_of_eq := H3 }

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

@[reducible, inline]

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

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

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

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

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

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

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

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.toMap ↑y)

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.toMap ↑y)

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.toMap ↑x.2 = f.toMap x.1

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.toMap ↑x.2 = f.toMap x.1

abbrev AddSubmonoid.LocalizationMap.surj₂.match_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) (motive : (∃ (x : M × ↥S), z + f.toMap ↑x.2 = f.toMap x.1) → Prop) : ∀ (x : ∃ (x : M × ↥S), z + f.toMap ↑x.2 = f.toMap x.1), (∀ (a : M × ↥S) (ha : z + f.toMap ↑a.2 = f.toMap a.1), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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) (w : N) : ∃ (z' : M) (w' : M) (d : ↥S), z + f.toMap ↑d = f.toMap z' ∧ w + f.toMap ↑d = f.toMap 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.surj₂ {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (z : N) (w : N) : ∃ (z' : M) (w' : M) (d : ↥S), z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap 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.eq_iff_exists {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x : M} {y : M} : f.toMap x = f.toMap y ↔ ∃ (c : ↥S), ↑c + x = ↑c + y

abbrev AddSubmonoid.LocalizationMap.eq_iff_exists.match_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {x : M} {y : M} (motive : (∃ (c : ↥S), ↑c + x = ↑c + y) → Prop) : ∀ (x_1 : ∃ (c : ↥S), ↑c + x = ↑c + y), (∀ (c : ↥S) (h : ↑c + x = ↑c + y), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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 : M} {y : M} : f.toMap x = f.toMap y ↔ ∃ (c : ↥S), ↑c * x = ↑c * y

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 ⋯

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 ⋯

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.toMap ↑(f.sec z).2 = f.toMap (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) : z * f.toMap ↑(f.sec z).2 = f.toMap (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) : f.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 + z

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.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 * 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 : N) (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_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 : N) (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_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 : N) (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.

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 : N) (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.

@[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₁ : M} {x₂ : M} {y₁ : ↥S} {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₁).

@[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₁ : M} {x₂ : M} {y₁ : ↥S} {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₁).

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 : ↥S} {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_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 : ↥S} {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_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.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.map_right_cancel {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {x : M} {y : M} {c : ↥S} (h : f.toMap (↑c + x) = f.toMap (↑c + y)) : f.toMap x = f.toMap y

abbrev AddSubmonoid.LocalizationMap.map_right_cancel.match_1 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [AddCommMonoid N] (f : S.LocalizationMap N) {c : ↥S} (motive : IsAddUnit (f.toMap ↑c) → Prop) : ∀ (x : IsAddUnit (f.toMap ↑c)), (∀ (u : AddUnits N) (hu : ↑u = f.toMap ↑c), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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 : M} {y : M} {c : ↥S} (h : f.toMap (↑c * x) = f.toMap (↑c * y)) : f.toMap x = f.toMap 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 : M} {y : M} {c : ↥S} (h : f.toMap (x + ↑c) = f.toMap (y + ↑c)) : f.toMap x = f.toMap 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 : M} {y : M} {c : ↥S} (h : f.toMap (x * ↑c) = f.toMap (y * ↑c)) : f.toMap x = f.toMap y

theorem AddSubmonoid.LocalizationMap.mk'.proof_1 {M : Type u_1} [AddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

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.toMap x + ↑(-(IsAddUnit.liftRight (f.toMap.restrict S) ⋯) 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.toMap x * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) 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₁ : M) (x₂ : M) (y₁ : ↥S) (y₂ : ↥S) : f.mk' (x₁ + x₂) (y₁ + y₂) = f.mk' x₁ y₁ + f.mk' x₂ 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₁ : M) (x₂ : M) (y₁ : ↥S) (y₂ : ↥S) : f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

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.toMap x

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.toMap x

@[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 a Submonoid S ⊆ M, for all z : N we have that if x : M, y ∈ S are such that z + f y = f x, then f x - f y = z.

@[simp]

theorem Submonoid.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.

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'_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'_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.toMap ↑y = f.toMap 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.mk' x y * f.toMap ↑y = f.toMap 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.toMap ↑y + f.mk' x y = f.toMap 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.toMap ↑y * f.mk' x y = f.toMap 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.toMap ↑y = f.toMap 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.toMap ↑y = f.toMap x

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.toMap x = z + f.toMap ↑y

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.toMap x = z * f.toMap ↑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₁ : M} {x₂ : M} {y₁ : ↥S} {y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (↑y₂ + x₁) = f.toMap (↑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₁ : M} {x₂ : M} {y₁ : ↥S} {y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (↑y₂ * x₁) = f.toMap (↑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₁ : M} {x₂ : M} {y₁ : ↥S} {y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ + ↑y₂) = f.toMap (x₂ + ↑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₁ : M} {x₂ : M} {y₁ : ↥S} {y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * ↑y₂) = f.toMap (x₂ * ↑y₁)

theorem AddSubmonoid.LocalizationMap.eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a₁ : M} {b₁ : M} {a₂ : ↥S} {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₁ : M} {b₁ : M} {a₂ : ↥S} {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₁ : M} {b₁ : M} {a₂ : ↥S} {b₂ : ↥S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (AddLocalization.r S) (a₁, a₂) (b₁, 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₁ : M} {b₁ : M} {a₂ : ↥S} {b₂ : ↥S} : f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)

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 : M} {y : M} : f.toMap x = f.toMap y ↔ g.toMap x = g.toMap y

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 : M} {y : M} : f.toMap x = f.toMap y ↔ g.toMap x = g.toMap 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₁ : M} {x₂ : M} {y₁ : ↥S} {y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ 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₁ : M} {x₂ : M} {y₁ : ↥S} {y₂ : ↥S} : f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

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.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.mk'_eq_of_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {a₁ : M} {b₁ : M} {a₂ : ↥S} {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₁ : M} {b₁ : M} {a₂ : ↥S} {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₁ : M} {b₁ : M} {a₂ : ↥S} {b₂ : ↥S} (H : b₁ + ↑a₂ = a₁ + ↑b₂) : 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₁ : M} {b₁ : M} {a₂ : ↥S} {b₂ : ↥S} (H : b₁ * ↑a₂ = a₁ * ↑b₂) : f.mk' a₁ a₂ = f.mk' b₁ 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 : ↥S) (c : ↥S) : f.mk' (a + ↑c) (b + c) = f.mk' a 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 : ↥S) (c : ↥S) : f.mk' (a * ↑c) (b * c) = f.mk' a 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 : M} {b : M} {d : ↥S} : f.mk' a d = f.mk' b d ↔ ∃ (c : ↥S), ↑c + a = ↑c + 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 : M} {b : M} {d : ↥S} : f.mk' a d = f.mk' b d ↔ ∃ (c : ↥S), ↑c * a = ↑c * b

@[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) (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) (x : M) (H : x ∈ S) : f.mk' x ⟨x, H⟩ = 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

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₁ : M) (x₂ : M) (y : ↥S) : f.toMap x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y

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₁ : M) (x₂ : M) (y : ↥S) : f.toMap x₁ * f.mk' x₂ y = 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₁ : M) (x₂ : M) (y : ↥S) : f.mk' x₂ y + f.toMap x₁ = 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₁ : M) (x₂ : M) (y : ↥S) : f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * 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.toMap x + f.mk' 0 y = f.mk' 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.toMap x * f.mk' 1 y = f.mk' x y

@[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.toMap x

@[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.toMap 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.toMap 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.toMap x

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.toMap) ↑y)

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.toMap) ↑y)

theorem AddSubmonoid.LocalizationMap.eq_of_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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) {x : M} {y : M} (h : f.toMap x = f.toMap y) : g x = g y

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

theorem Submonoid.LocalizationMap.eq_of_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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) {x : M} {y : M} (h : f.toMap x = f.toMap y) : g x = g y

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

theorem AddSubmonoid.LocalizationMap.comp_eq_of_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 : M →+ P} {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] (hg : ∀ (y : ↥S), g ↑y ∈ T) (k : T.LocalizationMap Q) {x : M} {y : M} (h : f.toMap x = f.toMap y) : k.toMap (g x) = k.toMap (g y)

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

theorem Submonoid.LocalizationMap.comp_eq_of_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 : M →* P} {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] (hg : ∀ (y : ↥S), g ↑y ∈ T) (k : T.LocalizationMap Q) {x : M} {y : M} (h : f.toMap x = f.toMap y) : k.toMap (g x) = k.toMap (g y)

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

theorem AddSubmonoid.LocalizationMap.lift.proof_1 {M : Type u_1} [AddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

noncomputable def AddSubmonoid.LocalizationMap.lift {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) : N →+ P

Given a localization map f : M →+ N for a submonoid S ⊆ M and a map of AddCommMonoids g : M →+ P such that g y is invertible for all y : S, the homomorphism induced from N to P sending z : N to g x - g y, where (x, y) : M × S are such that z = f x - f y.

Equations

• f.lift hg = { toFun := fun (z : N) => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) (f.sec z).2), map_zero' := ⋯, map_add' := ⋯ }

theorem AddSubmonoid.LocalizationMap.lift.proof_2 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [AddCommMonoid N] {P : Type u_1} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) : (fun (z : N) => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) (f.sec z).2)) 0 = 0

theorem AddSubmonoid.LocalizationMap.lift.proof_3 {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_1} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : N) (y : N) : { toFun := fun (z : N) => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) (f.sec z).2), map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (z : N) => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) (f.sec z).2), map_zero' := ⋯ }.toFun x + { toFun := fun (z : N) => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) (f.sec z).2), map_zero' := ⋯ }.toFun y

noncomputable def Submonoid.LocalizationMap.lift {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : N →* P

Given a Localization map f : M →* N for a Submonoid S ⊆ M and a map of CommMonoids g : M →* P such that g y is invertible for all y : S, the homomorphism induced from N to P sending z : N to g x * (g y)⁻¹, where (x, y) : M × S are such that z = f x * (f y)⁻¹.

Equations

• f.lift hg = { toFun := fun (z : N) => g (f.sec z).1 * ↑((IsUnit.liftRight (g.restrict S) hg) (f.sec z).2)⁻¹, map_one' := ⋯, map_mul' := ⋯ }

theorem AddSubmonoid.LocalizationMap.lift_mk' {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M) (y : ↥S) : (f.lift hg) (f.mk' x y) = g x + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) y)

Given a Localization map f : M →+ N for a Submonoid S ⊆ M and a map of AddCommMonoids g : M →+ P such that g y is invertible for all y : S, the homomorphism induced from N to P maps f x - f y to g x - g y for all x : M, y ∈ S.

theorem Submonoid.LocalizationMap.lift_mk' {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M) (y : ↥S) : (f.lift hg) (f.mk' x y) = g x * ↑((IsUnit.liftRight (g.restrict S) hg) y)⁻¹

Given a Localization map f : M →* N for a Submonoid S ⊆ M and a map of CommMonoids g : M →* P such that g y is invertible for all y : S, the homomorphism induced from N to P maps f x * (f y)⁻¹ to g x * (g y)⁻¹ for all x : M, y ∈ S.

theorem AddSubmonoid.LocalizationMap.lift_spec {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) (v : P) : (f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 + v

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

theorem Submonoid.LocalizationMap.lift_spec {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) (v : P) : (f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 * v

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

theorem AddSubmonoid.LocalizationMap.lift_spec_add {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) (w : P) (v : P) : (f.lift hg) z + w = v ↔ g (f.sec z).1 + w = g ↑(f.sec z).2 + v

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

theorem Submonoid.LocalizationMap.lift_spec_mul {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) (w : P) (v : P) : (f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v

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

theorem AddSubmonoid.LocalizationMap.lift_mk'_spec {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M) (v : P) (y : ↥S) : (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y + v

theorem Submonoid.LocalizationMap.lift_mk'_spec {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M) (v : P) (y : ↥S) : (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v

theorem AddSubmonoid.LocalizationMap.lift_add_right {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) : (f.lift hg) z + g ↑(f.sec z).2 = g (f.sec z).1

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

theorem Submonoid.LocalizationMap.lift_mul_right {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) : (f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1

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

theorem AddSubmonoid.LocalizationMap.lift_add_left {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) : g ↑(f.sec z).2 + (f.lift hg) z = g (f.sec z).1

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

theorem Submonoid.LocalizationMap.lift_mul_left {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) : g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1

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

@[simp]

theorem AddSubmonoid.LocalizationMap.lift_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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M) : (f.lift hg) (f.toMap x) = g x

@[simp]

theorem Submonoid.LocalizationMap.lift_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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M) : (f.lift hg) (f.toMap x) = g x

theorem AddSubmonoid.LocalizationMap.lift_eq_iff {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) {x : M × ↥S} {y : M × ↥S} : (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 + ↑y.2) = g (y.1 + ↑x.2)

theorem Submonoid.LocalizationMap.lift_eq_iff {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) {x : M × ↥S} {y : M × ↥S} : (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

@[simp]

theorem AddSubmonoid.LocalizationMap.lift_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) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) : (f.lift hg).comp f.toMap = g

@[simp]

theorem Submonoid.LocalizationMap.lift_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) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : (f.lift hg).comp f.toMap = g

@[simp]

theorem AddSubmonoid.LocalizationMap.lift_of_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) : f.lift ⋯ = j

@[simp]

theorem Submonoid.LocalizationMap.lift_of_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) : f.lift ⋯ = j

theorem AddSubmonoid.LocalizationMap.epic_of_localizationMap {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} {k : N →+ P} (h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a) : j = k

theorem Submonoid.LocalizationMap.epic_of_localizationMap {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} {k : N →* P} (h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a) : j = k

theorem AddSubmonoid.LocalizationMap.lift_unique {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) {j : N →+ P} (hj : ∀ (x : M), j (f.toMap x) = g x) : f.lift hg = j

theorem Submonoid.LocalizationMap.lift_unique {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) {j : N →* P} (hj : ∀ (x : M), j (f.toMap x) = g x) : f.lift hg = j

@[simp]

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

@[simp]

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

theorem AddSubmonoid.LocalizationMap.lift_comp_lift {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {T : AddSubmonoid M} (hST : S ≤ T) {Q : Type u_4} [AddCommMonoid Q] (k : T.LocalizationMap Q) {A : Type u_5} [AddCommMonoid A] {l : M →+ A} (hl : ∀ (w : ↥T), IsAddUnit (l ↑w)) : (k.lift hl).comp (f.lift ⋯) = f.lift ⋯

Given Localization maps f : M →+ N for a Submonoid S ⊆ M and k : M →+ Q for a Submonoid T ⊆ M, such that S ≤ T, and we have l : M →+ A, the composition of the induced map f.lift for k with the induced map k.lift for l is equal to the induced map f.lift for l

theorem Submonoid.LocalizationMap.lift_comp_lift {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {T : Submonoid M} (hST : S ≤ T) {Q : Type u_4} [CommMonoid Q] (k : T.LocalizationMap Q) {A : Type u_5} [CommMonoid A] {l : M →* A} (hl : ∀ (w : ↥T), IsUnit (l ↑w)) : (k.lift hl).comp (f.lift ⋯) = f.lift ⋯

Given Localization maps f : M →* N for a Submonoid S ⊆ M and k : M →* Q for a Submonoid T ⊆ M, such that S ≤ T, and we have l : M →* A, the composition of the induced map f.lift for k with the induced map k.lift for l is equal to the induced map f.lift for l.

theorem AddSubmonoid.LocalizationMap.lift_comp_lift_eq {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) {Q : Type u_4} [AddCommMonoid Q] (k : S.LocalizationMap Q) {A : Type u_5} [AddCommMonoid A] {l : M →+ A} (hl : ∀ (w : ↥S), IsAddUnit (l ↑w)) : (k.lift hl).comp (f.lift ⋯) = f.lift hl

theorem Submonoid.LocalizationMap.lift_comp_lift_eq {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) {Q : Type u_4} [CommMonoid Q] (k : S.LocalizationMap Q) {A : Type u_5} [CommMonoid A] {l : M →* A} (hl : ∀ (w : ↥S), IsUnit (l ↑w)) : (k.lift hl).comp (f.lift ⋯) = f.lift hl

@[simp]

theorem AddSubmonoid.LocalizationMap.lift_left_inverse {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) {k : S.LocalizationMap P} (z : N) : (k.lift ⋯) ((f.lift ⋯) z) = z

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

@[simp]

theorem Submonoid.LocalizationMap.lift_left_inverse {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) {k : S.LocalizationMap P} (z : N) : (k.lift ⋯) ((f.lift ⋯) z) = z

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

theorem AddSubmonoid.LocalizationMap.lift_surjective_iff {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) : Function.Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ (x : M × ↥S), v + g ↑x.2 = g x.1

theorem Submonoid.LocalizationMap.lift_surjective_iff {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : Function.Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ (x : M × ↥S), v * g ↑x.2 = g x.1

theorem AddSubmonoid.LocalizationMap.lift_injective_iff {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 : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) : Function.Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f.toMap x = f.toMap y ↔ g x = g y

theorem Submonoid.LocalizationMap.lift_injective_iff {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 : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : Function.Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f.toMap x = f.toMap y ↔ g x = g y

theorem AddSubmonoid.LocalizationMap.map.proof_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_3} [AddCommMonoid P] {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_2} [AddCommMonoid Q] (k : T.LocalizationMap Q) (y : ↥S) : IsAddUnit (k.toMap ↑⟨g ↑y, ⋯⟩)

noncomputable def AddSubmonoid.LocalizationMap.map {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] (k : T.LocalizationMap Q) : N →+ Q

Given an AddCommMonoid homomorphism g : M →+ P where for Submonoids S ⊆ M, T ⊆ P we have g(S) ⊆ T, the induced AddMonoid homomorphism from the Localization of M at S to the Localization of P at T: if f : M →+ N and k : P →+ Q are Localization maps for S and T respectively, we send z : N to k (g x) - k (g y), where (x, y) : M × S are such that z = f x - f y.

Equations

• f.map hy k = f.lift ⋯

noncomputable def Submonoid.LocalizationMap.map {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] (k : T.LocalizationMap Q) : N →* Q

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

Equations

• f.map hy k = f.lift ⋯

theorem AddSubmonoid.LocalizationMap.map_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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (x : M) : (f.map hy k) (f.toMap x) = k.toMap (g x)

theorem Submonoid.LocalizationMap.map_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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} (x : M) : (f.map hy k) (f.toMap x) = k.toMap (g x)

@[simp]

theorem AddSubmonoid.LocalizationMap.map_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) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} : (f.map hy k).comp f.toMap = k.toMap.comp g

@[simp]

theorem Submonoid.LocalizationMap.map_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) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} : (f.map hy k).comp f.toMap = k.toMap.comp g

theorem AddSubmonoid.LocalizationMap.map_mk' {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (x : M) (y : ↥S) : (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

theorem Submonoid.LocalizationMap.map_mk' {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} (x : M) (y : ↥S) : (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

theorem AddSubmonoid.LocalizationMap.map_spec {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q) : (f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) + u

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

theorem Submonoid.LocalizationMap.map_spec {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q) : (f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) * u

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

theorem AddSubmonoid.LocalizationMap.map_add_right {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) : (f.map hy k) z + k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1)

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

theorem Submonoid.LocalizationMap.map_mul_right {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} (z : N) : (f.map hy k) z * k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1)

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

theorem AddSubmonoid.LocalizationMap.map_add_left {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) : k.toMap (g ↑(f.sec z).2) + (f.map hy k) z = k.toMap (g (f.sec z).1)

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

theorem Submonoid.LocalizationMap.map_mul_left {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} (z : N) : k.toMap (g ↑(f.sec z).2) * (f.map hy k) z = k.toMap (g (f.sec z).1)

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

@[simp]

theorem AddSubmonoid.LocalizationMap.map_id {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) : (f.map ⋯ f) z = z

@[simp]

theorem Submonoid.LocalizationMap.map_id {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) (z : N) : (f.map ⋯ f) z = z

theorem AddSubmonoid.LocalizationMap.map_comp_map {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_6} [AddCommMonoid R] (j : U.LocalizationMap R) {l : P →+ A} (hl : ∀ (w : ↥T), l ↑w ∈ U) : (k.map hl j).comp (f.map hy k) = f.map ⋯ j

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

theorem Submonoid.LocalizationMap.map_comp_map {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [CommMonoid A] {U : Submonoid A} {R : Type u_6} [CommMonoid R] (j : U.LocalizationMap R) {l : P →* A} (hl : ∀ (w : ↥T), l ↑w ∈ U) : (k.map hl j).comp (f.map hy k) = f.map ⋯ j

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

theorem AddSubmonoid.LocalizationMap.map_map {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 : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_6} [AddCommMonoid R] (j : U.LocalizationMap R) {l : P →+ A} (hl : ∀ (w : ↥T), l ↑w ∈ U) (x : N) : (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x

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

theorem Submonoid.LocalizationMap.map_map {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 : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [CommMonoid A] {U : Submonoid A} {R : Type u_6} [CommMonoid R] (j : U.LocalizationMap R) {l : P →* A} (hl : ∀ (w : ↥T), l ↑w ∈ U) (x : N) : (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x

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

theorem AddSubmonoid.LocalizationMap.map_injective_of_injective {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 : M →+ P} {Q : Type u_4} [AddCommMonoid Q] (hg : Function.Injective ⇑g) (k : (AddSubmonoid.map g S).LocalizationMap Q) : Function.Injective ⇑(f.map ⋯ k)

Given an injective AddCommMonoid homomorphism g : M →+ P, and a submonoid S ⊆ M, the induced monoid homomorphism from the localization of M at S to the localization of P at g S, is injective.

abbrev AddSubmonoid.LocalizationMap.map_injective_of_injective.match_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) (w : N) (motive : (∃ (z' : M) (w' : M) (d : ↥S), z + f.toMap ↑d = f.toMap z' ∧ w + f.toMap ↑d = f.toMap w') → Prop) : ∀ (x : ∃ (z' : M) (w' : M) (d : ↥S), z + f.toMap ↑d = f.toMap z' ∧ w + f.toMap ↑d = f.toMap w'), (∀ (z' w' : M) (x : ↥S) (hxz : z + f.toMap ↑x = f.toMap z') (hxw : w + f.toMap ↑x = f.toMap w'), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Submonoid.LocalizationMap.map_injective_of_injective {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 : M →* P} {Q : Type u_4} [CommMonoid Q] (hg : Function.Injective ⇑g) (k : (Submonoid.map g S).LocalizationMap Q) : Function.Injective ⇑(f.map ⋯ k)

Given an injective CommMonoid homomorphism g : M →* P, and a submonoid S ⊆ M, the induced monoid homomorphism from the localization of M at S to the localization of P at g S, is injective.

@[reducible]

def AddSubmonoid.LocalizationMap.AwayMap {M : Type u_1} [AddCommMonoid M] (x : M) (N' : Type u_5) [AddCommMonoid N'] : Type (max u_1 u_5)

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

Equations

• AddSubmonoid.LocalizationMap.AwayMap x N' = (AddSubmonoid.multiples x).LocalizationMap N'

@[reducible]

def Submonoid.LocalizationMap.AwayMap {M : Type u_1} [CommMonoid M] (x : M) (N' : Type u_5) [CommMonoid N'] : Type (max u_1 u_5)

Given x : M, the type of CommMonoid homomorphisms f : M →* N such that N is isomorphic to the Localization of M at the Submonoid generated by x.

Equations

• Submonoid.LocalizationMap.AwayMap x N' = (Submonoid.powers x).LocalizationMap N'

noncomputable def Submonoid.LocalizationMap.AwayMap.invSelf {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) : N

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

Equations

• Submonoid.LocalizationMap.AwayMap.invSelf x F = Submonoid.LocalizationMap.mk' F 1 ⟨x, ⋯⟩

noncomputable def Submonoid.LocalizationMap.AwayMap.lift {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) : N →* P

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

Equations

• Submonoid.LocalizationMap.AwayMap.lift x F hg = Submonoid.LocalizationMap.lift F ⋯

@[simp]

theorem Submonoid.LocalizationMap.AwayMap.lift_eq {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) (a : M) : (Submonoid.LocalizationMap.AwayMap.lift x F hg) ((Submonoid.LocalizationMap.toMap F) a) = g a

@[simp]

theorem Submonoid.LocalizationMap.AwayMap.lift_comp {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) : (Submonoid.LocalizationMap.AwayMap.lift x F hg).comp (Submonoid.LocalizationMap.toMap F) = g

noncomputable def Submonoid.LocalizationMap.awayToAwayRight {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (y : M) (G : Submonoid.LocalizationMap.AwayMap (x * y) P) : N →* P

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

Equations

• Submonoid.LocalizationMap.awayToAwayRight x F y G = Submonoid.LocalizationMap.AwayMap.lift x F ⋯

noncomputable def AddSubmonoid.LocalizationMap.AwayMap.negSelf {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) : B

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

Equations

• AddSubmonoid.LocalizationMap.AwayMap.negSelf x F = AddSubmonoid.LocalizationMap.mk' F 0 ⟨x, ⋯⟩

noncomputable def AddSubmonoid.LocalizationMap.AwayMap.lift {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] {g : A →+ C} (hg : IsAddUnit (g x)) : B →+ C

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

Equations

• AddSubmonoid.LocalizationMap.AwayMap.lift x F hg = AddSubmonoid.LocalizationMap.lift F ⋯

@[simp]

theorem AddSubmonoid.LocalizationMap.AwayMap.lift_eq {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] {g : A →+ C} (hg : IsAddUnit (g x)) (a : A) : (AddSubmonoid.LocalizationMap.AwayMap.lift x F hg) ((AddSubmonoid.LocalizationMap.toMap F) a) = g a

@[simp]

theorem AddSubmonoid.LocalizationMap.AwayMap.lift_comp {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] {g : A →+ C} (hg : IsAddUnit (g x)) : (AddSubmonoid.LocalizationMap.AwayMap.lift x F hg).comp (AddSubmonoid.LocalizationMap.toMap F) = g

noncomputable def AddSubmonoid.LocalizationMap.awayToAwayRight {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] (y : A) (G : AddSubmonoid.LocalizationMap.AwayMap (x + y) C) : B →+ C

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

Equations

• AddSubmonoid.LocalizationMap.awayToAwayRight x F y G = AddSubmonoid.LocalizationMap.AwayMap.lift x F ⋯

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations.proof_1 {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_1} [AddCommMonoid P] (f : S.LocalizationMap N) (k : S.LocalizationMap P) (a : N) (b : N) : (f.lift ⋯) (a + b) = (f.lift ⋯) a + (f.lift ⋯) b

noncomputable def AddSubmonoid.LocalizationMap.addEquivOfLocalizations {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) (k : S.LocalizationMap P) : N ≃+ P

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

Equations

• f.addEquivOfLocalizations k = { toFun := ⇑(f.lift ⋯), invFun := ⇑(k.lift ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

noncomputable def Submonoid.LocalizationMap.mulEquivOfLocalizations {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) (k : S.LocalizationMap P) : N ≃* P

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

Equations

• f.mulEquivOfLocalizations k = { toFun := ⇑(f.lift ⋯), invFun := ⇑(k.lift ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_apply {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) {k : S.LocalizationMap P} {x : N} : (f.addEquivOfLocalizations k) x = (f.lift ⋯) x

@[simp]

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_apply {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) {k : S.LocalizationMap P} {x : N} : (f.mulEquivOfLocalizations k) x = (f.lift ⋯) x

@[simp]

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_symm_apply {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) {k : S.LocalizationMap P} {x : P} : (f.addEquivOfLocalizations k).symm x = (k.lift ⋯) x

@[simp]

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_apply {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) {k : S.LocalizationMap P} {x : P} : (f.mulEquivOfLocalizations k).symm x = (k.lift ⋯) x

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_symm_eq_addEquivOfLocalizations {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) {k : S.LocalizationMap P} : (k.addEquivOfLocalizations f).symm = f.addEquivOfLocalizations k

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations {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) {k : S.LocalizationMap P} : (k.mulEquivOfLocalizations f).symm = f.mulEquivOfLocalizations k

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations.proof_3 {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_1} [AddCommMonoid P] (f : S.LocalizationMap N) (k : N ≃+ P) (x : M) (y : M) : k (f.toMap x) = k (f.toMap y) → ∃ (c : ↥S), ↑c + x = ↑c + y

def AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations {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) (k : N ≃+ P) : S.LocalizationMap P

If f : M →+ N is a Localization map for a Submonoid S and k : N ≃+ P is an isomorphism of AddCommMonoids, k ∘ f is a Localization map for M at S.

Equations

• f.ofAddEquivOfLocalizations k = (k.toAddMonoidHom.comp f.toMap).toLocalizationMap ⋯ ⋯ ⋯

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations.match_1 {N : Type u_1} [AddCommMonoid N] {P : Type u_2} [AddCommMonoid P] (k : N ≃+ P) (v : P) (motive : (∃ (a : N), k.toEquiv a = v) → Prop) : ∀ (x : ∃ (a : N), k.toEquiv a = v), (∀ (z : N) (hz : k.toEquiv z = v), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations.proof_2 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [AddCommMonoid N] {P : Type u_2} [AddCommMonoid P] (f : S.LocalizationMap N) (k : N ≃+ P) (v : P) : ∃ (x : M × ↥S), v + (k.toAddMonoidHom.comp f.toMap) ↑x.2 = (k.toAddMonoidHom.comp f.toMap) x.1

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations.proof_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_3} [AddCommMonoid N] {P : Type u_2} [AddCommMonoid P] (f : S.LocalizationMap N) (k : N ≃+ P) (y : ↥S) : IsAddUnit ((k.toAddMonoidHom.comp f.toMap) ↑y)

def Submonoid.LocalizationMap.ofMulEquivOfLocalizations {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) (k : N ≃* P) : S.LocalizationMap P

If f : M →* N is a Localization map for a Submonoid S and k : N ≃* P is an isomorphism of CommMonoids, k ∘ f is a Localization map for M at S.

Equations

• f.ofMulEquivOfLocalizations k = (k.toMonoidHom.comp f.toMap).toLocalizationMap ⋯ ⋯ ⋯

@[simp]

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_apply {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) {k : N ≃+ P} (x : M) : (f.ofAddEquivOfLocalizations k).toMap x = k (f.toMap x)

@[simp]

theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_apply {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) {k : N ≃* P} (x : M) : (f.ofMulEquivOfLocalizations k).toMap x = k (f.toMap x)

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_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) {k : N ≃+ P} : (f.ofAddEquivOfLocalizations k).toMap = k.toAddMonoidHom.comp f.toMap

theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_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) {k : N ≃* P} : (f.ofMulEquivOfLocalizations k).toMap = k.toMonoidHom.comp f.toMap

theorem AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply {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) {k : N ≃+ P} (x : M) : k.symm ((f.ofAddEquivOfLocalizations k).toMap x) = f.toMap x

theorem Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply {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) {k : N ≃* P} (x : M) : k.symm ((f.ofMulEquivOfLocalizations k).toMap x) = f.toMap x

theorem AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply' {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) {k : P ≃+ N} (x : M) : k ((f.ofAddEquivOfLocalizations k.symm).toMap x) = f.toMap x

theorem Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply' {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) {k : P ≃* N} (x : M) : k ((f.ofMulEquivOfLocalizations k.symm).toMap x) = f.toMap x

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_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) {k : N ≃+ P} {x : M} {y : P} : (f.ofAddEquivOfLocalizations k).toMap x = y ↔ f.toMap x = k.symm y

theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_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) {k : N ≃* P} {x : M} {y : P} : (f.ofMulEquivOfLocalizations k).toMap x = y ↔ f.toMap x = k.symm y

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_right_inv {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) (k : S.LocalizationMap P) : f.ofAddEquivOfLocalizations (f.addEquivOfLocalizations k) = k

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv {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) (k : S.LocalizationMap P) : f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_right_inv_apply {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) {k : S.LocalizationMap P} {x : M} : (f.ofAddEquivOfLocalizations (f.addEquivOfLocalizations k)).toMap x = k.toMap x

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv_apply {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) {k : S.LocalizationMap P} {x : M} : (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)).toMap x = k.toMap x

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_left_neg {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) (k : N ≃+ P) : f.addEquivOfLocalizations (f.ofAddEquivOfLocalizations k) = k

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv {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) (k : N ≃* P) : f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k

theorem AddSubmonoid.LocalizationMap.addEquivOfLocalizations_left_neg_apply {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) {k : N ≃+ P} (x : N) : (f.addEquivOfLocalizations (f.ofAddEquivOfLocalizations k)) x = k x

theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv_apply {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) {k : N ≃* P} (x : N) : (f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k)) x = k x

@[simp]

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_id {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) : f.ofAddEquivOfLocalizations (AddEquiv.refl N) = f

@[simp]

theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_id {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) : f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_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) {Q : Type u_4} [AddCommMonoid Q] {k : N ≃+ P} {j : P ≃+ Q} : (f.ofAddEquivOfLocalizations (k.trans j)).toMap = j.toAddMonoidHom.comp (f.ofAddEquivOfLocalizations k).toMap

theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_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) {Q : Type u_4} [CommMonoid Q] {k : N ≃* P} {j : P ≃* Q} : (f.ofMulEquivOfLocalizations (k.trans j)).toMap = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom.proof_3 {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_1} [AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) (y : ↥T) : IsAddUnit ((f.toMap.comp k.toAddMonoidHom) ↑y)

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfDom.match_5 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_2} [AddCommMonoid P] {k : P ≃+ M} (x : P) (y : P) (motive : (∃ (c : ↥S), ↑c + k.toAddMonoidHom x = ↑c + k.toAddMonoidHom y) → Prop) : ∀ (x_1 : ∃ (c : ↥S), ↑c + k.toAddMonoidHom x = ↑c + k.toAddMonoidHom y), (∀ (c : ↥S) (hc : ↑c + k.toAddMonoidHom x = ↑c + k.toAddMonoidHom y), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfDom.match_2 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_1} [AddCommMonoid P] {k : P ≃+ M} (x : M × ↥S) (motive : (∃ (a : P), k.toEquiv a = ↑x.2) → Prop) : ∀ (x_1 : ∃ (a : P), k.toEquiv a = ↑x.2), (∀ (w : P) (hw : k.toEquiv w = ↑x.2), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfDom.match_1 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) (y : ↥T) (motive : IsAddUnit (f.toMap ↑⟨k ↑y, ⋯⟩) → Prop) : ∀ (x : IsAddUnit (f.toMap ↑⟨k ↑y, ⋯⟩)), (∀ (z : AddUnits N) (hz : ↑z = f.toMap ↑⟨k ↑y, ⋯⟩), motive ⋯) → motive x

Equations

• ⋯ = ⋯

def AddSubmonoid.LocalizationMap.ofAddEquivOfDom {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) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) : T.LocalizationMap N

Given AddCommMonoids M, P and AddSubmonoids S ⊆ M, T ⊆ P, if f : M →* N is a Localization map for S and k : P ≃+ M is an isomorphism of AddCommMonoids such that k(T) = S, f ∘ k is a Localization map for T.

Equations

• f.ofAddEquivOfDom H = let H' := ⋯; (f.toMap.comp k.toAddMonoidHom).toLocalizationMap ⋯ ⋯ ⋯

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfDom.match_3 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_1} [AddCommMonoid P] {k : P ≃+ M} (x : M × ↥S) (motive : (∃ (a : P), k.toEquiv a = x.1) → Prop) : ∀ (x_1 : ∃ (a : P), k.toEquiv a = x.1), (∀ (v : P) (hv : k.toEquiv v = x.1), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom.proof_4 {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_1} [AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) (z : N) : ∃ (x : P × ↥T), z + (f.toMap.comp k.toAddMonoidHom) ↑x.2 = (f.toMap.comp k.toAddMonoidHom) x.1

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom.proof_2 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_1} [AddCommMonoid P] {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) : AddSubmonoid.comap k.toAddMonoidHom S = T

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom.proof_1 {M : Type u_1} [AddCommMonoid M] {P : Type u_2} [AddCommMonoid P] : AddMonoidHomClass (P →+ M) P M

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom.proof_5 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_1} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) (x : P) (y : P) : f.toMap (k.toAddMonoidHom x) = f.toMap (k.toAddMonoidHom y) → ∃ (c : ↥T), ↑c + x = ↑c + y

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfDom.match_4 {M : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_1} [AddCommMonoid P] {k : P ≃+ M} (c : ↥S) (motive : (∃ (a : P), k.toEquiv a = ↑c) → Prop) : ∀ (x : ∃ (a : P), k.toEquiv a = ↑c), (∀ (d : P) (hd : k.toEquiv d = ↑c), motive ⋯) → motive x

Equations

• ⋯ = ⋯

def Submonoid.LocalizationMap.ofMulEquivOfDom {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) {T : Submonoid P} {k : P ≃* M} (H : Submonoid.map k.toMonoidHom T = S) : T.LocalizationMap N

Given CommMonoids M, P and Submonoids S ⊆ M, T ⊆ P, if f : M →* N is a Localization map for S and k : P ≃* M is an isomorphism of CommMonoids such that k(T) = S, f ∘ k is a Localization map for T.

Equations

• f.ofMulEquivOfDom H = let H' := ⋯; (f.toMap.comp k.toMonoidHom).toLocalizationMap ⋯ ⋯ ⋯

@[simp]

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom_apply {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) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) (x : P) : (f.ofAddEquivOfDom H).toMap x = f.toMap (k x)

@[simp]

theorem Submonoid.LocalizationMap.ofMulEquivOfDom_apply {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) {T : Submonoid P} {k : P ≃* M} (H : Submonoid.map k.toMonoidHom T = S) (x : P) : (f.ofMulEquivOfDom H).toMap x = f.toMap (k x)

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom_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) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) : (f.ofAddEquivOfDom H).toMap = f.toMap.comp k.toAddMonoidHom

theorem Submonoid.LocalizationMap.ofMulEquivOfDom_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) {T : Submonoid P} {k : P ≃* M} (H : Submonoid.map k.toMonoidHom T = S) : (f.ofMulEquivOfDom H).toMap = f.toMap.comp k.toMonoidHom

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp_symm {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) {T : AddSubmonoid P} {k : P ≃+ M} (H : AddSubmonoid.map k.toAddMonoidHom T = S) (x : M) : (f.ofAddEquivOfDom H).toMap (k.symm x) = f.toMap x

theorem Submonoid.LocalizationMap.ofMulEquivOfDom_comp_symm {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) {T : Submonoid P} {k : P ≃* M} (H : Submonoid.map k.toMonoidHom T = S) (x : M) : (f.ofMulEquivOfDom H).toMap (k.symm x) = f.toMap x

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom_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) {T : AddSubmonoid P} {k : M ≃+ P} (H : AddSubmonoid.map k.symm.toAddMonoidHom T = S) (x : M) : (f.ofAddEquivOfDom H).toMap (k x) = f.toMap x

theorem Submonoid.LocalizationMap.ofMulEquivOfDom_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) {T : Submonoid P} {k : M ≃* P} (H : Submonoid.map k.symm.toMonoidHom T = S) (x : M) : (f.ofMulEquivOfDom H).toMap (k x) = f.toMap x

@[simp]

theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom_id {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) : f.ofAddEquivOfDom ⋯ = f

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

abbrev AddSubmonoid.LocalizationMap.ofAddEquivOfDom_id.match_1 {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} (x : M) (motive : x ∈ AddSubmonoid.map (AddEquiv.refl M).toAddMonoidHom S → Prop) : ∀ (x_1 : x ∈ AddSubmonoid.map (AddEquiv.refl M).toAddMonoidHom S), (∀ (w : M) (hy : w ∈ ↑S) (h : (AddEquiv.refl M).toAddMonoidHom w = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

@[simp]

theorem Submonoid.LocalizationMap.ofMulEquivOfDom_id {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) : f.ofMulEquivOfDom ⋯ = f

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

noncomputable def AddSubmonoid.LocalizationMap.addEquivOfAddEquiv {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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] (k : T.LocalizationMap Q) {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) : N ≃+ Q

Given Localization maps f : M →+ N, k : P →+ U for Submonoids S, T respectively, an isomorphism j : M ≃+ P such that j(S) = T induces an isomorphism of localizations N ≃+ U.

Equations

• f.addEquivOfAddEquiv k H = f.addEquivOfLocalizations (k.ofAddEquivOfDom H)

theorem AddSubmonoid.LocalizationMap.addEquivOfAddEquiv.proof_1 {M : Type u_2} [AddCommMonoid M] {P : Type u_1} [AddCommMonoid P] : AddMonoidHomClass (M →+ P) M P

noncomputable def Submonoid.LocalizationMap.mulEquivOfMulEquiv {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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] (k : T.LocalizationMap Q) {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) : N ≃* Q

Given Localization maps f : M →* N, k : P →* U for Submonoids S, T respectively, an isomorphism j : M ≃* P such that j(S) = T induces an isomorphism of localizations N ≃* U.

Equations

• f.mulEquivOfMulEquiv k H = f.mulEquivOfLocalizations (k.ofMulEquivOfDom H)

@[simp]

theorem AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map_apply {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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : N) : (f.addEquivOfAddEquiv k H) x = (f.map ⋯ k) x

@[simp]

theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map_apply {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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : N) : (f.mulEquivOfMulEquiv k H) x = (f.map ⋯ k) x

theorem AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map {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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) : (f.addEquivOfAddEquiv k H).toAddMonoidHom = f.map ⋯ k

theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map {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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) : (f.mulEquivOfMulEquiv k H).toMonoidHom = f.map ⋯ k

@[simp]

theorem AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : M) : (f.addEquivOfAddEquiv k H) (f.toMap x) = k.toMap (j x)

@[simp]

theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : M) : (f.mulEquivOfMulEquiv k H) (f.toMap x) = k.toMap (j x)

@[simp]

theorem AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_mk' {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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : M) (y : ↥S) : (f.addEquivOfAddEquiv k H) (f.mk' x y) = k.mk' (j x) ⟨j ↑y, ⋯⟩

@[simp]

theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_mk' {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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : M) (y : ↥S) : (f.mulEquivOfMulEquiv k H) (f.mk' x y) = k.mk' (j x) ⟨j ↑y, ⋯⟩

@[simp]

theorem AddSubmonoid.LocalizationMap.of_addEquivOfAddEquiv_apply {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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : M) : (f.ofAddEquivOfLocalizations (f.addEquivOfAddEquiv k H)).toMap x = k.toMap (j x)

@[simp]

theorem Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_apply {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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : M) : (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap x = k.toMap (j x)

theorem AddSubmonoid.LocalizationMap.of_addEquivOfAddEquiv {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) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) : (f.ofAddEquivOfLocalizations (f.addEquivOfAddEquiv k H)).toMap = k.toMap.comp j.toAddMonoidHom

theorem Submonoid.LocalizationMap.of_mulEquivOfMulEquiv {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) {T : Submonoid P} {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) : (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap = k.toMap.comp j.toMonoidHom

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

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

theorem AddLocalization.addMonoidOf.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : M) (y : M) : (↑{ toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯, map_add' := ⋯ }).toFun x = (↑{ toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯, map_add' := ⋯ }).toFun y → ∃ (c : ↥S), ↑c + x = ↑c + y

theorem AddLocalization.addMonoidOf.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : M) (y : M) : { toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯ }.toFun x + { toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯ }.toFun y

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

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

theorem AddLocalization.addMonoidOf.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (z : AddLocalization S) : ∃ (x : M × ↥S), z + (↑{ toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯, map_add' := ⋯ }).toFun ↑x.2 = (↑{ toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯, map_add' := ⋯ }).toFun x.1

theorem AddLocalization.addMonoidOf.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (y : ↥S) : IsAddUnit ((↑{ toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯, map_add' := ⋯ }).toFun ↑y)

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[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}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : ((AddLocalization.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} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) : ((Localization.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_4} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥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 : ↥S) (d : ↥S) : ((AddLocalization.addMonoidOf S).mk' a b).liftOn₂ ((AddLocalization.addMonoidOf S).mk' c d) f H = f a b c d

@[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}, (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 : ↥S) (d : ↥S) : ((Localization.monoidOf S).mk' a b).liftOn₂ ((Localization.monoidOf S).mk' c d) f H = f a b c d

noncomputable def AddLocalization.addEquivOfQuotient {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) : AddLocalization S ≃+ N

Given a Localization map f : M →+ N for a Submonoid S, we get an isomorphism between the Localization of M at S as a quotient type and N.

Equations

• AddLocalization.addEquivOfQuotient f = (AddLocalization.addMonoidOf S).addEquivOfLocalizations f

noncomputable def Localization.mulEquivOfQuotient {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] (f : S.LocalizationMap N) : Localization S ≃* N

Given a Localization map f : M →* N for a Submonoid S, we get an isomorphism between the Localization of M at S as a quotient type and N.

Equations

• Localization.mulEquivOfQuotient f = (Localization.monoidOf S).mulEquivOfLocalizations f

@[simp]

theorem AddLocalization.addEquivOfQuotient_apply {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (x : AddLocalization S) : (AddLocalization.addEquivOfQuotient f) x = ((AddLocalization.addMonoidOf S).lift ⋯) x

@[simp]

theorem Localization.mulEquivOfQuotient_apply {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (x : Localization S) : (Localization.mulEquivOfQuotient f) x = ((Localization.monoidOf S).lift ⋯) x

@[simp]

theorem AddLocalization.addEquivOfQuotient_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (x : M) (y : ↥S) : (AddLocalization.addEquivOfQuotient f) ((AddLocalization.addMonoidOf S).mk' x y) = f.mk' x y

@[simp]

theorem Localization.mulEquivOfQuotient_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (x : M) (y : ↥S) : (Localization.mulEquivOfQuotient f) ((Localization.monoidOf S).mk' x y) = f.mk' x y

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

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

theorem AddLocalization.addEquivOfQuotient_addMonoidOf {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (x : M) : (AddLocalization.addEquivOfQuotient f) ((AddLocalization.addMonoidOf S).toMap x) = f.toMap x

theorem Localization.mulEquivOfQuotient_monoidOf {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (x : M) : (Localization.mulEquivOfQuotient f) ((Localization.monoidOf S).toMap x) = f.toMap x

@[simp]

theorem AddLocalization.addEquivOfQuotient_symm_mk' {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (x : M) (y : ↥S) : (AddLocalization.addEquivOfQuotient f).symm (f.mk' x y) = (AddLocalization.addMonoidOf S).mk' x y

@[simp]

theorem Localization.mulEquivOfQuotient_symm_mk' {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (x : M) (y : ↥S) : (Localization.mulEquivOfQuotient f).symm (f.mk' x y) = (Localization.monoidOf S).mk' x y

theorem AddLocalization.addEquivOfQuotient_symm_mk {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (x : M) (y : ↥S) : (AddLocalization.addEquivOfQuotient f).symm (f.mk' x y) = AddLocalization.mk x y

theorem Localization.mulEquivOfQuotient_symm_mk {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (x : M) (y : ↥S) : (Localization.mulEquivOfQuotient f).symm (f.mk' x y) = Localization.mk x y

@[simp]

theorem AddLocalization.addEquivOfQuotient_symm_addMonoidOf {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {f : S.LocalizationMap N} (x : M) : (AddLocalization.addEquivOfQuotient f).symm (f.toMap x) = (AddLocalization.addMonoidOf S).toMap x

@[simp]

theorem Localization.mulEquivOfQuotient_symm_monoidOf {M : Type u_1} [CommMonoid M] {S : Submonoid M} {N : Type u_2} [CommMonoid N] {f : S.LocalizationMap N} (x : M) : (Localization.mulEquivOfQuotient f).symm (f.toMap x) = (Localization.monoidOf S).toMap x

@[reducible]

def AddLocalization.Away {M : Type u_1} [AddCommMonoid M] (x : M) : Type u_1

Given x : M, the Localization of M at the Submonoid generated by x, as a quotient.

Equations

• AddLocalization.Away x = AddLocalization (AddSubmonoid.multiples x)

@[reducible]

def Localization.Away {M : Type u_1} [CommMonoid M] (x : M) : Type u_1

Given x : M, the Localization of M at the Submonoid generated by x, as a quotient.

Equations

• Localization.Away x = Localization (Submonoid.powers x)

def AddLocalization.Away.negSelf {M : Type u_1} [AddCommMonoid M] (x : M) : AddLocalization.Away x

Given x : M, negSelf is -x in the Localization (as a quotient type) of M at the Submonoid generated by x.

Equations

• AddLocalization.Away.negSelf x = AddLocalization.mk 0 ⟨x, ⋯⟩

theorem AddLocalization.Away.negSelf.proof_1 {M : Type u_1} [AddCommMonoid M] (x : M) : x ∈ AddSubmonoid.multiples x

def Localization.Away.invSelf {M : Type u_1} [CommMonoid M] (x : M) : Localization.Away x

Given x : M, invSelf is x⁻¹ in the Localization (as a quotient type) of M at the Submonoid generated by x.

Equations

• Localization.Away.invSelf x = Localization.mk 1 ⟨x, ⋯⟩

@[reducible]

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

Given x : M, the natural hom sending y : M, M an AddCommMonoid, to the equivalence class of (y, 0) in the Localization of M at the Submonoid generated by x.

Equations

• AddLocalization.Away.addMonoidOf x = AddLocalization.addMonoidOf (AddSubmonoid.multiples x)

@[reducible]

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

Given x : M, the natural hom sending y : M, M a CommMonoid, to the equivalence class of (y, 1) in the Localization of M at the Submonoid generated by x.

Equations

• Localization.Away.monoidOf x = Localization.monoidOf (Submonoid.powers x)

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

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

noncomputable def AddLocalization.Away.addEquivOfQuotient {M : Type u_1} [AddCommMonoid M] {N : Type u_2} [AddCommMonoid N] (x : M) (f : AddSubmonoid.LocalizationMap.AwayMap x N) : AddLocalization.Away x ≃+ N

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

Equations

• AddLocalization.Away.addEquivOfQuotient x f = AddLocalization.addEquivOfQuotient f

noncomputable def Localization.Away.mulEquivOfQuotient {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] (x : M) (f : Submonoid.LocalizationMap.AwayMap x N) : Localization.Away x ≃* N

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

Equations

• Localization.Away.mulEquivOfQuotient x f = Localization.mulEquivOfQuotient f

theorem Submonoid.LocalizationMap.subsingleton {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) (h : 0 ∈ S) : Subsingleton N

If S contains 0 then the localization at S is trivial.

structure Submonoid.LocalizationWithZeroMap {M : Type u_1} [CommMonoidWithZero M] (S : Submonoid M) (N : Type u_2) [CommMonoidWithZero N] extends Submonoid.LocalizationMap : Type (max u_1 u_2)

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

• toFun : M → N
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' : ∀ (x y : M), (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• map_units' : ∀ (y : ↥S), IsUnit ((↑self.toMonoidHom).toFun ↑y)
• surj' : ∀ (z : N), ∃ (x : M × ↥S), z * (↑self.toMonoidHom).toFun ↑x.2 = (↑self.toMonoidHom).toFun x.1
• exists_of_eq : ∀ (x y : M), (↑self.toMonoidHom).toFun x = (↑self.toMonoidHom).toFun y → ∃ (c : ↥S), ↑c * x = ↑c * y
• map_zero' : (↑self.toMonoidHom).toFun 0 = 0

theorem Submonoid.LocalizationWithZeroMap.map_zero' {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (self : S.LocalizationWithZeroMap N) : (↑self.toMonoidHom).toFun 0 = 0

def Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) : M →*₀ N

The monoid with zero hom underlying a LocalizationMap.

Equations

• f.toMonoidWithZeroHom = { toFun := (↑f.toMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Localization.zero_def {M : Type u_4} [CommMonoidWithZero M] (S : Submonoid M) : Localization.zero S = Localization.mk 0 1

@[irreducible]

def Localization.zero {M : Type u_4} [CommMonoidWithZero M] (S : Submonoid M) : Localization S

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

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

Equations

• @Localization.zero = Localization.wrapped✝.1

instance Localization.instZero {M : Type u_1} [CommMonoidWithZero M] (S : Submonoid M) : Zero (Localization S)

Equations

• Localization.instZero S = { zero := Localization.zero S }

theorem Localization.mk_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} (x : ↥S) : Localization.mk 0 x = 0

instance Localization.instCommMonoidWithZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} : CommMonoidWithZero (Localization S)

Equations

• Localization.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

theorem Localization.liftOn_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {p : Type u_4} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d) : Localization.liftOn 0 f H = f 0 1

@[simp]

theorem Submonoid.LocalizationMap.sec_zero_fst {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {f : S.LocalizationMap N} : f.toMap (f.sec 0).1 = 0

noncomputable def Submonoid.LocalizationWithZeroMap.lift {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {P : Type u_3} [CommMonoidWithZero P] (f : S.LocalizationWithZeroMap N) (g : M →*₀ P) (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : N →*₀ P

Given a Localization map f : M →*₀ N for a Submonoid S ⊆ M and a map of CommMonoidWithZeros g : M →*₀ P such that g y is invertible for all y : S, the homomorphism induced from N to P sending z : N to g x * (g y)⁻¹, where (x, y) : M × S are such that z = f x * (f y)⁻¹.

Equations

• f.lift g hg = let __src := f.lift hg; { toFun := (↑__src).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) [IsLeftCancelMulZero M] (h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x) : IsLeftCancelMulZero N

Given a Localization map f : M →*₀ N for a Submonoid S ⊆ M, if M is left cancellative monoid with zero, and all elements of S are left regular, then N is a left cancellative monoid with zero.

theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) [IsCancelMulZero M] (h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x) : IsCancelMulZero N

Given a Localization map f : M →*₀ N for a Submonoid S ⊆ M, if M is a cancellative monoid with zero, and all elements of S are regular, then N is a cancellative monoid with zero.

@[deprecated Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero]

theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_IsCancelMulZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) [IsCancelMulZero M] (h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x) : IsCancelMulZero N

Alias of Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero.

---

Given a Localization map f : M →*₀ N for a Submonoid S ⊆ M, if M is a cancellative monoid with zero, and all elements of S are regular, then N is a cancellative monoid with zero.

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

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

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

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

theorem AddLocalization.decidableEq.proof_1 {α : Type u_1} [AddCancelCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : ↥s) (d : ↥s) : Subsingleton (Decidable (AddLocalization.mk a b = AddLocalization.mk c d))

instance AddLocalization.decidableEq {α : Type u_1} [AddCancelCommMonoid α] {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) ⋯

instance Localization.decidableEq {α : Type u_1} [CancelCommMonoid α] {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) ⋯

Order

instance AddLocalization.le {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : LE (AddLocalization s)

Equations

• AddLocalization.le = { le := fun (a b : AddLocalization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) ⋯ }

theorem AddLocalization.le.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a₁ : α) (b₁ : α) (a₂ : ↥s) (b₂ : ↥s) (c₁ : α) (d₁ : α) (c₂ : ↥s) (d₂ : ↥s) (hab : (AddLocalization.r s) (a₁, a₂) (b₁, b₂)) (hcd : (AddLocalization.r s) (c₁, c₂) (d₁, d₂)) : (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) a₁ a₂ c₁ c₂ = (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ ≤ ↑a₂ + b₁) b₁ b₂ d₁ d₂

instance Localization.le {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} : LE (Localization s)

Equations

• Localization.le = { le := fun (a b : Localization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ * a₁ ≤ ↑a₂ * b₁) ⋯ }

instance AddLocalization.lt {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : LT (AddLocalization s)

Equations

• AddLocalization.lt = { lt := fun (a b : AddLocalization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ < ↑a₂ + b₁) ⋯ }

theorem AddLocalization.lt.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a₁ : α) (b₁ : α) (a₂ : ↥s) (b₂ : ↥s) (c₁ : α) (d₁ : α) (c₂ : ↥s) (d₂ : ↥s) (hab : (AddLocalization.r s) (a₁, a₂) (b₁, b₂)) (hcd : (AddLocalization.r s) (c₁, c₂) (d₁, d₂)) : (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ < ↑a₂ + b₁) a₁ a₂ c₁ c₂ = (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ + a₁ < ↑a₂ + b₁) b₁ b₂ d₁ d₂

instance Localization.lt {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} : LT (Localization s)

Equations

• Localization.lt = { lt := fun (a b : Localization s) => a.liftOn₂ b (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) => ↑b₂ * a₁ < ↑a₂ * b₁) ⋯ }

theorem AddLocalization.mk_le_mk {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : ↥s} {b₂ : ↥s} : AddLocalization.mk a₁ a₂ ≤ AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁

theorem Localization.mk_le_mk {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} {a₁ : α} {b₁ : α} {a₂ : ↥s} {b₂ : ↥s} : Localization.mk a₁ a₂ ≤ Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁

theorem AddLocalization.mk_lt_mk {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ : α} {b₁ : α} {a₂ : ↥s} {b₂ : ↥s} : AddLocalization.mk a₁ a₂ < AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁

theorem Localization.mk_lt_mk {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} {a₁ : α} {b₁ : α} {a₂ : ↥s} {b₂ : ↥s} : Localization.mk a₁ a₂ < Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁

theorem AddLocalization.partialOrder.proof_4 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a ≤ b → b ≤ a → a = b

theorem AddLocalization.partialOrder.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) : a ≤ a

instance AddLocalization.partialOrder {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : PartialOrder (AddLocalization s)

Equations

• AddLocalization.partialOrder = PartialOrder.mk ⋯

theorem AddLocalization.partialOrder.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) (c : AddLocalization s) : a ≤ b → b ≤ c → a ≤ c

theorem AddLocalization.partialOrder.proof_3 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a < b ↔ a ≤ b ∧ ¬b ≤ a

instance Localization.partialOrder {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} : PartialOrder (Localization s)

Equations

• Localization.partialOrder = PartialOrder.mk ⋯

theorem AddLocalization.orderedAddCancelCommMonoid.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) (c : AddLocalization s) : a + b ≤ a + c → b ≤ c

instance AddLocalization.orderedAddCancelCommMonoid {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : OrderedCancelAddCommMonoid (AddLocalization s)

Equations

• AddLocalization.orderedAddCancelCommMonoid = let __src := AddLocalization.addCommMonoid s; let __src_1 := AddLocalization.partialOrder; OrderedCancelAddCommMonoid.mk ⋯

theorem AddLocalization.orderedAddCancelCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a ≤ b → ∀ (c : AddLocalization s), c + a ≤ c + b

instance Localization.orderedCancelCommMonoid {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} : OrderedCancelCommMonoid (Localization s)

Equations

• Localization.orderedCancelCommMonoid = let __src := Localization.commMonoid s; let __src_1 := Localization.partialOrder; OrderedCancelCommMonoid.mk ⋯

theorem AddLocalization.decidableLE.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : ↥s) (d : ↥s) : Subsingleton (Decidable ((fun (x x_1 : AddLocalization s) => x ≤ x_1) (AddLocalization.mk a b) (AddLocalization.mk c d)))

instance AddLocalization.decidableLE {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} [DecidableRel fun (x x_1 : α) => x ≤ x_1] : DecidableRel fun (x x_1 : AddLocalization s) => x ≤ x_1

Equations

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

instance Localization.decidableLE {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} [DecidableRel fun (x x_1 : α) => x ≤ x_1] : DecidableRel fun (x x_1 : Localization s) => x ≤ x_1

Equations

• a.decidableLE 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.decidableLT {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} [DecidableRel fun (x x_1 : α) => x < x_1] : DecidableRel fun (x x_1 : AddLocalization s) => x < x_1

Equations

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

theorem AddLocalization.decidableLT.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : α) (c : α) (b : ↥s) (d : ↥s) : Subsingleton (Decidable ((fun (x x_1 : AddLocalization s) => x < x_1) (AddLocalization.mk a b) (AddLocalization.mk c d)))

instance Localization.decidableLT {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} [DecidableRel fun (x x_1 : α) => x < x_1] : DecidableRel fun (x x_1 : Localization s) => x < x_1

Equations

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

theorem AddLocalization.mkOrderEmbedding.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : ↥s) {a : α} {b : α} : AddLocalization.mk a b✝ ≤ AddLocalization.mk b b✝ ↔ a ≤ b

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

def AddLocalization.mkOrderEmbedding {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : ↥s) : α ↪o AddLocalization s

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

Equations

• AddLocalization.mkOrderEmbedding b = { toFun := fun (a : α) => AddLocalization.mk a b, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Localization.mkOrderEmbedding_apply {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} (b : ↥s) (a : α) : (Localization.mkOrderEmbedding b) a = (Localization.monoidOf s).mk' a b

@[simp]

theorem AddLocalization.mkOrderEmbedding_apply {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (b : ↥s) (a : α) : (AddLocalization.mkOrderEmbedding b) a = (AddLocalization.addMonoidOf s).mk' a b

def Localization.mkOrderEmbedding {α : Type u_1} [OrderedCancelCommMonoid α] {s : Submonoid α} (b : ↥s) : α ↪o Localization s

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

Equations

• Localization.mkOrderEmbedding b = { toFun := fun (a : α) => Localization.mk a b, inj' := ⋯, map_rel_iff' := ⋯ }

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} (a : AddLocalization s) (b : AddLocalization s) : a ≤ b ∨ b ≤ a

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_3 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : ∀ (a b : AddLocalization s), max a b = max a b

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_4 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : ∀ (a b : AddLocalization s), compare a b = compare a b

instance AddLocalization.instLinearOrderedAddCancelCommMonoid {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : LinearOrderedCancelAddCommMonoid (AddLocalization s)

Equations

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

theorem AddLocalization.instLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] {s : AddSubmonoid α} : ∀ (a b : AddLocalization s), min a b = min a b

instance Localization.instLinearOrderedCancelCommMonoid {α : Type u_1} [LinearOrderedCancelCommMonoid α] {s : Submonoid α} : LinearOrderedCancelCommMonoid (Localization s)

Equations

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

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 = { toFun := ⇑OreLocalization.numeratorHom, map_one' := ⋯, map_mul' := ⋯, map_units' := ⋯, surj' := ⋯, exists_of_eq := ⋯ }

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 = Localization.mulEquivOfQuotient (OreLocalization.localizationMap R S)