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 #
def
WithZero.lift.proof_1
{α : Type u_2}
{β : Type u_1}
[inst : Add α]
[inst : AddZeroClass β]
(f : AddHom α β)
:
(fun x => Option.casesOn x 0 ↑f) 0 = (fun x => Option.casesOn x 0 ↑f) 0
Equations
- (_ : (fun x => Option.casesOn x 0 ↑f) 0 = (fun x => Option.casesOn x 0 ↑f) 0) = (_ : (fun x => Option.casesOn x 0 ↑f) 0 = (fun x => Option.casesOn x 0 ↑f) 0)
def
WithZero.lift.proof_3
{α : Type u_1}
{β : Type u_2}
[inst : Add α]
[inst : 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
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 : 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
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 : 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
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 : AddZeroClass β]
(f : AddHom α β)
(x : α)
:
↑(↑WithZero.lift f) ↑x = ↑f x
@[simp]
theorem
WithOne.lift_coe
{α : Type u}
{β : Type v}
[inst : Mul α]
[inst : MulOneClass β]
(f : α →ₙ* β)
(x : α)
:
↑(↑WithOne.lift f) ↑x = ↑f x
theorem
WithZero.lift_zero
{α : Type u}
{β : Type v}
[inst : Add α]
[inst : AddZeroClass β]
(f : AddHom α β)
:
↑(↑WithZero.lift f) 0 = 0
theorem
WithOne.lift_one
{α : Type u}
{β : Type v}
[inst : Mul α]
[inst : MulOneClass β]
(f : α →ₙ* β)
:
↑(↑WithOne.lift f) 1 = 1
theorem
WithZero.lift_unique
{α : Type u}
{β : Type v}
[inst : Add α]
[inst : AddZeroClass β]
(f : WithZero α →+ β)
:
f = ↑WithZero.lift (AddHom.comp (↑f) WithZero.coeAddHom)
theorem
WithOne.lift_unique
{α : Type u}
{β : Type v}
[inst : Mul α]
[inst : MulOneClass β]
(f : WithOne α →* β)
:
f = ↑WithOne.lift (MulHom.comp (↑f) WithOne.coeMulHom)
@[simp]
theorem
WithZero.map_coe
{α : Type u}
{β : Type v}
[inst : Add α]
[inst : Add β]
(f : AddHom α β)
(a : α)
:
↑(WithZero.map f) ↑a = ↑(↑f a)
@[simp]
theorem
WithOne.map_coe
{α : Type u}
{β : Type v}
[inst : Mul α]
[inst : Mul β]
(f : α →ₙ* β)
(a : α)
:
↑(WithOne.map f) ↑a = ↑(↑f a)
@[simp]
theorem
WithZero.map_id
{α : Type u}
[inst : Add α]
:
WithZero.map (AddHom.id α) = AddMonoidHom.id (WithZero α)
@[simp]
theorem
WithOne.map_id
{α : Type u}
[inst : Mul α]
:
WithOne.map (MulHom.id α) = MonoidHom.id (WithOne α)
theorem
WithZero.map_map
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Add α]
[inst : Add β]
[inst : 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}
[inst : Mul α]
[inst : Mul β]
[inst : 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}
[inst : Add α]
[inst : Add β]
[inst : 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}
[inst : Mul α]
[inst : Mul β]
[inst : Mul γ]
(f : α →ₙ* β)
(g : β →ₙ* γ)
:
WithOne.map (MulHom.comp g f) = MonoidHom.comp (WithOne.map g) (WithOne.map f)
def
AddEquiv.withZeroCongr.proof_1
{α : Type u_1}
{β : Type u_2}
[inst : Add α]
[inst : Add β]
(e : α ≃+ β)
:
∀ (x : WithZero α), ↑(WithZero.map (AddEquiv.toAddHom (AddEquiv.symm e))) (↑(WithZero.map (AddEquiv.toAddHom e)) 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 : WithZero β), ↑(WithZero.map (AddEquiv.toAddHom e)) (↑(WithZero.map (AddEquiv.toAddHom (AddEquiv.symm e))) 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 : 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
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 : WithZero α)
:
↑(AddEquiv.withZeroCongr e) a = ↑(WithZero.map (AddEquiv.toAddHom e)) a
@[simp]
theorem
MulEquiv.withOneCongr_apply
{α : Type u}
{β : Type v}
[inst : Mul α]
[inst : 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}
[inst : Mul α]
[inst : Mul β]
[inst : Mul γ]
(e₁ : α ≃* β)
(e₂ : β ≃* γ)
:
MulEquiv.trans (MulEquiv.withOneCongr e₁) (MulEquiv.withOneCongr e₂) = MulEquiv.withOneCongr (MulEquiv.trans e₁ e₂)