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

def WithOne (α : Type u_1) : Type u_1

Add an extra element 1 to a type

def WithZero (α : Type u_1) : Type u_1

Add an extra element 0 to a type

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance WithOne.instMonad : Monad WithOne

@[instance_reducible]

instance WithZero.instMonad : Monad WithZero

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

instance WithOne.instNontrivial {α : Type u} [Nonempty α] : Nontrivial (WithOne α)

instance WithZero.instNontrivial {α : Type u} [Nonempty α] : Nontrivial (WithZero α)

instance WithOne.instSubsingletonOfIsEmpty {α : Type u} [IsEmpty α] : Subsingleton (WithOne α)

instance WithZero.instSubsingletonOfIsEmpty {α : Type u} [IsEmpty α] : Subsingleton (WithZero α)

@[match_pattern]

def WithOne.coe {α : Type u} : α → WithOne α

The canonical map from α into WithOne α

@[match_pattern]

def WithZero.coe {α : Type u} : α → WithZero α

The canonical map from α into WithZero α

@[instance_reducible]

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

@[instance_reducible]

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

theorem WithOne.forall {α : Type u} {p : WithOne α → Prop} : (∀ (x : WithOne α), p x) ↔ p 1 ∧ ∀ (a : α), p ↑a

theorem WithZero.forall {α : Type u} {p : WithZero α → Prop} : (∀ (x : WithZero α), p x) ↔ p 0 ∧ ∀ (a : α), p ↑a

theorem WithOne.exists {α : Type u} {p : WithOne α → Prop} : (∃ (x : WithOne α), p x) ↔ p 1 ∨ ∃ (a : α), p ↑a

theorem WithZero.exists {α : Type u} {p : WithZero α → Prop} : (∃ (x : WithZero α), p x) ↔ p 0 ∨ ∃ (a : α), p ↑a

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.

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.

@[simp]

theorem WithOne.recOneCoe_one {α : Type u} {motive : WithOne α → Sort u_1} (h₁ : motive 1) (h₂ : (a : α) → motive ↑a) : recOneCoe h₁ h₂ 1 = h₁

@[simp]

theorem WithZero.recZeroCoe_zero {α : Type u} {motive : WithZero α → Sort u_1} (h₁ : motive 0) (h₂ : (a : α) → motive ↑a) : recZeroCoe h₁ h₂ 0 = h₁

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

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

def WithOne.unone {α : Type u} {x : WithOne α} : x ≠ 1 → α

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

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

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

@[simp]

theorem WithOne.unone_coe {α : Type u} {x : α} (hx : ↑x ≠ 1) : unone hx = x

@[simp]

theorem WithZero.unzero_coe {α : Type u} {x : α} (hx : ↑x ≠ 0) : unzero hx = x

@[simp]

theorem WithOne.coe_unone {α : Type u} {x : WithOne α} (hx : x ≠ 1) : ↑(unone hx) = x

@[simp]

theorem WithZero.coe_unzero {α : Type u} {x : WithZero α} (hx : x ≠ 0) : ↑(unzero hx) = x

@[simp]

theorem WithOne.coe_ne_one {α : Type u} {a : α} : ↑a ≠ 1

@[simp]

theorem WithZero.coe_ne_zero {α : Type u} {a : α} : ↑a ≠ 0

@[simp]

theorem WithOne.one_ne_coe {α : Type u} {a : α} : 1 ≠ ↑a

@[simp]

theorem WithZero.zero_ne_coe {α : Type u} {a : α} : 0 ≠ ↑a

theorem WithOne.ne_one_iff_exists {α : Type u} {x : WithOne α} : x ≠ 1 ↔ ∃ (a : α), ↑a = x

theorem WithZero.ne_zero_iff_exists {α : Type u} {x : WithZero α} : x ≠ 0 ↔ ∃ (a : α), ↑a = x

instance WithOne.instCanLift {α : Type u} : CanLift (WithOne α) α coe fun (a : WithOne α) => a ≠ 1

instance WithZero.instCanLift {α : Type u} : CanLift (WithZero α) α coe fun (a : WithZero α) => a ≠ 0

@[simp]

theorem WithOne.coe_inj {α : Type u} {a b : α} : ↑a = ↑b ↔ a = b

@[simp]

theorem WithZero.coe_inj {α : Type u} {a b : α} : ↑a = ↑b ↔ a = b

theorem WithOne.coe_injective {α : Type u} : Function.Injective coe

theorem WithZero.coe_injective {α : Type u} : Function.Injective coe

theorem WithOne.cases_on {α : Type u} {P : WithOne α → Prop} (x : WithOne α) : P 1 → (∀ (a : α), P ↑a) → P x

theorem WithZero.cases_on {α : Type u} {P : WithZero α → Prop} (x : WithZero α) : P 0 → (∀ (a : α), P ↑a) → P x

@[instance_reducible]

instance WithOne.instMulOneClass {α : Type u} [Mul α] : MulOneClass (WithOne α)

@[instance_reducible]

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

@[simp]

theorem WithOne.coe_mul {α : Type u} [Mul α] (a b : α) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem WithZero.coe_add {α : Type u} [Add α] (a b : α) : ↑(a + b) = ↑a + ↑b

@[instance_reducible]

instance WithOne.instMonoid {α : Type u} [Semigroup α] : Monoid (WithOne α)

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[simp]

theorem WithOne.coe_inv {α : Type u} [Inv α] (a : α) : ↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem WithZero.coe_neg {α : Type u} [Neg α] (a : α) : ↑(-a) = -↑a

def WithOne.unoneD {α : Type u} (d : α) (x : WithOne α) : α

Specialization of Option.getD to values in WithOne α that respects API boundaries.

def WithZero.unzeroD {α : Type u} (d : α) (x : WithZero α) : α

Specialization of Option.getD to values in WithZero α that respects API boundaries.

@[simp]

theorem WithOne.unoneD_one {α : Type u} (d : α) : unoneD d 1 = d

@[simp]

theorem WithZero.unzeroD_zero {α : Type u} (d : α) : unzeroD d 0 = d

@[simp]

theorem WithOne.unoneD_coe {α : Type u} (d x : α) : unoneD d ↑x = x

@[simp]

theorem WithZero.unzeroD_coe {α : Type u} (d x : α) : unzeroD d ↑x = x

theorem WithOne.unoneD_eq_iff {α : Type u} {d y : α} {x : WithOne α} : unoneD d x = y ↔ x = ↑y ∨ x = 1 ∧ y = d

theorem WithZero.unzeroD_eq_iff {α : Type u} {d y : α} {x : WithZero α} : unzeroD d x = y ↔ x = ↑y ∨ x = 0 ∧ y = d

@[simp]

theorem WithOne.unoneD_eq_self_iff {α : Type u} {d : α} {x : WithOne α} : unoneD d x = d ↔ x = ↑d ∨ x = 1

@[simp]

theorem WithZero.unzeroD_eq_self_iff {α : Type u} {d : α} {x : WithZero α} : unzeroD d x = d ↔ x = ↑d ∨ x = 0

theorem WithOne.unoneD_eq_unoneD_iff {α : Type u} {d : α} {x y : WithOne α} : unoneD d x = unoneD d y ↔ x = y ∨ x = ↑d ∧ y = 1 ∨ x = 1 ∧ y = ↑d

theorem WithZero.unzeroD_eq_unzeroD_iff {α : Type u} {d : α} {x y : WithZero α} : unzeroD d x = unzeroD d y ↔ x = y ∨ x = ↑d ∧ y = 0 ∨ x = 0 ∧ y = ↑d

theorem WithOne.unoneD_eq_unone {α : Type u} {d : α} {x : WithOne α} (hx : x ≠ 1) : unoneD d x = unone hx

theorem WithZero.unzeroD_eq_unzero {α : Type u} {d : α} {x : WithZero α} (hx : x ≠ 0) : unzeroD d x = unzero hx