Documentation

Mathlib.Algebra.Group.WithOne.Defs

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.

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)

Porting notes #

In Lean 3, we use id here and there to get correct types of proofs. This is required because WithOne and WithZero are marked as irreducible at the end of Mathlib.Algebra.Group.WithOne.Defs, so proofs that use Option α instead of WithOne α no longer typecheck. In Lean 4, both types are plain defs, so we don't need these ids.

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

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

Add an extra element 0 to a type

Equations
instance WithOne.instReprWithZero {α : Type u} [Repr α] :
Equations
instance WithOne.instRepr {α : Type u} [Repr α] :
Equations
instance WithZero.instRepr {α : Type u} [Repr α] :
Equations
instance WithOne.one {α : Type u} :
Equations
  • WithOne.one = { one := none }
instance WithZero.zero {α : Type u} :
Equations
  • WithZero.zero = { zero := none }
instance WithOne.mul {α : Type u} [Mul α] :
Equations
instance WithZero.add {α : Type u} [Add α] :
Equations
instance WithOne.inv {α : Type u} [Inv α] :
Equations
instance WithZero.neg {α : Type u} [Neg α] :
Equations
instance WithOne.invOneClass {α : Type u} [Inv α] :
Equations
instance WithZero.negZeroClass {α : Type u} [Neg α] :
Equations
instance WithOne.inhabited {α : Type u} :
Equations
  • WithOne.inhabited = { default := 1 }
instance WithZero.inhabited {α : Type u} :
Equations
  • WithZero.inhabited = { default := 0 }
instance WithOne.nontrivial {α : Type u} [Nonempty α] :
Equations
  • =
instance WithZero.nontrivial {α : Type u} [Nonempty α] :
Equations
  • =
def WithOne.coe {α : Type u} :
αWithOne α

The canonical map from α into WithOne α

Equations
  • WithOne.coe = some
def WithZero.coe {α : Type u} :
αWithZero α

The canonical map from α into WithZero α

Equations
  • WithZero.coe = some
instance WithOne.coeTC {α : Type u} :
CoeTC α (WithOne α)
Equations
  • WithOne.coeTC = { coe := WithOne.coe }
instance WithZero.coeTC {α : Type u} :
CoeTC α (WithZero α)
Equations
  • WithZero.coeTC = { coe := WithZero.coe }
def WithOne.recOneCoe {α : Type u} {C : WithOne αSort u_1} (h₁ : C 1) (h₂ : (a : α) → C a) (n : WithOne α) :
C n

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

Equations
def WithZero.recZeroCoe {α : Type u} {C : WithZero αSort u_1} (h₁ : C 0) (h₂ : (a : α) → C a) (n : WithZero α) :
C n

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

Equations
@[simp]
theorem WithOne.recOneCoe_one {α : Type u} {C : WithOne αSort u_1} (h₁ : C 1) (h₂ : (a : α) → C a) :
WithOne.recOneCoe h₁ h₂ 1 = h₁
@[simp]
theorem WithZero.recZeroCoe_zero {α : Type u} {C : WithZero αSort u_1} (h₁ : C 0) (h₂ : (a : α) → C a) :
WithZero.recZeroCoe h₁ h₂ 0 = h₁
@[simp]
theorem WithOne.recOneCoe_coe {α : Type u} {C : WithOne αSort u_1} (h₁ : C 1) (h₂ : (a : α) → C a) (a : α) :
WithOne.recOneCoe h₁ h₂ a = h₂ a
@[simp]
theorem WithZero.recZeroCoe_coe {α : Type u} {C : WithZero αSort u_1} (h₁ : C 0) (h₂ : (a : α) → C a) (a : α) :
WithZero.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.

Equations
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
@[simp]
theorem WithOne.unone_coe {α : Type u} {x : α} (hx : x 1) :
@[simp]
theorem WithZero.unzero_coe {α : Type u} {x : α} (hx : x 0) :
@[simp]
theorem WithOne.coe_unone {α : Type u} {x : WithOne α} (hx : x 1) :
(WithOne.unone hx) = x
@[simp]
theorem WithZero.coe_unzero {α : Type u} {x : WithZero α} (hx : x 0) :
(WithZero.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.canLift {α : Type u} :
CanLift (WithOne α) α WithOne.coe fun (a : WithOne α) => a 1
Equations
  • =
instance WithZero.canLift {α : Type u} :
CanLift (WithZero α) α WithZero.coe fun (a : WithZero α) => a 0
Equations
  • =
@[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.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 WithOne.mulOneClass {α : Type u} [Mul α] :
Equations
instance WithZero.addZeroClass {α : Type u} [Add α] :
Equations
@[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 WithOne.monoid {α : Type u} [Semigroup α] :
Equations
  • WithOne.monoid = Monoid.mk npowRecAuto
Equations
Equations
Equations
@[simp]
theorem WithOne.coe_inv {α : Type u} [Inv α] (a : α) :
a⁻¹ = (↑a)⁻¹
@[simp]
theorem WithZero.coe_neg {α : Type u} [Neg α] (a : α) :
(-a) = -a