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 WithZero (α : Type u_1) : Type u_1

Add an extra element 0 to a type

Equations

• WithZero α = Option α

def WithOne (α : Type u_1) : Type u_1

Add an extra element 1 to a type

Equations

• WithOne α = Option α

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

Equations

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

abbrev WithZero.instReprWithZero.match_1 {α : Type u_1} (motive : WithZero α → Sort u_2) : (o : WithZero α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive o

Equations

• WithZero.instReprWithZero.match_1 motive o h_1 h_2 = Option.casesOn o (h_1 ()) fun (val : α) => h_2 val

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

Equations

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

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

Equations

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

instance WithZero.monad : Monad WithZero

Equations

• WithZero.monad = instMonadOption

instance WithOne.monad : Monad WithOne

Equations

• WithOne.monad = instMonadOption

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

Equations

• WithZero.zero = { zero := none }

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

Equations

• WithOne.one = { one := none }

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

Equations

• WithZero.add = { add := Option.liftOrGet fun (x x_1 : α) => x + x_1 }

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

Equations

• WithOne.mul = { mul := Option.liftOrGet fun (x x_1 : α) => x * x_1 }

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

Equations

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

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

Equations

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

theorem WithZero.negZeroClass.proof_1 {α : Type u_1} [Neg α] : -0 = -0

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

Equations

• WithZero.negZeroClass = let __src := WithZero.zero; let __src_1 := WithZero.neg; NegZeroClass.mk ⋯

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

Equations

• WithOne.invOneClass = let __src := WithOne.one; let __src_1 := WithOne.inv; InvOneClass.mk ⋯

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

Equations

• WithZero.inhabited = { default := 0 }

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

Equations

• WithOne.inhabited = { default := 1 }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

The canonical map from α into WithZero α

Equations

• WithZero.coe = some

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

The canonical map from α into WithOne α

Equations

• WithOne.coe = some

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

Equations

• WithZero.coeTC = { coe := WithZero.coe }

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

Equations

• WithOne.coeTC = { coe := WithOne.coe }

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

• WithZero.recZeroCoe h₁ h₂ x = WithZero.instReprWithZero.match_1 (fun (x : WithZero α) => C x) x (fun (_ : Unit) => h₁) fun (x : α) => h₂ x

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

• WithOne.recOneCoe h₁ h₂ x = match x with | none => h₁ | some x => h₂ x

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 = WithZero.unzero.match_1 (fun (x : WithZero α) (x : x ≠ 0) => α) x✝ x fun (x : α) (x_1 : ↑x ≠ 0) => x

abbrev WithZero.unzero.match_1 {α : Type u_1} (motive : (x : WithZero α) → x ≠ 0 → Sort u_2) : (x : WithZero α) → (x_1 : x ≠ 0) → ((x : α) → (x_2 : ↑x ≠ 0) → motive (some x) x_2) → motive x x_1

Equations

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

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 = match x✝, x with | some x, x_1 => x

@[simp]

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

@[simp]

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

abbrev WithZero.coe_unzero.match_1 {α : Type u_1} (motive : (x : WithZero α) → x ≠ 0 → Prop) : ∀ (x : WithZero α) (x_1 : x ≠ 0), (∀ (x : α) (x_2 : ↑x ≠ 0), motive (some x) x_2) → motive x x_1

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

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

theorem WithZero.addZeroClass.proof_2 {α : Type u_1} [Add α] (a : Option α) : Option.liftOrGet (fun (x x_1 : α) => x + x_1) a none = a

theorem WithZero.addZeroClass.proof_1 {α : Type u_1} [Add α] (a : Option α) : Option.liftOrGet (fun (x x_1 : α) => x + x_1) none a = a

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

Equations

• WithZero.addZeroClass = AddZeroClass.mk ⋯ ⋯

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

Equations

• WithOne.mulOneClass = MulOneClass.mk ⋯ ⋯

@[simp]

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

@[simp]

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

theorem WithZero.addMonoid.proof_5 {α : Type u_1} [AddSemigroup α] : ∀ (n : ℕ) (x : WithZero α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem WithZero.addMonoid.proof_2 {α : Type u_1} [AddSemigroup α] (a : WithZero α) : 0 + a = a

theorem WithZero.addMonoid.proof_3 {α : Type u_1} [AddSemigroup α] (a : WithZero α) : a + 0 = a

theorem WithZero.addMonoid.proof_4 {α : Type u_1} [AddSemigroup α] : ∀ (x : WithZero α), nsmulRec 0 x = nsmulRec 0 x

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

Equations

• WithZero.addMonoid = let __spread.0 := WithZero.addZeroClass; AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

abbrev WithZero.addMonoid.match_1 {α : Type u_1} (motive : WithZero α → WithZero α → WithZero α → Prop) : ∀ (a b c : WithZero α), (∀ (b c : WithZero α), motive none b c) → (∀ (a : α) (c : WithZero α), motive (some a) none c) → (∀ (a b : α), motive (some a) (some b) none) → (∀ (a b c : α), motive (some a) (some b) (some c)) → motive a b c

Equations

• ⋯ = ⋯

theorem WithZero.addMonoid.proof_1 {α : Type u_1} [AddSemigroup α] (a : WithZero α) (b : WithZero α) (c : WithZero α) : a + b + c = a + (b + c)

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

Equations

• WithOne.monoid = let __spread.0 := WithOne.mulOneClass; Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

abbrev WithZero.addCommMonoid.match_1 {α : Type u_1} (motive : WithZero α → WithZero α → Prop) : ∀ (a b : WithZero α), (∀ (a b : α), motive (some a) (some b)) → (∀ (val : α), motive (some val) none) → (∀ (val : α), motive none (some val)) → (Unit → motive none none) → motive a b

Equations

• ⋯ = ⋯

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

Equations

• WithZero.addCommMonoid = AddCommMonoid.mk ⋯

theorem WithZero.addCommMonoid.proof_1 {α : Type u_1} [AddCommSemigroup α] (a : WithZero α) (b : WithZero α) : a + b = b + a

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

Equations

• WithOne.commMonoid = CommMonoid.mk ⋯

@[simp]

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

@[simp]

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