mathlib documentation

algebra.group.with_one

Adjoining a zero/one to semigroups and related algebraic structures #

This file contains different results about adjoining an element to an algebraic structure which then behaves like a zero or a one. An example is adjoining a one to a semigroup to obtain a monoid. That this provides an example of an adjunction is proved in algebra.category.Mon.adjunctions.

Another result says that adjoining to a group an element zero gives a group_with_zero. For more information about these structures (which are not that standard in informal mathematics, see algebra.group_with_zero.basic)

@[protected, instance]
def with_one.with_zero.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def with_one.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def with_zero.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def with_one.has_one {α : Type u} :
Equations
@[protected, instance]
def with_zero.has_zero {α : Type u} :
Equations
@[protected, instance]
def with_zero.has_add {α : Type u} [has_add α] :
Equations
@[protected, instance]
def with_one.has_mul {α : Type u} [has_mul α] :
Equations
@[protected, instance]
def with_one.has_inv {α : Type u} [has_inv α] :
Equations
@[protected, instance]
def with_zero.has_neg {α : Type u} [has_neg α] :
Equations
@[protected, instance]
def with_one.inhabited {α : Type u} :
Equations
@[protected, instance]
def with_zero.inhabited {α : Type u} :
Equations
@[protected, instance]
def with_one.nontrivial {α : Type u} [nonempty α] :
@[protected, instance]
def with_zero.nontrivial {α : Type u} [nonempty α] :
@[protected, instance]
def with_zero.has_coe_t {α : Type u} :
Equations
@[protected, instance]
def with_one.has_coe_t {α : Type u} :
Equations
def with_zero.rec_zero_coe {α : Type u} {C : with_zero αSort u_1} (h₁ : C 0) (h₂ : Π (a : α), C a) (n : with_zero α) :
C n

Recursor for with_zero using the preferred forms 0 and ↑a.

Equations
def with_one.rec_one_coe {α : Type u} {C : with_one αSort u_1} (h₁ : C 1) (h₂ : Π (a : α), C a) (n : with_one α) :
C n

Recursor for with_one using the preferred forms 1 and ↑a.

Equations
def with_zero.unzero {α : Type u} {x : with_zero α} (hx : x 0) :
α

Deconstruct a x : with_zero α to the underlying value in α, given a proof that x ≠ 0.

Equations
def with_one.unone {α : Type u} {x : with_one α} (hx : x 1) :
α

Deconstruct a x : with_one α to the underlying value in α, given a proof that x ≠ 1.

Equations
@[simp]
theorem with_zero.unzero_coe {α : Type u} {x : α} (hx : x 0) :
@[simp]
theorem with_one.unone_coe {α : Type u} {x : α} (hx : x 1) :
@[simp]
theorem with_zero.coe_unzero {α : Type u} {x : with_zero α} (hx : x 0) :
@[simp]
theorem with_one.coe_unone {α : Type u} {x : with_one α} (hx : x 1) :
theorem with_one.some_eq_coe {α : Type u} {a : α} :
theorem with_zero.some_eq_coe {α : Type u} {a : α} :
@[simp]
theorem with_zero.coe_ne_zero {α : Type u} {a : α} :
a 0
@[simp]
theorem with_one.coe_ne_one {α : Type u} {a : α} :
a 1
@[simp]
theorem with_one.one_ne_coe {α : Type u} {a : α} :
1 a
@[simp]
theorem with_zero.zero_ne_coe {α : Type u} {a : α} :
0 a
theorem with_one.ne_one_iff_exists {α : Type u} {x : with_one α} :
x 1 ∃ (a : α), a = x
theorem with_zero.ne_zero_iff_exists {α : Type u} {x : with_zero α} :
x 0 ∃ (a : α), a = x
@[protected, instance]
def with_zero.can_lift {α : Type u} :
Equations
@[protected, instance]
def with_one.can_lift {α : Type u} :
Equations
@[simp, norm_cast]
theorem with_one.coe_inj {α : Type u} {a b : α} :
a = b a = b
@[simp, norm_cast]
theorem with_zero.coe_inj {α : Type u} {a b : α} :
a = b a = b
@[protected]
theorem with_one.cases_on {α : Type u} {P : with_one α → Prop} (x : with_one α) :
P 1(∀ (a : α), P a)P x
@[protected]
theorem with_zero.cases_on {α : Type u} {P : with_zero α → Prop} (x : with_zero α) :
P 0(∀ (a : α), P a)P x
@[protected, instance]
def with_zero.add_zero_class {α : Type u} [has_add α] :
Equations
@[protected, instance]
def with_one.mul_one_class {α : Type u} [has_mul α] :
Equations
@[simp]
theorem with_one.coe_mul_hom_apply {α : Type u} [has_mul α] (ᾰ : α) :
def with_zero.coe_add_hom {α : Type u} [has_add α] :

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 α] [add_zero_class β] :
add_hom α β (with_zero α →+ β)

Lift an add_semigroup homomorphism f to a bundled add_monoid homorphism.

Equations
def with_one.lift {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] :
→ₙ* β) (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 α] [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 α β) :
@[simp]
theorem with_one.lift_one {α : Type u} {β : Type v} [has_mul α] [mul_one_class β] (f : α →ₙ* β) :
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 α →* β) :
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 : add_hom α β) :

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 : add_hom α β) (a : α) :
@[simp]
@[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 : add_hom α β) (g : add_hom β γ) (x : with_zero α) :
@[simp]
theorem with_zero.map_comp {α : Type u} {β : Type v} {γ : Type w} [has_add α] [has_add β] [has_add γ] (f : add_hom α β) (g : add_hom β γ) :
@[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 α) :
@[simp]
theorem add_equiv.with_zero_congr_apply {α : Type u} {β : Type v} [has_add α] [has_add β] (e : α ≃+ β) (ᾰ : with_zero α) :
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_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₂ : β ≃* γ) :
@[simp, norm_cast]
theorem with_one.coe_mul {α : Type u} [has_mul α] (a b : α) :
(a * b) = a * b
@[simp, norm_cast]
theorem with_zero.coe_add {α : Type u} [has_add α] (a b : α) :
(a + b) = a + b
@[simp, norm_cast]
theorem with_one.coe_inv {α : Type u} [has_inv α] (a : α) :
@[simp, norm_cast]
theorem with_zero.coe_neg {α : Type u} [has_neg α] (a : α) :
@[protected, instance]
def with_zero.has_one {α : Type u} [one : has_one α] :
Equations
@[simp, norm_cast]
theorem with_zero.coe_one {α : Type u} [has_one α] :
1 = 1
@[protected, instance]
def with_zero.mul_zero_class {α : Type u} [has_mul α] :
Equations
@[simp, norm_cast]
theorem with_zero.coe_mul {α : Type u} [has_mul α] {a b : α} :
(a * b) = a * b
@[simp]
theorem with_zero.zero_mul {α : Type u} [has_mul α] (a : with_zero α) :
0 * a = 0
@[simp]
theorem with_zero.mul_zero {α : Type u} [has_mul α] (a : with_zero α) :
a * 0 = 0
@[protected, instance]
@[protected, instance]
def with_zero.nat.has_pow {α : Type u} [has_one α] [has_pow α ] :
Equations
@[simp, norm_cast]
theorem with_zero.coe_pow {α : Type u} [has_one α] [has_pow α ] {a : α} (n : ) :
(a ^ n) = a ^ n
@[protected, instance]
def with_zero.has_inv {α : Type u} [has_inv α] :

Given an inverse operation on α there is an inverse operation on with_zero α sending 0 to 0

Equations
@[simp, norm_cast]
theorem with_zero.coe_inv {α : Type u} [has_inv α] (a : α) :
@[simp]
theorem with_zero.inv_zero {α : Type u} [has_inv α] :
0⁻¹ = 0
@[protected, instance]
def with_zero.has_div {α : Type u} [has_div α] :
Equations
@[norm_cast]
theorem with_zero.coe_div {α : Type u} [has_div α] (a b : α) :
(a / b) = a / b
@[protected, instance]
def with_zero.int.has_pow {α : Type u} [has_one α] [has_pow α ] :
Equations
@[simp, norm_cast]
theorem with_zero.coe_zpow {α : Type u} [div_inv_monoid α] {a : α} (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem with_zero.inv_one {α : Type u} [group α] :
1⁻¹ = 1
def with_zero.units_with_zero_equiv {α : Type u} [group α] :

Any group is isomorphic to the units of itself adjoined with 0.

Equations