Mapping properties of monoid localizations

Given an S-localization map f : M →* N, we can define 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.

Tags

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

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 y : M} (h : f x = f 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.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 y : M} (h : f x = f y) : g x = g y

Given a Localization map f : M →+ N for an AddSubmonoid 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.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 y : M} (h : f x = f y) : k (g x) = k (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.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 y : M} (h : f x = f y) : k (g x) = k (g y)

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

noncomputable def Submonoid.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)⁻¹.

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.

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

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

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_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 an AddSubmonoid 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.

@[simp]

theorem Submonoid.LocalizationMap.lift_localizationMap_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 : S.LocalizationMap P) (x : M) (y : ↥S) : (f.lift ⋯) (f.mk' x y) = g.mk' x y

Given a Localization map f : M →* N for a Submonoid S ⊆ M and a localization map g : M →* P for the same submonoid, the homomorphism induced from N to P maps f x * (f y)⁻¹ to g x * (g y)⁻¹ for all x : M, y ∈ S.

@[simp]

theorem AddSubmonoid.LocalizationMap.lift_localizationMap_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 : S.LocalizationMap P) (x : M) (y : ↥S) : (f.lift ⋯) (f.mk' x y) = g.mk' x y

Given a Localization map f : M →+ N for an AddSubmonoid S ⊆ M and a localization map g : M →+ P for the same submonoid, 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_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 {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 an AddSubmonoid 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_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 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_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 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 an AddSubmonoid 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_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_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_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_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 an AddSubmonoid 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_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.

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 an AddSubmonoid 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.

@[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 x) = g 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 x) = g x

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 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 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 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 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.toMonoidHom = g

@[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.toAddMonoidHom = g

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

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

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 x) = g x) : f.lift hg = j

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 x) = g x) : f.lift hg = j

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

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

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 {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_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

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

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

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

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_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_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 x = f y ↔ g x = g y

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 x = f y ↔ g x = g y

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)⁻¹.

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

@[simp]

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 x) = k (g x)

@[simp]

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 x) = k (g x)

@[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.toMonoidHom = k.toMonoidHom.comp g

@[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.toAddMonoidHom = k.toAddMonoidHom.comp g

@[simp]

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, ⋯⟩

@[simp]

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_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 (g (f.sec z).1) = k (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_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 (g (f.sec z).1) = k (g ↑(f.sec z).2) + u

Given Localization maps f : M →+ N, k : P →+ Q for AddSubmonoids 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_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 (g ↑(f.sec z).2) = k (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_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 (g ↑(f.sec z).2) = k (g (f.sec z).1)

Given Localization maps f : M →+ N, k : P →+ Q for AddSubmonoids 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_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 (g ↑(f.sec z).2) * (f.map hy k) z = k (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.

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 (g ↑(f.sec z).2) + (f.map hy k) z = k (g (f.sec z).1)

Given Localization maps f : M →+ N, k : P →+ Q for AddSubmonoids 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.

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

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

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_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_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_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_injective_of_surjOn_or_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} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [CommMonoid Q] {k : T.LocalizationMap Q} (or : Set.SurjOn ⇑g ↑S ↑T ∨ Function.Injective ⇑k) (hg : Function.Injective ⇑g) : Function.Injective ⇑(f.map hy k)

theorem AddSubmonoid.LocalizationMap.map_injective_of_surjOn_or_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} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (or : Set.SurjOn ⇑g ↑S ↑T ∨ Function.Injective ⇑k) (hg : Function.Injective ⇑g) : Function.Injective ⇑(f.map hy k)

theorem Submonoid.LocalizationMap.map_surjective_of_surjOn {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} (surj : Set.SurjOn ⇑g ↑S ↑T) (hg : Function.Surjective ⇑g) : Function.Surjective ⇑(f.map hy k)

theorem AddSubmonoid.LocalizationMap.map_surjective_of_surjOn {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} (surj : Set.SurjOn ⇑g ↑S ↑T) (hg : Function.Surjective ⇑g) : Function.Surjective ⇑(f.map hy k)

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.

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.

theorem Submonoid.LocalizationMap.map_surjective_of_surjective {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.Surjective ⇑g) (k : (Submonoid.map g S).LocalizationMap Q) : Function.Surjective ⇑(f.map ⋯ k)

Given a surjective 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 surjective.

theorem AddSubmonoid.LocalizationMap.map_surjective_of_surjective {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.Surjective ⇑g) (k : (AddSubmonoid.map g S).LocalizationMap Q) : Function.Surjective ⇑(f.map ⋯ k)

Given a surjective 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 surjective.

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.

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.

@[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_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_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

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

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

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.

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.

@[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) x = k (f x)

@[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) x = k (f x)

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).toMonoidHom = k.toMonoidHom.comp f.toMonoidHom

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).toAddMonoidHom = k.toAddMonoidHom.comp f.toAddMonoidHom

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

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) x = y ↔ f x = k.symm y

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) x = y ↔ f x = k.symm y

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 {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_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)) x = k x

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)) x = k x

@[simp]

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

@[simp]

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_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

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

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

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

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)).toMonoidHom = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom

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)).toAddMonoidHom = j.toAddMonoidHom.comp (f.ofAddEquivOfLocalizations k).toAddMonoidHom

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.

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.

@[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) x = f (k x)

@[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) x = f (k x)

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).toMonoidHom = f.toMonoidHom.comp k.toMonoidHom

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).toAddMonoidHom = f.toAddMonoidHom.comp k.toAddMonoidHom

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) (k.symm x) = f x

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) (k.symm x) = f 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) (k x) = f 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) (k x) = f x

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

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

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.

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.

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

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

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

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 {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 x) = k (j x)

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 x) = k (j x)

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, ⋯⟩

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, ⋯⟩

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)) x = k (j x)

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)) x = k (j x)

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)).toMonoidHom = k.toMonoidHom.comp j.toMonoidHom

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)).toAddMonoidHom = k.toAddMonoidHom.comp j.toAddMonoidHom

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.

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.

@[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) : (mulEquivOfQuotient f) x = ((monoidOf S).lift ⋯) x

@[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) : (addEquivOfQuotient f) x = ((addMonoidOf S).lift ⋯) x

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) : (mulEquivOfQuotient f) ((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) : (addEquivOfQuotient f) ((addMonoidOf S).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) : (mulEquivOfQuotient f) (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) : (addEquivOfQuotient f) (mk x y) = f.mk' x y

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) : (mulEquivOfQuotient f) ((monoidOf S) x) = f x

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) : (addEquivOfQuotient f) ((addMonoidOf S) x) = f x

@[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) : (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y

@[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) : (addEquivOfQuotient f).symm (f.mk' x y) = (addMonoidOf S).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) : (mulEquivOfQuotient f).symm (f.mk' x y) = 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) : (addEquivOfQuotient f).symm (f.mk' x y) = mk x y

@[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) : (mulEquivOfQuotient f).symm (f x) = (monoidOf S) x

@[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) : (addEquivOfQuotient f).symm (f x) = (addMonoidOf S) x