More operations on WithOne and WithZero

This file defines various bundled morphisms on WithOne and WithZero that were not available in Algebra/Group/WithOne/Defs.

Main definitions

• WithOne.lift, WithZero.lift
• WithOne.map, WithZero.map

instance WithOne.instInvolutiveInv {α : Type u} [InvolutiveInv α] : InvolutiveInv (WithOne α)

Equations

• WithOne.instInvolutiveInv = { toInv := WithOne.instInv, inv_inv := ⋯ }

instance WithZero.instInvolutiveNeg {α : Type u} [InvolutiveNeg α] : InvolutiveNeg (WithZero α)

Equations

• WithZero.instInvolutiveNeg = { toNeg := WithZero.instNeg, neg_neg := ⋯ }

def WithOne.coeMulHom {α : Type u} [Mul α] : α →ₙ* WithOne α

WithOne.coe as a bundled morphism

Equations

• WithOne.coeMulHom = { toFun := WithOne.coe, map_mul' := ⋯ }

def WithZero.coeAddHom {α : Type u} [Add α] : α →ₙ+ WithZero α

WithZero.coe as a bundled morphism

Equations

• WithZero.coeAddHom = { toFun := WithZero.coe, map_add' := ⋯ }

@[simp]

theorem WithZero.coeAddHom_apply {α : Type u} [Add α] (a✝ : α) : coeAddHom a✝ = ↑a✝

@[simp]

theorem WithOne.coeMulHom_apply {α : Type u} [Mul α] (a✝ : α) : coeMulHom a✝ = ↑a✝

def WithOne.lift {α : Type u} {β : Type v} [Mul α] [MulOneClass β] : (α →ₙ* β) ≃ (WithOne α →* β)

Lift a semigroup homomorphism f to a bundled monoid homomorphism.

Equations

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

def WithZero.lift {α : Type u} {β : Type v} [Add α] [AddZeroClass β] : (α →ₙ+ β) ≃ (WithZero α →+ β)

Lift an additive semigroup homomorphism f to a bundled additive monoid homomorphism.

Equations

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

@[simp]

theorem WithOne.lift_coe {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) (x : α) : (lift f) ↑x = f x

@[simp]

theorem WithZero.lift_coe {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : α →ₙ+ β) (x : α) : (lift f) ↑x = f x

@[simp]

theorem WithOne.lift_one {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : α →ₙ* β) : (lift f) 1 = 1

@[simp]

theorem WithZero.lift_zero {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : α →ₙ+ β) : (lift f) 0 = 0

theorem WithOne.lift_unique {α : Type u} {β : Type v} [Mul α] [MulOneClass β] (f : WithOne α →* β) : f = lift ((↑f).comp coeMulHom)

theorem WithZero.lift_unique {α : Type u} {β : Type v} [Add α] [AddZeroClass β] (f : WithZero α →+ β) : f = lift ((↑f).comp coeAddHom)

def WithOne.mapMulHom {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) : WithOne α →* WithOne β

Given a multiplicative map from α → β returns a monoid homomorphism from WithOne α to WithOne β

Equations

• WithOne.mapMulHom f = WithOne.lift (WithOne.coeMulHom.comp f)

def WithZero.mapAddHom {α : Type u} {β : Type v} [Add α] [Add β] (f : α →ₙ+ β) : WithZero α →+ WithZero β

Given an additive map from α → β returns an additive monoid homomorphism from WithZero α to WithZero β

Equations

• WithZero.mapAddHom f = WithZero.lift (WithZero.coeAddHom.comp f)

@[simp]

theorem WithOne.mapMulHom_coe {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) (a : α) : (mapMulHom f) ↑a = ↑(f a)

@[simp]

theorem WithZero.mapAddHom_coe {α : Type u} {β : Type v} [Add α] [Add β] (f : α →ₙ+ β) (a : α) : (mapAddHom f) ↑a = ↑(f a)

@[simp]

theorem WithOne.mapMulHom_id {α : Type u} [Mul α] : mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α)

@[simp]

theorem WithZero.mapAddHom_id {α : Type u} [Add α] : mapAddHom (AddHom.id α) = AddMonoidHom.id (WithZero α)

@[deprecated WithOne.mapMulHom_id (since := "2025-08-26")]

theorem WithOne.map_id {α : Type u} [Mul α] : mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α)

Alias of WithOne.mapMulHom_id.

@[deprecated WithZero.mapAddHom_id (since := "2025-08-26")]

theorem WithZero.map_id {α : Type u} [Add α] : mapAddHom (AddHom.id α) = AddMonoidHom.id (WithZero α)

Alias of WithZero.mapAddHom_id.

theorem WithOne.mapMulHom_injective {α : Type u} {β : Type v} [Mul α] [Mul β] {f : α →ₙ* β} (hf : Function.Injective ⇑f) : Function.Injective ⇑(mapMulHom f)

theorem WithZero.mapAddHom_injective {α : Type u} {β : Type v} [Add α] [Add β] {f : α →ₙ+ β} (hf : Function.Injective ⇑f) : Function.Injective ⇑(mapAddHom f)

@[deprecated WithOne.mapMulHom_injective (since := "2025-08-26")]

theorem WithOne.map_injective {α : Type u} {β : Type v} [Mul α] [Mul β] {f : α →ₙ* β} (hf : Function.Injective ⇑f) : Function.Injective ⇑(mapMulHom f)

Alias of WithOne.mapMulHom_injective.

@[deprecated WithZero.mapAddHom_injective (since := "2025-08-26")]

theorem WithZero.map_injective {α : Type u} {β : Type v} [Add α] [Add β] {f : α →ₙ+ β} (hf : Function.Injective ⇑f) : Function.Injective ⇑(mapAddHom f)

Alias of WithZero.mapAddHom_injective.

theorem WithOne.mapMulHom_injective' {α : Type u} {β : Type v} [Mul α] [Mul β] : Function.Injective mapMulHom

theorem WithZero.mapAddHom_injective' {α : Type u} {β : Type v} [Add α] [Add β] : Function.Injective mapAddHom

@[deprecated WithOne.mapMulHom_injective' (since := "2025-08-26")]

theorem WithOne.map_injective' {α : Type u} {β : Type v} [Mul α] [Mul β] : Function.Injective mapMulHom

Alias of WithOne.mapMulHom_injective'.

@[deprecated WithZero.mapAddHom_injective' (since := "2025-08-26")]

theorem WithZero.map_injective' {α : Type u} {β : Type v} [Add α] [Add β] : Function.Injective mapAddHom

Alias of WithZero.mapAddHom_injective'.

@[simp]

theorem WithOne.mapMulHom_inj {α : Type u} {β : Type v} [Mul α] [Mul β] {f g : α →ₙ* β} : mapMulHom f = mapMulHom g ↔ f = g

@[simp]

theorem WithZero.mapAddHom_inj {α : Type u} {β : Type v} [Add α] [Add β] {f g : α →ₙ+ β} : mapAddHom f = mapAddHom g ↔ f = g

@[deprecated WithOne.mapMulHom_inj (since := "2025-08-26")]

theorem WithOne.map_inj {α : Type u} {β : Type v} [Mul α] [Mul β] {f g : α →ₙ* β} : mapMulHom f = mapMulHom g ↔ f = g

Alias of WithOne.mapMulHom_inj.

@[deprecated WithZero.mapAddHom_inj (since := "2025-08-26")]

theorem WithZero.map_inj {α : Type u} {β : Type v} [Add α] [Add β] {f g : α →ₙ+ β} : mapAddHom f = mapAddHom g ↔ f = g

Alias of WithZero.mapAddHom_inj.

theorem WithOne.mapMulHom_mapMulHom {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : WithOne α) : (mapMulHom g) ((mapMulHom f) x) = (mapMulHom (g.comp f)) x

theorem WithZero.mapAddHom_mapAddHom {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ) (x : WithZero α) : (mapAddHom g) ((mapAddHom f) x) = (mapAddHom (g.comp f)) x

@[deprecated WithOne.mapMulHom_mapMulHom (since := "2025-08-26")]

theorem WithOne.map_map {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : WithOne α) : (mapMulHom g) ((mapMulHom f) x) = (mapMulHom (g.comp f)) x

Alias of WithOne.mapMulHom_mapMulHom.

@[deprecated WithZero.mapAddHom_mapAddHom (since := "2025-08-26")]

theorem WithZero.map_map {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ) (x : WithZero α) : (mapAddHom g) ((mapAddHom f) x) = (mapAddHom (g.comp f)) x

Alias of WithZero.mapAddHom_mapAddHom.

@[simp]

theorem WithOne.mapMulHom_comp {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) : mapMulHom (g.comp f) = (mapMulHom g).comp (mapMulHom f)

@[simp]

theorem WithZero.mapAddHom_comp {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ) : mapAddHom (g.comp f) = (mapAddHom g).comp (mapAddHom f)

@[deprecated WithOne.mapMulHom_comp (since := "2025-08-26")]

theorem WithOne.map_comp {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) : mapMulHom (g.comp f) = (mapMulHom g).comp (mapMulHom f)

Alias of WithOne.mapMulHom_comp.

@[deprecated WithZero.mapAddHom_comp (since := "2025-08-26")]

theorem WithZero.map_comp {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ) : mapAddHom (g.comp f) = (mapAddHom g).comp (mapAddHom f)

Alias of WithZero.mapAddHom_comp.

def MulEquiv.withOneCongr {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) : WithOne α ≃* WithOne β

A version of Equiv.optionCongr for WithOne.

Equations

• e.withOneCongr = { toFun := ⇑(WithOne.mapMulHom e.toMulHom), invFun := ⇑(WithOne.mapMulHom e.symm.toMulHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

def AddEquiv.withZeroCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) : WithZero α ≃+ WithZero β

A version of Equiv.optionCongr for WithZero.

Equations

• e.withZeroCongr = { toFun := ⇑(WithZero.mapAddHom e.toAddHom), invFun := ⇑(WithZero.mapAddHom e.symm.toAddHom), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem MulEquiv.withOneCongr_apply {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) (a : WithOne α) : e.withOneCongr a = (WithOne.mapMulHom e.toMulHom) a

@[simp]

theorem AddEquiv.withZeroCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a : WithZero α) : e.withZeroCongr a = (WithZero.mapAddHom e.toAddHom) a

@[simp]

theorem MulEquiv.withOneCongr_refl {α : Type u} [Mul α] : (refl α).withOneCongr = refl (WithOne α)

@[simp]

theorem AddEquiv.withZeroCongr_refl {α : Type u} [Add α] : (refl α).withZeroCongr = refl (WithZero α)

@[simp]

theorem MulEquiv.withOneCongr_symm {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) : e.withOneCongr.symm = e.symm.withOneCongr

@[simp]

theorem AddEquiv.withZeroCongr_symm {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) : e.withZeroCongr.symm = e.symm.withZeroCongr

@[simp]

theorem MulEquiv.withOneCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ) : e₁.withOneCongr.trans e₂.withOneCongr = (e₁.trans e₂).withOneCongr

@[simp]

theorem AddEquiv.withZeroCongr_trans {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) : e₁.withZeroCongr.trans e₂.withZeroCongr = (e₁.trans e₂).withZeroCongr