# 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

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

Instances

source
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

Instances For

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

Instances For

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

Instances For

source
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 }

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

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

source
instance MonoidWithZeroHom.monoidWithZeroHomClass {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
MonoidWithZeroHomClass (α →*₀ β) α β
source
instance MonoidWithZeroHom.instSubsingleton {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] [Subsingleton α] :
Subsingleton (α →*₀ β)
source
@[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

source
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 }

source
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 }

source
@[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
source
@[simp]
theorem MonoidWithZeroHom.toZeroHom_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
⇑↑f = ⇑f
source
theorem MonoidWithZeroHom.toMonoidHom_coe {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
(↑↑f).toFun = ⇑f
source
theorem MonoidWithZeroHom.ext {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] ⦃f g : α →*₀ β⦄ (h : ∀ (x : α), f x = g x) :
f = g
source
theorem MonoidWithZeroHom.ext_iff {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] {f g : α →*₀ β} :
f = g ↔ ∀ (x : α), f x = g x
source
@[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
source
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' := ⋯ }

Instances For

source
@[simp]
theorem MonoidWithZeroHom.coe_copy {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem MonoidWithZeroHom.copy_eq {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = ↑f
source
theorem MonoidWithZeroHom.map_one {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
f 1 = 1
source
theorem MonoidWithZeroHom.map_zero {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
f 0 = 0
source
theorem MonoidWithZeroHom.map_mul {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (a b : α) :
f (a * b) = f a * f b
source
@[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
source
@[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
source
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' := ⋯ }

Instances For

source
@[simp]
theorem MonoidWithZeroHom.id_apply (α : Type u_7) [MulZeroOneClass α] (x : α) :
(id α) x = x
source
def MonoidWithZeroHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (hnp : β →*₀ γ) (hmn : α →*₀ β) :
α →*₀ γ

Composition of `MonoidWithZeroHom`s as a `MonoidWithZeroHom`.

Equations

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

Instances For

source
@[simp]
theorem MonoidWithZeroHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) :
⇑(g.comp f) = ⇑g ∘ ⇑f
source
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)
source
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)
source
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₂
source
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₂
source
theorem MonoidWithZeroHom.toMonoidHom_injective {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
Function.Injective toMonoidHom
source
theorem MonoidWithZeroHom.toZeroHom_injective {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
Function.Injective toZeroHom
source
@[simp]
theorem MonoidWithZeroHom.comp_id {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
f.comp (id α) = f
source
@[simp]
theorem MonoidWithZeroHom.id_comp {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) :
(id β).comp f = f
source
instance MonoidWithZeroHom.instInhabited {α : Type u_2} [MulZeroOneClass α] :
Inhabited (α →*₀ α)
Equations

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

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

source
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 0 to 0 and all other elements to 1.

Equations

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

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

Instances For

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