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.

Notations

• →*₀: 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_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] extends MonoidHomClass , ZeroHomClass : Prop

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

You should also extend this typeclass when you extend MonoidWithZeroHom.

structure MonoidWithZeroHom (α : Type u_6) (β : Type u_7) [MulZeroOneClass α] [MulZeroOneClass β] extends ZeroHom : Type (max u_6 u_7)

α →*₀ β 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

  The proposition that the function preserves 1

• map_mul' : ∀ (x y : α), self.toFun (x * y) = self.toFun x * self.toFun y

  The proposition that the function preserves multiplication

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 = let __src := ↑f; let __src_1 := ↑f; { toZeroHom := { toFun := __src.toFun, map_zero' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

instance instCoeTCMonoidWithZeroHom {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

• instCoeTCMonoidWithZeroHom = { 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 (α →*₀ β) α β

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

@[deprecated DFunLike.congr_fun]

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

@[deprecated DFunLike.congr_arg]

theorem MonoidWithZeroHom.congr_arg {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) {x : α} {y : α} (h : x = y) : f x = f y

@[deprecated DFunLike.coe_injective]

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

@[deprecated DFunLike.ext_iff]

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

• MonoidWithZeroHom.copy f f' h = let __src := ZeroHom.copy (↑f) f' h; let __src_1 := MonoidHom.copy (↑f) f' h; { toOneHom := { toFun := __src.toFun, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

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

theorem MonoidWithZeroHom.copy_eq {α : Type u_2} {β : Type u_3} : ∀ {x : MulZeroOneClass α} {x_1 : MulZeroOneClass β} (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f), MonoidWithZeroHom.copy f 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.id_apply (α : Type u_6) [MulZeroOneClass α] (x : α) : (MonoidWithZeroHom.id α) x = x

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

The identity map from a MonoidWithZero to itself.

Equations

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

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

Composition of MonoidWithZeroHoms as a MonoidWithZeroHom.

Equations

• MonoidWithZeroHom.comp hnp hmn = { toZeroHom := { 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 : α →*₀ β) : ⇑(MonoidWithZeroHom.comp g f) = ⇑g ∘ ⇑f

theorem MonoidWithZeroHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β) (x : α) : (MonoidWithZeroHom.comp g 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 : γ →*₀ δ) : MonoidWithZeroHom.comp (MonoidWithZeroHom.comp h g) f = MonoidWithZeroHom.comp h (MonoidWithZeroHom.comp g f)

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

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

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

@[simp]

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

@[simp]

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

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

Equations

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

instance MonoidWithZeroHom.instMulMonoidWithZeroHomToMulZeroOneClassToMonoidWithZero {α : Type u_2} [MulZeroOneClass α] {β : Type u_6} [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

• One or more equations did not get rendered due to their size.

Equivalences

instance MulEquivClass.toZeroHomClass {F : Type u_6} {α : Type u_7} {β : Type u_8} [EquivLike F α β] [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] : ZeroHomClass F α β

Equations

• ⋯ = ⋯

instance MulEquivClass.toMonoidWithZeroHomClass {F : Type u_6} {α : Type u_7} {β : Type u_8} [EquivLike F α β] [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] : MonoidWithZeroHomClass F α β

Equations

• ⋯ = ⋯