Module docstring
{"# Localizations of commutative monoids with zeroes
"}
Submonoid.LocalizationMap.toMap_injective_iff
theorem
{M N : Type*} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : LocalizationMap S N) :
Injective (LocalizationMap.toMap f) ↔ ∀ ⦃x⦄, x ∈ S → IsLeftRegular x
Full source
@[to_additive]
theorem toMap_injective_iff
{M N : Type*} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : LocalizationMap S N) :
InjectiveInjective (LocalizationMap.toMap f) ↔ ∀ ⦃x⦄, x ∈ S → IsLeftRegular x := by
rw [Injective]
constructor <;> intro h
· intro x hx y z hyz
simp_rw [LocalizationMap.eq_iff_exists] at h
apply (fun y z _ => h) y z x
lift x to S using hx
use x
· intro a b hab
rw [LocalizationMap.eq_iff_exists] at hab
obtain ⟨c,hc⟩ := hab
apply (fun x a => h a) c (SetLike.coe_mem c) hcInformal description
Let $M$ and $N$ be commutative monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Then the homomorphism $f$ is injective if and only if every element of $S$ is left regular (i.e., left cancellative).
Submonoid.LocalizationMap.subsingleton
theorem
(f : Submonoid.LocalizationMap S N) (h : 0 ∈ S) : Subsingleton N
Full source
/-- If `S` contains `0` then the localization at `S` is trivial. -/
theorem LocalizationMap.subsingleton (f : Submonoid.LocalizationMap S N) (h : 0 ∈ S) :
Subsingleton N := by
refine ⟨fun a b ↦ ?_⟩
rw [← LocalizationMap.mk'_sec f a, ← LocalizationMap.mk'_sec f b, LocalizationMap.eq]
exact ⟨⟨0, h⟩, by simp only [zero_mul]⟩Informal description
Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. If $0$ belongs to $S$, then the localization $N$ is a subsingleton (i.e., has at most one element).
Submonoid.LocalizationWithZeroMap
structure
extends LocalizationMap S N
Full source
/-- The type of homomorphisms between monoids with zero satisfying the characteristic predicate:
if `f : M →*₀ N` satisfies this predicate, then `N` is isomorphic to the localization of `M` at
`S`. -/
structure LocalizationWithZeroMap extends LocalizationMap S N where
map_zero' : toFun 0 = 0Informal description
The structure representing a homomorphism between monoids with zero that satisfies the characteristic predicate for localization. Specifically, if `f : M →*₀ N` satisfies this predicate, then `N` is isomorphic to the localization of `M` at the submonoid `S`. This extends the `LocalizationMap` structure to include the zero element.
Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom
definition
(f : LocalizationWithZeroMap S N) : M →*₀ N
Full source
/-- The monoid with zero hom underlying a `LocalizationMap`. -/
def LocalizationWithZeroMap.toMonoidWithZeroHom (f : LocalizationWithZeroMap S N) : M →*₀ N :=
{ f with }Informal description
Given a localization map `f` from a monoid with zero `M` to a monoid with zero `N` at a submonoid `S`, the underlying monoid with zero homomorphism of `f` is a structure-preserving map from `M` to `N` that respects both the multiplicative and zero structures.
Localization.mk_zero
theorem
(x : S) : mk 0 (x : S) = 0
Full source
theorem mk_zero (x : S) : mk 0 (x : S) = 0 := OreLocalization.zero_oreDiv' _Informal description
For any element $x$ in the submonoid $S$ of a commutative monoid $M$, the equivalence class of the pair $(0, x)$ in the localization $M[S^{-1}]$ is equal to the zero element of the localization, i.e., $\frac{0}{x} = 0$.
Localization.instCommMonoidWithZero
instance
: CommMonoidWithZero (Localization S)
Full source
instance : CommMonoidWithZero (Localization S) where
zero_mul := fun x ↦ Localization.induction_on x fun y => by
simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]
mul_zero := fun x ↦ Localization.induction_on x fun y => by
simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]Informal description
The localization of a commutative monoid $M$ at a submonoid $S$ is a commutative monoid with zero.
Localization.liftOn_zero
theorem
{p : Type*} (f : M → S → p) (H) : liftOn 0 f H = f 0 1
Full source
theorem liftOn_zero {p : Type*} (f : M → S → p) (H) : liftOn 0 f H = f 0 1 := by
rw [← mk_zero 1, liftOn_mk]Informal description
For any type $p$, any function $f \colon M \times S \to p$ that respects the localization congruence relation, and any proof $H$ of this compatibility, the function `liftOn` applied to the zero element of the localization $M[S^{-1}]$ satisfies $\text{liftOn}(0, f, H) = f(0, 1)$.
Submonoid.LocalizationMap.sec_zero_fst
theorem
{f : LocalizationMap S N} : f.toMap (f.sec 0).fst = 0
Full source
@[simp]
theorem LocalizationMap.sec_zero_fst {f : LocalizationMap S N} : f.toMap (f.sec 0).fst = 0 := by
rw [LocalizationMap.sec_spec', mul_zero]Informal description
Let $M$ be a commutative monoid, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. Then for the zero element $0 \in N$, the first component of the section $\mathrm{sec}(0)$ satisfies $f(x) = 0$, where $(x, y) = \mathrm{sec}(0)$.
Submonoid.LocalizationWithZeroMap.lift
definition
(f : LocalizationWithZeroMap S N) (g : M →*₀ P) (hg : ∀ y : S, IsUnit (g y)) : N →*₀ P
Full source
/-- Given a Localization map `f : M →*₀ N` for a Submonoid `S ⊆ M` and a map of
`CommMonoidWithZero`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)⁻¹`. -/
noncomputable def lift (f : LocalizationWithZeroMap S N) (g : M →*₀ P)
(hg : ∀ y : S, IsUnit (g y)) : N →*₀ P :=
{ @LocalizationMap.lift _ _ _ _ _ _ _ f.toLocalizationMap g.toMonoidHom hg with
map_zero' := by
dsimp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
rw [LocalizationMap.lift_spec f.toLocalizationMap hg 0 0, mul_zero, ← map_zero g,
← g.toMonoidHom_coe]
refine f.toLocalizationMap.eq_of_eq hg ?_
rw [LocalizationMap.sec_zero_fst]
exact f.toMonoidWithZeroHom.map_zero.symm }Informal description
Given a localization map \( f \colon M \to N \) for a commutative monoid with zero \( M \) at a submonoid \( S \), and a monoid with zero homomorphism \( g \colon M \to P \) such that \( g(y) \) is a unit in \( P \) for every \( y \in S \), the function \( \text{lift} \) is the induced homomorphism from \( N \) to \( P \) defined by sending \( z \in N \) to \( g(x) \cdot (g(y))^{-1} \), where \( (x, y) \in M \times S \) is any pair such that \( z = f(x) \cdot (f(y))^{-1} \). This homomorphism preserves the zero element.
Submonoid.LocalizationWithZeroMap.lift_def
theorem
(f : LocalizationWithZeroMap S N) (g : M →*₀ P) (hg : ∀ y : S, IsUnit (g y)) :
⇑(f.lift g hg) = f.toLocalizationMap.lift (g := ↑g) hg
Full source
lemma lift_def (f : LocalizationWithZeroMap S N) (g : M →*₀ P) (hg : ∀ y : S, IsUnit (g y)) :
⇑(f.lift g hg) = f.toLocalizationMap.lift (g := ↑g) hg := rflInformal description
Let $M$ be a commutative monoid with zero, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map at $S$. Given a monoid with zero homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, the underlying function of the induced homomorphism $\text{lift}(g, hg) \colon N \to P$ is equal to the lift of $g$ (viewed as a monoid homomorphism) via the localization map $f$.
Submonoid.LocalizationWithZeroMap.lift_apply
theorem
(f : LocalizationWithZeroMap S N) (g : M →*₀ P) (hg : ∀ y : S, IsUnit (g y)) (x) :
(f.lift g hg) x = g (f.sec x).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec x).2)⁻¹
Full source
lemma lift_apply (f : LocalizationWithZeroMap S N) (g : M →*₀ P) (hg : ∀ y : S, IsUnit (g y)) (x) :
(f.lift g hg) x = g (f.sec x).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec x).2)⁻¹ := rflInformal description
Let $M$ and $N$ be commutative monoids with zero, and let $S$ be a submonoid of $M$. Given a localization map $f \colon M \to N$ at $S$ and a monoid with zero homomorphism $g \colon M \to P$ such that $g(y)$ is a unit in $P$ for every $y \in S$, then for any $x \in N$, the induced homomorphism $\text{lift}(f, g, hg) \colon N \to P$ satisfies:
\[
\text{lift}(f, g, hg)(x) = g(a) \cdot \left(\text{liftRight}(g|_S, hg)(b)\right)^{-1}
\]
where $(a, b) \in M \times S$ is any pair such that $x = f(a) \cdot (f(b))^{-1}$ (i.e., $(a, b) = f.\text{sec}(x)$), and $\text{liftRight}(g|_S, hg)$ is the lift of the restriction $g|_S$ to the group of units of $P$.
Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular
theorem
(f : LocalizationWithZeroMap S N) [IsLeftCancelMulZero M] (h : ∀ ⦃x⦄, x ∈ S → IsLeftRegular x) : IsLeftCancelMulZero N
Full source
/-- Given a Localization map `f : M →*₀ N` for a Submonoid `S ⊆ M`,
if `M` is left cancellative monoid with zero, and all elements of `S` are
left regular, then N is a left cancellative monoid with zero. -/
theorem leftCancelMulZero_of_le_isLeftRegular
(f : LocalizationWithZeroMap S N) [IsLeftCancelMulZero M]
(h : ∀ ⦃x⦄, x ∈ S → IsLeftRegular x) : IsLeftCancelMulZero N := by
let fl := f.toLocalizationMap
let g := f.toMap
constructor
intro a z w ha hazw
obtain ⟨b, hb⟩ := LocalizationMap.surj fl a
obtain ⟨x, hx⟩ := LocalizationMap.surj fl z
obtain ⟨y, hy⟩ := LocalizationMap.surj fl w
rw [(LocalizationMap.eq_mk'_iff_mul_eq fl).mpr hx,
(LocalizationMap.eq_mk'_iff_mul_eq fl).mpr hy, LocalizationMap.eq]
use 1
rw [OneMemClass.coe_one, one_mul, one_mul]
-- The hypothesis `a ≠ 0` in `P` is equivalent to this
have b1ne0 : b.1 ≠ 0 := by
intro hb1
have m0 : (LocalizationMap.toMap fl) 0 = 0 := f.map_zero'
have a0 : a * (LocalizationMap.toMap fl) b.2 = 0 ↔ a = 0 :=
(f.toLocalizationMap.map_units' b.2).mul_left_eq_zero
rw [hb1, m0, a0] at hb
exact ha hb
have main : g (b.1 * (x.2 * y.1)) = g (b.1 * (y.2 * x.1)) :=
calc
g (b.1 * (x.2 * y.1)) = g b.1 * (g x.2 * g y.1) := by rw [map_mul g,map_mul g]
_ = a * g b.2 * (g x.2 * (w * g y.2)) := by rw [hb, hy]
_ = a * w * g b.2 * (g x.2 * g y.2) := by
rw [← mul_assoc, ← mul_assoc _ w, mul_comm _ w, mul_assoc w, mul_assoc,
← mul_assoc w, ← mul_assoc w, mul_comm w]
_ = a * z * g b.2 * (g x.2 * g y.2) := by rw [hazw]
_ = a * g b.2 * (z * g x.2 * g y.2) := by
rw [mul_assoc a, mul_comm z, ← mul_assoc a, mul_assoc, mul_assoc z]
_ = g b.1 * g (y.2 * x.1) := by rw [hx, hb, mul_comm (g x.1), ← map_mul g]
_ = g (b.1 * (y.2 * x.1)) := by rw [← map_mul g]
-- The hypothesis `h` gives that `f` (so, `g`) is injective, and we can cancel out `b.1`.
exact (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero b1ne0
((LocalizationMap.toMap_injective_iff fl).mpr h main)).symmInformal description
Let $M$ be a left cancellative monoid with zero, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. If every element of $S$ is left regular (i.e., left cancellative), then the localization $N$ is also a left cancellative monoid with zero.
Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero
theorem
(f : LocalizationWithZeroMap S N) [IsCancelMulZero M] (h : ∀ ⦃x⦄, x ∈ S → IsRegular x) : IsCancelMulZero N
Full source
/-- Given a Localization map `f : M →*₀ N` for a Submonoid `S ⊆ M`,
if `M` is a cancellative monoid with zero, and all elements of `S` are
regular, then N is a cancellative monoid with zero. -/
theorem isLeftRegular_of_le_isCancelMulZero (f : LocalizationWithZeroMap S N)
[IsCancelMulZero M] (h : ∀ ⦃x⦄, x ∈ S → IsRegular x) : IsCancelMulZero N := by
have : IsLeftCancelMulZero N :=
leftCancelMulZero_of_le_isLeftRegular f (fun x h' => (h h').left)
exact IsLeftCancelMulZero.to_isCancelMulZeroInformal description
Let $M$ be a cancellative monoid with zero, $S$ a submonoid of $M$, and $f \colon M \to N$ a localization map for $S$. If every element of $S$ is regular (i.e., both left and right cancellative), then the localization $N$ is also a cancellative monoid with zero.