Isomorphisms of monoids with zero

@[instance 100]

instance MulEquivClass.toZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] : ZeroHomClass F α β

@[instance 100]

instance MulEquivClass.toMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] : MonoidWithZeroHomClass F α β

def MulEquiv.toMonoidWithZeroHom {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) : G →*₀ H

An isomorphism of monoids with zero can be treated as a homomorphism preserving zero. This is a helper projection that utilizes the MonoidWithZeroHomClass instance.

Equations

• f.toMonoidWithZeroHom = ↑f

@[simp]

theorem MulEquiv.toMonoidWithZeroHom_apply {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) (x : G) : f.toMonoidWithZeroHom x = f x

theorem MulEquiv.toMonoidWithZeroHom_injective {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) : Function.Injective ⇑f.toMonoidWithZeroHom

theorem MulEquiv.toMonoidWithZeroHom_surjective {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) : Function.Surjective ⇑f.toMonoidWithZeroHom

theorem MulEquiv.toMonoidWithZeroHom_bijective {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) : Function.Bijective ⇑f.toMonoidWithZeroHom

@[simp]

theorem MulEquiv.toMonoidWithZeroHom_inj {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] {f g : G ≃* H} : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g