mathlib3documentation

algebra.group.with_one.basic

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 #

• with_one.lift, with_zero.lift
• with_one.map, with_zero.map
@[simp]
theorem with_one.coe_mul_hom_apply {α : Type u} [has_mul α] (ᾰ : α) :
(with_zero α)

coe as a bundled morphism

Equations
@[simp]
theorem with_zero.coe_add_hom_apply {α : Type u} [has_add α] (ᾰ : α) :
def with_one.coe_mul_hom {α : Type u} [has_mul α] :

coe as a bundled morphism

Equations
def with_zero.lift {α : Type u} {β : Type v} [has_add α]  :
β →+ β)

Lift an add_semigroup homomorphism f to a bundled add_monoid homorphism.

Equations
def with_one.lift {α : Type u} {β : Type v} [has_mul α]  :
→ₙ* β) (with_one α →* β)

Lift a semigroup homomorphism f to a bundled monoid homorphism.

Equations
@[simp]
theorem with_zero.lift_coe {α : Type u} {β : Type v} [has_add α] (f : β) (x : α) :
x = f x
@[simp]
theorem with_one.lift_coe {α : Type u} {β : Type v} [has_mul α] (f : α →ₙ* β) (x : α) :
x = f x
@[simp]
theorem with_zero.lift_zero {α : Type u} {β : Type v} [has_add α] (f : β) :
0 = 0
@[simp]
theorem with_one.lift_one {α : Type u} {β : Type v} [has_mul α] (f : α →ₙ* β) :
1 = 1
theorem with_zero.lift_unique {α : Type u} {β : Type v} [has_add α] (f : →+ β) :
theorem with_one.lift_unique {α : Type u} {β : Type v} [has_mul α] (f : →* β) :
def with_one.map {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α →ₙ* β) :

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

Equations
def with_zero.map {α : Type u} {β : Type v} [has_add α] [has_add β] (f : β) :

Given an additive map from α → β returns an add_monoid homomorphism from with_zero α to with_zero β

Equations
@[simp]
theorem with_one.map_coe {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : α →ₙ* β) (a : α) :
@[simp]
theorem with_zero.map_coe {α : Type u} {β : Type v} [has_add α] [has_add β] (f : β) (a : α) :
a = (f a)
@[simp]
theorem with_zero.map_id {α : Type u} [has_add α] :
@[simp]
theorem with_one.map_id {α : Type u} [has_mul α] :
theorem with_one.map_map {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) (x : with_one α) :
theorem with_zero.map_map {α : Type u} {β : Type v} {γ : Type w} [has_add α] [has_add β] [has_add γ] (f : β) (g : γ) (x : with_zero α) :
( 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 : β) (g : γ) :
@[simp]
theorem with_one.map_comp {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (f : α →ₙ* β) (g : β →ₙ* γ) :
@[simp]
theorem mul_equiv.with_one_congr_apply {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) (ᾰ : with_one α) :
(e.with_one_congr) ᾰ =
@[simp]
theorem add_equiv.with_zero_congr_apply {α : Type u} {β : Type v} [has_add α] [has_add β] (e : α ≃+ β) (ᾰ : with_zero α) :
(e.with_zero_congr) ᾰ =
def add_equiv.with_zero_congr {α : Type u} {β : Type v} [has_add α] [has_add β] (e : α ≃+ β) :

A version of equiv.option_congr for with_zero.

Equations
def mul_equiv.with_one_congr {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) :

A version of equiv.option_congr for with_one.

Equations
@[simp]
theorem mul_equiv.with_one_congr_refl {α : Type u} [has_mul α] :
@[simp]
theorem mul_equiv.with_one_congr_symm {α : Type u} {β : Type v} [has_mul α] [has_mul β] (e : α ≃* β) :
@[simp]
theorem mul_equiv.with_one_congr_trans {α : Type u} {β : Type v} {γ : Type w} [has_mul α] [has_mul β] [has_mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ) :
= (e₁.trans e₂).with_one_congr