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 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 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
Instances For
    def WithOne (α : Type u_1) :
    Type u_1

    Add an extra element 1 to a type

    Equations
    Instances For
      instance WithOne.instReprWithZero {α : Type u} [Repr α] :
      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 α) → (Unitmotive none)((a : α) → motive (some a))motive o
      Equations
      Instances For
        instance WithZero.instReprWithZero {α : Type u} [Repr α] :
        Equations
        • One or more equations did not get rendered due to their size.
        instance WithOne.instReprWithOne {α : Type u} [Repr α] :
        Equations
        • One or more equations did not get rendered due to their size.
        instance WithZero.zero {α : Type u} :
        Equations
        • WithZero.zero = { zero := none }
        instance WithOne.one {α : Type u} :
        Equations
        • WithOne.one = { one := none }
        instance WithZero.add {α : Type u} [Add α] :
        Equations
        instance WithOne.mul {α : Type u} [Mul α] :
        Equations
        instance WithZero.neg {α : Type u} [Neg α] :
        Equations
        instance WithOne.inv {α : Type u} [Inv α] :
        Equations
        theorem WithZero.negZeroClass.proof_1 {α : Type u_1} [Neg α] :
        -0 = -0
        instance WithZero.negZeroClass {α : Type u} [Neg α] :
        Equations
        • WithZero.negZeroClass = let __src := WithZero.zero; let __src_1 := WithZero.neg; NegZeroClass.mk
        instance WithOne.invOneClass {α : Type u} [Inv α] :
        Equations
        • WithOne.invOneClass = let __src := WithOne.one; let __src_1 := WithOne.inv; InvOneClass.mk
        instance WithZero.inhabited {α : Type u} :
        Equations
        • WithZero.inhabited = { default := 0 }
        instance WithOne.inhabited {α : Type u} :
        Equations
        • WithOne.inhabited = { default := 1 }
        instance WithZero.nontrivial {α : Type u} [Nonempty α] :
        Equations
        • =
        instance WithOne.nontrivial {α : Type u} [Nonempty α] :
        Equations
        • =
        def WithZero.coe {α : Type u} :
        αWithZero α

        The canonical map from α into WithZero α

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

          The canonical map from α into WithOne α

          Equations
          • WithOne.coe = some
          Instances For
            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
            Instances For
              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
              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
                  abbrev WithZero.unzero.match_1 {α : Type u_1} (motive : (x : WithZero α) → x 0Sort 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.
                  Instances For
                    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
                      @[simp]
                      theorem WithZero.unzero_coe {α : Type u} {x : α} (hx : x 0) :
                      @[simp]
                      theorem WithOne.unone_coe {α : Type u} {x : α} (hx : x 1) :
                      abbrev WithZero.coe_unzero.match_1 {α : Type u_1} (motive : (x : WithZero α) → x 0Prop) :
                      ∀ (x : WithZero α) (x_1 : x 0), (∀ (x : α) (x_2 : x 0), motive (some x) x_2)motive x x_1
                      Equations
                      • =
                      Instances For
                        @[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
                        instance WithZero.addZeroClass {α : Type u} [Add α] :
                        Equations
                        theorem WithZero.addZeroClass.proof_1 {α : Type u_1} [Add α] (a : Option α) :
                        Option.liftOrGet (fun (x x_1 : α) => x + x_1) none a = a
                        theorem WithZero.addZeroClass.proof_2 {α : Type u_1} [Add α] (a : Option α) :
                        Option.liftOrGet (fun (x x_1 : α) => x + x_1) a none = a
                        instance WithOne.mulOneClass {α : Type u} [Mul α] :
                        Equations
                        @[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
                        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
                        • =
                        Instances For
                          theorem WithZero.addMonoid.proof_1 {α : Type u_1} [AddSemigroup α] (a : WithZero α) (b : WithZero α) (c : WithZero α) :
                          a + b + c = a + (b + c)
                          theorem WithZero.addMonoid.proof_2 {α : Type u_1} [AddSemigroup α] (a : WithZero α) :
                          0 + a = a
                          theorem WithZero.addMonoid.proof_4 {α : Type u_1} [AddSemigroup α] :
                          ∀ (x : WithZero α), nsmulRec 0 x = nsmulRec 0 x
                          theorem WithZero.addMonoid.proof_3 {α : Type u_1} [AddSemigroup α] (a : WithZero α) :
                          a + 0 = a
                          Equations
                          • WithZero.addMonoid = let __spread.0 := WithZero.addZeroClass; AddMonoid.mk nsmulRec
                          instance WithOne.monoid {α : Type u} [Semigroup α] :
                          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))(Unitmotive none none)motive a b
                          Equations
                          • =
                          Instances For
                            Equations
                            theorem WithZero.addCommMonoid.proof_1 {α : Type u_1} [AddCommSemigroup α] (a : WithZero α) (b : WithZero α) :
                            a + b = b + a
                            Equations
                            @[simp]
                            theorem WithZero.coe_neg {α : Type u} [Neg α] (a : α) :
                            (-a) = -a
                            @[simp]
                            theorem WithOne.coe_inv {α : Type u} [Inv α] (a : α) :
                            a⁻¹ = (a)⁻¹
                            instance WithZero.one {α : Type u} [one : One α] :
                            Equations
                            • WithZero.one = { one := One.one }
                            @[simp]
                            theorem WithZero.coe_one {α : Type u} [One α] :
                            1 = 1
                            instance WithZero.mulZeroClass {α : Type u} [Mul α] :
                            Equations
                            @[simp]
                            theorem WithZero.coe_mul {α : Type u} [Mul α] {a : α} {b : α} :
                            (a * b) = a * b
                            Equations
                            • =
                            Equations
                            Equations
                            • WithZero.commSemigroup = let __src := WithZero.semigroupWithZero; CommSemigroup.mk
                            Equations
                            • WithZero.mulZeroOneClass = let __src := WithZero.mulZeroClass; let __src_1 := WithZero.one; MulZeroOneClass.mk
                            instance WithZero.pow {α : Type u} [One α] [Pow α ] :
                            Equations
                            • WithZero.pow = { pow := fun (x : WithZero α) (n : ) => match x, n with | none, 0 => 1 | none, Nat.succ n => 0 | some x, n => (x ^ n) }
                            @[simp]
                            theorem WithZero.coe_pow {α : Type u} [One α] [Pow α ] {a : α} (n : ) :
                            (a ^ n) = a ^ n
                            Equations
                            • WithZero.monoidWithZero = let __src := WithZero.mulZeroOneClass; let __src_1 := WithZero.semigroupWithZero; MonoidWithZero.mk
                            Equations
                            • WithZero.commMonoidWithZero = let __src := WithZero.monoidWithZero; let __src_1 := WithZero.commSemigroup; CommMonoidWithZero.mk
                            instance WithZero.inv {α : Type u} [Inv α] :

                            Given an inverse operation on α there is an inverse operation on WithZero α sending 0 to 0.

                            Equations
                            @[simp]
                            theorem WithZero.coe_inv {α : Type u} [Inv α] (a : α) :
                            a⁻¹ = (a)⁻¹
                            @[simp]
                            theorem WithZero.inv_zero {α : Type u} [Inv α] :
                            0⁻¹ = 0
                            Equations
                            • WithZero.invOneClass = let __src := WithZero.one; let __src_1 := WithZero.inv; InvOneClass.mk
                            instance WithZero.div {α : Type u} [Div α] :
                            Equations
                            theorem WithZero.coe_div {α : Type u} [Div α] (a : α) (b : α) :
                            (a / b) = a / b
                            instance WithZero.instPowWithZeroInt {α : Type u} [One α] [Pow α ] :
                            Equations
                            • One or more equations did not get rendered due to their size.
                            @[simp]
                            theorem WithZero.coe_zpow {α : Type u} [DivInvMonoid α] {a : α} (n : ) :
                            (a ^ n) = a ^ n
                            Equations
                            • WithZero.divInvMonoid = let __src := WithZero.div; let __src_1 := WithZero.inv; let __src_2 := WithZero.monoidWithZero; DivInvMonoid.mk (fun (n : ) (x : WithZero α) => x ^ n)
                            Equations
                            • WithZero.divInvOneMonoid = let __src := WithZero.divInvMonoid; let __src_1 := WithZero.invOneClass; DivInvOneMonoid.mk

                            if G is a group then WithZero G is a group with zero.

                            Equations
                            • WithZero.groupWithZero = let __src := WithZero.monoidWithZero; let __src_1 := WithZero.divInvMonoid; let __src_2 := ; GroupWithZero.mk DivInvMonoid.zpow
                            Equations
                            • WithZero.commGroupWithZero = let __src := WithZero.groupWithZero; let __src_1 := WithZero.commMonoidWithZero; CommGroupWithZero.mk GroupWithZero.zpow
                            Equations
                            • WithZero.addMonoidWithOne = let __src := WithZero.addMonoid; let __src_1 := WithZero.one; AddMonoidWithOne.mk