# Documentation

Mathlib.Algebra.Group.WithOne.Basic

# 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
∀ (x x_1 : α), ↑(x + x_1) = ↑(x + x_1)
Equations
• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

WithZero.coe as a bundled morphism

Equations
• WithZero.coeAddHom = { toFun := WithZero.coe, map_add' := (_ : ∀ (x x_1 : α), ↑(x + x_1) = ↑(x + x_1)) }
@[simp]
theorem WithOne.coeMulHom_apply {α : Type u} [inst : Mul α] :
∀ (a : α), WithOne.coeMulHom a = a
@[simp]
∀ (a : α), WithZero.coeAddHom a = a
def WithOne.coeMulHom {α : Type u} [inst : Mul α] :

WithOne.coe as a bundled morphism

Equations
• WithOne.coeMulHom = { toFun := WithOne.coe, map_mul' := (_ : ∀ (x x_1 : α), ↑(x * x_1) = ↑(x * x_1)) }
def WithZero.lift {α : Type u} {β : Type v} [inst : Add α] [inst : ] :
AddHom α β ( →+ β)

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

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

Lift a semigroup homomorphism f to a bundled monoid homorphism.

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

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

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

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

Equations
@[simp]
theorem WithZero.map_coe {α : Type u} {β : Type v} [inst : Add α] [inst : Add β] (f : AddHom α β) (a : α) :
↑() a = ↑(f a)
@[simp]
theorem WithOne.map_coe {α : Type u} {β : Type v} [inst : Mul α] [inst : Mul β] (f : α →ₙ* β) (a : α) :
↑() a = ↑(f a)
@[simp]
theorem WithZero.map_id {α : Type u} [inst : Add α] :
@[simp]
theorem WithOne.map_id {α : Type u} [inst : Mul α] :
=
theorem WithZero.map_map {α : Type u} {β : Type v} {γ : Type w} [inst : Add α] [inst : Add β] [inst : Add γ] (f : AddHom α β) (g : AddHom β γ) (x : ) :
↑() (↑() x) = ↑(WithZero.map ()) x
theorem WithOne.map_map {α : Type u} {β : Type v} {γ : Type w} [inst : Mul α] [inst : Mul β] [inst : Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : ) :
↑() (↑() x) = ↑(WithOne.map ()) x
@[simp]
theorem WithZero.map_comp {α : Type u} {β : Type v} {γ : Type w} [inst : Add α] [inst : Add β] [inst : Add γ] (f : AddHom α β) (g : AddHom β γ) :
@[simp]
theorem WithOne.map_comp {α : Type u} {β : Type v} {γ : Type w} [inst : Mul α] [inst : Mul β] [inst : Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :
def AddEquiv.withZeroCongr.proof_1 {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] (e : α ≃+ β) :
∀ (x : ), ↑() (↑() x) = x
Equations
• One or more equations did not get rendered due to their size.
def AddEquiv.withZeroCongr.proof_2 {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Add β] (e : α ≃+ β) :
∀ (x : ), ↑() (↑() x) = x
Equations
• One or more equations did not get rendered due to their size.
def AddEquiv.withZeroCongr.proof_3 {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] (e : α ≃+ β) (x : ) (y : ) :
ZeroHom.toFun (↑()) (x + y) = ZeroHom.toFun (↑()) x + ZeroHom.toFun (↑()) y
Equations
• One or more equations did not get rendered due to their size.
def AddEquiv.withZeroCongr {α : Type u} {β : Type v} [inst : Add α] [inst : Add β] (e : α ≃+ β) :

A version of Equiv.optionCongr for WithZero.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddEquiv.withZeroCongr_apply {α : Type u} {β : Type v} [inst : Add α] [inst : Add β] (e : α ≃+ β) (a : ) :
↑() a = ↑() a
@[simp]
theorem MulEquiv.withOneCongr_apply {α : Type u} {β : Type v} [inst : Mul α] [inst : Mul β] (e : α ≃* β) (a : ) :
↑() a = ↑() a
def MulEquiv.withOneCongr {α : Type u} {β : Type v} [inst : Mul α] [inst : Mul β] (e : α ≃* β) :

A version of Equiv.optionCongr for WithOne.

Equations
• One or more equations did not get rendered due to their size.
@[simp]