Documentation

Mathlib.Algebra.Category.Semigrp.Basic

Category instances for Mul, Add, Semigroup and AddSemigroup #

We introduce the bundled categories:

This closely follows Mathlib.Algebra.Category.MonCat.Basic.

TODO #

def MagmaCat :
Type (u + 1)

The category of magmas and magma morphisms.

Equations
Instances For
    def AddMagmaCat :
    Type (u + 1)

    The category of additive magmas and additive magma morphisms.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      Instances For
        Equations
        Instances For
          instance MagmaCat.instMulα (X : MagmaCat) :
          Mul X
          Equations
          • X.instMulα = X.str
          Equations
          • X.instMulα = X.str
          instance MagmaCat.instFunLike (X Y : MagmaCat) :
          FunLike (X Y) X Y
          Equations
          instance AddMagmaCat.instFunLike (X Y : AddMagmaCat) :
          FunLike (X Y) X Y
          Equations
          instance MagmaCat.instMulHomClass (X Y : MagmaCat) :
          MulHomClass (X Y) X Y
          def MagmaCat.of (M : Type u) [Mul M] :

          Construct a bundled MagmaCat from the underlying type and typeclass.

          Equations
          Instances For

            Construct a bundled AddMagmaCat from the underlying type and typeclass.

            Equations
            Instances For
              @[simp]
              theorem MagmaCat.coe_of (R : Type u) [Mul R] :
              (MagmaCat.of R) = R
              @[simp]
              theorem AddMagmaCat.coe_of (R : Type u) [Add R] :
              (AddMagmaCat.of R) = R
              @[simp]
              theorem MagmaCat.mulEquiv_coe_eq {X Y : Type u_1} [Mul X] [Mul Y] (e : X ≃* Y) :
              e = e
              @[simp]
              theorem AddMagmaCat.addEquiv_coe_eq {X Y : Type u_1} [Add X] [Add Y] (e : X ≃+ Y) :
              e = e
              def MagmaCat.ofHom {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) :

              Typecheck a MulHom as a morphism in MagmaCat.

              Equations
              Instances For
                def AddMagmaCat.ofHom {X Y : Type u} [Add X] [Add Y] (f : X →ₙ+ Y) :

                Typecheck an AddHom as a morphism in AddMagmaCat.

                Equations
                Instances For
                  theorem MagmaCat.ofHom_apply {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) (x : X) :
                  (MagmaCat.ofHom f) x = f x
                  theorem AddMagmaCat.ofHom_apply {X Y : Type u} [Add X] [Add Y] (f : X →ₙ+ Y) (x : X) :
                  def Semigrp :
                  Type (u + 1)

                  The category of semigroups and semigroup morphisms.

                  Equations
                  Instances For
                    def AddSemigrp :
                    Type (u + 1)

                    The category of additive semigroups and semigroup morphisms.

                    Equations
                    Instances For
                      Equations
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          • X.instSemigroupα = X.str
                          Equations
                          • X.instSemigroupα = X.str
                          instance Semigrp.instFunLike (X Y : Semigrp) :
                          FunLike (X Y) X Y
                          Equations
                          instance AddSemigrp.instFunLike (X Y : AddSemigrp) :
                          FunLike (X Y) X Y
                          Equations
                          instance Semigrp.instMulHomClass (X Y : Semigrp) :
                          MulHomClass (X Y) X Y
                          def Semigrp.of (M : Type u) [Semigroup M] :

                          Construct a bundled Semigrp from the underlying type and typeclass.

                          Equations
                          Instances For

                            Construct a bundled AddSemigrp from the underlying type and typeclass.

                            Equations
                            Instances For
                              @[simp]
                              theorem Semigrp.coe_of (R : Type u) [Semigroup R] :
                              (Semigrp.of R) = R
                              @[simp]
                              theorem AddSemigrp.coe_of (R : Type u) [AddSemigroup R] :
                              (AddSemigrp.of R) = R
                              @[simp]
                              theorem Semigrp.mulEquiv_coe_eq {X Y : Type u_1} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
                              e = e
                              @[simp]
                              theorem AddSemigrp.addEquiv_coe_eq {X Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) :
                              e = e
                              def Semigrp.ofHom {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) :

                              Typecheck a MulHom as a morphism in Semigrp.

                              Equations
                              Instances For

                                Typecheck an AddHom as a morphism in AddSemigrp.

                                Equations
                                Instances For
                                  theorem Semigrp.ofHom_apply {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) (x : X) :
                                  (Semigrp.ofHom f) x = f x
                                  theorem AddSemigrp.ofHom_apply {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (f : X →ₙ+ Y) (x : X) :
                                  def MulEquiv.toMagmaCatIso {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) :

                                  Build an isomorphism in the category MagmaCat from a MulEquiv between Muls.

                                  Equations
                                  • e.toMagmaCatIso = { hom := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := , inv_hom_id := }
                                  Instances For

                                    Build an isomorphism in the category AddMagmaCat from an AddEquiv between Adds.

                                    Equations
                                    • e.toAddMagmaCatIso = { hom := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := , inv_hom_id := }
                                    Instances For
                                      @[simp]
                                      theorem AddEquiv.toAddMagmaCatIso_inv_apply {X Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) (a✝ : Y) :
                                      e.toAddMagmaCatIso.inv a✝ = e.symm.toFun a✝
                                      @[simp]
                                      theorem AddEquiv.toAddMagmaCatIso_hom_apply {X Y : Type u} [Add X] [Add Y] (e : X ≃+ Y) (a✝ : X) :
                                      e.toAddMagmaCatIso.hom a✝ = e.toFun a✝
                                      @[simp]
                                      theorem MulEquiv.toMagmaCatIso_hom_apply {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) (a✝ : X) :
                                      e.toMagmaCatIso.hom a✝ = e.toFun a✝
                                      @[simp]
                                      theorem MulEquiv.toMagmaCatIso_inv_apply {X Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) (a✝ : Y) :
                                      e.toMagmaCatIso.inv a✝ = e.symm.toFun a✝

                                      Build an isomorphism in the category Semigroup from a MulEquiv between Semigroups.

                                      Equations
                                      • e.toSemigrpIso = { hom := e.toMulHom, inv := e.symm.toMulHom, hom_inv_id := , inv_hom_id := }
                                      Instances For

                                        Build an isomorphism in the category AddSemigroup from an AddEquiv between AddSemigroups.

                                        Equations
                                        • e.toAddSemigrpIso = { hom := e.toAddHom, inv := e.symm.toAddHom, hom_inv_id := , inv_hom_id := }
                                        Instances For
                                          @[simp]
                                          theorem MulEquiv.toSemigrpIso_inv_apply {X Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) (a✝ : Y) :
                                          e.toSemigrpIso.inv a✝ = e.symm.toFun a✝
                                          @[simp]
                                          theorem AddEquiv.toAddSemigrpIso_hom_apply {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) (a✝ : X) :
                                          e.toAddSemigrpIso.hom a✝ = e.toFun a✝
                                          @[simp]
                                          theorem MulEquiv.toSemigrpIso_hom_apply {X Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) (a✝ : X) :
                                          e.toSemigrpIso.hom a✝ = e.toFun a✝
                                          @[simp]
                                          theorem AddEquiv.toAddSemigrpIso_inv_apply {X Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) (a✝ : Y) :
                                          e.toAddSemigrpIso.inv a✝ = e.symm.toFun a✝

                                          Build a MulEquiv from an isomorphism in the category MagmaCat.

                                          Equations
                                          Instances For

                                            Build an AddEquiv from an isomorphism in the category AddMagmaCat.

                                            Equations
                                            Instances For
                                              def CategoryTheory.Iso.semigrpIsoToMulEquiv {X Y : Semigrp} (i : X Y) :
                                              X ≃* Y

                                              Build a MulEquiv from an isomorphism in the category Semigroup.

                                              Equations
                                              Instances For

                                                Build an AddEquiv from an isomorphism in the category AddSemigroup.

                                                Equations
                                                Instances For

                                                  multiplicative equivalences between Muls are the same as (isomorphic to) isomorphisms in MagmaCat

                                                  Equations
                                                  • mulEquivIsoMagmaIso = { hom := fun (e : X ≃* Y) => e.toMagmaCatIso, inv := fun (i : MagmaCat.of X MagmaCat.of Y) => i.magmaCatIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                  Instances For

                                                    additive equivalences between Adds are the same as (isomorphic to) isomorphisms in AddMagmaCat

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

                                                      multiplicative equivalences between Semigroups are the same as (isomorphic to) isomorphisms in Semigroup

                                                      Equations
                                                      • mulEquivIsoSemigrpIso = { hom := fun (e : X ≃* Y) => e.toSemigrpIso, inv := fun (i : Semigrp.of X Semigrp.of Y) => i.semigrpIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                      Instances For

                                                        additive equivalences between AddSemigroups are the same as (isomorphic to) isomorphisms in AddSemigroup

                                                        Equations
                                                        • addEquivIsoAddSemigrpIso = { hom := fun (e : X ≃+ Y) => e.toAddSemigrpIso, inv := fun (i : AddSemigrp.of X AddSemigrp.of Y) => i.addSemigrpIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
                                                        Instances For

                                                          Once we've shown that the forgetful functors to type reflect isomorphisms, we automatically obtain that the forget₂ functors between our concrete categories reflect isomorphisms.