Monoid with zero and group with zero homomorphisms

This file defines homomorphisms of monoids with zero.

We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.

Notation

• →*₀: MonoidWithZeroHom, the type of bundled MonoidWithZero homs. Also use for GroupWithZero homs.

Implementation notes

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type MonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Tags

monoid homomorphism

theorem NeZero.of_map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α} (f : F) [neZero : NeZero (f a)] : NeZero a

theorem NeZero.of_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [FunLike F α β] [ZeroHomClass F α β] {a : α} {f : F} (hf : Function.Injective ⇑f) [NeZero a] : NeZero (f a)

class MonoidWithZeroHomClass (F : Type u_7) (α : outParam (Type u_8)) (β : outParam (Type u_9)) [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] extends MonoidHomClass F α β, ZeroHomClass F α β : Prop

MonoidWithZeroHomClass F α β states that F is a type of MonoidWithZero-preserving homomorphisms.

You should also extend this typeclass when you extend MonoidWithZeroHom.

• map_mul (f : F) (x y : α) : f (x * y) = f x * f y
• map_one (f : F) : f 1 = 1
• map_zero (f : F) : f 0 = 0

structure MonoidWithZeroHom (α : Type u_7) (β : Type u_8) [MulZeroOneClass α] [MulZeroOneClass β] extends ZeroHom α β, α →* β : Type (max u_7 u_8)

α →*₀ β is the type of functions α → β that preserve the MonoidWithZero structure.

MonoidWithZeroHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : α →*₀ β), you should parametrize over (F : Type*) [MonoidWithZeroHomClass F α β] (f : F).

When you extend this structure, make sure to extend MonoidWithZeroHomClass.

• toFun : α → β
• map_zero' : (↑self).toFun 0 = 0
• map_one' : (↑self).toFun 1 = 1
• map_mul' (x y : α) : (↑self).toFun (x * y) = (↑self).toFun x * (↑self).toFun y

def «term_→*₀_» : Lean.TrailingParserDescr

α →*₀ β denotes the type of zero-preserving monoid homomorphisms from α to β.

Equations

• «term_→*₀_» = Lean.ParserDescr.trailingNode `«term_→*₀_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →*₀ ") (Lean.ParserDescr.cat `term 25))

def MonoidWithZeroHomClass.toMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) : α →*₀ β

Turn an element of a type F satisfying MonoidWithZeroHomClass F α β into an actual MonoidWithZeroHom. This is declared as the default coercion from F to α →*₀ β.

Equations

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

instance instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀ β)

Any type satisfying MonoidWithZeroHomClass can be cast into MonoidWithZeroHom via MonoidWithZeroHomClass.toMonoidWithZeroHom.

Equations

• instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass = { coe := MonoidWithZeroHomClass.toMonoidWithZeroHom }

instance MonoidWithZeroHom.funLike {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : FunLike (α →*₀ β) α β

Equations

• MonoidWithZeroHom.funLike = { coe := fun (f : α →*₀ β) => (↑f).toFun, coe_injective' := ⋯ }

instance MonoidWithZeroHom.monoidWithZeroHomClass {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : MonoidWithZeroHomClass (α →*₀ β) α β

instance MonoidWithZeroHom.instSubsingleton {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [Subsingleton α] : Subsingleton (α →*₀ β)

@[simp]

theorem MonoidWithZeroHom.coe_coe {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) : ⇑↑f = ⇑f

Bundled morphisms can be down-cast to weaker bundlings

instance MonoidWithZeroHom.coeToMonoidHom {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : Coe (α →*₀ β) (α →* β)

MonoidWithZeroHom down-cast to a MonoidHom, forgetting the 0-preserving property.

Equations

• MonoidWithZeroHom.coeToMonoidHom = { coe := MonoidWithZeroHom.toMonoidHom }

instance MonoidWithZeroHom.coeToZeroHom {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : Coe (α →*₀ β) (ZeroHom α β)

MonoidWithZeroHom down-cast to a ZeroHom, forgetting the monoidal property.

Equations

• MonoidWithZeroHom.coeToZeroHom = { coe := MonoidWithZeroHom.toZeroHom }

@[simp]

theorem MonoidWithZeroHom.coe_mk {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : ZeroHom α β) (h1 : f.toFun 1 = 1) (hmul : ∀ (x y : α), f.toFun (x * y) = f.toFun x * f.toFun y) : ⇑{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = ⇑f

@[simp]

theorem MonoidWithZeroHom.toZeroHom_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) : ⇑↑f = ⇑f

theorem MonoidWithZeroHom.toMonoidHom_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) : (↑↑f).toFun = ⇑f

theorem MonoidWithZeroHom.ext {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] ⦃f g : α →*₀ β⦄ (h : ∀ (x : α), f x = g x) : f = g

theorem MonoidWithZeroHom.ext_iff {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] {f g : α →*₀ β} : f = g ↔ ∀ (x : α), f x = g x

@[simp]

theorem MonoidWithZeroHom.mk_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (h1 : (↑f).toFun 1 = 1) (hmul : ∀ (x y : α), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y) : { toZeroHom := ↑f, map_one' := h1, map_mul' := hmul } = f

def MonoidWithZeroHom.copy {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f) : α →* β

Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toFun := ((↑f).copy f' h).toFun, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidWithZeroHom.coe_copy {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem MonoidWithZeroHom.copy_eq {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = ↑f

theorem MonoidWithZeroHom.map_one {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) : f 1 = 1

theorem MonoidWithZeroHom.map_zero {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) : f 0 = 0

theorem MonoidWithZeroHom.map_mul {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (a b : α) : f (a * b) = f a * f b

@[simp]

theorem MonoidWithZeroHom.map_ite_zero_one {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] {F : Type u_7} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [Decidable p] : f (if p then 0 else 1) = if p then 0 else 1

@[simp]

theorem MonoidWithZeroHom.map_ite_one_zero {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] {F : Type u_7} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [Decidable p] : f (if p then 1 else 0) = if p then 1 else 0

def MonoidWithZeroHom.id (α : Type u_7) [MulZeroOneClass α] : α →*₀ α

The identity map from a MonoidWithZero to itself.

Equations

• MonoidWithZeroHom.id α = { toFun := fun (x : α) => x, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidWithZeroHom.id_apply (α : Type u_7) [MulZeroOneClass α] (x : α) : (id α) x = x

def MonoidWithZeroHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (hnp : β →*₀ γ) (hmn : α →*₀ β) : α →*₀ γ

Composition of MonoidWithZeroHoms as a MonoidWithZeroHom.

Equations

• hnp.comp hmn = { toFun := ⇑hnp ∘ ⇑hmn, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidWithZeroHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) : ⇑(g.comp f) = ⇑g ∘ ⇑f

theorem MonoidWithZeroHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) (x : α) : (g.comp f) x = g (f x)

theorem MonoidWithZeroHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] [MulZeroOneClass δ] (f : α →*₀ β) (g : β →*₀ γ) (h : γ →*₀ δ) : (h.comp g).comp f = h.comp (g.comp f)

theorem MonoidWithZeroHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g₁ g₂ : β →*₀ γ} {f : α →*₀ β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

theorem MonoidWithZeroHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g : β →*₀ γ} {f₁ f₂ : α →*₀ β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

theorem MonoidWithZeroHom.toMonoidHom_injective {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : Function.Injective toMonoidHom

theorem MonoidWithZeroHom.toZeroHom_injective {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : Function.Injective toZeroHom

@[simp]

theorem MonoidWithZeroHom.comp_id {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) : f.comp (id α) = f

@[simp]

theorem MonoidWithZeroHom.id_comp {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) : (id β).comp f = f

instance MonoidWithZeroHom.instInhabited {α : Type u_2} [MulZeroOneClass α] : Inhabited (α →*₀ α)

Equations

• MonoidWithZeroHom.instInhabited = { default := MonoidWithZeroHom.id α }

instance MonoidWithZeroHom.instMul {α : Type u_2} [MulZeroOneClass α] {β : Type u_7} [CommMonoidWithZero β] : Mul (α →*₀ β)

Given two monoid with zero morphisms f, g to a commutative monoid with zero, f * g is the monoid with zero morphism sending x to f x * g x.

Equations

• MonoidWithZeroHom.instMul = { mul := fun (f g : α →*₀ β) => let __src := ↑f * ↑g; { toFun := (↑__src).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } }

instance MonoidWithZeroHom.one (M₀ : Type u_7) (N₀ : Type u_8) [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] : One (M₀ →*₀ N₀)

The trivial homomorphism between monoids with zero, sending everything to 1 other than 0.

Equations

• MonoidWithZeroHom.one M₀ N₀ = { one := { toFun := fun (x : M₀) => if x = 0 then 0 else 1, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } }

theorem MonoidWithZeroHom.one_apply_def {M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] (x : M₀) : 1 x = if x = 0 then 0 else 1

@[simp]

theorem MonoidWithZeroHom.one_apply_zero {M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] : 1 0 = 0

theorem MonoidWithZeroHom.one_apply_of_ne_zero {M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] {x : M₀} (hx : x ≠ 0) : 1 x = 1

@[simp]

theorem MonoidWithZeroHom.one_apply_eq_zero_iff {M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] [Nontrivial N₀] {x : M₀} : 1 x = 0 ↔ x = 0

@[simp]

theorem MonoidWithZeroHom.one_apply_eq_one_iff {M₀ : Type u_7} {N₀ : Type u_8} [MulZeroOneClass M₀] [MulZeroOneClass N₀] [DecidablePred fun (x : M₀) => x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] [Nontrivial N₀] {x : M₀} : 1 x = 1 ↔ x ≠ 0

def powMonoidWithZeroHom {M₀ : Type u_6} [CommMonoidWithZero M₀] {n : ℕ} (hn : n ≠ 0) : M₀ →*₀ M₀

We define x ↦ x^n (for positive n : ℕ) as a MonoidWithZeroHom

Equations

• powMonoidWithZeroHom hn = { toFun := (↑(powMonoidHom n)).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem coe_powMonoidWithZeroHom {M₀ : Type u_6} [CommMonoidWithZero M₀] {n : ℕ} (hn : n ≠ 0) : ⇑(powMonoidWithZeroHom hn) = fun (x : M₀) => x ^ n

@[simp]

theorem powMonoidWithZeroHom_apply {M₀ : Type u_6} [CommMonoidWithZero M₀] {n : ℕ} (hn : n ≠ 0) (a : M₀) : (powMonoidWithZeroHom hn) a = a ^ n