Mathlib.Algebra.GroupWithZero.Hom

NeZero.of_map theorem

(f : F) [neZero : NeZero (f a)] : NeZero a

Full source

lemma of_map (f : F) [neZero : NeZero (f a)] : NeZero a :=
  ⟨fun h ↦ ne (f a) <| by rw [h]; exact ZeroHomClass.map_zero f⟩

Nonzero Element Preservation Under Zero-Preserving Homomorphisms

Informal description

Let $F$ be a type of zero-preserving homomorphisms between types with zero elements, and let $f \colon F$ be such a homomorphism. If $f(a)$ is a nonzero element, then $a$ itself must be nonzero.

NeZero.of_injective theorem

{f : F} (hf : Injective f) [NeZero a] : NeZero (f a)

Full source

lemma of_injective {f : F} (hf : Injective f) [NeZero a] : NeZero (f a) :=
  ⟨by rw [← ZeroHomClass.map_zero f]; exact hf.ne NeZero.out⟩

Injective Zero-Preserving Homomorphisms Preserve Nonzero Elements

Informal description

Let $F$ be a type of zero-preserving homomorphisms between types with zero elements, and let $f \colon F$ be an injective homomorphism. If $a$ is a nonzero element, then $f(a)$ is also nonzero.

MonoidWithZeroHomClass structure

(F : Type*) (α β : outParam Type*) [MulZeroOneClass α]
    [MulZeroOneClass β] [FunLike F α β] : Prop
  extends MonoidHomClass F α β, ZeroHomClass F α β

Full source

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

You should also extend this typeclass when you extend `MonoidWithZeroHom`. -/
class MonoidWithZeroHomClass (F : Type*) (α β : outParam Type*) [MulZeroOneClass α]
    [MulZeroOneClass β] [FunLike F α β] : Prop
  extends MonoidHomClass F α β, ZeroHomClass F α β

Class of Monoid with Zero Homomorphisms

Informal description

The class `MonoidWithZeroHomClass F α β` states that `F` is a type of homomorphisms between monoids with zero (i.e., types equipped with a multiplication, a multiplicative identity, and a zero element) that preserve both the multiplicative structure (including the identity) and the zero element. More precisely, for any `f : F`, the function `f` maps the zero element of `α` to the zero element of `β`, the multiplicative identity of `α` to the multiplicative identity of `β`, and preserves multiplication: `f (x * y) = f x * f y` for all `x, y ∈ α`.

MonoidWithZeroHom structure

(α β : Type*) [MulZeroOneClass α] [MulZeroOneClass β]
  extends ZeroHom α β, MonoidHom α β

Full source

/-- `α →*₀ β` 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`. -/
structure MonoidWithZeroHom (α β : Type*) [MulZeroOneClass α] [MulZeroOneClass β]
  extends ZeroHom α β, MonoidHom α β

Monoid with zero homomorphism

Informal description

The structure representing bundled homomorphisms between monoids with zero, i.e., functions that preserve both the multiplicative structure (including the identity element) and the zero element. This structure is also used for group homomorphisms when the target is a group with zero.

term_→*₀_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `α →*₀ β` denotes the type of zero-preserving monoid homomorphisms from `α` to `β`. -/
infixr:25 " →*₀ " => MonoidWithZeroHom

Zero-preserving monoid homomorphism notation

Informal description

The notation `α →*₀ β` represents the type of zero-preserving monoid homomorphisms from `α` to `β`, i.e., functions that preserve both the multiplicative structure and the zero element.

MonoidWithZeroHomClass.toMonoidWithZeroHom definition

[FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) : α →*₀ β

Full source

/-- Turn an element of a type `F` satisfying `MonoidWithZeroHomClass F α β` into an actual
`MonoidWithZeroHom`. This is declared as the default coercion from `F` to `α →*₀ β`. -/
@[coe]
def MonoidWithZeroHomClass.toMonoidWithZeroHom [FunLike F α β] [MonoidWithZeroHomClass F α β]
    (f : F) : α →*₀ β := { (f : α →* β), (f : ZeroHom α β) with }

Conversion from Monoid-with-Zero Homomorphism Class to Monoid-with-Zero Homomorphism

Informal description

Given a type `F` satisfying `MonoidWithZeroHomClass F α β`, the function converts an element `f : F` into a bundled monoid-with-zero homomorphism from `α` to `β`, preserving both the multiplicative structure (including the identity element) and the zero element.

instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass instance

[FunLike F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀ β)

Full source

/-- Any type satisfying `MonoidWithZeroHomClass` can be cast into `MonoidWithZeroHom` via
`MonoidWithZeroHomClass.toMonoidWithZeroHom`. -/
instance [FunLike F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀ β) :=
  ⟨MonoidWithZeroHomClass.toMonoidWithZeroHom⟩

Coercion from Monoid-with-Zero Homomorphism Class to Bundled Homomorphisms

Informal description

For any type $F$ that satisfies `MonoidWithZeroHomClass F α β`, there is a canonical coercion from $F$ to the type of bundled monoid-with-zero homomorphisms $\alpha \to*₀ \beta$. This means any element $f : F$ can be treated as a monoid-with-zero homomorphism preserving the multiplicative structure (including the identity element) and the zero element.

MonoidWithZeroHom.funLike instance

: FunLike (α →*₀ β) α β

Full source

instance funLike : FunLike (α →*₀ β) α β where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

Function-Like Structure on Monoid-with-Zero Homomorphisms

Informal description

For any two monoids with zero $\alpha$ and $\beta$, the type $\alpha \to*₀ \beta$ of monoid-with-zero homomorphisms is equipped with a function-like structure, meaning each homomorphism can be treated as a function from $\alpha$ to $\beta$.

MonoidWithZeroHom.monoidWithZeroHomClass instance

: MonoidWithZeroHomClass (α →*₀ β) α β

Full source

instance monoidWithZeroHomClass : MonoidWithZeroHomClass (α →*₀ β) α β where
  map_mul := MonoidWithZeroHom.map_mul'
  map_one := MonoidWithZeroHom.map_one'
  map_zero f := f.map_zero'

Monoid-with-Zero Homomorphisms as a Homomorphism Class

Informal description

For any two monoids with zero $\alpha$ and $\beta$, the type $\alpha \to*₀ \beta$ of monoid-with-zero homomorphisms forms a `MonoidWithZeroHomClass`, meaning each homomorphism preserves the multiplicative structure (including the identity element) and the zero element.

MonoidWithZeroHom.instSubsingleton instance

[Subsingleton α] : Subsingleton (α →*₀ β)

Full source

instance [Subsingleton α] : Subsingleton (α →*₀ β) := .of_oneHomClass

Subsingleton Property of Monoid-with-Zero Homomorphisms from a Subsingleton

Informal description

For any monoid with zero $\alpha$ that is a subsingleton (i.e., has at most one element) and any monoid with zero $\beta$, the type of monoid-with-zero homomorphisms from $\alpha$ to $\beta$ is also a subsingleton.

MonoidWithZeroHom.coe_coe theorem

[MonoidWithZeroHomClass F α β] (f : F) : ((f : α →*₀ β) : α → β) = f

Full source

@[simp] lemma coe_coe [MonoidWithZeroHomClass F α β] (f : F) : ((f : α →*₀ β) : α → β) = f := rfl

Coercion Identity for Monoid-with-Zero Homomorphisms

Informal description

For any type `F` that is a `MonoidWithZeroHomClass` from `α` to `β`, and for any `f : F`, the underlying function of `f` when viewed as a monoid-with-zero homomorphism is equal to `f` itself. In other words, the coercion from `F` to `α →*₀ β` and then to `α → β` is the identity on `f`.

MonoidWithZeroHom.coeToMonoidHom instance

: Coe (α →*₀ β) (α →* β)

Full source

/-- `MonoidWithZeroHom` down-cast to a `MonoidHom`, forgetting the 0-preserving property. -/
instance coeToMonoidHom : Coe (α →*₀ β) (α →* β) :=
  ⟨toMonoidHom⟩

Monoid-with-Zero Homomorphism as Monoid Homomorphism

Informal description

Every monoid with zero homomorphism $f \colon \alpha \to \beta$ can be viewed as a monoid homomorphism, preserving the multiplicative structure (including the identity element) but forgetting the preservation of the zero element.

MonoidWithZeroHom.coeToZeroHom instance

: Coe (α →*₀ β) (ZeroHom α β)

Full source

/-- `MonoidWithZeroHom` down-cast to a `ZeroHom`, forgetting the monoidal property. -/
instance coeToZeroHom :
  Coe (α →*₀ β) (ZeroHom α β) := ⟨toZeroHom⟩

Monoid with Zero Homomorphism as Zero-Preserving Homomorphism

Informal description

Every monoid with zero homomorphism $f \colon \alpha \to \beta$ can be viewed as a zero-preserving homomorphism, where the zero element is preserved by $f$.

MonoidWithZeroHom.coe_mk theorem

(f h1 hmul) : (mk f h1 hmul : α → β) = (f : α → β)

Full source

@[simp] lemma coe_mk (f h1 hmul) : (mk f h1 hmul : α → β) = (f : α → β) := rfl

Underlying Function of Monoid-with-Zero Homomorphism Construction

Informal description

For any monoid with zero homomorphism constructed as `mk f h1 hmul`, the underlying function from $\alpha$ to $\beta$ is equal to the function $f$ used in the construction.

MonoidWithZeroHom.toZeroHom_coe theorem

(f : α →*₀ β) : (f.toZeroHom : α → β) = f

Full source

@[simp] lemma toZeroHom_coe (f : α →*₀ β) : (f.toZeroHom : α → β) = f := rfl

Equality of Monoid-with-Zero Homomorphism and its Zero-Preserving Component

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to \beta$, the underlying function of its zero-preserving homomorphism component equals $f$ itself. That is, $(f.\text{toZeroHom})(x) = f(x)$ for all $x \in \alpha$.

MonoidWithZeroHom.toMonoidHom_coe theorem

(f : α →*₀ β) : f.toMonoidHom.toFun = f

Full source

lemma toMonoidHom_coe (f : α →*₀ β) : f.toMonoidHom.toFun = f := rfl

Equality of Monoid-with-Zero Homomorphism and its Monoid Homomorphism Component

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to \beta$, the underlying function of its monoid homomorphism component equals $f$ itself. That is, $(f.\text{toMonoidHom})(x) = f(x)$ for all $x \in \alpha$.

MonoidWithZeroHom.ext theorem

⦃f g : α →*₀ β⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[ext] lemma ext ⦃f g : α →*₀ β⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h

Extensionality of Monoid-with-Zero Homomorphisms

Informal description

For any two monoid-with-zero homomorphisms $f, g \colon \alpha \to*₀ \beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

MonoidWithZeroHom.mk_coe theorem

(f : α →*₀ β) (h1 hmul) : mk f h1 hmul = f

Full source

@[simp] lemma mk_coe (f : α →*₀ β) (h1 hmul) : mk f h1 hmul = f := ext fun _ ↦ rfl

Constructor Equality for Monoid-with-Zero Homomorphisms

Informal description

Given a monoid-with-zero homomorphism $f \colon \alpha \to*₀ \beta$ and proofs $h_1$ and $h_{\text{mul}}$ that $f$ preserves the identity and multiplication respectively, the constructed homomorphism $\text{mk}(f, h_1, h_{\text{mul}})$ is equal to $f$.

MonoidWithZeroHom.copy definition

(f : α →*₀ β) (f' : α → β) (h : f' = f) : α →* β

Full source

/-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : α →*₀ β) (f' : α → β) (h : f' = f) : α →* β :=
  { f.toZeroHom.copy f' h, f.toMonoidHom.copy f' h with }

Copy of a monoid-with-zero homomorphism with a new function

Informal description

Given a monoid-with-zero homomorphism $f \colon \alpha \to*₀ \beta$ and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `MonoidWithZeroHom.copy` constructs a new monoid-with-zero homomorphism with the underlying function $f'$ that preserves both the multiplicative and zero structures. This is useful for fixing definitional equalities while maintaining the homomorphism structure.

MonoidWithZeroHom.coe_copy theorem

(f : α →*₀ β) (f' : α → β) (h) : (f.copy f' h) = f'

Full source

@[simp]
lemma coe_copy (f : α →*₀ β) (f' : α → β) (h) : (f.copy f' h) = f' := rfl

Underlying function of copied monoid-with-zero homomorphism equals the new function

Informal description

Given a monoid-with-zero homomorphism $f \colon \alpha \to*₀ \beta$ and a function $f' \colon \alpha \to \beta$ such that $f' = f$ (as functions), the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

MonoidWithZeroHom.copy_eq theorem

(f : α →*₀ β) (f' : α → β) (h) : f.copy f' h = f

Full source

lemma copy_eq (f : α →*₀ β) (f' : α → β) (h) : f.copy f' h = f := DFunLike.ext' h

Copy of Monoid-with-Zero Homomorphism Equals Original

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to \beta$ and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

MonoidWithZeroHom.map_one theorem

(f : α →*₀ β) : f 1 = 1

Full source

protected lemma map_one (f : α →*₀ β) : f 1 = 1 := f.map_one'

Monoid-with-zero homomorphisms preserve identity

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to \beta$ between monoids with zero, $f$ preserves the multiplicative identity element, i.e., $f(1) = 1$.

MonoidWithZeroHom.map_zero theorem

(f : α →*₀ β) : f 0 = 0

Full source

protected lemma map_zero (f : α →*₀ β) : f 0 = 0 := f.map_zero'

Preservation of Zero under Monoid-with-Zero Homomorphisms

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to \beta$ between monoids with zero $\alpha$ and $\beta$, the image of the zero element under $f$ is the zero element in $\beta$, i.e., $f(0) = 0$.

MonoidWithZeroHom.map_mul theorem

(f : α →*₀ β) (a b : α) : f (a * b) = f a * f b

Full source

protected lemma map_mul (f : α →*₀ β) (a b : α) : f (a * b) = f a * f b := f.map_mul' a b

Multiplicative Preservation Property of Monoid-with-Zero Homomorphisms

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to \beta$ between monoids with zero $\alpha$ and $\beta$, and for any elements $a, b \in \alpha$, the homomorphism preserves multiplication, i.e., $f(a \cdot b) = f(a) \cdot f(b)$.

MonoidWithZeroHom.map_ite_zero_one theorem

 {F : Type*} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [Decidable p] : f (ite p 0 1) = ite p 0 1

Full source

@[simp]
theorem map_ite_zero_one {F : Type*} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F)
    (p : Prop) [Decidable p] :
    f (ite p 0 1) = ite p 0 1 := by
  split_ifs with h <;> simp [h]

Preservation of Conditional Zero/One under Monoid with Zero Homomorphisms

Informal description

Let $F$ be a type of homomorphisms between monoids with zero, and let $f \colon \alpha \to \beta$ be a homomorphism in $F$. For any proposition $p$ with a decision procedure, the image under $f$ of the term $\text{ite}(p, 0, 1)$ (which evaluates to $0$ if $p$ is true and $1$ otherwise) is equal to $\text{ite}(p, 0, 1)$. In other words, $f$ preserves the conditional expression $\text{ite}(p, 0, 1)$.

MonoidWithZeroHom.map_ite_one_zero theorem

 {F : Type*} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [Decidable p] : f (ite p 1 0) = ite p 1 0

Full source

@[simp]
theorem map_ite_one_zero {F : Type*} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F)
    (p : Prop) [Decidable p] :
    f (ite p 1 0) = ite p 1 0 := by
  split_ifs with h <;> simp [h]

Preservation of Conditional Identity-Zero by Monoid with Zero Homomorphisms

Informal description

Let $F$ be a type of homomorphisms between monoids with zero, and let $f : F$ be such a homomorphism. For any proposition $p$ with a decision procedure, the image of the conditional expression $\text{ite}(p, 1, 0)$ (which evaluates to $1$ if $p$ is true and $0$ otherwise) under $f$ is equal to $\text{ite}(p, 1, 0)$ itself. In other words, $f$ preserves the conditional expression that selects between the multiplicative identity and the zero element.

MonoidWithZeroHom.id definition

(α : Type*) [MulZeroOneClass α] : α →*₀ α

Full source

/-- The identity map from a `MonoidWithZero` to itself. -/
@[simps]
def id (α : Type*) [MulZeroOneClass α] : α →*₀ α where
  toFun x := x
  map_zero' := rfl
  map_one' := rfl
  map_mul' _ _ := rfl

Identity homomorphism for monoids with zero

Informal description

The identity homomorphism from a monoid with zero to itself, which maps every element $x$ to itself, preserves the zero element, the multiplicative identity, and the multiplication operation.

MonoidWithZeroHom.comp definition

(hnp : β →*₀ γ) (hmn : α →*₀ β) : α →*₀ γ

Full source

/-- Composition of `MonoidWithZeroHom`s as a `MonoidWithZeroHom`. -/
def comp (hnp : β →*₀ γ) (hmn : α →*₀ β) : α →*₀ γ where
  toFun := hnp ∘ hmn
  map_zero' := by rw [comp_apply, map_zero, map_zero]
  map_one' := by simp
  map_mul' := by simp

Composition of monoid-with-zero homomorphisms

Informal description

The composition of two monoid-with-zero homomorphisms $g : \beta \to*₀ \gamma$ and $f : \alpha \to*₀ \beta$ is a monoid-with-zero homomorphism $g \circ f : \alpha \to*₀ \gamma$ defined by $(g \circ f)(x) = g(f(x))$ for all $x \in \alpha$. This composition preserves the zero element, the multiplicative identity, and the multiplication operation.

MonoidWithZeroHom.coe_comp theorem

(g : β →*₀ γ) (f : α →*₀ β) : ↑(g.comp f) = g ∘ f

Full source

@[simp] lemma coe_comp (g : β →*₀ γ) (f : α →*₀ β) : ↑(g.comp f) = g ∘ f := rfl

Composition of Monoid-with-Zero Homomorphisms Preserves Underlying Functions

Informal description

For any monoid-with-zero homomorphisms $g \colon \beta \to*₀ \gamma$ and $f \colon \alpha \to*₀ \beta$, the underlying function of the composition $g \circ f$ is equal to the composition of the underlying functions of $g$ and $f$, i.e., $(g \circ f)(x) = g(f(x))$ for all $x \in \alpha$.

MonoidWithZeroHom.comp_apply theorem

(g : β →*₀ γ) (f : α →*₀ β) (x : α) : g.comp f x = g (f x)

Full source

lemma comp_apply (g : β →*₀ γ) (f : α →*₀ β) (x : α) : g.comp f x = g (f x) := rfl

Evaluation of Composition of Monoid-with-Zero Homomorphisms: $(g \circ f)(x) = g(f(x))$

Informal description

For any monoid-with-zero homomorphisms $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$, and any element $x \in \alpha$, the composition $g \circ f$ evaluated at $x$ equals $g$ evaluated at $f(x)$, i.e., $(g \circ f)(x) = g(f(x))$.

MonoidWithZeroHom.comp_assoc theorem

(f : α →*₀ β) (g : β →*₀ γ) (h : γ →*₀ δ) : (h.comp g).comp f = h.comp (g.comp f)

Full source

lemma comp_assoc (f : α →*₀ β) (g : β →*₀ γ) (h : γ →*₀ δ) :
    (h.comp g).comp f = h.comp (g.comp f) := rfl

Associativity of Composition for Monoid-with-Zero Homomorphisms

Informal description

For any monoid-with-zero homomorphisms $f \colon \alpha \to \beta$, $g \colon \beta \to \gamma$, and $h \colon \gamma \to \delta$, the composition of homomorphisms is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

MonoidWithZeroHom.cancel_right theorem

{g₁ g₂ : β →*₀ γ} {f : α →*₀ β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

lemma cancel_right {g₁ g₂ : β →*₀ γ} {f : α →*₀ β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h ↦ ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h ↦ h ▸ rfl⟩

Right Cancellation Property for Monoid-with-Zero Homomorphisms under Surjective Maps

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be monoids with zero. For any two monoid-with-zero homomorphisms $g_1, g_2 \colon \beta \to*₀ \gamma$ and a surjective monoid-with-zero homomorphism $f \colon \alpha \to*₀ \beta$, the composition $g_1 \circ f$ equals $g_2 \circ f$ if and only if $g_1 = g_2$.

MonoidWithZeroHom.cancel_left theorem

{g : β →*₀ γ} {f₁ f₂ : α →*₀ β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

lemma cancel_left {g : β →*₀ γ} {f₁ f₂ : α →*₀ β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h ↦ ext fun x ↦ hg <| by rw [← comp_apply, h,
    comp_apply], fun h ↦ h ▸ rfl⟩

Left Cancellation Property for Monoid-with-Zero Homomorphisms under Injective Maps

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be monoids with zero. For any injective monoid-with-zero homomorphism $g \colon \beta \to*₀ \gamma$ and any two monoid-with-zero homomorphisms $f_1, f_2 \colon \alpha \to*₀ \beta$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

MonoidWithZeroHom.toMonoidHom_injective theorem

: Injective (toMonoidHom : (α →*₀ β) → α →* β)

Full source

lemma toMonoidHom_injective : Injective (toMonoidHom : (α →*₀ β) → α →* β) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Monoid-with-Zero to Monoid Homomorphism Map

Informal description

The canonical map from the type of monoid-with-zero homomorphisms $\alpha \to*₀ \beta$ to the type of monoid homomorphisms $\alpha \to* \beta$ is injective. That is, if two monoid-with-zero homomorphisms $f, g : \alpha \to*₀ \beta$ induce the same monoid homomorphism, then $f = g$.

MonoidWithZeroHom.toZeroHom_injective theorem

: Injective (toZeroHom : (α →*₀ β) → ZeroHom α β)

Full source

lemma toZeroHom_injective : Injective (toZeroHom : (α →*₀ β) → ZeroHom α β) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Monoid-with-Zero to Zero Homomorphism Map

Informal description

The canonical map from the type of monoid-with-zero homomorphisms $\alpha \to*₀ \beta$ to the type of zero-preserving homomorphisms $\text{ZeroHom}(\alpha, \beta)$ is injective. That is, if two monoid-with-zero homomorphisms $f, g : \alpha \to*₀ \beta$ induce the same zero-preserving homomorphism, then $f = g$.

MonoidWithZeroHom.comp_id theorem

(f : α →*₀ β) : f.comp (id α) = f

Full source

@[simp] lemma comp_id (f : α →*₀ β) : f.comp (id α) = f := ext fun _ ↦ rfl

Right identity law for monoid-with-zero homomorphism composition

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to*₀ \beta$, the composition of $f$ with the identity homomorphism on $\alpha$ equals $f$, i.e., $f \circ \text{id}_\alpha = f$.

MonoidWithZeroHom.id_comp theorem

(f : α →*₀ β) : (id β).comp f = f

Full source

@[simp] lemma id_comp (f : α →*₀ β) : (id β).comp f = f := ext fun _ ↦ rfl

Identity Homomorphism Acts as Left Identity under Composition

Informal description

For any monoid-with-zero homomorphism $f \colon \alpha \to*₀ \beta$, the composition of the identity homomorphism on $\beta$ with $f$ is equal to $f$, i.e., $\text{id}_\beta \circ f = f$.

MonoidWithZeroHom.instInhabited instance

: Inhabited (α →*₀ α)

Full source

instance : Inhabited (α →*₀ α) := ⟨id α⟩

Inhabited Type of Monoid with Zero Endomorphisms

Informal description

For any monoid with zero $\alpha$, the type of monoid with zero homomorphisms from $\alpha$ to itself is inhabited, with the identity homomorphism as a canonical element.

MonoidWithZeroHom.instMul instance

{β} [CommMonoidWithZero β] : Mul (α →*₀ β)

Full source

/-- 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`. -/
instance {β} [CommMonoidWithZero β] : Mul (α →*₀ β) where
  mul f g :=
    { (f * g : α →* β) with
      map_zero' := by dsimp; rw [map_zero, zero_mul] }

Pointwise Multiplication of Monoid-with-Zero Homomorphisms to a Commutative Monoid with Zero

Informal description

For any commutative monoid with zero $\beta$, the set of monoid-with-zero homomorphisms from $\alpha$ to $\beta$ forms a monoid under pointwise multiplication. That is, given two homomorphisms $f, g \colon \alpha \to \beta$, their product $f \cdot g$ is the homomorphism defined by $(f \cdot g)(x) = f(x) \cdot g(x)$ for all $x \in \alpha$.

powMonoidWithZeroHom definition

: M₀ →*₀ M₀

Full source

/-- We define `x ↦ x^n` (for positive `n : ℕ`) as a `MonoidWithZeroHom` -/
def powMonoidWithZeroHom : M₀ →*₀ M₀ :=
  { powMonoidHom n with map_zero' := zero_pow hn }

$n$-th power monoid with zero homomorphism

Informal description

For a monoid with zero $M_0$ and a positive natural number $n$, the $n$-th power map $x \mapsto x^n$ is a monoid with zero homomorphism from $M_0$ to itself. It preserves both the multiplicative structure (including the identity element) and the zero element (i.e., $0^n = 0$).

coe_powMonoidWithZeroHom theorem

: (powMonoidWithZeroHom hn : M₀ → M₀) = fun x ↦ x ^ n

Full source

@[simp] lemma coe_powMonoidWithZeroHom : (powMonoidWithZeroHom hn : M₀ → M₀) = fun x ↦ x ^ n := rfl

Coefficient of Power Homomorphism Equals Power Function

Informal description

For a monoid with zero $M_0$ and a positive natural number $n$, the monoid-with-zero homomorphism `powMonoidWithZeroHom hn` (given by $x \mapsto x^n$) is equal to the function $\lambda x, x^n$ when viewed as a function from $M_0$ to itself.

powMonoidWithZeroHom_apply theorem

(a : M₀) : powMonoidWithZeroHom hn a = a ^ n

Full source

@[simp] lemma powMonoidWithZeroHom_apply (a : M₀) : powMonoidWithZeroHom hn a = a ^ n := rfl

Evaluation of Power Homomorphism: $\text{powMonoidWithZeroHom}_n(a) = a^n$

Informal description

For any element $a$ in a monoid with zero $M_0$ and any positive natural number $n$, the $n$-th power monoid-with-zero homomorphism evaluated at $a$ equals $a^n$, i.e., $\text{powMonoidWithZeroHom}_n(a) = a^n$.

Mathlib.Algebra.GroupWithZero.Hom

Notations

Implementation notes

Tags