mathlib documentation

algebra.group.with_one

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)

def with_one (α : Type u_1) :

Type u_1

Add an extra element 1 to a type

Equations

with_one α = option α

def with_zero (α : Type u_1) :

Type u_1

Add an extra element 0 to a type

Equations

with_zero α = option α

@[protected, instance]

def with_zero.monad :

monad with_zero

Equations

with_zero.monad = option.monad

@[protected, instance]

def with_one.monad :

Equations

with_one.monad = option.monad

@[protected, instance]

def with_one.has_one {α : Type u} :

has_one (with_one α)

Equations

with_one.has_one = {one := none α}

@[protected, instance]

def with_zero.has_zero {α : Type u} :

has_zero (with_zero α)

Equations

with_zero.has_zero = {zero := none α}

@[protected, instance]

def with_zero.has_add {α : Type u} [has_add α] :

has_add (with_zero α)

Equations

with_zero.has_add = {add := option.lift_or_get has_add.add}

@[protected, instance]

def with_one.has_mul {α : Type u} [has_mul α] :

has_mul (with_one α)

Equations

with_one.has_mul = {mul := option.lift_or_get has_mul.mul}

@[protected, instance]

def with_one.has_inv {α : Type u} [has_inv α] :

has_inv (with_one α)

Equations

with_one.has_inv = {inv := λ (a : with_one α), option.map has_inv.inv a}

@[protected, instance]

def with_zero.has_neg {α : Type u} [has_neg α] :

has_neg (with_zero α)

Equations

with_zero.has_neg = {neg := λ (a : with_zero α), option.map has_neg.neg a}

@[protected, instance]

def with_one.inhabited {α : Type u} :

inhabited (with_one α)

Equations

with_one.inhabited = {default := 1}

@[protected, instance]

def with_zero.inhabited {α : Type u} :

inhabited (with_zero α)

Equations

with_zero.inhabited = {default := 0}

@[protected, instance]

def with_one.nontrivial {α : Type u} [nonempty α] :

nontrivial (with_one α)

@[protected, instance]

def with_zero.nontrivial {α : Type u} [nonempty α] :

nontrivial (with_zero α)

@[protected, instance]

def with_zero.has_coe_t {α : Type u} :

has_coe_t α (with_zero α)

Equations

with_zero.has_coe_t = {coe := some α}

@[protected, instance]

def with_one.has_coe_t {α : Type u} :

has_coe_t α (with_one α)

Equations

with_one.has_coe_t = {coe := some α}

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 : α} :

@[simp]

theorem with_one.coe_ne_one {α : Type u} {a : α} :

@[simp]

theorem with_one.one_ne_coe {α : Type u} {a : α} :

@[simp]

theorem with_zero.zero_ne_coe {α : Type u} {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} :

can_lift (with_zero α) α

Equations

with_zero.can_lift = {coe := coe coe_to_lift, cond := λ (a : with_zero α), a ≠ 0, prf := _}

@[protected, instance]

def with_one.can_lift {α : Type u} :

can_lift (with_one α) α

Equations

with_one.can_lift = {coe := coe coe_to_lift, cond := λ (a : with_one α), a ≠ 1, prf := _}

@[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 α] :

add_zero_class (with_zero α)

Equations

with_zero.add_zero_class = {zero := 0, add := has_add.add with_zero.has_add, zero_add := _, add_zero := _}

@[protected, instance]

def with_one.mul_one_class {α : Type u} [has_mul α] :

mul_one_class (with_one α)

Equations

with_one.mul_one_class = {one := 1, mul := has_mul.mul with_one.has_mul, one_mul := _, mul_one := _}

@[protected, instance]

def with_zero.add_monoid {α : Type u} [add_semigroup α] :

add_monoid (with_zero α)

Equations

with_zero.add_monoid = {add := add_zero_class.add with_zero.add_zero_class, add_assoc := _, zero := add_zero_class.zero with_zero.add_zero_class, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (with_zero α)), nsmul_zero' := _, nsmul_succ' := _}

@[protected, instance]

def with_one.monoid {α : Type u} [semigroup α] :

monoid (with_one α)

Equations

with_one.monoid = {mul := mul_one_class.mul with_one.mul_one_class, mul_assoc := _, one := mul_one_class.one with_one.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (with_one α)), npow_zero' := _, npow_succ' := _}

@[protected, instance]

def with_zero.add_comm_monoid {α : Type u} [add_comm_semigroup α] :

add_comm_monoid (with_zero α)

Equations

with_zero.add_comm_monoid = {add := add_monoid.add with_zero.add_monoid, add_assoc := _, zero := add_monoid.zero with_zero.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul with_zero.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

@[protected, instance]

def with_one.comm_monoid {α : Type u} [comm_semigroup α] :

comm_monoid (with_one α)

Equations

with_one.comm_monoid = {mul := monoid.mul with_one.monoid, mul_assoc := _, one := monoid.one with_one.monoid, one_mul := _, mul_one := _, npow := monoid.npow with_one.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

@[simp]

theorem with_one.coe_mul_hom_apply {α : Type u} [has_mul α] (ᾰ : α) :

⇑with_one.coe_mul_hom ᾰ = ↑ᾰ

def with_zero.coe_add_hom {α : Type u} [has_add α] :

add_hom α (with_zero α)

coe as a bundled morphism

Equations

with_zero.coe_add_hom = {to_fun := coe coe_to_lift, map_add' := _}

@[simp]

theorem with_zero.coe_add_hom_apply {α : Type u} [has_add α] (ᾰ : α) :

⇑with_zero.coe_add_hom ᾰ = ↑ᾰ

def with_one.coe_mul_hom {α : Type u} [has_mul α] :

mul_hom α (with_one α)

coe as a bundled morphism

Equations

with_one.coe_mul_hom = {to_fun := coe coe_to_lift, map_mul' := _}

def with_zero.lift {α : Type u} [has_add α] {β : Type v} [add_zero_class β] :

add_hom α β ≃ (with_zero α →+ β)

Lift an add_semigroup homomorphism f to a bundled add_monoid homorphism.

Equations

with_zero.lift = {to_fun := λ (f : add_hom α β), {to_fun := λ (x : with_zero α), option.cases_on x 0 ⇑f, map_zero' := _, map_add' := _}, inv_fun := λ (F : with_zero α →+ β), F.to_add_hom.comp with_zero.coe_add_hom, left_inv := _, right_inv := _}

def with_one.lift {α : Type u} [has_mul α] {β : Type v} [mul_one_class β] :

mul_hom α β ≃ (with_one α →* β)

Lift a semigroup homomorphism f to a bundled monoid homorphism.

Equations

with_one.lift = {to_fun := λ (f : mul_hom α β), {to_fun := λ (x : with_one α), option.cases_on x 1 ⇑f, map_one' := _, map_mul' := _}, inv_fun := λ (F : with_one α →* β), F.to_mul_hom.comp with_one.coe_mul_hom, left_inv := _, right_inv := _}

@[simp]

theorem with_zero.lift_coe {α : Type u} [has_add α] {β : Type v} [add_zero_class β] (f : add_hom α β) (x : α) :

⇑(⇑with_zero.lift f) ↑x = ⇑f x

@[simp]

theorem with_one.lift_coe {α : Type u} [has_mul α] {β : Type v} [mul_one_class β] (f : mul_hom α β) (x : α) :

⇑(⇑with_one.lift f) ↑x = ⇑f x

@[simp]

theorem with_zero.lift_zero {α : Type u} [has_add α] {β : Type v} [add_zero_class β] (f : add_hom α β) :

⇑(⇑with_zero.lift f) 0 = 0

@[simp]

theorem with_one.lift_one {α : Type u} [has_mul α] {β : Type v} [mul_one_class β] (f : mul_hom α β) :

⇑(⇑with_one.lift f) 1 = 1

theorem with_zero.lift_unique {α : Type u} [has_add α] {β : Type v} [add_zero_class β] (f : with_zero α →+ β) :

f = ⇑with_zero.lift (f.to_add_hom.comp with_zero.coe_add_hom)

theorem with_one.lift_unique {α : Type u} [has_mul α] {β : Type v} [mul_one_class β] (f : with_one α →* β) :

f = ⇑with_one.lift (f.to_mul_hom.comp with_one.coe_mul_hom)

def with_one.map {α : Type u} {β : Type v} [has_mul α] [has_mul β] (f : mul_hom α β) :

with_one α →* with_one β

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

Equations

with_one.map f = ⇑with_one.lift (with_one.coe_mul_hom.comp f)

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

with_zero α →+ with_zero β

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

Equations

with_zero.map f = ⇑with_zero.lift (with_zero.coe_add_hom.comp f)

@[simp]

theorem with_zero.map_id {α : Type u} [has_add α] :

with_zero.map (add_hom.id α) = add_monoid_hom.id (with_zero α)

@[simp]

theorem with_one.map_id {α : Type u} [has_mul α] :

with_one.map (mul_hom.id α) = monoid_hom.id (with_one α)

@[simp]

theorem with_zero.map_comp {α : Type u} {β : Type v} [has_add α] [has_add β] {γ : Type w} [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} [has_mul α] [has_mul β] {γ : Type w} [has_mul γ] (f : mul_hom α β) (g : mul_hom β γ) :

with_one.map (g.comp f) = (with_one.map g).comp (with_one.map f)

@[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 : α) :

↑a⁻¹ = (↑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 α] :

has_one (with_zero α)

Equations

with_zero.has_one = {one := ↑1}

@[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 α] :

mul_zero_class (with_zero α)

Equations

with_zero.mul_zero_class = {mul := λ (o₁ o₂ : with_zero α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a * b) o₂), zero := 0, zero_mul := _, mul_zero := _}

@[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]

def with_zero.semigroup_with_zero {α : Type u} [semigroup α] :

semigroup_with_zero (with_zero α)

Equations

with_zero.semigroup_with_zero = {mul := mul_zero_class.mul with_zero.mul_zero_class, mul_assoc := _, zero := mul_zero_class.zero with_zero.mul_zero_class, zero_mul := _, mul_zero := _}

@[protected, instance]

def with_zero.comm_semigroup {α : Type u} [comm_semigroup α] :

comm_semigroup (with_zero α)

Equations

with_zero.comm_semigroup = {mul := semigroup_with_zero.mul with_zero.semigroup_with_zero, mul_assoc := _, mul_comm := _}

@[protected, instance]

def with_zero.mul_zero_one_class {α : Type u} [mul_one_class α] :

mul_zero_one_class (with_zero α)

Equations

with_zero.mul_zero_one_class = {one := 1, mul := mul_zero_class.mul with_zero.mul_zero_class, one_mul := _, mul_one := _, zero := mul_zero_class.zero with_zero.mul_zero_class, zero_mul := _, mul_zero := _}

@[protected, instance]

def with_zero.nat.has_pow {α : Type u} [has_one α] [has_pow α ℕ] :

has_pow (with_zero α) ℕ

Equations

with_zero.nat.has_pow = {pow := λ (x : with_zero α) (n : ℕ), with_zero.nat.has_pow._match_1 x n}
with_zero.nat.has_pow._match_1 (some x) n = ↑(x ^ n)
with_zero.nat.has_pow._match_1 none (n + 1) = 0
with_zero.nat.has_pow._match_1 none 0 = 1

@[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.monoid_with_zero {α : Type u} [monoid α] :

monoid_with_zero (with_zero α)

Equations

with_zero.monoid_with_zero = {mul := mul_zero_one_class.mul with_zero.mul_zero_one_class, mul_assoc := _, one := mul_zero_one_class.one with_zero.mul_zero_one_class, one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : with_zero α), x ^ n, npow_zero' := _, npow_succ' := _, zero := mul_zero_one_class.zero with_zero.mul_zero_one_class, zero_mul := _, mul_zero := _}

@[protected, instance]

def with_zero.comm_monoid_with_zero {α : Type u} [comm_monoid α] :

comm_monoid_with_zero (with_zero α)

Equations

with_zero.comm_monoid_with_zero = {mul := monoid_with_zero.mul with_zero.monoid_with_zero, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, npow := monoid_with_zero.npow with_zero.monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := monoid_with_zero.zero with_zero.monoid_with_zero, zero_mul := _, mul_zero := _}

@[protected, instance]

def with_zero.has_inv {α : Type u} [has_inv α] :

has_inv (with_zero α)

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

Equations

with_zero.has_inv = {inv := λ (a : with_zero α), option.map has_inv.inv a}

@[simp, norm_cast]

theorem with_zero.coe_inv {α : Type u} [has_inv α] (a : α) :

↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem with_zero.inv_zero {α : Type u} [has_inv α] :

@[protected, instance]

def with_zero.has_div {α : Type u} [has_div α] :

has_div (with_zero α)

Equations

with_zero.has_div = {div := λ (o₁ o₂ : with_zero α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a / b) o₂)}

@[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 α ℤ] :

has_pow (with_zero α) ℤ

Equations

with_zero.int.has_pow = {pow := λ (x : with_zero α) (n : ℤ), with_zero.int.has_pow._match_1 x n}
with_zero.int.has_pow._match_1 (some x) n = ↑(x ^ n)
with_zero.int.has_pow._match_1 none -[1+ n] = 0
with_zero.int.has_pow._match_1 none (int.of_nat n.succ) = 0
with_zero.int.has_pow._match_1 none (int.of_nat 0) = 1

@[simp, norm_cast]

theorem with_zero.coe_zpow {α : Type u} [div_inv_monoid α] {a : α} (n : ℤ) :

↑(a ^ n) = ↑a ^ n

@[protected, instance]

def with_zero.div_inv_monoid {α : Type u} [div_inv_monoid α] :

div_inv_monoid (with_zero α)

Equations

with_zero.div_inv_monoid = {mul := monoid_with_zero.mul with_zero.monoid_with_zero, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, npow := monoid_with_zero.npow with_zero.monoid_with_zero, npow_zero' := _, npow_succ' := _, inv := has_inv.inv with_zero.has_inv, div := has_div.div with_zero.has_div, div_eq_mul_inv := _, zpow := λ (n : ℤ) (x : with_zero α), x ^ n, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}

@[simp]

theorem with_zero.inv_one {α : Type u} [group α] :

@[protected, instance]

def with_zero.group_with_zero {α : Type u} [group α] :

group_with_zero (with_zero α)

if G is a group then with_zero G is a group with zero.

Equations

with_zero.group_with_zero = {mul := monoid_with_zero.mul with_zero.monoid_with_zero, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, npow := monoid_with_zero.npow with_zero.monoid_with_zero, npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero with_zero.monoid_with_zero, zero_mul := _, mul_zero := _, inv := div_inv_monoid.inv with_zero.div_inv_monoid, div := div_inv_monoid.div with_zero.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow with_zero.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

@[protected, instance]

def with_zero.comm_group_with_zero {α : Type u} [comm_group α] :

comm_group_with_zero (with_zero α)

Equations

with_zero.comm_group_with_zero = {mul := group_with_zero.mul with_zero.group_with_zero, mul_assoc := _, one := group_with_zero.one with_zero.group_with_zero, one_mul := _, mul_one := _, npow := group_with_zero.npow with_zero.group_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := group_with_zero.zero with_zero.group_with_zero, zero_mul := _, mul_zero := _, inv := group_with_zero.inv with_zero.group_with_zero, div := group_with_zero.div with_zero.group_with_zero, div_eq_mul_inv := _, zpow := group_with_zero.zpow with_zero.group_with_zero, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

@[protected, instance]

def with_zero.semiring {α : Type u} [semiring α] :

semiring (with_zero α)

Equations

with_zero.semiring = {add := add_comm_monoid.add with_zero.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_zero.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_zero.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_class.mul with_zero.mul_zero_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid_with_zero.one with_zero.monoid_with_zero, one_mul := _, mul_one := _, npow := monoid_with_zero.npow with_zero.monoid_with_zero, npow_zero' := _, npow_succ' := _}