Localizations of commutative monoids with zeroes

theorem Submonoid.LocalizationMap.toMap_injective_iff {M : Type u_1} {N : Type u_2} [CommMonoid M] {S : Submonoid M} [CommMonoid N] (f : S.LocalizationMap N) : Function.Injective ⇑f.toMap ↔ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x

theorem AddSubmonoid.LocalizationMap.toMap_injective_iff {M : Type u_1} {N : Type u_2} [AddCommMonoid M] {S : AddSubmonoid M} [AddCommMonoid N] (f : S.LocalizationMap N) : Function.Injective ⇑f.toMap ↔ ∀ ⦃x : M⦄, x ∈ S → IsAddLeftRegular x

theorem Submonoid.LocalizationMap.subsingleton {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) (h : 0 ∈ S) : Subsingleton N

If S contains 0 then the localization at S is trivial.

structure Submonoid.LocalizationWithZeroMap {M : Type u_1} [CommMonoidWithZero M] (S : Submonoid M) (N : Type u_2) [CommMonoidWithZero N] extends S.LocalizationMap N : Type (max u_1 u_2)

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.

• toFun : M → N
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : M) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• map_units' (y : ↥S) : IsUnit ((↑self.toMonoidHom).toFun ↑y)
• surj' (z : N) : ∃ (x : M × ↥S), z * (↑self.toMonoidHom).toFun ↑x.2 = (↑self.toMonoidHom).toFun x.1
• exists_of_eq (x y : M) : (↑self.toMonoidHom).toFun x = (↑self.toMonoidHom).toFun y → ∃ (c : ↥S), ↑c * x = ↑c * y
• map_zero' : (↑self.toMonoidHom).toFun 0 = 0

def Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) : M →*₀ N

The monoid with zero hom underlying a LocalizationMap.

Equations

• f.toMonoidWithZeroHom = { toFun := (↑f.toMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Localization.mk_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} (x : ↥S) : mk 0 x = 0

instance Localization.instCommMonoidWithZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} : CommMonoidWithZero (Localization S)

Equations

• Localization.instCommMonoidWithZero = { toCommMonoid := OreLocalization.instCommMonoid, toZero := OreLocalization.instZero, zero_mul := ⋯, mul_zero := ⋯ }

theorem Localization.liftOn_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {p : Type u_4} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d) : liftOn 0 f H = f 0 1

@[simp]

theorem Submonoid.LocalizationMap.sec_zero_fst {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {f : S.LocalizationMap N} : f.toMap (f.sec 0).1 = 0

noncomputable def Submonoid.LocalizationWithZeroMap.lift {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {P : Type u_3} [CommMonoidWithZero P] (f : S.LocalizationWithZeroMap N) (g : M →*₀ P) (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : N →*₀ P

Given a Localization map f : M →*₀ N for a Submonoid S ⊆ M and a map of CommMonoidWithZeros 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 g hg = { toFun := (↑(f.lift hg)).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Submonoid.LocalizationWithZeroMap.lift_def {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {P : Type u_3} [CommMonoidWithZero P] (f : S.LocalizationWithZeroMap N) (g : M →*₀ P) (hg : ∀ (y : ↥S), IsUnit (g ↑y)) : ⇑(f.lift g hg) = ⇑(f.lift hg)

theorem Submonoid.LocalizationWithZeroMap.lift_apply {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {P : Type u_3} [CommMonoidWithZero P] (f : S.LocalizationWithZeroMap N) (g : M →*₀ P) (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : N) : (f.lift g hg) x = g (f.sec x).1 * ↑((IsUnit.liftRight ((↑g).restrict S) hg) (f.sec x).2)⁻¹

theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) [IsLeftCancelMulZero M] (h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x) : IsLeftCancelMulZero N

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 Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationWithZeroMap N) [IsCancelMulZero M] (h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x) : IsCancelMulZero N

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.