# 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 `Mathlib/Algebra/Category/MonCat/Adjunctions.lean`.

Another result says that adjoining to a group an element `zero` gives a `GroupWithZero`. For more information about these structures (which are not that standard in informal mathematics, see `Mathlib/Algebra/GroupWithZero/Basic.lean`)

## TODO #

`WithOne.coe_mul` and `WithZero.coe_mul` have inconsistent use of implicit parameters

source
def WithOne (α : Type u_1) :
Type u_1

Add an extra element `1` to a type

Equations

- WithOne α = Option α

Instances For

source
def WithZero (α : Type u_1) :
Type u_1

Add an extra element `0` to a type

Equations

- WithZero α = Option α

Instances For

source
instance WithZero.instRepr {α : Type u} [Repr α] :
Repr (WithZero α)
Equations

- WithZero.instRepr = { reprPrec := fun (o : WithZero α) (x : ℕ) => match o with | none => Std.Format.text "0" | some a => Std.Format.text "↑" ++ repr a }

source
instance WithOne.instRepr {α : Type u} [Repr α] :
Repr (WithOne α)
Equations

- WithOne.instRepr = { reprPrec := fun (o : WithOne α) (x : ℕ) => match o with | none => Std.Format.text "1" | some a => Std.Format.text "↑" ++ repr a }

source
instance WithOne.instMonad :
Monad WithOne
Equations

- WithOne.instMonad = instMonadOption

source
instance WithZero.instMonad :
Monad WithZero
Equations

- WithZero.instMonad = instMonadOption

source
instance WithOne.instOne {α : Type u} :
One (WithOne α)
Equations

- WithOne.instOne = { one := none }

source
instance WithZero.instZero {α : Type u} :
Zero (WithZero α)
Equations

- WithZero.instZero = { zero := none }

source
instance WithOne.instMul {α : Type u} [Mul α] :
Mul (WithOne α)
Equations

- WithOne.instMul = { mul := Option.merge fun (x1 x2 : α) => x1 * x2 }

source
instance WithZero.instAdd {α : Type u} [Add α] :
Add (WithZero α)
Equations

- WithZero.instAdd = { add := Option.merge fun (x1 x2 : α) => x1 + x2 }

source
instance WithOne.instInv {α : Type u} [Inv α] :
Inv (WithOne α)
Equations

- WithOne.instInv = { inv := fun (a : WithOne α) => Option.map Inv.inv a }

source
instance WithZero.instNeg {α : Type u} [Neg α] :
Neg (WithZero α)
Equations

- WithZero.instNeg = { neg := fun (a : WithZero α) => Option.map Neg.neg a }

source
instance WithOne.instInvOneClass {α : Type u} [Inv α] :
InvOneClass (WithOne α)
Equations

- WithOne.instInvOneClass = { toOne := WithOne.instOne, toInv := WithOne.instInv, inv_one := ⋯ }

source
instance WithZero.instNegZeroClass {α : Type u} [Neg α] :
NegZeroClass (WithZero α)
Equations

- WithZero.instNegZeroClass = { toZero := WithZero.instZero, toNeg := WithZero.instNeg, neg_zero := ⋯ }

source
instance WithOne.inhabited {α : Type u} :
Inhabited (WithOne α)
Equations

- WithOne.inhabited = { default := 1 }

source
instance WithZero.inhabited {α : Type u} :
Inhabited (WithZero α)
Equations

- WithZero.inhabited = { default := 0 }

source
instance WithOne.instNontrivial {α : Type u} [Nonempty α] :
Nontrivial (WithOne α)
source
instance WithZero.instNontrivial {α : Type u} [Nonempty α] :
Nontrivial (WithZero α)
source
@[match_pattern]
def WithOne.coe {α : Type u} :
α → WithOne α

The canonical map from `α` into `WithOne α`

Equations

- WithOne.coe = some

Instances For

source
@[match_pattern]
def WithZero.coe {α : Type u} :
α → WithZero α

The canonical map from `α` into `WithZero α`

Equations

- WithZero.coe = some

Instances For

source
instance WithOne.instCoeTC {α : Type u} :
CoeTC α (WithOne α)
Equations

- WithOne.instCoeTC = { coe := WithOne.coe }

source
instance WithZero.instCoeTC {α : Type u} :
CoeTC α (WithZero α)
Equations

- WithZero.instCoeTC = { coe := WithZero.coe }

source
theorem WithOne.forall {α : Type u} {p : WithZero α → Prop} :
(∀ (x : WithZero α), p x) ↔ p 0 ∧ ∀ (a : α), p ↑a
source
theorem WithZero.forall {α : Type u} {p : WithZero α → Prop} :
(∀ (x : WithZero α), p x) ↔ p 0 ∧ ∀ (a : α), p ↑a
source
theorem WithOne.exists {α : Type u} {p : WithZero α → Prop} :
(∃ (x : WithZero α), p x) ↔ p 0 ∨ ∃ (a : α), p ↑a
source
theorem WithZero.exists {α : Type u} {p : WithZero α → Prop} :
(∃ (x : WithZero α), p x) ↔ p 0 ∨ ∃ (a : α), p ↑a
source
def WithZero.recZeroCoe {α : Type u} {motive : WithZero α → Sort u_1} (zero : motive 0) (coe : (a : α) → motive ↑a) (n : WithZero α) :
motive n

Recursor for `WithZero` using the preferred forms `0` and `↑a`.

Equations

- WithZero.recZeroCoe zero coe none = zero
- WithZero.recZeroCoe zero coe (some a) = coe a

Instances For

source
def WithOne.recOneCoe {α : Type u} {motive : WithOne α → Sort u_1} (one : motive 1) (coe : (a : α) → motive ↑a) (n : WithOne α) :
motive n

Recursor for `WithOne` using the preferred forms `1` and `↑a`.

Equations

- WithOne.recOneCoe one coe none = one
- WithOne.recOneCoe one coe (some a) = coe a

Instances For

source
@[simp]
theorem WithOne.recOneCoe_one {α : Type u} {motive : WithOne α → Sort u_1} (h₁ : motive 1) (h₂ : (a : α) → motive ↑a) :
recOneCoe h₁ h₂ 1 = h₁
source
@[simp]
theorem WithZero.recZeroCoe_zero {α : Type u} {motive : WithZero α → Sort u_1} (h₁ : motive 0) (h₂ : (a : α) → motive ↑a) :
recZeroCoe h₁ h₂ 0 = h₁
source
@[simp]
theorem WithOne.recOneCoe_coe {α : Type u} {motive : WithOne α → Sort u_1} (h₁ : motive 1) (h₂ : (a : α) → motive ↑a) (a : α) :
recOneCoe h₁ h₂ ↑a = h₂ a
source
@[simp]
theorem WithZero.recZeroCoe_coe {α : Type u} {motive : WithZero α → Sort u_1} (h₁ : motive 0) (h₂ : (a : α) → motive ↑a) (a : α) :
recZeroCoe h₁ h₂ ↑a = h₂ a
source
def WithOne.unone {α : Type u} {x : WithOne α} :
x ≠ 1 → α

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

Equations

- WithOne.unone x_3 = x_2

Instances For

source
def WithZero.unzero {α : Type u} {x : WithZero α} :
x ≠ 0 → α

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

Equations

- WithZero.unzero x_3 = x_2

Instances For

source
@[simp]
theorem WithOne.unone_coe {α : Type u} {x : α} (hx : ↑x ≠ 1) :
unone hx = x
source
@[simp]
theorem WithZero.unzero_coe {α : Type u} {x : α} (hx : ↑x ≠ 0) :
unzero hx = x
source
@[simp]
theorem WithOne.coe_unone {α : Type u} {x : WithOne α} (hx : x ≠ 1) :
↑(unone hx) = x
source
@[simp]
theorem WithZero.coe_unzero {α : Type u} {x : WithZero α} (hx : x ≠ 0) :
↑(unzero hx) = x
source
@[simp]
theorem WithOne.coe_ne_one {α : Type u} {a : α} :
↑a ≠ 1
source
@[simp]
theorem WithZero.coe_ne_zero {α : Type u} {a : α} :
↑a ≠ 0
source
@[simp]
theorem WithOne.one_ne_coe {α : Type u} {a : α} :
1 ≠ ↑a
source
@[simp]
theorem WithZero.zero_ne_coe {α : Type u} {a : α} :
0 ≠ ↑a
source
theorem WithOne.ne_one_iff_exists {α : Type u} {x : WithOne α} :
x ≠ 1 ↔ ∃ (a : α), ↑a = x
source
theorem WithZero.ne_zero_iff_exists {α : Type u} {x : WithZero α} :
x ≠ 0 ↔ ∃ (a : α), ↑a = x
source
instance WithOne.instCanLift {α : Type u} :
CanLift (WithOne α) α coe fun (a : WithOne α) => a ≠ 1
source
instance WithZero.instCanLift {α : Type u} :
CanLift (WithZero α) α coe fun (a : WithZero α) => a ≠ 0
source
@[simp]
theorem WithOne.coe_inj {α : Type u} {a b : α} :
↑a = ↑b ↔ a = b
source
@[simp]
theorem WithZero.coe_inj {α : Type u} {a b : α} :
↑a = ↑b ↔ a = b
source
theorem WithOne.coe_injective {α : Type u} :
Function.Injective coe
source
theorem WithZero.coe_injective {α : Type u} :
Function.Injective coe
source
theorem WithOne.cases_on {α : Type u} {P : WithOne α → Prop} (x : WithOne α) :
P 1 → (∀ (a : α), P ↑a) → P x
source
theorem WithZero.cases_on {α : Type u} {P : WithZero α → Prop} (x : WithZero α) :
P 0 → (∀ (a : α), P ↑a) → P x
source
instance WithOne.instMulOneClass {α : Type u} [Mul α] :
MulOneClass (WithOne α)
Equations

- WithOne.instMulOneClass = { toOne := WithOne.instOne, toMul := WithOne.instMul, one_mul := ⋯, mul_one := ⋯ }

source
instance WithZero.instAddZeroClass {α : Type u} [Add α] :
AddZeroClass (WithZero α)
Equations

- WithZero.instAddZeroClass = { toZero := WithZero.instZero, toAdd := WithZero.instAdd, zero_add := ⋯, add_zero := ⋯ }

source
@[simp]
theorem WithOne.coe_mul {α : Type u} [Mul α] (a b : α) :
↑(a * b) = ↑a * ↑b
source
@[simp]
theorem WithZero.coe_add {α : Type u} [Add α] (a b : α) :
↑(a + b) = ↑a + ↑b
source
instance WithOne.instMonoid {α : Type u} [Semigroup α] :
Monoid (WithOne α)
Equations

- One or more equations did not get rendered due to their size.

source
instance WithZero.instAddMonoid {α : Type u} [AddSemigroup α] :
AddMonoid (WithZero α)
Equations

- One or more equations did not get rendered due to their size.

source
instance WithOne.instCommMonoid {α : Type u} [CommSemigroup α] :
CommMonoid (WithOne α)
Equations

- WithOne.instCommMonoid = { toMonoid := WithOne.instMonoid, mul_comm := ⋯ }

source
instance WithZero.instAddCommMonoid {α : Type u} [AddCommSemigroup α] :
AddCommMonoid (WithZero α)
Equations

- WithZero.instAddCommMonoid = { toAddMonoid := WithZero.instAddMonoid, add_comm := ⋯ }

source
@[simp]
theorem WithOne.coe_inv {α : Type u} [Inv α] (a : α) :
↑a⁻¹ = (↑a)⁻¹
source
@[simp]
theorem WithZero.coe_neg {α : Type u} [Neg α] (a : α) :
↑(-a) = -↑a