Localizations of commutative monoids with zeroes #

source

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.

source

theorem Submonoid.LocalizationMap.subsingleton_iff {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) :

Subsingleton N ↔ 0 ∈ S

source

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

Nontrivial N

source

theorem Submonoid.LocalizationMap.map_zero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) :

f 0 = 0

source

def Submonoid.LocalizationMap.toMonoidWithZeroHom {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) :

M →*₀ N

The monoid with zero hom underlying a LocalizationMap.

Equations

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

Instances For

source

@[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

@Submonoid.LocalizationWithZeroMap = @Submonoid.LocalizationMap

Instances For

source

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

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

M →*₀ N

Alias of Submonoid.LocalizationMap.toMonoidWithZeroHom.

The monoid with zero hom underlying a LocalizationMap.

Equations

@Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom = @Submonoid.LocalizationMap.toMonoidWithZeroHom

Instances For

source

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

mk 0 x = 0

source

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 := ⋯ }

source

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

source

@[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

source

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

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' := ⋯ }

Instances For

source

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)

source

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)⁻¹

source

theorem Submonoid.LocalizationMap.isCancelMulZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) [IsCancelMulZero M] :

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.

source

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

source

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

source

@[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

source

theorem Submonoid.LocalizationMap.nonZeroDivisors_le_comap {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) :

nonZeroDivisors M ≤ comap f (nonZeroDivisors N)

source

theorem Submonoid.LocalizationMap.map_nonZeroDivisors_le {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) :

Submonoid.map f (nonZeroDivisors M) ≤ nonZeroDivisors N

source

theorem Submonoid.LocalizationMap.noZeroDivisors {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) [NoZeroDivisors M] :

NoZeroDivisors N

source

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

theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) [IsCancelMulZero M] :

IsCancelMulZero N

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.

source

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

theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] (f : S.LocalizationMap N) [IsCancelMulZero M] :

IsCancelMulZero N

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.

source

@[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)) :

N →*₀ P

Alias of Submonoid.LocalizationMap.lift₀.

Equations

@Submonoid.LocalizationWithZeroMap.lift = @Submonoid.LocalizationMap.lift₀

Instances For

source

@[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.

source

@[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.

Documentation

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Localizations of commutative monoids with zeroes #