More operations on with_one and with_zero #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines various bundled morphisms on with_one and with_zero
that were not available in algebra/group/with_one/defs.
Main definitions #
@[simp]
coe as a bundled morphism
Equations
- with_zero.coe_add_hom = {to_fun := coe coe_to_lift, map_add' := _}
@[simp]
coe as a bundled morphism
Equations
- with_one.coe_mul_hom = {to_fun := coe coe_to_lift, map_mul' := _}
Lift an add_semigroup homomorphism f to a bundled add_monoid homorphism.
Lift a semigroup homomorphism f to a bundled monoid homorphism.
@[simp]
theorem
with_zero.lift_coe
{α : Type u}
{β : Type v}
[has_add α]
[add_zero_class β]
(f : add_hom α β)
(x : α) :
@[simp]
theorem
with_one.lift_coe
{α : Type u}
{β : Type v}
[has_mul α]
[mul_one_class β]
(f : α →ₙ* β)
(x : α) :
@[simp]
theorem
with_zero.lift_zero
{α : Type u}
{β : Type v}
[has_add α]
[add_zero_class β]
(f : add_hom α β) :
⇑(⇑with_zero.lift f) 0 = 0
@[simp]
theorem
with_one.lift_one
{α : Type u}
{β : Type v}
[has_mul α]
[mul_one_class β]
(f : α →ₙ* β) :
⇑(⇑with_one.lift f) 1 = 1
theorem
with_zero.lift_unique
{α : Type u}
{β : Type v}
[has_add α]
[add_zero_class β]
(f : with_zero α →+ β) :
theorem
with_one.lift_unique
{α : Type u}
{β : Type v}
[has_mul α]
[mul_one_class β]
(f : with_one α →* β) :
@[simp]
@[simp]
theorem
with_one.map_id
{α : Type u}
[has_mul α] :
with_one.map (mul_hom.id α) = monoid_hom.id (with_one α)
theorem
with_one.map_map
{α : Type u}
{β : Type v}
{γ : Type w}
[has_mul α]
[has_mul β]
[has_mul γ]
(f : α →ₙ* β)
(g : β →ₙ* γ)
(x : with_one α) :
⇑(with_one.map g) (⇑(with_one.map f) x) = ⇑(with_one.map (g.comp f)) x
theorem
with_zero.map_map
{α : Type u}
{β : Type v}
{γ : Type w}
[has_add α]
[has_add β]
[has_add γ]
(f : add_hom α β)
(g : add_hom β γ)
(x : with_zero α) :
⇑(with_zero.map g) (⇑(with_zero.map f) x) = ⇑(with_zero.map (g.comp f)) x
@[simp]
theorem
with_zero.map_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[has_add α]
[has_add β]
[has_add γ]
(f : add_hom α β)
(g : add_hom β γ) :
with_zero.map (g.comp f) = (with_zero.map g).comp (with_zero.map f)
@[simp]
theorem
with_one.map_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[has_mul α]
[has_mul β]
[has_mul γ]
(f : α →ₙ* β)
(g : β →ₙ* γ) :
with_one.map (g.comp f) = (with_one.map g).comp (with_one.map f)
@[simp]
theorem
mul_equiv.with_one_congr_apply
{α : Type u}
{β : Type v}
[has_mul α]
[has_mul β]
(e : α ≃* β)
(ᾰ : with_one α) :
⇑(e.with_one_congr) ᾰ = ⇑(with_one.map e.to_mul_hom) ᾰ
@[simp]
theorem
add_equiv.with_zero_congr_apply
{α : Type u}
{β : Type v}
[has_add α]
[has_add β]
(e : α ≃+ β)
(ᾰ : with_zero α) :
⇑(e.with_zero_congr) ᾰ = ⇑(with_zero.map e.to_add_hom) ᾰ
A version of equiv.option_congr for with_zero.
Equations
- e.with_zero_congr = {to_fun := ⇑(with_zero.map e.to_add_hom), inv_fun := ⇑(with_zero.map e.symm.to_add_hom), left_inv := _, right_inv := _, map_add' := _}
A version of equiv.option_congr for with_one.
Equations
- e.with_one_congr = {to_fun := ⇑(with_one.map e.to_mul_hom), inv_fun := ⇑(with_one.map e.symm.to_mul_hom), left_inv := _, right_inv := _, map_mul' := _}
@[simp]
@[simp]
theorem
mul_equiv.with_one_congr_trans
{α : Type u}
{β : Type v}
{γ : Type w}
[has_mul α]
[has_mul β]
[has_mul γ]
(e₁ : α ≃* β)
(e₂ : β ≃* γ) :
e₁.with_one_congr.trans e₂.with_one_congr = (e₁.trans e₂).with_one_congr