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
such thatf x = f y
, there existsc ∈ S
such thatx * c = y * c
. (The converse is a consequence of 1.)
Given such a localization map f : M →* N
, we can define the surjection
Submonoid.LocalizationMap.mk'
sending (x, y) : M × S
to f x * (f y)⁻¹
, and
Submonoid.LocalizationMap.lift
, the homomorphism from N
induced by a homomorphism from M
which
maps elements of S
to invertible elements of the codomain. Similarly, given commutative monoids
P, Q
, a submonoid T
of P
and a localization map for T
from P
to Q
, then a homomorphism
g : M →* P
such that g(S) ⊆ T
induces a homomorphism of localizations, LocalizationMap.map
,
from N
to Q
. We treat the special case of localizing away from an element in the sections
AwayMap
and Away
.
We also define the quotient of M × S
by the unique congruence relation (equivalence relation
preserving a binary operation) r
such that for any other congruence relation s
on M × S
satisfying '∀ y ∈ S
, (1, 1) ∼ (y, y)
under s
', we have that (x₁, y₁) ∼ (x₂, y₂)
by s
whenever (x₁, y₁) ∼ (x₂, y₂)
by r
. We show this relation is equivalent to the standard
localization relation.
This defines the localization as a quotient type, Localization
, but the majority of
subsequent lemmas in the file are given in terms of localizations up to isomorphism, using maps
which satisfy the characteristic predicate.
The Grothendieck group construction corresponds to localizing at the top submonoid, namely making every element invertible.
Implementation notes #
In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally rewrite
one
structure with an isomorphic one; one way around this is to isolate a predicate characterizing
a structure up to isomorphism, and reason about things that satisfy the predicate.
The infimum form of the localization congruence relation is chosen as 'canonical' here, since it shortens some proofs.
To apply a localization map f
as a function, we use f.toMap
, as coercions don't work well for
this structure.
To reason about the localization as a quotient type, use mk_eq_monoidOf_mk'
and associated
lemmas. These show the quotient map mk : M → S → Localization S
equals the
surjection LocalizationMap.mk'
induced by the map
Localization.monoidOf : Submonoid.LocalizationMap S (Localization S)
(where of
establishes the
localization as a quotient type satisfies the characteristic predicate). The lemma
mk_eq_monoidOf_mk'
hence gives you access to the results in the rest of the file, which are about
the LocalizationMap.mk'
induced by any localization map.
TODO #
- Show that the localization at the top monoid is a group.
- Generalise to (nonempty) subsemigroups.
- If we acquire more bundlings, we can make
Localization.mkOrderEmbedding
be an ordered monoid embedding.
Tags #
localization, monoid localization, quotient monoid, congruence relation, characteristic predicate, commutative monoid, grothendieck group
The type of AddMonoid homomorphisms satisfying the characteristic predicate: if f : M →+ N
satisfies this predicate, then N
is isomorphic to the localization of M
at S
.
- toFun : M → N
- map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
- map_add_units' : ∀ (y : ↥S), IsAddUnit ((↑self.toAddMonoidHom).toFun ↑y)
Instances For
The type of monoid homomorphisms satisfying the characteristic predicate: if f : M →* N
satisfies this predicate, then N
is isomorphic to the localization of M
at S
.
- toFun : M → N
- map_one' : (↑self.toMonoidHom).toFun 1 = 1
- map_units' : ∀ (y : ↥S), IsUnit ((↑self.toMonoidHom).toFun ↑y)
Instances For
The congruence relation on M × S
, M
an AddCommMonoid
and S
an AddSubmonoid
of M
,
whose quotient is the localization of M
at S
, defined as the unique congruence relation on
M × S
such that for any other congruence relation s
on M × S
where for all y ∈ S
,
(0, 0) ∼ (y, y)
under s
, we have that (x₁, y₁) ∼ (x₂, y₂)
by r
implies
(x₁, y₁) ∼ (x₂, y₂)
by s
.
Equations
- AddLocalization.r S = sInf {c : AddCon (M × ↥S) | ∀ (y : ↥S), c 0 (↑y, y)}
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
.
Equations
- Localization.r S = sInf {c : Con (M × ↥S) | ∀ (y : ↥S), c 1 (↑y, y)}
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
.
Equations
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
.
Equations
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'
).
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
Instances For
The localization of a CommMonoid
at one of its submonoids (as a quotient type).
Equations
- Localization S = OreLocalization S M
Instances For
Given an AddCommMonoid
M
and submonoid S
, mk
sends x : M
, y ∈ S
to
the equivalence class of (x, y)
in the localization of M
at S
.
Equations
- AddLocalization.mk x y = x -ₒ y
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
.
Equations
- Localization.mk x y = x /ₒ y
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
.
Equations
- AddLocalization.rec f H x = Quot.rec (fun (y : M × ↥S) => ⋯ ▸ f y.1 y.2) ⋯ x
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
.
Equations
- Localization.rec f H x = Quot.rec (fun (y : M × ↥S) => ⋯ ▸ f y.1 y.2) ⋯ x
Instances For
Copy of Quotient.recOnSubsingleton₂
for AddLocalization
Equations
- One or more equations did not get rendered due to their size.
Instances For
Copy of Quotient.recOnSubsingleton₂
for Localization
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- x.liftOn f H = AddLocalization.rec f ⋯ x
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
.
Equations
- x.liftOn f H = Localization.rec f ⋯ x
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
.
Equations
- x.liftOn₂ y f H = x.liftOn (fun (a : M) (b : ↥S) => y.liftOn (f a b) ⋯) ⋯
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
.
Equations
- x.liftOn₂ y f H = x.liftOn (fun (a : M) (b : ↥S) => y.liftOn (f a b) ⋯) ⋯
Instances For
Equations
- ⋯ = ⋯
Makes a localization map from an AddCommMonoid
hom satisfying the characteristic predicate.
Equations
- f.toLocalizationMap H1 H2 H3 = { toAddMonoidHom := f, map_add_units' := H1, surj' := H2, exists_of_eq := H3 }
Instances For
Makes a localization map from a CommMonoid
hom satisfying the characteristic predicate.
Equations
- f.toLocalizationMap H1 H2 H3 = { toMonoidHom := f, map_units' := H1, surj' := H2, exists_of_eq := H3 }
Instances For
Short for toAddMonoidHom
; used to apply a localization map as a function.
Equations
- f.toMap = f.toAddMonoidHom
Instances For
Short for toMonoidHom
; used to apply a localization map as a function.
Equations
- f.toMap = f.toMonoidHom
Instances For
Given a localization map f : M →+ N
, and z w : N
, there exist z' w' : M
and d : S
such that f z' - f d = z
and f w' - f d = w
.
Given a localization map f : M →* N
, and z w : N
, there exist z' w' : M
and d : S
such that f z' / f d = z
and f w' / f d = w
.
Given a localization map f : M →+ N
, a section function sending z : N
to some (x, y) : M × S
such that f x - f y = z
.
Equations
- f.sec z = Classical.choose ⋯
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
.
Equations
- f.sec z = Classical.choose ⋯
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
.
Equations
- f.mk' x y = f.toMap x + ↑(-(IsAddUnit.liftRight (f.toMap.restrict S) ⋯) y)
Instances For
Given a localization map f : M →* N
, the surjection sending (x, y) : M × S
to
f x * (f y)⁻¹
.
Equations
- f.mk' x y = f.toMap x * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y)⁻¹
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
.
Equations
- f.lift hg = { toFun := fun (z : N) => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) (f.sec z).2), map_zero' := ⋯, map_add' := ⋯ }
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)⁻¹
.
Equations
- f.lift hg = { toFun := fun (z : N) => g (f.sec z).1 * ↑((IsUnit.liftRight (g.restrict S) hg) (f.sec z).2)⁻¹, map_one' := ⋯, map_mul' := ⋯ }
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 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
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
.
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
.
Equations
- f.map hy k = f.lift ⋯
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)⁻¹
.
Equations
- f.map hy k = f.lift ⋯
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 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.
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.
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.
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.
Given x : M
, the type of AddCommMonoid
homomorphisms f : M →+ N
such that N
is isomorphic to the localization of M
at the AddSubmonoid generated by x
.
Equations
- AddSubmonoid.LocalizationMap.AwayMap x N' = (AddSubmonoid.multiples x).LocalizationMap N'
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
.
Equations
- Submonoid.LocalizationMap.AwayMap x N' = (Submonoid.powers x).LocalizationMap N'
Instances For
Given x : M
and a Localization map F : M →* N
away from x
, invSelf
is (F x)⁻¹
.
Equations
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)⁻ⁿ
.
Equations
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
.
Equations
Instances For
Given x : A
and a Localization map F : A →+ B
away from x
, neg_self
is - (F x)
.
Equations
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
.
Equations
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
.
Equations
Instances For
If f : M →+ N
and k : M →+ R
are Localization maps for an AddSubmonoid S
, we get an
isomorphism of N
and R
.
Equations
- f.addEquivOfLocalizations k = { toFun := ⇑(f.lift ⋯), invFun := ⇑(k.lift ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
If f : M →* N
and k : M →* P
are Localization maps for a Submonoid S
, we get an
isomorphism of N
and P
.
Equations
- f.mulEquivOfLocalizations k = { toFun := ⇑(f.lift ⋯), invFun := ⇑(k.lift ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
If f : M →+ N
is a Localization map for a Submonoid S
and k : N ≃+ P
is an isomorphism
of AddCommMonoid
s, k ∘ f
is a Localization map for M
at S
.
Equations
- f.ofAddEquivOfLocalizations k = (k.toAddMonoidHom.comp f.toMap).toLocalizationMap ⋯ ⋯ ⋯
Instances For
If f : M →* N
is a Localization map for a Submonoid S
and k : N ≃* P
is an isomorphism
of CommMonoid
s, k ∘ f
is a Localization map for M
at S
.
Equations
- f.ofMulEquivOfLocalizations k = (k.toMonoidHom.comp f.toMap).toLocalizationMap ⋯ ⋯ ⋯
Instances For
Given AddCommMonoid
s M, P
and AddSubmonoid
s S ⊆ M, T ⊆ P
, if f : M →* N
is a
Localization map for S
and k : P ≃+ M
is an isomorphism of AddCommMonoid
s such that
k(T) = S
, f ∘ k
is a Localization map for T
.
Equations
- f.ofAddEquivOfDom H = (f.toMap.comp k.toAddMonoidHom).toLocalizationMap ⋯ ⋯ ⋯
Instances For
Given CommMonoid
s 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 CommMonoid
s such that k(T) = S
, f ∘ k
is a Localization map for T
.
Equations
- f.ofMulEquivOfDom H = (f.toMap.comp k.toMonoidHom).toLocalizationMap ⋯ ⋯ ⋯
Instances For
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
.
Equations
- f.addEquivOfAddEquiv k H = f.addEquivOfLocalizations (k.ofAddEquivOfDom H)
Instances For
Given Localization maps f : M →* N, k : P →* U
for Submonoids S, T
respectively, an
isomorphism j : M ≃* P
such that j(S) = T
induces an isomorphism of localizations N ≃* U
.
Equations
- f.mulEquivOfMulEquiv k H = f.mulEquivOfLocalizations (k.ofMulEquivOfDom H)
Instances For
Natural homomorphism sending x : M
, M
an AddCommMonoid
, to the equivalence class of
(x, 0)
in the Localization of M
at a Submonoid.
Equations
- AddLocalization.addMonoidOf S = { toFun := fun (x : M) => AddLocalization.mk x 0, map_zero' := ⋯, map_add' := ⋯, map_add_units' := ⋯, surj' := ⋯, exists_of_eq := ⋯ }
Instances For
Natural homomorphism sending x : M
, M
a CommMonoid
, to the equivalence class of
(x, 1)
in the Localization of M
at a Submonoid.
Equations
- Localization.monoidOf S = { toFun := fun (x : M) => Localization.mk x 1, map_one' := ⋯, map_mul' := ⋯, map_units' := ⋯, surj' := ⋯, exists_of_eq := ⋯ }
Instances For
Given a Localization map f : M →+ N
for a Submonoid S
, we get an isomorphism between
the Localization of M
at S
as a quotient type and N
.
Equations
- AddLocalization.addEquivOfQuotient f = (AddLocalization.addMonoidOf S).addEquivOfLocalizations f
Instances For
Given a Localization map f : M →* N
for a Submonoid S
, we get an isomorphism between
the Localization of M
at S
as a quotient type and N
.
Equations
- Localization.mulEquivOfQuotient f = (Localization.monoidOf S).mulEquivOfLocalizations f
Instances For
Given x : M
, the Localization of M
at the Submonoid generated by x
, as a quotient.
Equations
Instances For
Given x : M
, the Localization of M
at the Submonoid generated by x
, as a quotient.
Equations
Instances For
Given x : M
, negSelf
is -x
in the Localization (as a quotient type) of M
at the
Submonoid generated by x
.
Equations
- AddLocalization.Away.negSelf x = AddLocalization.mk 0 ⟨x, ⋯⟩
Instances For
Given x : M
, invSelf
is x⁻¹
in the Localization (as a quotient type) of M
at the
Submonoid generated by x
.
Equations
- Localization.Away.invSelf x = Localization.mk 1 ⟨x, ⋯⟩
Instances For
Given x : M
, the natural hom sending y : M
, M
an AddCommMonoid
, to the equivalence
class of (y, 0)
in the Localization of M
at the Submonoid generated by x
.
Equations
Instances For
Given x : M
, the natural hom sending y : M
, M
a CommMonoid
, to the equivalence class
of (y, 1)
in the Localization of M
at the Submonoid generated by x
.
Equations
Instances For
Given x : M
and a Localization map f : M →+ N
away from x
, we get an isomorphism between
the Localization of M
at the Submonoid generated by x
as a quotient type and N
.
Instances For
Given x : M
and a Localization map f : M →* N
away from x
, we get an isomorphism between
the Localization of M
at the Submonoid generated by x
as a quotient type and N
.
Equations
Instances For
Equations
- a.decidableEq b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 + x = ↑x_2 + x_1) ⋯
Equations
- a.decidableEq b = a.recOnSubsingleton₂ b fun (x x_1 : α) (x_2 x_3 : ↥s) => decidable_of_iff' (↑x_3 * x = ↑x_2 * x_1) ⋯
The morphism numeratorHom
is a monoid localization map in the case of commutative R
.
Equations
Instances For
If R
is commutative, Ore localization and monoid localization are isomorphic.