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:
- For all
y ∈ S
,f y
is a unit; - For all
z : N
, there exists(x, y) : M × S
such thatz * f y = f x
; - For all
x, y : M
,f x = f y
iff there existsc ∈ S
such thatx * c = y * c
.
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
- toFun : M → N
- map_zero' : ZeroHom.toFun (↑s.toAddMonoidHom) 0 = 0
- map_add' : ∀ (x y : M), ZeroHom.toFun (↑s.toAddMonoidHom) (x + y) = ZeroHom.toFun (↑s.toAddMonoidHom) x + ZeroHom.toFun (↑s.toAddMonoidHom) y
- map_add_units' : ∀ (y : { x // x ∈ S }), IsAddUnit (ZeroHom.toFun ↑s.toAddMonoidHom ↑y)
- surj' : ∀ (z : N), ∃ x, z + ZeroHom.toFun ↑s.toAddMonoidHom ↑x.snd = ZeroHom.toFun (↑s.toAddMonoidHom) x.fst
- eq_iff_exists' : ∀ (x y : M), ZeroHom.toFun (↑s.toAddMonoidHom) x = ZeroHom.toFun (↑s.toAddMonoidHom) y ↔ ∃ c, ↑c + x = ↑c + y
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
.
Instances For
- toFun : M → N
- map_one' : OneHom.toFun (↑s.toMonoidHom) 1 = 1
- map_mul' : ∀ (x y : M), OneHom.toFun (↑s.toMonoidHom) (x * y) = OneHom.toFun (↑s.toMonoidHom) x * OneHom.toFun (↑s.toMonoidHom) y
- map_units' : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑s.toMonoidHom ↑y)
- surj' : ∀ (z : N), ∃ x, z * OneHom.toFun ↑s.toMonoidHom ↑x.snd = OneHom.toFun (↑s.toMonoidHom) x.fst
- eq_iff_exists' : ∀ (x y : M), OneHom.toFun (↑s.toMonoidHom) x = OneHom.toFun (↑s.toMonoidHom) y ↔ ∃ c, ↑c * x = ↑c * y
The type of monoid homomorphisms satisfying the characteristic predicate: if f : M →* N
satisfies this predicate, then N
is isomorphic to the localization of M
at S
.
Instances For
The congruence relation on M × S
, M
an AddCommMonoid
and S
an add_submonoid
of M
,
whose quotient is the localization of M
at S
, defined as the unique congruence relation on
M × S
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
.
Instances For
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
.
Instances For
Instances For
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
.
Instances For
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
.
Instances For
Instances For
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'
).
Instances For
Instances For
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'
).
The localization of an AddCommMonoid
at one of its submonoids (as a quotient type).
Instances For
The localization of a CommMonoid
at one of its submonoids (as a quotient type).
Instances For
Multiplication in a Localization
is defined as ⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c, b * d⟩
.
Instances For
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⟩
.
Instances For
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⟩
.
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⟩
.
Instances For
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⟩
.
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.
Instances For
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.
Instances For
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.
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
.
Instances For
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
.
Instances For
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
.
Instances For
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
.
Instances For
Copy of Quotient.recOnSubsingleton₂
for AddLocalization
Instances For
Copy of Quotient.recOnSubsingleton₂
for Localization
Instances For
Non-dependent recursion principle for AddLocalization
s: 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
.
Instances For
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
.
Instances For
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
.
Instances For
Instances For
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
.
Instances For
Scalar multiplication in a monoid localization is defined as c • ⟨a, b⟩ = ⟨c • a, b⟩
.
Instances For
Makes a localization map from an AddCommMonoid
hom satisfying the characteristic predicate.
Instances For
Makes a localization map from a CommMonoid
hom satisfying the characteristic predicate.
Instances For
Short for toAddMonoidHom
; used to apply a localization map as a function.
Instances For
Short for toMonoidHom
; used to apply a localization map as a function.
Instances For
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
.
Instances For
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
.
Instances For
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
.
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
.
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
.
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
.
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₁)
.
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₁)
.
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
.
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
.
Given an AddMonoidHom f : M →+ N
and Submonoid S ⊆ M
such that
f(S) ⊆ AddUnits N
, for all y ∈ S
, - (f y)
is unique.
Given a MonoidHom f : M →* N
and Submonoid S ⊆ M
such that f(S) ⊆ Nˣ
, for all
y ∈ S
, (f y)⁻¹
is unique.
Given a localization map f : M →+ N
, the surjection sending (x, y) : M × S
to f x - f y
.
Instances For
Given a localization map f : M →* N
, the surjection sending (x, y) : M × S
to
f x * (f y)⁻¹
.
Instances For
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
.
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
.
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
.
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
.
Given a Localization map f : M →+ N
for a Submonoid S ⊆ M
and a map of
AddCommMonoid
s g : M →+ P
such that g(S) ⊆ AddUnits P
, f x = f y → g x = g y
for all x y : M
.
Given a Localization map f : M →* N
for a Submonoid S ⊆ M
and a map of CommMonoid
s
g : M →* P
such that g(S) ⊆ Units P
, f x = f y → g x = g y
for all x y : M
.
Given AddCommMonoid
s 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)
.
Given CommMonoid
s 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)
.
Given a localization map f : M →+ N
for a submonoid S ⊆ M
and a map of
AddCommMonoid
s 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
.
Instances For
Given a Localization map f : M →* N
for a Submonoid S ⊆ M
and a map of CommMonoid
s
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)⁻¹
.
Instances For
Given a Localization map f : M →+ N
for a Submonoid S ⊆ M
and a map of
AddCommMonoid
s 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
.
Given a Localization map f : M →* N
for a Submonoid S ⊆ M
and a map of CommMonoid
s
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
Instances For
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)⁻¹
.
Instances For
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
Instances For
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
.
Instances For
Given x : M
and a Localization map F : M →* N
away from x
, invSelf
is (F x)⁻¹
.
Instances For
Given x : M
, a Localization map F : M →* N
away from x
, and a map of CommMonoid
s
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)⁻ⁿ
.
Instances For
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
.
Instances For
Given x : A
and a Localization map F : A →+ B
away from x
, neg_self
is - (F x)
.
Instances For
Given x : A
, a localization map F : A →+ B
away from x
, and a map of AddCommMonoid
s
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
.
Instances For
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
.