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.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

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

      Add an extra element 0 to a type

      Equations
        Instances For
          instance WithZero.instRepr {α : Type u} [Repr α] :
          Equations
            instance WithOne.instRepr {α : Type u} [Repr α] :
            Equations
              instance WithOne.instOne {α : Type u} :
              Equations
                instance WithZero.instZero {α : Type u} :
                Equations
                  instance WithOne.instMul {α : Type u} [Mul α] :
                  Equations
                    instance WithZero.instAdd {α : Type u} [Add α] :
                    Equations
                      instance WithOne.instInv {α : Type u} [Inv α] :
                      Equations
                        instance WithZero.instNeg {α : Type u} [Neg α] :
                        Equations
                          instance WithOne.instInvOneClass {α : Type u} [Inv α] :
                          Equations
                            Equations
                              instance WithOne.inhabited {α : Type u} :
                              Equations
                                instance WithZero.inhabited {α : Type u} :
                                Equations
                                  def WithOne.coe {α : Type u} :
                                  αWithOne α

                                  The canonical map from α into WithOne α

                                  Equations
                                    Instances For
                                      def WithZero.coe {α : Type u} :
                                      αWithZero α

                                      The canonical map from α into WithZero α

                                      Equations
                                        Instances For
                                          instance WithOne.instCoeTC {α : Type u} :
                                          CoeTC α (WithOne α)
                                          Equations
                                            instance WithZero.instCoeTC {α : Type u} :
                                            CoeTC α (WithZero α)
                                            Equations
                                              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.

                                              Equations
                                                Instances For
                                                  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.

                                                  Equations
                                                    Instances For
                                                      @[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.

                                                      Equations
                                                        Instances For
                                                          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
                                                            Instances For
                                                              @[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.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.instMulOneClass {α : Type u} [Mul α] :
                                                              Equations
                                                                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.instMonoid {α : Type u} [Semigroup α] :
                                                                  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