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 AddMagmaCat :
Type (u + 1)

The category of additive magmas and additive magma morphisms.

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

    The category of magmas and magma morphisms.

    Equations
    Instances For
      theorem AddMagmaCat.bundledHom.proof_1 :
      ∀ {α β : Type u_1} ( : Add α) ( : Add β), Function.Injective fun (f : AddHom α β) => f
      Equations
      • One or more equations did not get rendered due to their size.
      theorem AddMagmaCat.bundledHom.proof_2 {α : Type u_1} (I : Add α) :
      (AddHom.id α).toFun = id
      theorem AddMagmaCat.bundledHom.proof_3 {α : Type u_1} {β : Type u_1} {γ : Type u_1} (Iα : Add α) (Iβ : Add β) (Iγ : Add γ) (f : AddHom α β) (g : AddHom β γ) :
      g f = g f
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      Instances For
        Equations
        Instances For
          Equations
          • X.instMulα = X.str
          instance MagmaCat.instMulα (X : MagmaCat) :
          Mul X
          Equations
          • X.instMulα = X.str
          instance AddMagmaCat.instFunLike (X : AddMagmaCat) (Y : AddMagmaCat) :
          FunLike (X Y) X Y
          Equations
          instance MagmaCat.instFunLike (X : MagmaCat) (Y : MagmaCat) :
          FunLike (X Y) X Y
          Equations
          instance AddMagmaCat.instAddHomClass (X : AddMagmaCat) (Y : AddMagmaCat) :
          AddHomClass (X Y) X Y
          Equations
          • =
          instance MagmaCat.instMulHomClass (X : MagmaCat) (Y : MagmaCat) :
          MulHomClass (X Y) X Y
          Equations
          • =

          Construct a bundled AddMagmaCat from the underlying type and typeclass.

          Equations
          Instances For
            def MagmaCat.of (M : Type u) [Mul M] :

            Construct a bundled MagmaCat from the underlying type and typeclass.

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

              Typecheck an AddHom as a morphism in AddMagmaCat.

              Equations
              Instances For
                def MagmaCat.ofHom {X : Type u} {Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) :

                Typecheck a MulHom as a morphism in MagmaCat.

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

                  The category of additive semigroups and semigroup morphisms.

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

                    The category of 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 AddSemigrp.instFunLike (X : AddSemigrp) (Y : AddSemigrp) :
                          FunLike (X Y) X Y
                          Equations
                          instance Semigrp.instFunLike (X : Semigrp) (Y : Semigrp) :
                          FunLike (X Y) X Y
                          Equations
                          instance AddSemigrp.instAddHomClass (X : AddSemigrp) (Y : AddSemigrp) :
                          AddHomClass (X Y) X Y
                          Equations
                          • =
                          instance Semigrp.instMulHomClass (X : Semigrp) (Y : Semigrp) :
                          MulHomClass (X Y) X Y
                          Equations
                          • =

                          Construct a bundled AddSemigrp from the underlying type and typeclass.

                          Equations
                          Instances For
                            def Semigrp.of (M : Type u) [Semigroup M] :

                            Construct a bundled Semigrp from the underlying type and typeclass.

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

                              Typecheck an AddHom as a morphism in AddSemigrp.

                              Equations
                              Instances For
                                def Semigrp.ofHom {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) :

                                Typecheck a MulHom as a morphism in Semigrp.

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

                                  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 : Type u} {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 : Type u} {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 : Type u} {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 : Type u} {Y : Type u} [Mul X] [Mul Y] (e : X ≃* Y) :
                                    ∀ (a : Y), e.toMagmaCatIso.inv a = e.symm.toFun a
                                    def MulEquiv.toMagmaCatIso {X : Type u} {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 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 AddEquiv.toAddSemigrpIso_hom_apply {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) :
                                        ∀ (a : X), e.toAddSemigrpIso.hom a = e.toFun a
                                        @[simp]
                                        theorem MulEquiv.toSemigrpIso_inv_apply {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
                                        ∀ (a : Y), e.toSemigrpIso.inv a = e.symm.toFun a
                                        @[simp]
                                        theorem AddEquiv.toAddSemigrpIso_inv_apply {X : Type u} {Y : Type u} [AddSemigroup X] [AddSemigroup Y] (e : X ≃+ Y) :
                                        ∀ (a : Y), e.toAddSemigrpIso.inv a = e.symm.toFun a
                                        @[simp]
                                        theorem MulEquiv.toSemigrpIso_hom_apply {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
                                        ∀ (a : X), e.toSemigrpIso.hom a = e.toFun a
                                        def MulEquiv.toSemigrpIso {X : Type u} {Y : Type u} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :

                                        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 AddEquiv from an isomorphism in the category AddMagmaCat.

                                          Equations
                                          Instances For

                                            Build a MulEquiv from an isomorphism in the category MagmaCat.

                                            Equations
                                            Instances For

                                              Build an AddEquiv from an isomorphism in the category AddSemigroup.

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

                                                Build a MulEquiv from an isomorphism in the category Semigroup.

                                                Equations
                                                Instances For
                                                  theorem addEquivIsoAddMagmaIso.proof_2 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] :
                                                  (CategoryTheory.CategoryStruct.comp (fun (i : AddMagmaCat.of X AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMagmaCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddMagmaCat.of X AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMagmaCatIso

                                                  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
                                                    theorem addEquivIsoAddMagmaIso.proof_1 {X : Type u_1} {Y : Type u_1} [Add X] [Add Y] :
                                                    (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddMagmaCatIso) fun (i : AddMagmaCat.of X AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddMagmaCatIso) fun (i : AddMagmaCat.of X AddMagmaCat.of Y) => i.addMagmaCatIsoToAddEquiv
                                                    def mulEquivIsoMagmaIso {X : Type u} {Y : Type u} [Mul X] [Mul Y] :

                                                    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 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
                                                        theorem addEquivIsoAddSemigrpIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] :
                                                        (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddSemigrpIso) fun (i : AddSemigrp.of X AddSemigrp.of Y) => i.addSemigrpIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddSemigrpIso) fun (i : AddSemigrp.of X AddSemigrp.of Y) => i.addSemigrpIsoToAddEquiv
                                                        theorem addEquivIsoAddSemigrpIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddSemigroup X] [AddSemigroup Y] :
                                                        (CategoryTheory.CategoryStruct.comp (fun (i : AddSemigrp.of X AddSemigrp.of Y) => i.addSemigrpIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddSemigrpIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddSemigrp.of X AddSemigrp.of Y) => i.addSemigrpIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddSemigrpIso

                                                        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

                                                          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.