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 yis a unit; - For all
z : N, there exists(x, y) : M × Ssuch thatz * f y = f x; - For all
x, y : M,f x = f yiff there existsc ∈ Ssuch thatx * c = y * c.
Given such a localization map f : M →* N, we can define the surjection
localization_map.mk' sending (x, y) : M × S to f x * (f y)⁻¹, and
localization_map.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,
localization_map.map, from N to Q.
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.
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.to_map, as coercions don't work well for
this structure.
To reason about the localization as a quotient type, use mk_eq_monoid_of_mk' and associated
lemmas. These show the quotient map mk : M → S → localization S equals the
surjection localization_map.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_monoid_of_mk' hence gives you access to the results in the rest of the file, which are
about the localization_map.mk' induced by any localization map.
Tags
localization, monoid localization, quotient monoid, congruence relation, characteristic predicate, commutative monoid
The add_monoid hom underlying a localization_map of add_comm_monoids.
- to_fun : M → N
- map_zero' : c.to_fun 0 = 0
- map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_add_units' : ∀ (y : ↥S), is_add_unit (c.to_fun ↑y)
- surj' : ∀ (z : N), ∃ (x : M × ↥S), z + c.to_fun ↑(x.snd) = c.to_fun x.fst
- eq_iff_exists' : ∀ (x y : M), c.to_fun x = c.to_fun y ↔ ∃ (c : ↥S), x + ↑c = y + ↑c
The type of add_monoid homomorphisms satisfying the characteristic predicate: if f : M →+ N
satisfies this predicate, then N is isomorphic to the localization of M at S.
- to_fun : M → N
- map_one' : c.to_fun 1 = 1
- map_mul' : ∀ (x y : M), c.to_fun (x * y) = c.to_fun x * c.to_fun y
- map_units' : ∀ (y : ↥S), is_unit (c.to_fun ↑y)
- surj' : ∀ (z : N), ∃ (x : M × ↥S), z * c.to_fun ↑(x.snd) = c.to_fun x.fst
- eq_iff_exists' : ∀ (x y : M), c.to_fun x = c.to_fun y ↔ ∃ (c : ↥S), x * ↑c = y * ↑c
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.
The monoid hom underlying a localization_map.
The congruence relation on M × S, M a comm_monoid and S a submonoid of M, whose
quotient is the localization of M at S, defined as the unique congruence relation on
M × S such that for any other congruence relation s on M × S where for all y ∈ S,
(1, 1) ∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂) by r implies
(x₁, y₁) ∼ (x₂, y₂) by s.
Equations
- localization.r S = has_Inf.Inf {c : con (M × ↥S) | ∀ (y : ↥S), ⇑c 1 (↑y, y)}
The congruence relation on M × S, M an add_comm_monoid 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.
An alternate form of the congruence relation on M × S, M a comm_monoid and S a
submonoid of M, whose quotient is the localization of M at S.
An alternate form of the congruence relation on M × S, M a comm_monoid and
S a submonoid of M, whose quotient is the localization of M at S.
The additive congruence relation used to localize an add_comm_monoid at a
submonoid can be expressed equivalently as an infimum (see add_localization.r) or
explicitly (see add_localization.r').
The congruence relation used to localize a comm_monoid at a submonoid can be expressed
equivalently as an infimum (see localization.r) or explicitly
(see localization.r').
The localization of an add_comm_monoid at one
of its submonoids (as a quotient type).
The localization of a comm_monoid at one of its submonoids (as a quotient type).
Equations
- localization S = (localization.r S).quotient
Equations
Equations
Given a comm_monoid M and submonoid S, mk sends x : M, y ∈ S to the equivalence
class of (x, y) in the localization of M at S.
Equations
- localization.mk x y = ⇑((localization.r S).mk') (x, y)
Given an add_comm_monoid M and submonoid S, mk sends x : M, y ∈ S to
the equivalence class of (x, y) in the localization of M at S.
Makes a localization map from an add_comm_monoid hom satisfying the characteristic
predicate.
Makes a localization map from a comm_monoid hom satisfying the characteristic predicate.
Equations
- f.to_localization_map H1 H2 H3 = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_units' := H1, surj' := H2, eq_iff_exists' := H3}
Short for to_add_monoid_hom; used to apply a localization map as a function.
Short for to_monoid_hom; used to apply a localization map as a function.
Given a localization map f : M →* N, a section function sending z : N to some
(x, y) : M × S such that f x * (f y)⁻¹ = z.
Equations
- f.sec z = classical.some _
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.
Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ units N, for all
w : M, z : N and y ∈ S, we have w * (f y)⁻¹ = z ↔ w = f y * z.
Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that
f(S) ⊆ add_units N, for all w : M, z : N and y ∈ S, we have w - f y = z ↔ w = f y + z.
Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that
f(S) ⊆ add_units N, for all w : M, z : N and y ∈ S, we have z = w - f y ↔ z + f y = w.
Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ units N, for all
w : M, z : N and y ∈ S, we have z = w * (f y)⁻¹ ↔ z * f y = w.
Given a monoid hom f : M →* N and submonoid S ⊆ M such that
f(S) ⊆ units 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 add_monoid hom f : M →+ N and submonoid S ⊆ M such that
f(S) ⊆ add_units 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 monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ units N, for all
y, z ∈ S, we have (f y)⁻¹ = (f z)⁻¹ → f y = f z.
Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that
f(S) ⊆ add_units N, for all y, z ∈ S, we have - (f y) = - (f z) → f y = f z.
Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that
f(S) ⊆ add_units N, for all y ∈ S, - (f y) is unique.
Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ units 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)⁻¹.
Given a localization map f : M →+ N, the surjection sending (x, y) : M × S
to f x - f y.
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 comm_monoids
g : M →* P such that g(S) ⊆ units 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 add_comm_monoids g : M →+ P such that g(S) ⊆ add_units P, f x = f y → g x = g y
for all x y : M.
Given add_comm_monoids 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 comm_monoids 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 add_comm_monoids 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.
Given a localization map f : M →* N for a submonoid S ⊆ M and a map of comm_monoids
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)⁻¹.
Given a localization map f : M →+ N for a submonoid S ⊆ M and a map
of add_comm_monoids 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 comm_monoids
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 a comm_monoid 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 add_comm_monoid 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 comm_monoid 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 add_comm_monoid 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 comm_monoid 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 add_comm_monoid 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 comm_monoid 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
an add_comm_monoid 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 a add_comm_monoid homomorphism g : M →+ P where for submonoids
S ⊆ M, T ⊆ P we have g(S) ⊆ T, the induced add_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.
Given a comm_monoid 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)⁻¹.
Given localization maps f : M →* N, k : P →* Q for submonoids S, T respectively, if a
comm_monoid 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 add_comm_monoid 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 add_comm_monoid 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
comm_monoid 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 add_comm_monoid 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
comm_monoid 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 comm_monoid 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 add_comm_monoid 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 add_comm_monoid 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 comm_monoid 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 f : M →* N and k : M →* P are localization maps for a submonoid S, we get an
isomorphism of N and P.
If f : M →+ N and k : M →+ R are localization maps for a submonoid S,
we get an isomorphism of N and R.
If f : M →* N is a localization map for a submonoid S and k : N ≃* P is an isomorphism
of comm_monoids, k ∘ f is a localization map for M at S.
Equations
- f.of_mul_equiv_of_localizations k = (k.to_monoid_hom.comp f.to_map).to_localization_map _ _ _
If f : M →+ N is a localization map for a submonoid S and k : N ≃+ P is an
isomorphism of add_comm_monoids, k ∘ f is a localization map for M at S.
Given comm_monoids 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 comm_monoids such that k(T) = S, f ∘ k
is a localization map for T.
Equations
- f.of_mul_equiv_of_dom H = let H' : submonoid.comap k.to_monoid_hom S = T := _ in (f.to_map.comp k.to_monoid_hom).to_localization_map _ _ _
Given comm_monoids 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 comm_monoids such that
k(T) = S, f ∘ k is a localization map for T.
A special case of f ∘ id = f, f a localization map.
A special case of f ∘ id = f, f a localization map.
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.
Given localization maps f : M →* N, k : P →* U for submonoids S, T respectively, an
isomorphism j : M ≃* P such that j(S) = T induces an isomorphism of localizations
N ≃* U.
Equations
- f.mul_equiv_of_mul_equiv k H = f.mul_equiv_of_localizations (k.of_mul_equiv_of_dom H)
Natural homomorphism sending x : M, M an add_comm_monoid, to the equivalence
class of (x, 0) in the localization of M at a submonoid.
Natural hom sending x : M, M a comm_monoid, to the equivalence class of
(x, 1) in the localization of M at a submonoid.
Equations
- localization.monoid_of S = {to_fun := ((localization.r S).mk'.comp (monoid_hom.inl M ↥S)).to_fun, map_one' := _, map_mul' := _, map_units' := _, surj' := _, eq_iff_exists' := _}
Given a localization map f : M →* N for a submonoid S, we get an isomorphism between
the localization of M at S as a quotient type and N.
Equations
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.