# 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
theorem WithZero.involutiveNeg.proof_1 {α : Type u_1} [] (a : ) :
Option.map Neg.neg (Option.map Neg.neg a) = a
instance WithZero.involutiveNeg {α : Type u} [] :
Equations
• WithZero.involutiveNeg = let __src := WithZero.neg;
instance WithOne.involutiveInv {α : Type u} [] :
Equations
• WithOne.involutiveInv = let __src := WithOne.inv;
∀ (x x_1 : α), (x + x_1) = (x + x_1)

WithZero.coe as a bundled morphism

Equations
Instances For
@[simp]
∀ (a : α), WithZero.coeAddHom a = a
@[simp]
theorem WithOne.coeMulHom_apply {α : Type u} [Mul α] :
∀ (a : α), WithOne.coeMulHom a = a
def WithOne.coeMulHom {α : Type u} [Mul α] :

WithOne.coe as a bundled morphism

Equations
• WithOne.coeMulHom = { toFun := WithOne.coe, map_mul' := }
Instances For
def WithZero.lift {α : Type u} {β : Type v} [Add α] [] :
AddHom α β ( →+ β)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem WithZero.lift.proof_1 {α : Type u_2} {β : Type u_1} [Add α] [] (f : AddHom α β) :
(fun (x : ) => Option.casesOn x 0 f) 0 = (fun (x : ) => Option.casesOn x 0 f) 0
theorem WithZero.lift.proof_4 {α : Type u_1} {β : Type u_2} [Add α] [] (F : →+ β) :
(fun (f : AddHom α β) => { toFun := fun (x : ) => Option.casesOn x 0 f, map_zero' := , map_add' := }) ((fun (F : →+ β) => (↑F).comp WithZero.coeAddHom) F) = F
theorem WithZero.lift.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [] (f : AddHom α β) :
(fun (F : →+ β) => (↑F).comp WithZero.coeAddHom) ((fun (f : AddHom α β) => { toFun := fun (x : ) => Option.casesOn x 0 f, map_zero' := , map_add' := }) f) = f
theorem WithZero.lift.proof_2 {α : Type u_1} {β : Type u_2} [Add α] [] (f : AddHom α β) (x : ) (y : ) :
{ toFun := fun (x : ) => Option.casesOn x 0 f, map_zero' := }.toFun (x + y) = { toFun := fun (x : ) => Option.casesOn x 0 f, map_zero' := }.toFun x + { toFun := fun (x : ) => Option.casesOn x 0 f, map_zero' := }.toFun y
def WithOne.lift {α : Type u} {β : Type v} [Mul α] [] :
(α →ₙ* β) ( →* β)

Lift a semigroup homomorphism f to a bundled monoid homomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem WithZero.lift_coe {α : Type u} {β : Type v} [Add α] [] (f : AddHom α β) (x : α) :
(WithZero.lift f) x = f x
@[simp]
theorem WithOne.lift_coe {α : Type u} {β : Type v} [Mul α] [] (f : α →ₙ* β) (x : α) :
(WithOne.lift f) x = f x
theorem WithZero.lift_zero {α : Type u} {β : Type v} [Add α] [] (f : AddHom α β) :
(WithZero.lift f) 0 = 0
theorem WithOne.lift_one {α : Type u} {β : Type v} [Mul α] [] (f : α →ₙ* β) :
(WithOne.lift f) 1 = 1
theorem WithZero.lift_unique {α : Type u} {β : Type v} [Add α] [] (f : →+ β) :
theorem WithOne.lift_unique {α : Type u} {β : Type v} [Mul α] [] (f : →* β) :
f = WithOne.lift ((↑f).comp WithOne.coeMulHom)
def WithZero.map {α : Type u} {β : Type v} [Add α] [Add β] (f : AddHom α β) :

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

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

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

Equations
• = WithOne.lift (WithOne.coeMulHom.comp f)
Instances For
@[simp]
theorem WithZero.map_coe {α : Type u} {β : Type v} [Add α] [Add β] (f : AddHom α β) (a : α) :
(WithZero.map f) a = (f a)
@[simp]
theorem WithOne.map_coe {α : Type u} {β : Type v} [Mul α] [Mul β] (f : α →ₙ* β) (a : α) :
(WithOne.map f) a = (f a)
@[simp]
theorem WithZero.map_id {α : Type u} [Add α] :
@[simp]
theorem WithOne.map_id {α : Type u} [Mul α] :
=
theorem WithZero.map_map {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : AddHom α β) (g : AddHom β γ) (x : ) :
(WithZero.map g) ((WithZero.map f) x) = (WithZero.map (g.comp f)) x
theorem WithOne.map_map {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : ) :
(WithOne.map g) ((WithOne.map f) x) = (WithOne.map (g.comp f)) x
@[simp]
theorem WithZero.map_comp {α : Type u} {β : Type v} {γ : Type w} [Add α] [Add β] [Add γ] (f : AddHom α β) (g : AddHom β γ) :
WithZero.map (g.comp f) = (WithZero.map g).comp (WithZero.map f)
@[simp]
theorem WithOne.map_comp {α : Type u} {β : Type v} {γ : Type w} [Mul α] [Mul β] [Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :
WithOne.map (g.comp f) = (WithOne.map g).comp (WithOne.map f)
theorem AddEquiv.withZeroCongr.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (x : ) (y : ) :
def AddEquiv.withZeroCongr {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :

A version of Equiv.optionCongr for WithZero.

Equations
• e.withZeroCongr = let __src := WithZero.map e.toAddHom; { toFun := (WithZero.map e.toAddHom), invFun := (WithZero.map e.symm.toAddHom), left_inv := , right_inv := , map_add' := }
Instances For
theorem AddEquiv.withZeroCongr.proof_2 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (e : α ≃+ β) :
theorem AddEquiv.withZeroCongr.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) :
@[simp]
theorem AddEquiv.withZeroCongr_apply {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) (a : ) :
e.withZeroCongr a = (WithZero.map e.toAddHom) a
@[simp]
theorem MulEquiv.withOneCongr_apply {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) (a : ) :
e.withOneCongr a = (WithOne.map e.toMulHom) a
def MulEquiv.withOneCongr {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) :

A version of Equiv.optionCongr for WithOne.

Equations
• e.withOneCongr = let __src := WithOne.map e.toMulHom; { toFun := (WithOne.map e.toMulHom), invFun := (WithOne.map e.symm.toMulHom), left_inv := , right_inv := , map_mul' := }
Instances For
@[simp]
.withZeroCongr =
@[simp]
theorem MulEquiv.withOneCongr_refl {α : Type u} [Mul α] :
.withOneCongr =
@[simp]
theorem AddEquiv.withZeroCongr_symm {α : Type u} {β : Type v} [Add α] [Add β] (e : α ≃+ β) :
e.withZeroCongr.symm = e.symm.withZeroCongr
@[simp]
theorem MulEquiv.withOneCongr_symm {α : Type u} {β : Type v} [Mul α] [Mul β] (e : α ≃* β) :
e.withOneCongr.symm = e.symm.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
@[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