Documentation

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Localizations of commutative monoids with zeroes #

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

The monoid with zero hom underlying a LocalizationMap.

Equations
Instances For
    @[deprecated Submonoid.LocalizationMap (since := "2025-08-01")]
    def Submonoid.LocalizationWithZeroMap {M : Type u_1} [CommMonoid M] (S : Submonoid M) (N : Type u_2) [CommMonoid N] :
    Type (max u_1 u_2)

    Alias of Submonoid.LocalizationMap.


    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.

    Equations
    Instances For
      @[deprecated Submonoid.LocalizationMap.toMonoidWithZeroHom (since := "2025-08-01")]

      Alias of Submonoid.LocalizationMap.toMonoidWithZeroHom.


      The monoid with zero hom underlying a LocalizationMap.

      Equations
      Instances For
        theorem Localization.mk_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} (x : S) :
        mk 0 x = 0
        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}, (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 (f.sec 0).1 = 0
        noncomputable def Submonoid.LocalizationMap.lift₀ {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {P : Type u_3} [CommMonoidWithZero P] (f : S.LocalizationMap 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.LocalizationMap.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.LocalizationMap N) (g : M →*₀ P) (hg : ∀ (y : S), IsUnit (g y)) :
          (f.lift₀ g hg) = (f.lift hg)
          theorem Submonoid.LocalizationMap.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.LocalizationMap 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)⁻¹

          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 Submonoid.LocalizationMap.map_eq_zero_iff {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) {m : M} :
          f m = 0 ∃ (s : S), s * m = 0
          theorem Submonoid.LocalizationMap.mk'_eq_zero_iff {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) (m : M) (s : S) :
          f.mk' m s = 0 ∃ (s : S), s * m = 0
          @[simp]
          theorem Submonoid.LocalizationMap.mk'_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) (s : S) :
          f.mk' 0 s = 0
          @[deprecated Submonoid.LocalizationMap.isCancelMulZero (since := "2025-08-01")]

          Alias of Submonoid.LocalizationMap.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.

          @[deprecated Submonoid.LocalizationMap.isCancelMulZero (since := "2025-08-01")]

          Alias of Submonoid.LocalizationMap.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.

          @[deprecated Submonoid.LocalizationMap.lift₀ (since := "2025-08-01")]
          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.LocalizationMap N) (g : M →*₀ P) (hg : ∀ (y : S), IsUnit (g y)) :

          Alias of Submonoid.LocalizationMap.lift₀.


          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
          Instances For
            @[deprecated Submonoid.LocalizationMap.lift₀_def (since := "2025-08-01")]
            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.LocalizationMap N) (g : M →*₀ P) (hg : ∀ (y : S), IsUnit (g y)) :
            (f.lift₀ g hg) = (f.lift hg)

            Alias of Submonoid.LocalizationMap.lift₀_def.

            @[deprecated Submonoid.LocalizationMap.lift₀_apply (since := "2025-08-01")]
            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.LocalizationMap 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)⁻¹

            Alias of Submonoid.LocalizationMap.lift₀_apply.