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 = MonoidWithZeroHom.ofClass f

@[instance_reducible]

instance MulEquiv.instCoeMonoidWithZeroHom {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] : Coe (G ≃* H) (G →*₀ H)

Equations

• MulEquiv.instCoeMonoidWithZeroHom = { coe := MulEquiv.toMonoidWithZeroHom }

@[simp]

theorem MulEquiv.coe_toMonoidWithZeroHom {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) : ⇑↑f = ⇑f

theorem MulEquiv.toMonoidWithZeroHom_apply {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) (x : G) : ↑f 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

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

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

@[simp]

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