Documentation

Mathlib.Algebra.Group.WithOne.Defs

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)

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

WithOne α = Option α

Instances For

def WithZero (α : Type u_1) :

Type u_1

Add an extra element 0 to a type

Equations

WithZero α = Option α

Instances For

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

Repr (WithZero α)

Equations

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

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 }

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

Repr (WithZero α)

Equations

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

instance WithOne.monad :

Equations

WithOne.monad = instMonadOption

instance WithZero.monad :

Equations

WithZero.monad = instMonadOption

instance WithOne.one {α : Type u} :

One (WithOne α)

Equations

WithOne.one = { one := none }

instance WithZero.zero {α : Type u} :

Zero (WithZero α)

Equations

WithZero.zero = { zero := none }

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

Mul (WithOne α)

Equations

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

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

Add (WithZero α)

Equations

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

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

Inv (WithOne α)

Equations

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

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

Neg (WithZero α)

Equations

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

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

InvOneClass (WithOne α)

Equations

WithOne.invOneClass = InvOneClass.mk ⋯

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

NegZeroClass (WithZero α)

Equations

WithZero.negZeroClass = NegZeroClass.mk ⋯

instance WithOne.inhabited {α : Type u} :

Inhabited (WithOne α)

Equations

WithOne.inhabited = { default := 1 }

instance WithZero.inhabited {α : Type u} :

Inhabited (WithZero α)

Equations

WithZero.inhabited = { default := 0 }

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

Nontrivial (WithOne α)

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

Nontrivial (WithZero α)

def WithOne.coe {α : Type u} :

α → WithOne α

The canonical map from α into WithOne α

Equations

WithOne.coe = some

Instances For

WithOne.canLift

def WithZero.coe {α : Type u} :

α → WithZero α

The canonical map from α into WithZero α

Equations

WithZero.coe = some

Instances For

WithZero.canLift

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

WithOne.recOneCoe h₁ h₂ none = h₁
WithOne.recOneCoe h₁ h₂ (some a) = h₂ a

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₂ none = h₁
WithZero.recZeroCoe h₁ h₂ (some a) = h₂ a

@[simp]

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

recOneCoe h₁ h₂ 1 = h₁

@[simp]

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

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

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

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

WithOne.unone x_3 = x_2

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

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

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

CanLift (WithOne α) α coe fun (a : WithOne α) => a ≠ 1

instance WithZero.canLift {α : 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.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 α] :

MulOneClass (WithOne α)

Equations

WithOne.mulOneClass = MulOneClass.mk ⋯ ⋯

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

AddZeroClass (WithZero α)

Equations

WithZero.addZeroClass = AddZeroClass.mk ⋯ ⋯

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

Monoid (WithOne α)

Equations

WithOne.monoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

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

AddMonoid (WithZero α)

Equations

WithZero.addMonoid = AddMonoid.mk ⋯ ⋯ nsmulRecAuto ⋯ ⋯

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

CommMonoid (WithOne α)

Equations

WithOne.commMonoid = CommMonoid.mk ⋯

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

AddCommMonoid (WithZero α)

Equations

WithZero.addCommMonoid = AddCommMonoid.mk ⋯

@[simp]

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

↑a⁻¹ = (↑a)⁻¹

@[simp]

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

↑(-a) = -↑a