Localizations of commutative monoids #
Localizing a commutative ring at one of its submonoids does not rely on the ring's addition, so we can generalize localizations to commutative monoids.
We characterize the localization of a commutative monoid M
at a submonoid S
up to
isomorphism; that is, a commutative monoid N
is the localization of M
at S
iff we can find a
monoid homomorphism f : M →* N→* N
satisfying 3 properties:
- For all
y ∈ S∈ S
,f y
is a unit; - For all
z : N
, there exists(x, y) : M × S× S
such thatz * f y = f x
; - For all
x, y : M
,f x = f y
iff there existsc ∈ S∈ S
such thatx * c = y * c
.
Given such a localization map f : M →* N→* N
, we can define the surjection
LocalizationMap.mk'
sending (x, y) : M × S× S
to f x * (f y)⁻¹⁻¹
, and
LocalizationMap.lift
, the homomorphism from N
induced by a homomorphism from M
which maps
elements of S
to invertible elements of the codomain. Similarly, given commutative monoids
P, Q
, a submonoid T
of P
and a localization map for T
from P
to Q
, then a homomorphism
g : M →* P→* P
such that g(S) ⊆ T⊆ T
induces a homomorphism of localizations,
LocalizationMap.map
, from N
to Q
.
We treat the special case of localizing away from an element in the sections AwayMap
and Away
.
We also define the quotient of M × S× S
by the unique congruence relation (equivalence relation
preserving a binary operation) r
such that for any other congruence relation s
on M × S× S
satisfying '∀ y ∈ S∀ y ∈ S∈ S
, (1, 1) ∼ (y, y)∼ (y, y)
under s
', we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂)
by s
whenever (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂)
by r
. We show this relation is equivalent to the standard
localization relation.
This defines the localization as a quotient type, Localization
, but the majority of
subsequent lemmas in the file are given in terms of localizations up to isomorphism, using maps
which satisfy the characteristic predicate.
Implementation notes #
In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally rewrite
one
structure with an isomorphic one; one way around this is to isolate a predicate characterizing
a structure up to isomorphism, and reason about things that satisfy the predicate.
The infimum form of the localization congruence relation is chosen as 'canonical' here, since it shortens some proofs.
To apply a localization map f
as a function, we use f.toMap
, as coercions don't work well for
this structure.
To reason about the localization as a quotient type, use mk_eq_monoidOf_mk'
and associated
lemmas. These show the quotient map mk : M → S → Localization S→ S → Localization S→ Localization S
equals the
surjection LocalizationMap.mk'
induced by the map
monoid_of : localization_map S (localization S)
(where of
establishes the
localization as a quotient type satisfies the characteristic predicate). The lemma
mk_eq_monoidOf_mk'
hence gives you access to the results in the rest of the file, which are
about the LocalizationMap.mk'
induced by any localization map.
Tags #
localization, monoid localization, quotient monoid, congruence relation, characteristic predicate, commutative monoid
- map_add_units' : ∀ (y : { x // x ∈ S }), IsAddUnit (ZeroHom.toFun ↑toAddMonoidHom ↑y)
- surj' : ∀ (z : N), ∃ x, z + ZeroHom.toFun ↑toAddMonoidHom ↑x.snd = ZeroHom.toFun (↑toAddMonoidHom) x.fst
- eq_iff_exists' : ∀ (x y : M), ZeroHom.toFun (↑toAddMonoidHom) x = ZeroHom.toFun (↑toAddMonoidHom) y ↔ ∃ c, ↑c + x = ↑c + y
The type of AddMonoid homomorphisms satisfying the characteristic predicate: if f : M →+ N→+ N
satisfies this predicate, then N
is isomorphic to the localization of M
at S
.
Instances For
- map_units' : ∀ (y : { x // x ∈ S }), IsUnit (OneHom.toFun ↑toMonoidHom ↑y)
- surj' : ∀ (z : N), ∃ x, z * OneHom.toFun ↑toMonoidHom ↑x.snd = OneHom.toFun (↑toMonoidHom) x.fst
- eq_iff_exists' : ∀ (x y : M), OneHom.toFun (↑toMonoidHom) x = OneHom.toFun (↑toMonoidHom) y ↔ ∃ c, ↑c * x = ↑c * y
The type of monoid homomorphisms satisfying the characteristic predicate: if f : M →* N→* N
satisfies this predicate, then N
is isomorphic to the localization of M
at S
.
Instances For
The congruence relation on M × S× S
, M
an AddCommMonoid
and S
an add_submonoid
of M
,
whose quotient is the localization of M
at S
, defined as the unique congruence relation on
M × S× S
such that for any other congruence relation s
on M × S× S
where for all y ∈ S∈ S
,
(0, 0) ∼ (y, y)∼ (y, y)
under s
, we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂)
by r
implies
(x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂)
by s
.
Equations
- addLocalization.r S = infₛ { c | ∀ (y : { x // x ∈ S }), ↑c 0 (↑y, y) }
The congruence relation on M × S× S
, M
a CommMonoid
and S
a submonoid of M
, whose
quotient is the localization of M
at S
, defined as the unique congruence relation on
M × S× S
such that for any other congruence relation s
on M × S× S
where for all y ∈ S∈ S
,
(1, 1) ∼ (y, y)∼ (y, y)
under s
, we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂)
by r
implies
(x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂)
by s
.
Equations
- Localization.r S = infₛ { c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y) }
An alternate form of the congruence relation on M × S× S
, M
a CommMonoid
and S
a
submonoid of M
, whose quotient is the localization of M
at S
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- addLocalization.r'.match_1 S motive x h_1 = Exists.casesOn x fun w h => h_1 w h
An alternate form of the congruence relation on M × S× S
, M
a CommMonoid
and S
a
submonoid of M
, whose quotient is the localization of M
at S
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- addLocalization.r_eq_r'.match_1 S p q x y motive x h_1 = Exists.casesOn x fun w h => h_1 w h
Equations
- addLocalization.r_eq_r'.match_3 S x motive x x h_1 = Prod.casesOn M { x // x ∈ S } (fun x => (x_1 : ↑(addLocalization.r' S) x x) → motive x x_1) x (fun fst snd x => h_1 fst snd x) x
Equations
- addLocalization.r_eq_r'.match_2 S p q motive x x h_1 = Prod.casesOn M { x // x ∈ S } (fun x => (x_1 : ↑(addLocalization.r' S) (p, q) x) → motive x x_1) x (fun fst snd x => h_1 fst snd x) x
The additive congruence relation used to localize an AddCommMonoid
at a submonoid can be
expressed equivalently as an infimum (see addLocalization.r
) or explicitly
(see addLocalization.r'
).
The congruence relation used to localize a CommMonoid
at a submonoid can be expressed
equivalently as an infimum (see Localization.r
) or explicitly
(see Localization.r'
).
The localization of an AddCommMonoid
at one of its submonoids (as a quotient type).
Equations
The localization of a CommMonoid
at one of its submonoids (as a quotient type).
Equations
Equations
- addLocalization.inhabited S = AddCon.Quotient.inhabited
Equations
- Localization.inhabited S = Con.Quotient.inhabited
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 S = Add.add
Multiplication in a Localization
is defined as ⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c, b * d⟩
.
Equations
- Localization.mul S = Mul.mul
Equations
- addLocalization.instAddLocalization S = { add := addLocalization.add S }
Equations
- Localization.instMulLocalization S = { mul := Localization.mul 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 S = Zero.zero
The identity element of a Localization
is defined as ⟨1, 1⟩
.
Equations
- Localization.one S = One.one
Equations
- addLocalization.instZeroLocalization S = { zero := addLocalization.zero S }
Equations
- Localization.instOneLocalization S = { one := Localization.one 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 S = AddMonoid.nsmul
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 S = Monoid.npow
Equations
- (_ : ∀ (x : addLocalization S), addLocalization.nsmul S 0 x = 0) = (_ : ∀ (x : addLocalization S), addLocalization.nsmul S 0 x = 0)
Equations
- (_ : ∀ (x y : addLocalization S), x + y = y + x) = (_ : ∀ (x y : addLocalization S), x + y = y + x)
Equations
- addLocalization.instAddCommMonoidLocalization S = AddCommMonoid.mk (_ : ∀ (x y : addLocalization S), x + y = y + x)
Equations
- (_ : ∀ (x : addLocalization S), x + 0 = x) = (_ : ∀ (x : addLocalization S), x + 0 = x)
Equations
- (_ : ∀ (x : addLocalization S), 0 + x = x) = (_ : ∀ (x : addLocalization S), 0 + x = x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Localization.instCommMonoidLocalization S = CommMonoid.mk (_ : ∀ (x y : Localization S), x * y = y * x)
Given an AddCommMonoid
M
and submonoid S
, mk
sends x : M
, y ∈ S∈ S
to
the equivalence class of (x, y)
in the localization of M
at S
.
Equations
- addLocalization.mk x y = ↑(AddCon.mk' (addLocalization.r S)) (x, y)
Given a CommMonoid
M
and submonoid S
, mk
sends x : M
, y ∈ S∈ S
to the equivalence
class of (x, y)
in the localization of M
at S
.
Equations
- Localization.mk x y = ↑(Con.mk' (Localization.r S)) (x, y)
Dependent recursion principle for addLocalizations
: given elements f a b : p (mk a b)
for all a b
, such that r S (a, b) (c, d)
implies f a b = f c d
(with the correct coercions),
then f
is defined on the whole addLocalization S
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : addLocalization.mk a b = addLocalization.mk c d) = (_ : addLocalization.mk a b = addLocalization.mk c d)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : addLocalization.mk y.fst y.snd = addLocalization.mk y.fst y.snd) = (_ : addLocalization.mk y.fst y.snd = addLocalization.mk y.fst y.snd)
Dependent recursion principle for Localizations
: given elements f a b : p (mk a b)
for all a b
, such that r S (a, b) (c, d)
implies f a b = f c d
(with the correct coercions),
then f
is defined on the whole Localization S
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : (_ : addLocalization.mk a b = addLocalization.mk c d) ▸ f a b = f c d) = (_ : (_ : addLocalization.mk a b = addLocalization.mk c d) ▸ f a b = f c d)
Non-dependent recursion principle for add_localizations
: given elements f a b : p
for all a b
, such that r S (a, b) (c, d)
implies f a b = f c d
,
then f
is defined on the whole Localization S
.
Equations
- One or more equations did not get rendered due to their size.
Non-dependent recursion principle for localizations: given elements f a b : p
for all a b
, such that r S (a, b) (c, d)
implies f a b = f c d
,
then f
is defined on the whole Localization S
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- addLocalization.liftOn₂.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd
Non-dependent recursion principle for localizations: given elements f x y : p
for all x
and y
, such that r S x x'
and r S y y'
implies f x y = f x' y'
,
then f
is defined on the whole Localization S
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : f a b a b = f a b c d) = H a a b b a c b d (_ : ↑(addLocalization.r S) (a, b) (a, b)) hy
Non-dependent recursion principle for localizations: given elements f x y : p
for all x
and y
, such that r S x x'
and r S y y'
implies f x y = f x' y'
,
then f
is defined on the whole Localization S
.
Equations
- One or more equations did not get rendered due to their size.
Scalar multiplication in a monoid localization is defined as c • ⟨a, b⟩ = ⟨c • a, b⟩
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Localization.instSMulLocalization = { smul := Localization.smul }
Equations
- Localization.instMulActionLocalization = MulAction.mk (_ : ∀ (x : Localization S), 1 • x = x) (_ : ∀ (s₁ s₂ : R) (x : Localization S), (s₁ * s₂) • x = s₁ • s₂ • x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x y : M), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) = (_ : ∀ (x y : M), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y)
Makes a localization map from an AddCommMonoid
hom satisfying the characteristic predicate.
Equations
- One or more equations did not get rendered due to their size.
Makes a localization map from a CommMonoid
hom satisfying the characteristic predicate.
Equations
- One or more equations did not get rendered due to their size.
Short for toAddMonoidHom
; used to apply a localization map as a function.
Equations
- AddSubmonoid.LocalizationMap.toMap f = f.toAddMonoidHom
Short for toMonoidHom
; used to apply a localization map as a function.
Equations
- Submonoid.LocalizationMap.toMap f = f.toMonoidHom
Given a localization map f : M →+ N→+ N
, a section function sending z : N
to some (x, y) : M × S× S
such that f x - f y = z
.
Equations
- AddSubmonoid.LocalizationMap.sec f z = Classical.choose (_ : ∃ x, z + ↑(AddSubmonoid.LocalizationMap.toMap f) ↑x.snd = ↑(AddSubmonoid.LocalizationMap.toMap f) x.fst)
Given a localization map f : M →* N→* N
, a section function sending z : N
to some
(x, y) : M × S× S
such that f x * (f y)⁻¹ = z⁻¹ = z
.
Equations
- Submonoid.LocalizationMap.sec f z = Classical.choose (_ : ∃ x, z * ↑(Submonoid.LocalizationMap.toMap f) ↑x.snd = ↑(Submonoid.LocalizationMap.toMap f) x.fst)
Given an AddMonoidHom f : M →+ N→+ N
and Submonoid S ⊆ M⊆ M
such that
f(S) ⊆ AddUnits N⊆ AddUnits N
, for all w, z : N
and y ∈ S∈ S
, we have w - f y = z ↔ w = f y + z↔ w = f y + z
.
Given a MonoidHom f : M →* N→* N
and Submonoid S ⊆ M⊆ M
such that f(S) ⊆ Nˣ⊆ Nˣ
, for all
w, z : N
and y ∈ S∈ S
, we have w * (f y)⁻¹ = z ↔ w = f y * z⁻¹ = z ↔ w = f y * z↔ w = f y * z
.
Given an AddMonoidHom f : M →+ N→+ N
and Submonoid S ⊆ M⊆ M
such that
f(S) ⊆ AddUnits N⊆ AddUnits N
, for all w, z : N
and y ∈ S∈ S
, we have z = w - f y ↔ z + f y = w↔ z + f y = w
.
Given a MonoidHom f : M →* N→* N
and Submonoid S ⊆ M⊆ M
such that f(S) ⊆ Nˣ⊆ Nˣ
, for all
w, z : N
and y ∈ S∈ S
, we have z = w * (f y)⁻¹ ↔ z * f y = w⁻¹ ↔ z * f y = w↔ z * f y = w
.
Given an AddMonoidHom f : M →+ N→+ N
and Submonoid S ⊆ M⊆ M
such that
f(S) ⊆ AddUnits N⊆ AddUnits N
, for all x₁ x₂ : M
and y₁, y₂ ∈ S∈ S
, we have
f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁)↔ f (x₁ + y₂) = f (x₂ + y₁)
.
Given a MonoidHom f : M →* N→* N
and Submonoid S ⊆ M⊆ M
such that
f(S) ⊆ Nˣ⊆ Nˣ
, for all x₁ x₂ : M
and y₁, y₂ ∈ S∈ S
, we have
f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁)↔ f (x₁ * y₂) = f (x₂ * y₁)
.
Given an AddMonoidHom f : M →+ N→+ N
and Submonoid S ⊆ M⊆ M
such that
f(S) ⊆ AddUnits N⊆ AddUnits N
, for all y, z ∈ S∈ S
, we have - (f y) = - (f z) → f y = f z→ f y = f z
.
Given a MonoidHom f : M →* N→* N
and Submonoid S ⊆ M⊆ M
such that f(S) ⊆ Nˣ⊆ Nˣ
, for all
y, z ∈ S∈ S
, we have (f y)⁻¹ = (f z)⁻¹ → f y = f z⁻¹ = (f z)⁻¹ → f y = f z⁻¹ → f y = f z→ f y = f z
.
Given an AddMonoidHom f : M →+ N→+ N
and Submonoid S ⊆ M⊆ M
such that
f(S) ⊆ AddUnits N⊆ AddUnits N
, for all y ∈ S∈ S
, - (f y)
is unique.
Given a MonoidHom f : M →* N→* N
and Submonoid S ⊆ M⊆ M
such that f(S) ⊆ Nˣ⊆ Nˣ
, for all
y ∈ S∈ S
, (f y)⁻¹⁻¹
is unique.
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
Given a localization map f : M →+ N→+ N
, the surjection sending (x, y) : M × S× S
to f x - f y
.
Equations
- One or more equations did not get rendered due to their size.
Given a localization map f : M →* N→* N
, the surjection sending (x, y) : M × S× S
to
f x * (f y)⁻¹⁻¹
.
Equations
- One or more equations did not get rendered due to their size.
Given a localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
, for all z : N
we have that if x : M, y ∈ S∈ S
are such that z + f y = f x
, then f x - f y = z
.
Given a localization map f : M →* N→* N
for a submonoid S ⊆ M⊆ M
, for all z : N
we have that if
x : M, y ∈ S∈ S
are such that z * f y = f x
, then f x * (f y)⁻¹ = z⁻¹ = z
.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
, for all x₁ : M
and y₁ ∈ S∈ S
, if x₂ : M, y₂ ∈ S∈ S
are such that (f x₁ - f y₁) + f y₂ = f x₂
, then there exists
c ∈ S∈ S
such that x₁ + y₂ + c = x₂ + y₁ + c
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
, for all x₁ : M
and y₁ ∈ S∈ S
,
if x₂ : M, y₂ ∈ S∈ S
are such that f x₁ * (f y₁)⁻¹ * f y₂ = f x₂⁻¹ * f y₂ = f x₂
, then there exists c ∈ S∈ S
such that x₁ * y₂ * c = x₂ * y₁ * c
.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
and a map of
AddCommMonoid
s g : M →+ P→+ P
such that g(S) ⊆ AddUnits P⊆ AddUnits P
, f x = f y → g x = g y→ g x = g y
for all x y : M
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
and a map of CommMonoid
s
g : M →* P→* P
such that g(S) ⊆ Units P⊆ Units P
, f x = f y → g x = g y→ g x = g y
for all x y : M
.
Given AddCommMonoid
s M, P
, Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q
for Submonoids
S, T
respectively, and g : M →+ P→+ P
such that g(S) ⊆ T⊆ T
, f x = f y
implies k (g x) = k (g y)
.
Given CommMonoid
s M, P
, Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q
for Submonoids
S, T
respectively, and g : M →* P→* P
such that g(S) ⊆ T⊆ T
, f x = f y
implies
k (g x) = k (g y)
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
Given a localization map f : M →+ N→+ N
for a submonoid S ⊆ M⊆ M
and a map of
AddCommMonoid
s g : M →+ P→+ P
such that g y
is invertible for all y : S
, the homomorphism
induced from N
to P
sending z : N
to g x - g y
, where (x, y) : M × S× S
are such that
z = f x - f y
.
Equations
- One or more equations did not get rendered due to their size.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
and a map of CommMonoid
s
g : M →* P→* P
such that g y
is invertible for all y : S
, the homomorphism induced from
N
to P
sending z : N
to g x * (g y)⁻¹⁻¹
, where (x, y) : M × S× S
are such that
z = f x * (f y)⁻¹⁻¹
.
Equations
- One or more equations did not get rendered due to their size.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
and a map of
AddCommMonoid
s g : M →+ P→+ P
such that g y
is invertible for all y : S
, the homomorphism
induced from N
to P
maps f x - f y
to g x - g y
for all x : M, y ∈ S∈ S
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
and a map of CommMonoid
s
g : M →* P→* P
such that g y
is invertible for all y : S
, the homomorphism induced from
N
to P
maps f x * (f y)⁻¹⁻¹
to g x * (g y)⁻¹⁻¹
for all x : M, y ∈ S∈ S
.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
, if an
AddCommMonoid
map g : M →+ P→+ P
induces a map f.lift hg : N →+ P→+ P
then for all
z : N, v : P
, we have f.lift hg z = v ↔ g x = g y + v↔ g x = g y + v
, where x : M, y ∈ S∈ S
are such that
z + f y = f x
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
, if a CommMonoid
map
g : M →* P→* P
induces a map f.lift hg : N →* P→* P
then for all z : N, v : P
, we have
f.lift hg z = v ↔ g x = g y * v↔ g x = g y * v
, where x : M, y ∈ S∈ S
are such that z * f y = f x
.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
, if an AddCommMonoid
map
g : M →+ P→+ P
induces a map f.lift hg : N →+ P→+ P
then for all
z : N, v w : P
, we have f.lift hg z + w = v ↔ g x + w = g y + v↔ g x + w = g y + v
, where x : M, y ∈ S∈ S
are such
that z + f y = f x
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
, if a CommMonoid
map
g : M →* P→* P
induces a map f.lift hg : N →* P→* P
then for all z : N, v w : P
, we have
f.lift hg z * w = v ↔ g x * w = g y * v↔ g x * w = g y * v
, where x : M, y ∈ S∈ S
are such that
z * f y = f x
.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
, if an AddCommMonoid
map g : M →+ P→+ P
induces a map f.lift hg : N →+ P→+ P
then for all z : N
, we have
f.lift hg z + g y = g x
, where x : M, y ∈ S∈ S
are such that z + f y = f x
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
, if a CommMonoid
map
g : M →* P→* P
induces a map f.lift hg : N →* P→* P
then for all z : N
, we have
f.lift hg z * g y = g x
, where x : M, y ∈ S∈ S
are such that z * f y = f x
.
Given a Localization map f : M →+ N→+ N
for a Submonoid S ⊆ M⊆ M
, if an AddCommMonoid
map
g : M →+ P→+ P
induces a map f.lift hg : N →+ P→+ P
then for all z : N
, we have
g y + f.lift hg z = g x
, where x : M, y ∈ S∈ S
are such that z + f y = f x
.
Given a Localization map f : M →* N→* N
for a Submonoid S ⊆ M⊆ M
, if a CommMonoid
map
g : M →* P→* P
induces a map f.lift hg : N →* P→* P
then for all z : N
, we have
g y * f.lift hg z = g x
, where x : M, y ∈ S∈ S
are such that z * f y = f x
.
Given two Localization maps f : M →+ N, k : M →+ P→+ N, k : M →+ P→+ P
for a Submonoid S ⊆ M⊆ M
, the hom
from P
to N
induced by f
is left inverse to the hom from N
to P
induced by k
.
Given two Localization maps f : M →* N, k : M →* P→* N, k : M →* P→* P
for a Submonoid S ⊆ M⊆ M
, the hom
from P
to N
induced by f
is left inverse to the hom from N
to P
induced by k
.
Given a AddCommMonoid
homomorphism g : M →+ P→+ P
where for Submonoids S ⊆ M, T ⊆ P⊆ M, T ⊆ P⊆ P
we have
g(S) ⊆ T⊆ T
, the induced AddMonoid homomorphism from the Localization of M
at S
to the
Localization of P
at T
: if f : M →+ N→+ N
and k : P →+ Q→+ Q
are Localization maps for S
and
T
respectively, we send z : N
to k (g x) - k (g y)
, where (x, y) : M × S× S
are such
that z = f x - f y
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : IsAddUnit (↑(AddSubmonoid.LocalizationMap.toMap k) ↑{ val := ↑g ↑y, property := hy y })) = (_ : IsAddUnit (↑(AddSubmonoid.LocalizationMap.toMap k) ↑{ val := ↑g ↑y, property := hy y }))
Given a CommMonoid
homomorphism g : M →* P→* P
where for Submonoids S ⊆ M, T ⊆ P⊆ M, T ⊆ P⊆ P
we have
g(S) ⊆ T⊆ T
, the induced Monoid homomorphism from the Localization of M
at S
to the
Localization of P
at T
: if f : M →* N→* N
and k : P →* Q→* Q
are Localization maps for S
and
T
respectively, we send z : N
to k (g x) * (k (g y))⁻¹⁻¹
, where (x, y) : M × S× S
are such
that z = f x * (f y)⁻¹⁻¹
.
Equations
- Submonoid.LocalizationMap.map f hy k = Submonoid.LocalizationMap.lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(Submonoid.LocalizationMap.toMap k) ↑{ val := ↑g ↑y, property := hy y }))
Given Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q
for Submonoids S, T
respectively, if an
AddCommMonoid
homomorphism g : M →+ P→+ P
induces a f.map hy k : N →+ Q→+ Q
, then for all z : N
,
u : Q
, we have f.map hy k z = u ↔ k (g x) = k (g y) + u↔ k (g x) = k (g y) + u
where x : M, y ∈ S∈ S
are such that
z + f y = f x
.
Given Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q
for Submonoids S, T
respectively, if a
CommMonoid
homomorphism g : M →* P→* P
induces a f.map hy k : N →* Q→* Q
, then for all z : N
,
u : Q
, we have f.map hy k z = u ↔ k (g x) = k (g y) * u↔ k (g x) = k (g y) * u
where x : M, y ∈ S∈ S
are such that
z * f y = f x
.
Given Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q
for Submonoids S, T
respectively, if an
AddCommMonoid
homomorphism g : M →+ P→+ P
induces a f.map hy k : N →+ Q→+ Q
, then for all z : N
,
we have f.map hy k z + k (g y) = k (g x)
where x : M, y ∈ S∈ S
are such that
z + f y = f x
.
Given Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q
for Submonoids S, T
respectively, if a
CommMonoid
homomorphism g : M →* P→* P
induces a f.map hy k : N →* Q→* Q
, then for all z : N
,
we have f.map hy k z * k (g y) = k (g x)
where x : M, y ∈ S∈ S
are such that
z * f y = f x
.
Given Localization maps f : M →+ N, k : P →+ Q→+ N, k : P →+ Q→+ Q
for Submonoids S, T
respectively if an
AddCommMonoid
homomorphism g : M →+ P→+ P
induces a f.map hy k : N →+ Q→+ Q
, then for all z : N
,
we have k (g y) + f.map hy k z = k (g x)
where x : M, y ∈ S∈ S
are such that
z + f y = f x
.
Given Localization maps f : M →* N, k : P →* Q→* N, k : P →* Q→* Q
for Submonoids S, T
respectively, if a
CommMonoid
homomorphism g : M →* P→* P
induces a f.map hy k : N →* Q→* Q
, then for all z : N
,
we have k (g y) * f.map hy k z = k (g x)
where x : M, y ∈ S∈ S
are such that
z * f y = f x
.
If AddCommMonoid
homs g : M →+ P, l : P →+ A→+ P, l : P →+ A→+ A
induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g∘ g
.
If CommMonoid
homs g : M →* P, l : P →* A→* P, l : P →* A→* A
induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g∘ g
.
If AddCommMonoid
homs g : M →+ P, l : P →+ A→+ P, l : P →+ A→+ A
induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g∘ g
.
If CommMonoid
homs g : M →* P, l : P →* A→* P, l : P →* A→* A
induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g∘ g
.
Given x : M
, the type of AddCommMonoid
homomorphisms f : M →+ N→+ N
such that N
is isomorphic to the localization of M
at the Submonoid generated by x
.