doc-next-gen

Mathlib.Algebra.Group.WithOne.Defs

Module docstring

{"# 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)

TODO

WithOne.coe_mul and WithZero.coe_mul have inconsistent use of implicit parameters "}

WithOne definition
(α)
Full source 
/-- Add an extra element `1` to a type -/
@[to_additive "Add an extra element `0` to a type"]
def WithOne (α) :=
  Option α
Type with adjoined one element
Informal description
The type `WithOne α` is defined as the option type of `α`, which adjoins an extra element `1` to the type `α`. This construction is used to extend a semigroup to a monoid by adding a multiplicative identity element.
WithOne.instMonad instance
: Monad WithOne
Full source 
@[to_additive]
instance instMonad : Monad WithOne :=
  instMonadOption
Monad Structure on `WithOne`
Informal description
The type constructor `WithOne` forms a monad, where `WithOne α` adjoins a multiplicative identity element to the type `α`.
WithOne.instOne instance
: One (WithOne α)
Full source 
@[to_additive]
instance instOne : One (WithOne α) :=
  ⟨none⟩
The One Element in `WithOne α`
Informal description
The type `WithOne α` has a distinguished element `1` that serves as the multiplicative identity when `α` is extended to a monoid.
WithOne.instMul instance
[Mul α] : Mul (WithOne α)
Full source 
@[to_additive]
instance instMul [Mul α] : Mul (WithOne α) :=
  ⟨Option.merge (· * ·)⟩
Multiplication Operation on Type with Adjoined One
Informal description
For any type $\alpha$ with a multiplication operation, the type $\text{WithOne}\ \alpha$ (which adjoins a multiplicative identity element to $\alpha$) inherits a multiplication operation that extends the original operation on $\alpha$ and makes the adjoined element act as an identity.
WithOne.instInv instance
[Inv α] : Inv (WithOne α)
Full source 
@[to_additive]
instance instInv [Inv α] : Inv (WithOne α) :=
  ⟨fun a => Option.map Inv.inv a⟩
Inversion Operation on Type with Adjoined One
Informal description
For any type $\alpha$ equipped with an inversion operation, the type `WithOne α` (obtained by adjoining a multiplicative identity to $\alpha$) inherits an inversion operation that extends the inversion on $\alpha$ and satisfies $1^{-1} = 1$.
WithOne.instInvOneClass instance
[Inv α] : InvOneClass (WithOne α)
Full source 
@[to_additive]
instance instInvOneClass [Inv α] : InvOneClass (WithOne α) :=
  { WithOne.instOne, WithOne.instInv with inv_one := rfl }
Inverse of One is One in Adjoined One Structure
Informal description
For any type $\alpha$ equipped with an inversion operation, the type $\text{WithOne}\ \alpha$ (obtained by adjoining a multiplicative identity to $\alpha$) satisfies $1^{-1} = 1$.
WithOne.inhabited instance
: Inhabited (WithOne α)
Full source 
@[to_additive]
instance inhabited : Inhabited (WithOne α) :=
  ⟨1⟩
Inhabitedness of Type with Adjoined One
Informal description
The type `WithOne α` obtained by adjoining a multiplicative identity to a type `α` is always inhabited, meaning it contains at least one element (the adjoined identity).
WithOne.instNontrivial instance
[Nonempty α] : Nontrivial (WithOne α)
Full source 
@[to_additive]
instance instNontrivial [Nonempty α] : Nontrivial (WithOne α) :=
  Option.nontrivial
Nontriviality of Type with Adjoined One Element
Informal description
For any nonempty type $\alpha$, the type $\text{WithOne}\ \alpha$ obtained by adjoining a multiplicative identity to $\alpha$ is nontrivial (contains at least two distinct elements).
WithOne.coe definition
: α → WithOne α
Full source 
/-- The canonical map from `α` into `WithOne α` -/
@[to_additive (attr := coe) "The canonical map from `α` into `WithZero α`"]
def coe : α → WithOne α :=
  Option.some
Embedding into $\text{WithOne}\ \alpha$
Informal description
The canonical embedding function from a type $\alpha$ to $\text{WithOne}\ \alpha$, which maps each element $a \in \alpha$ to its corresponding element in $\text{WithOne}\ \alpha$ (represented as $\text{some}\ a$).
WithOne.instCoeTC instance
: CoeTC α (WithOne α)
Full source 
@[to_additive]
instance instCoeTC : CoeTC α (WithOne α) :=
  ⟨coe⟩
Canonical Embedding into Type with Adjoined One Element
Informal description
For any type $\alpha$, there is a canonical embedding of $\alpha$ into $\text{WithOne}\ \alpha$ that maps each element $a \in \alpha$ to its corresponding element in $\text{WithOne}\ \alpha$.
WithZero.recZeroCoe definition
{motive : WithZero α → Sort*} (zero : motive 0) (coe : ∀ a : α, motive a) : ∀ n : WithZero α, motive n
Full source 
/-- Recursor for `WithZero` using the preferred forms `0` and `↑a`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
def _root_.WithZero.recZeroCoe {motive : WithZero α → Sort*} (zero : motive 0)
    (coe : ∀ a : α, motive a) : ∀ n : WithZero α, motive n
  | Option.none => zero
  | Option.some x => coe x
Recursor for type with adjoined zero
Informal description
The recursor for `WithZero α` allows defining a function on `WithZero α` by specifying its value at `0` (the adjoined zero element) and its value on elements of `α` (via the canonical embedding `↑a`). Given: - A type family `motive : WithZero α → Sort*` - A term `zero : motive 0` for the zero case - A function `coe : ∀ a : α, motive (↑a)` for the embedded elements The recursor produces a function `f : ∀ n : WithZero α, motive n` that satisfies: - `f 0 = zero` - `f (↑a) = coe a` for any `a : α`
WithOne.recOneCoe definition
{motive : WithOne α → Sort*} (one : motive 1) (coe : ∀ a : α, motive a) : ∀ n : WithOne α, motive n
Full source 
/-- Recursor for `WithOne` using the preferred forms `1` and `↑a`. -/
@[to_additive existing, elab_as_elim, induction_eliminator, cases_eliminator]
def recOneCoe {motive : WithOne α → Sort*} (one : motive 1) (coe : ∀ a : α, motive a) :
    ∀ n : WithOne α, motive n
  | Option.none => one
  | Option.some x => coe x
Recursor for type with adjoined one element
Informal description
The recursor for `WithOne α` allows defining a function on `WithOne α` by specifying its value at `1` (the adjoined one element) and its value on elements of `α$ (via the canonical embedding `↑a`). Given: - A type family `motive : WithOne α → Sort*` - A term `one : motive 1` for the one case - A function `coe : ∀ a : α, motive (↑a)` for the embedded elements The recursor produces a function `f : ∀ n : WithOne α, motive n` that satisfies: - `f 1 = one` - `f (↑a) = coe a` for any `a : α`
WithOne.recOneCoe_one theorem
{motive : WithOne α → Sort*} (h₁ h₂) : recOneCoe h₁ h₂ (1 : WithOne α) = (h₁ : motive 1)
Full source 
@[to_additive (attr := simp)]
lemma recOneCoe_one {motive : WithOne α → Sort*} (h₁ h₂) :
    recOneCoe h₁ h₂ (1 : WithOne α) = (h₁ : motive 1) :=
  rfl
Recursor property for the one element in `WithOne α`
Informal description
For any type family `motive : WithOne α → Sort*`, given a term `h₁ : motive 1` and a function `h₂ : ∀ a : α, motive a`, the recursor `recOneCoe` satisfies `recOneCoe h₁ h₂ 1 = h₁`.
WithOne.recOneCoe_coe theorem
{motive : WithOne α → Sort*} (h₁ h₂) (a : α) : recOneCoe h₁ h₂ (a : WithOne α) = (h₂ : ∀ a : α, motive a) a
Full source 
@[to_additive (attr := simp)]
lemma recOneCoe_coe {motive : WithOne α → Sort*} (h₁ h₂) (a : α) :
    recOneCoe h₁ h₂ (a : WithOne α) = (h₂ : ∀ a : α, motive a) a :=
  rfl
Recursor Property for Embedded Elements in `WithOne α`
Informal description
For any type family `motive : WithOne α → Sort*`, given a term `h₁ : motive 1` and a function `h₂ : ∀ a : α, motive a`, the recursor `recOneCoe` satisfies `recOneCoe h₁ h₂ (a : WithOne α) = h₂ a` for any `a : α`.
WithOne.unone definition
: ∀ {x : WithOne α}, x ≠ 1 → α
Full source 
/-- Deconstruct an `x : WithOne α` to the underlying value in `α`, given a proof that `x ≠ 1`. -/
@[to_additive unzero
      "Deconstruct an `x : WithZero α` to the underlying value in `α`, given a proof that `x ≠ 0`."]
def unone : ∀ {x : WithOne α}, x ≠ 1 → α | (x : α), _ => x
Underlying value in $\alpha$ of a non-one element in `WithOne α`
Informal description
Given an element $x$ of type `WithOne α` (which is `α` with an adjoined one element) and a proof that $x \neq 1$, the function returns the underlying value of $x$ in $\alpha$. For any $x \in \alpha$, if $x$ is coerced to `WithOne α` and is not equal to $1$, then applying this function returns $x$ itself.
WithOne.unone_coe theorem
{x : α} (hx : (x : WithOne α) ≠ 1) : unone hx = x
Full source 
@[to_additive (attr := simp) unzero_coe]
theorem unone_coe {x : α} (hx : (x : WithOne α) ≠ 1) : unone hx = x :=
  rfl
Embedded Element Equals Its Underlying Value in $\text{WithOne}\ \alpha$
Informal description
For any element $x$ of type $\alpha$, if the canonical embedding of $x$ into $\text{WithOne}\ \alpha$ is not equal to $1$, then the underlying value of this embedded element (obtained via $\text{unone}$) is equal to $x$ itself.
WithOne.coe_unone theorem
: ∀ {x : WithOne α} (hx : x ≠ 1), unone hx = x
Full source 
@[to_additive (attr := simp) coe_unzero]
lemma coe_unone : ∀ {x : WithOne α} (hx : x ≠ 1), unone hx = x
  | (x : α), _ => rfl
Equality of Underlying Value and Original Element in $\text{WithOne}\ \alpha$
Informal description
For any element $x$ of type $\text{WithOne}\ \alpha$ such that $x \neq 1$, the underlying value of $x$ in $\alpha$ (obtained via $\text{unone}$) is equal to $x$ itself.
WithOne.coe_ne_one theorem
{a : α} : (a : WithOne α) ≠ (1 : WithOne α)
Full source 
@[to_additive (attr := simp)]
theorem coe_ne_one {a : α} : (a : WithOne α) ≠ (1 : WithOne α) :=
  Option.some_ne_none a
Non-identity Property of Embedded Elements in $\text{WithOne}\ \alpha$
Informal description
For any element $a$ of type $\alpha$, the canonical embedding of $a$ into $\text{WithOne}\ \alpha$ is not equal to the multiplicative identity $1$ in $\text{WithOne}\ \alpha$.
WithOne.one_ne_coe theorem
{a : α} : (1 : WithOne α) ≠ a
Full source 
@[to_additive (attr := simp)]
theorem one_ne_coe {a : α} : (1 : WithOne α) ≠ a :=
  coe_ne_one.symm
Identity Not Equal to Embedded Element in $\text{WithOne}\ \alpha$
Informal description
For any element $a$ of type $\alpha$, the multiplicative identity $1$ in $\text{WithOne}\ \alpha$ is not equal to the canonical embedding of $a$ into $\text{WithOne}\ \alpha$.
WithOne.ne_one_iff_exists theorem
{x : WithOne α} : x ≠ 1 ↔ ∃ a : α, ↑a = x
Full source 
@[to_additive]
theorem ne_one_iff_exists {x : WithOne α} : x ≠ 1x ≠ 1 ↔ ∃ a : α, ↑a = x :=
  Option.ne_none_iff_exists
Characterization of Non-Identity Elements in $\text{WithOne}\ \alpha$
Informal description
For any element $x$ in $\text{WithOne}\ \alpha$, $x$ is not equal to the multiplicative identity $1$ if and only if there exists an element $a \in \alpha$ such that the canonical embedding of $a$ into $\text{WithOne}\ \alpha$ equals $x$.
WithOne.instCanLift instance
: CanLift (WithOne α) α (↑) fun a => a ≠ 1
Full source 
@[to_additive]
instance instCanLift : CanLift (WithOne α) α (↑) fun a => a ≠ 1 where
  prf _ := ne_one_iff_exists.1
Lifting Condition for $\text{WithOne}\ \alpha$ to $\alpha$
Informal description
For any type $\alpha$, there is a lifting condition from $\text{WithOne}\ \alpha$ to $\alpha$ via the canonical embedding function, where an element of $\text{WithOne}\ \alpha$ can be lifted to $\alpha$ if and only if it is not equal to the multiplicative identity $1$.
WithOne.coe_inj theorem
{a b : α} : (a : WithOne α) = b ↔ a = b
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_inj {a b : α} : (a : WithOne α) = b ↔ a = b :=
  Option.some_inj
Injectivity of the canonical embedding into $\text{WithOne}\ \alpha$
Informal description
For any elements $a, b$ in a type $\alpha$, the canonical embeddings of $a$ and $b$ into $\text{WithOne}\ \alpha$ are equal if and only if $a = b$ in $\alpha$.
WithOne.cases_on theorem
{P : WithOne α → Prop} : ∀ x : WithOne α, P 1 → (∀ a : α, P a) → P x
Full source 
@[to_additive (attr := elab_as_elim)]
protected theorem cases_on {P : WithOne α → Prop} : ∀ x : WithOne α, P 1 → (∀ a : α, P a) → P x :=
  Option.casesOn
Case Analysis Principle for $\text{WithOne}\ \alpha$
Informal description
For any predicate $P$ on $\text{WithOne}\ \alpha$ and any element $x \in \text{WithOne}\ \alpha$, if $P(1)$ holds and $P(a)$ holds for all $a \in \alpha$, then $P(x)$ holds.
WithOne.instMulOneClass instance
[Mul α] : MulOneClass (WithOne α)
Full source 
@[to_additive]
instance instMulOneClass [Mul α] : MulOneClass (WithOne α) where
  mul := (· * ·)
  one := 1
  one_mul := (Option.lawfulIdentity_merge _).left_id
  mul_one := (Option.lawfulIdentity_merge _).right_id
Multiplicative Structure with Identity on $\text{WithOne}\ \alpha$
Informal description
For any type $\alpha$ equipped with a multiplication operation, the type $\text{WithOne}\ \alpha$ (obtained by adjoining a multiplicative identity element to $\alpha$) forms a multiplicative structure with identity. This means that the multiplication operation on $\text{WithOne}\ \alpha$ extends the original operation on $\alpha$ and satisfies the identity laws $1 * a = a$ and $a * 1 = a$ for all $a \in \text{WithOne}\ \alpha$.
WithOne.coe_mul theorem
[Mul α] (a b : α) : (↑(a * b) : WithOne α) = a * b
Full source 
@[to_additive (attr := simp, norm_cast)]
lemma coe_mul [Mul α] (a b : α) : (↑(a * b) : WithOne α) = a * b := rfl
Embedding Preserves Multiplication in $\text{WithOne}\ \alpha$
Informal description
For any type $\alpha$ with a multiplication operation, and for any elements $a, b \in \alpha$, the canonical embedding of the product $a * b$ into $\text{WithOne}\ \alpha$ is equal to the product of the embeddings of $a$ and $b$ in $\text{WithOne}\ \alpha$. In other words, $\uparrow(a * b) = \uparrow a * \uparrow b$.
WithOne.instMonoid instance
[Semigroup α] : Monoid (WithOne α)
Full source 
@[to_additive]
instance instMonoid [Semigroup α] : Monoid (WithOne α) where
  __ := instMulOneClass
  mul_assoc
    | 1, b, c => by simp
    | (a : α), 1, c => by simp
    | (a : α), (b : α), 1 => by simp
    | (a : α), (b : α), (c : α) => by simp_rw [← coe_mul, mul_assoc]
Monoid Structure on $\text{WithOne}\ \alpha$ for a Semigroup $\alpha$
Informal description
For any semigroup $\alpha$, the type $\text{WithOne}\ \alpha$ (obtained by adjoining a multiplicative identity element to $\alpha$) forms a monoid. The multiplication operation extends the original operation on $\alpha$ and satisfies the identity laws $1 \cdot a = a \cdot 1 = a$ for all $a \in \text{WithOne}\ \alpha$.
WithOne.instCommMonoid instance
[CommSemigroup α] : CommMonoid (WithOne α)
Full source 
@[to_additive]
instance instCommMonoid [CommSemigroup α] : CommMonoid (WithOne α) where
  mul_comm
    | (a : α), (b : α) => congr_arg some (mul_comm a b)
    | (_ : α), 1 => rfl
    | 1, (_ : α) => rfl
    | 1, 1 => rfl
Commutative Monoid Structure on $\text{WithOne}\ \alpha$ for a Commutative Semigroup $\alpha$
Informal description
For any commutative semigroup $\alpha$, the type $\text{WithOne}\ \alpha$ (obtained by adjoining a multiplicative identity element to $\alpha$) forms a commutative monoid. The multiplication operation extends the original commutative operation on $\alpha$ and satisfies the identity laws $1 \cdot a = a \cdot 1 = a$ for all $a \in \text{WithOne}\ \alpha$.
WithOne.coe_inv theorem
[Inv α] (a : α) : ((a⁻¹ : α) : WithOne α) = (a : WithOne α)⁻¹
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : WithOne α) = (a : WithOne α)⁻¹ :=
  rfl
Inversion Commutes with Embedding in $\text{WithOne}\ \alpha$
Informal description
For any type $\alpha$ equipped with an inversion operation and any element $a \in \alpha$, the canonical embedding of the inverse of $a$ into $\text{WithOne}\ \alpha$ is equal to the inverse of the canonical embedding of $a$ in $\text{WithOne}\ \alpha$. That is, $(a^{-1} : \text{WithOne}\ \alpha) = (a : \text{WithOne}\ \alpha)^{-1}$.