Documentation

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Localizations of commutative monoids with zeroes #

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 SIsAddLeftRegular x
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 SIsLeftRegular 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) :

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

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 : MN
  • 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
Instances For
    theorem Submonoid.LocalizationWithZeroMap.map_zero' {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (self : S.LocalizationWithZeroMap N) :
    (↑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) :

    The monoid with zero hom underlying a LocalizationMap.

    Equations
    • f.toMonoidWithZeroHom = { toFun := (↑f.toMonoidHom).toFun, map_zero' := , map_one' := , map_mul' := }
    Instances For
      theorem Localization.mk_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} (x : S) :
      Equations
      theorem Localization.liftOn_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {p : Type u_4} (f : MSp) (H : ∀ {a c : M} {b d : S}, (Localization.r S) (a, b) (c, d)f a b = f c d) :
      @[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)) :

      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' := }
      Instances For
        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 SIsLeftRegular x) :

        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 SIsRegular x) :

        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.

        @[deprecated Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero]
        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 SIsRegular x) :

        Alias of Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero.


        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.