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 #
Equations
Equations
WithOne.coe
as a bundled morphism
Equations
- WithOne.coeMulHom = { toFun := WithOne.coe, map_mul' := ⋯ }
Instances For
WithZero.coe
as a bundled morphism
Equations
- WithZero.coeAddHom = { toFun := WithZero.coe, map_add' := ⋯ }
Instances For
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
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
@[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 α →* β)
:
theorem
WithZero.lift_unique
{α : Type u}
{β : Type v}
[Add α]
[AddZeroClass β]
(f : WithZero α →+ β)
:
Given a multiplicative map from α → β
returns a monoid homomorphism
from WithOne α
to WithOne β
Equations
- WithOne.map f = WithOne.lift (WithOne.coeMulHom.comp f)
Instances For
Given an additive map from α → β
returns an add monoid homomorphism from
WithZero α
to WithZero β
Equations
- WithZero.map f = WithZero.lift (WithZero.coeAddHom.comp f)
Instances For
@[simp]
@[simp]
A version of Equiv.optionCongr
for WithOne
.
Equations
- e.withOneCongr = { toFun := ⇑(WithOne.map e.toMulHom), invFun := ⇑(WithOne.map e.symm.toMulHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
A version of Equiv.optionCongr
for WithZero
.
Equations
- e.withZeroCongr = { toFun := ⇑(WithZero.map e.toAddHom), invFun := ⇑(WithZero.map e.symm.toAddHom), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
MulEquiv.withOneCongr_apply
{α : Type u}
{β : Type v}
[Mul α]
[Mul β]
(e : α ≃* β)
(a : WithOne α)
:
e.withOneCongr a = (WithOne.map e.toMulHom) a
@[simp]
theorem
AddEquiv.withZeroCongr_apply
{α : Type u}
{β : Type v}
[Add α]
[Add β]
(e : α ≃+ β)
(a : WithZero α)
:
e.withZeroCongr a = (WithZero.map e.toAddHom) a