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 treat the special case of localizing away from an element in the sections away_map 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.
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
- to_add_monoid_hom : M →+ N
- map_add_units' : ∀ (y : ↥S), is_add_unit (self.to_add_monoid_hom.to_fun ↑y)
- surj' : ∀ (z : N), ∃ (x : M × ↥S), z + self.to_add_monoid_hom.to_fun ↑(x.snd) = self.to_add_monoid_hom.to_fun x.fst
- eq_iff_exists' : ∀ (x y : M), self.to_add_monoid_hom.to_fun x = self.to_add_monoid_hom.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_monoid_hom : M →* N
- map_units' : ∀ (y : ↥S), is_unit (self.to_monoid_hom.to_fun ↑y)
- surj' : ∀ (z : N), ∃ (x : M × ↥S), z * self.to_monoid_hom.to_fun ↑(x.snd) = self.to_monoid_hom.to_fun x.fst
- eq_iff_exists' : ∀ (x y : M), self.to_monoid_hom.to_fun x = self.to_monoid_hom.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 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.
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.
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 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 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 localization of a comm_monoid at one of its submonoids (as a quotient type).
Equations
- localization S = (localization.r S).quotient
The localization of an add_comm_monoid at one
of its submonoids (as a quotient type).
Equations
Equations
Equations
Multiplication in a localization is defined as ⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c, b * d⟩.
Equations
Addition in an add_localization 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
Equations
- localization.has_mul S = {mul := localization.mul S}
Equations
The identity element of a localization is defined as ⟨1, 1⟩.
Equations
The identity element of an add_localization is defined as ⟨0, 0⟩.
Should not be confused with the ring localization counterpart localization.zero,
which is defined as ⟨0, 1⟩.
Equations
Equations
Equations
- localization.has_one S = {one := localization.one S}
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
Multiplication with a natural in an add_localization 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
Equations
- add_localization.add_comm_monoid S = {add := has_add.add (add_localization.has_add S), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_localization.nsmul S, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- localization.comm_monoid S = {mul := has_mul.mul (localization.has_mul S), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := localization.npow S, npow_zero' := _, npow_succ' := _, mul_comm := _}
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.
Equations
- add_localization.mk x y = ⇑((add_localization.r S).mk') (x, y)
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 (wih the correct coercions),
then f is defined on the whole localization S.
Dependent recursion principle for add_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 (wih the correct coercions),
then f is defined on the whole add_localization S.
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
- x.lift_on f H = add_localization.rec f _ x
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.lift_on f H = localization.rec f _ x
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.
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.
Scalar multiplication in a monoid localization is defined as c • ⟨a, b⟩ = ⟨c • a, b⟩.
Equations
- localization.smul c z = z.lift_on (λ (a : M) (b : ↥S), localization.mk (c • a) b) _
Equations
- localization.has_scalar = {smul := localization.smul _inst_5}
Equations
- localization.mul_action = {to_has_scalar := localization.has_scalar _inst_6, one_smul := _, mul_smul := _}
Equations
- localization.mul_distrib_mul_action = {to_mul_action := localization.mul_action _inst_6, smul_mul := _, smul_one := _}
Makes a localization map from an add_comm_monoid hom satisfying the characteristic
predicate.
Equations
- f.to_localization_map H1 H2 H3 = {to_add_monoid_hom := {to_fun := f.to_fun, map_zero' := _, map_add' := _}, map_add_units' := H1, surj' := H2, eq_iff_exists' := H3}
Makes a localization map from a comm_monoid hom satisfying the characteristic predicate.
Equations
- f.to_localization_map H1 H2 H3 = {to_monoid_hom := {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.
Equations
- f.sec z = classical.some _
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 a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all
w : M, z : N and y ∈ S, we have w * (f y)⁻¹ = z ↔ w = f y * z.
Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all
w : M, z : N and y ∈ S, we have z = w * (f y)⁻¹ ↔ z * f y = w.
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 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) ⊆ 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 y, z ∈ S, we have - (f y) = - (f z) → f y = f z.
Given a monoid hom 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 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) ⊆ 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 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 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 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 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 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 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, 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
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 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 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 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 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 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 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 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 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.
Given x : M, the type of comm_monoid homomorphisms f : M →* N such that N
is isomorphic to the localization of M at the submonoid generated by x.
Equations
Given x : M, the type of add_comm_monoid homomorphisms f : M →+ N
such that N is isomorphic to the localization of M at the submonoid generated by x.
Equations
Given x : M and a localization map F : M →* N away from x, inv_self is (F x)⁻¹.
Equations
Given x : M, a localization map F : M →* N away from x, and a map of comm_monoids
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
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
Given x : A and a localization map F : A →+ B away from x, neg_self is - (F x).
Equations
Given x : A, a localization map F : A →+ B away from x, and a map of add_comm_monoids
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
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
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 and k : M →* P are localization maps for a submonoid S, we get an
isomorphism of N and P.
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.
Equations
- f.of_add_equiv_of_localizations k = (k.to_add_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 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 _ _ _
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_add_equiv_of_dom H = let H' : add_submonoid.comap k.to_add_monoid_hom S = T := _ in (f.to_map.comp k.to_add_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.
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 _ _ _
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.mul_equiv_of_mul_equiv k H = f.mul_equiv_of_localizations (k.of_mul_equiv_of_dom H)
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.add_equiv_of_add_equiv k H = f.add_equiv_of_localizations (k.of_add_equiv_of_dom H)
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_monoid_hom := {to_fun := λ (x : M), localization.mk x 1, map_one' := _, map_mul' := _}, map_units' := _, surj' := _, eq_iff_exists' := _}
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.
Equations
- add_localization.add_monoid_of S = {to_add_monoid_hom := {to_fun := λ (x : M), add_localization.mk x 0, map_zero' := _, map_add' := _}, map_add_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.
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 x : M, the localization of M at the submonoid generated
by x, as a quotient.
Equations
Given x : M, the localization of M at the submonoid generated by x, as a quotient.
Equations
Given x : M, inv_self is x⁻¹ in the localization (as a quotient type) of M at the
submonoid generated by x.
Equations
- localization.away.inv_self x = localization.mk 1 ⟨x, _⟩
Given x : M, neg_self is -x in the localization (as a quotient type) of M
at the submonoid generated by x.
Equations
Given x : M, the natural hom sending y : M, M a comm_monoid, to the equivalence class
of (y, 1) in the localization of M at the submonoid generated by x.
Equations
Given x : M, the natural hom sending y : M, M an add_comm_monoid,
to the equivalence class of (y, 0) in the localization of M at the submonoid
generated by x.
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.
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.