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 #
theorem
WithZero.involutiveNeg.proof_1
{α : Type u_1}
[InvolutiveNeg α]
(a : WithZero α)
:
Option.map Neg.neg (Option.map Neg.neg a) = a
WithZero.coe
as a bundled morphism
Instances For
@[simp]
@[simp]
WithOne.coe
as a bundled morphism
Instances For
Lift an add semigroup homomorphism f
to a bundled add monoid homorphism.
Instances For
theorem
WithZero.lift.proof_2
{α : Type u_1}
{β : Type u_2}
[Add α]
[AddZeroClass β]
(f : AddHom α β)
(x : WithZero α)
(y : WithZero α)
:
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
theorem
WithZero.lift.proof_3
{α : Type u_2}
{β : Type u_1}
[Add α]
[AddZeroClass β]
(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 : WithZero α),
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
theorem
WithZero.lift.proof_1
{α : Type u_2}
{β : Type u_1}
[Add α]
[AddZeroClass β]
(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_2}
{β : Type u_1}
[Add α]
[AddZeroClass β]
(F : WithZero α →+ β)
:
(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 : WithZero α),
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
Lift a semigroup homomorphism f
to a bundled monoid homorphism.
Instances For
@[simp]
theorem
WithZero.lift_coe
{α : Type u}
{β : Type v}
[Add α]
[AddZeroClass β]
(f : AddHom α β)
(x : α)
:
↑(↑WithZero.lift f) ↑x = ↑f x
@[simp]
theorem
WithOne.lift_coe
{α : Type u}
{β : Type v}
[Mul α]
[MulOneClass β]
(f : α →ₙ* β)
(x : α)
:
↑(↑WithOne.lift f) ↑x = ↑f x
theorem
WithZero.lift_zero
{α : Type u}
{β : Type v}
[Add α]
[AddZeroClass β]
(f : AddHom α β)
:
↑(↑WithZero.lift f) 0 = 0
theorem
WithOne.lift_one
{α : Type u}
{β : Type v}
[Mul α]
[MulOneClass β]
(f : α →ₙ* β)
:
↑(↑WithOne.lift f) 1 = 1
theorem
WithZero.lift_unique
{α : Type u}
{β : Type v}
[Add α]
[AddZeroClass β]
(f : WithZero α →+ β)
:
f = ↑WithZero.lift (AddHom.comp (↑f) WithZero.coeAddHom)
theorem
WithOne.lift_unique
{α : Type u}
{β : Type v}
[Mul α]
[MulOneClass β]
(f : WithOne α →* β)
:
f = ↑WithOne.lift (MulHom.comp (↑f) WithOne.coeMulHom)
@[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 α]
:
WithZero.map (AddHom.id α) = AddMonoidHom.id (WithZero α)
@[simp]
theorem
WithZero.map_map
{α : Type u}
{β : Type v}
{γ : Type w}
[Add α]
[Add β]
[Add γ]
(f : AddHom α β)
(g : AddHom β γ)
(x : WithZero α)
:
↑(WithZero.map g) (↑(WithZero.map f) x) = ↑(WithZero.map (AddHom.comp g f)) x
theorem
WithOne.map_map
{α : Type u}
{β : Type v}
{γ : Type w}
[Mul α]
[Mul β]
[Mul γ]
(f : α →ₙ* β)
(g : β →ₙ* γ)
(x : WithOne α)
:
↑(WithOne.map g) (↑(WithOne.map f) x) = ↑(WithOne.map (MulHom.comp g f)) x
@[simp]
theorem
WithZero.map_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[Add α]
[Add β]
[Add γ]
(f : AddHom α β)
(g : AddHom β γ)
:
WithZero.map (AddHom.comp g f) = AddMonoidHom.comp (WithZero.map g) (WithZero.map f)
@[simp]
theorem
WithOne.map_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[Mul α]
[Mul β]
[Mul γ]
(f : α →ₙ* β)
(g : β →ₙ* γ)
:
WithOne.map (MulHom.comp g f) = MonoidHom.comp (WithOne.map g) (WithOne.map f)
theorem
AddEquiv.withZeroCongr.proof_2
{α : Type u_2}
{β : Type u_1}
[Add α]
[Add β]
(e : α ≃+ β)
:
∀ (x : WithZero β), ↑(WithZero.map (AddEquiv.toAddHom e)) (↑(WithZero.map (AddEquiv.toAddHom (AddEquiv.symm e))) x) = x
theorem
AddEquiv.withZeroCongr.proof_3
{α : Type u_1}
{β : Type u_2}
[Add α]
[Add β]
(e : α ≃+ β)
(x : WithZero α)
(y : WithZero α)
:
ZeroHom.toFun (↑(WithZero.map (AddEquiv.toAddHom e))) (x + y) = ZeroHom.toFun (↑(WithZero.map (AddEquiv.toAddHom e))) x + ZeroHom.toFun (↑(WithZero.map (AddEquiv.toAddHom e))) y
theorem
AddEquiv.withZeroCongr.proof_1
{α : Type u_1}
{β : Type u_2}
[Add α]
[Add β]
(e : α ≃+ β)
:
∀ (x : WithZero α), ↑(WithZero.map (AddEquiv.toAddHom (AddEquiv.symm e))) (↑(WithZero.map (AddEquiv.toAddHom e)) x) = x
@[simp]
theorem
AddEquiv.withZeroCongr_apply
{α : Type u}
{β : Type v}
[Add α]
[Add β]
(e : α ≃+ β)
(a : WithZero α)
:
↑(AddEquiv.withZeroCongr e) a = ↑(WithZero.map (AddEquiv.toAddHom e)) a
@[simp]
theorem
MulEquiv.withOneCongr_apply
{α : Type u}
{β : Type v}
[Mul α]
[Mul β]
(e : α ≃* β)
(a : WithOne α)
:
↑(MulEquiv.withOneCongr e) a = ↑(WithOne.map (MulEquiv.toMulHom e)) a
@[simp]
@[simp]
@[simp]
theorem
MulEquiv.withOneCongr_trans
{α : Type u}
{β : Type v}
{γ : Type w}
[Mul α]
[Mul β]
[Mul γ]
(e₁ : α ≃* β)
(e₂ : β ≃* γ)
:
MulEquiv.trans (MulEquiv.withOneCongr e₁) (MulEquiv.withOneCongr e₂) = MulEquiv.withOneCongr (MulEquiv.trans e₁ e₂)