Documentation

Mathlib.Algebra.Category.MonCat.Basic

Category instances for Monoid, AddMonoid, CommMonoid, and AddCommMmonoid. #

We introduce the bundled categories:

def AddMonCat :
Type (u + 1)

The category of additive monoids and monoid morphisms.

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

    The category of monoids and monoid morphisms.

    Equations
    Instances For
      abbrev AddMonCat.AssocAddMonoidHom (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] :
      Type (max u_1 u_2)

      AddMonoidHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

      Equations
      Instances For
        @[reducible, inline]
        abbrev MonCat.AssocMonoidHom (M : Type u_1) (N : Type u_2) [Monoid M] [Monoid N] :
        Type (max u_1 u_2)

        MonoidHom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

        Equations
        Instances For
          theorem AddMonCat.bundledHom.proof_2 {α : Type u_1} (I : AddMonoid α) :
          (fun {X Y : Type u_1} (x : AddMonoid X) (x_1 : AddMonoid Y) (f : AddMonCat.AssocAddMonoidHom X Y) => f) I I ((fun {α : Type u_1} (x : AddMonoid α) => AddMonoidHom.id α) I) = id
          theorem AddMonCat.bundledHom.proof_3 {α : Type u_1} {β : Type u_1} {γ : Type u_1} (Iα : AddMonoid α) (Iβ : AddMonoid β) (Iγ : AddMonoid γ) (f : AddMonCat.AssocAddMonoidHom α β) (g : AddMonCat.AssocAddMonoidHom β γ) :
          g f = g f
          theorem AddMonCat.bundledHom.proof_1 {α : Type u_1} {β : Type u_1} (Iα : AddMonoid α) (Iβ : AddMonoid β) ⦃a₁ : AddMonCat.AssocAddMonoidHom α β ⦃a₂ : AddMonCat.AssocAddMonoidHom α β (a : (fun {X Y : Type u_1} (x : AddMonoid X) (x_1 : AddMonoid Y) (f : AddMonCat.AssocAddMonoidHom X Y) => f) a₁ = (fun {X Y : Type u_1} (x : AddMonoid X) (x_1 : AddMonoid Y) (f : AddMonCat.AssocAddMonoidHom X Y) => f) a₂) :
          a₁ = a₂
          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
          Equations
          • X.instMonoidα = X.str
          instance MonCat.instMonoidα (X : MonCat) :
          Monoid X
          Equations
          • X.instMonoidα = X.str
          instance AddMonCat.instCoeFunHomForallαAddMonoid {X : AddMonCat} {Y : AddMonCat} :
          CoeFun (X Y) fun (x : X Y) => XY
          Equations
          • AddMonCat.instCoeFunHomForallαAddMonoid = { coe := fun (f : X →+ Y) => f }
          instance MonCat.instCoeFunHomForallαMonoid {X : MonCat} {Y : MonCat} :
          CoeFun (X Y) fun (x : X Y) => XY
          Equations
          • MonCat.instCoeFunHomForallαMonoid = { coe := fun (f : X →* Y) => f }
          instance AddMonCat.instFunLike (X : AddMonCat) (Y : AddMonCat) :
          FunLike (X Y) X Y
          Equations
          instance MonCat.instFunLike (X : MonCat) (Y : MonCat) :
          FunLike (X Y) X Y
          Equations
          Equations
          • =
          instance MonCat.instMonoidHomClass (X : MonCat) (Y : MonCat) :
          MonoidHomClass (X Y) X Y
          Equations
          • =
          @[simp]
          theorem AddMonCat.coe_comp {X : AddMonCat} {Y : AddMonCat} {Z : AddMonCat} {f : X Y} {g : Y Z} :
          @[simp]
          theorem MonCat.coe_comp {X : MonCat} {Y : MonCat} {Z : MonCat} {f : X Y} {g : Y Z} :
          @[simp]
          theorem AddMonCat.forget_map {X : AddMonCat} {Y : AddMonCat} (f : X Y) :
          @[simp]
          theorem MonCat.forget_map {X : MonCat} {Y : MonCat} (f : X Y) :
          theorem AddMonCat.ext {X : AddMonCat} {Y : AddMonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
          f = g
          theorem MonCat.ext {X : MonCat} {Y : MonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
          f = g

          Construct a bundled AddMonCat from the underlying type and typeclass.

          Equations
          Instances For
            def MonCat.of (M : Type u) [Monoid M] :

            Construct a bundled MonCat from the underlying type and typeclass.

            Equations
            Instances For
              theorem AddMonCat.coe_of (R : Type u) [AddMonoid R] :
              (AddMonCat.of R) = R
              theorem MonCat.coe_of (R : Type u) [Monoid R] :
              (MonCat.of R) = R
              def AddMonCat.ofHom {X : Type u} {Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) :

              Typecheck an AddMonoidHom as a morphism in AddMonCat.

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

                Typecheck a MonoidHom as a morphism in MonCat.

                Equations
                Instances For
                  @[simp]
                  theorem AddMonCat.ofHom_apply {X : Type u} {Y : Type u} [AddMonoid X] [AddMonoid Y] (f : X →+ Y) (x : X) :
                  (AddMonCat.ofHom f) x = f x
                  @[simp]
                  theorem MonCat.ofHom_apply {X : Type u} {Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) (x : X) :
                  (MonCat.ofHom f) x = f x
                  instance AddMonCat.instZeroHom (X : AddMonCat) (Y : AddMonCat) :
                  Zero (X Y)
                  Equations
                  instance MonCat.instOneHom (X : MonCat) (Y : MonCat) :
                  One (X Y)
                  Equations
                  @[simp]
                  theorem AddMonCat.zeroHom_apply (X : AddMonCat) (Y : AddMonCat) (x : X) :
                  0 x = 0
                  @[simp]
                  theorem MonCat.oneHom_apply (X : MonCat) (Y : MonCat) (x : X) :
                  1 x = 1
                  @[simp]
                  theorem AddMonCat.zero_of {A : Type u_1} [AddMonoid A] :
                  0 = 0
                  @[simp]
                  theorem MonCat.one_of {A : Type u_1} [Monoid A] :
                  1 = 1
                  @[simp]
                  theorem AddMonCat.add_of {A : Type u_1} [AddMonoid A] (a : A) (b : A) :
                  a + b = a + b
                  @[simp]
                  theorem MonCat.mul_of {A : Type u_1} [Monoid A] (a : A) (b : A) :
                  a * b = a * b
                  Equations
                  • AddMonCat.instGroupαAddMonoidOf = inst
                  instance MonCat.instGroupαMonoidOf {G : Type u_1} [Group G] :
                  Equations
                  • MonCat.instGroupαMonoidOf = inst
                  theorem AddMonCat.uliftFunctor.proof_1 (X : AddMonCat) :
                  { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddMonCat} (f : X Y) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddMonCat} (f : X Y) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)
                  theorem AddMonCat.uliftFunctor.proof_2 {X : AddMonCat} {Y : AddMonCat} {Z : AddMonCat} (f : X Y) (g : Y Z) :
                  { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddMonCat} (f : X Y) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddMonCat) => AddMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddMonCat} (f : X Y) => AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)

                  Universe lift functor for additive monoids.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem AddMonCat.uliftFunctor_map {X : AddMonCat} {Y : AddMonCat} (f : X Y) :
                    AddMonCat.uliftFunctor.map f = AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))
                    @[simp]
                    theorem MonCat.uliftFunctor_map {X : MonCat} {Y : MonCat} (f : X Y) :
                    MonCat.uliftFunctor.map f = MonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))

                    Universe lift functor for monoids.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def AddCommMonCat :
                      Type (u + 1)

                      The category of additive commutative monoids and monoid morphisms.

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

                        The category of commutative monoids and monoid morphisms.

                        Equations
                        Instances For
                          Equations
                          • X.instCommMonoidα = X.str
                          Equations
                          • X.instCommMonoidα = X.str
                          instance AddCommMonCat.instCoeFunHomForallαAddCommMonoid {X : AddCommMonCat} {Y : AddCommMonCat} :
                          CoeFun (X Y) fun (x : X Y) => XY
                          Equations
                          • AddCommMonCat.instCoeFunHomForallαAddCommMonoid = { coe := fun (f : X →+ Y) => f }
                          instance CommMonCat.instCoeFunHomForallαCommMonoid {X : CommMonCat} {Y : CommMonCat} :
                          CoeFun (X Y) fun (x : X Y) => XY
                          Equations
                          • CommMonCat.instCoeFunHomForallαCommMonoid = { coe := fun (f : X →* Y) => f }
                          instance AddCommMonCat.instFunLike (X : AddCommMonCat) (Y : AddCommMonCat) :
                          FunLike (X Y) X Y
                          Equations
                          • X.instFunLike Y = let_fun this := inferInstance; this
                          instance CommMonCat.instFunLike (X : CommMonCat) (Y : CommMonCat) :
                          FunLike (X Y) X Y
                          Equations
                          • X.instFunLike Y = let_fun this := inferInstance; this
                          @[simp]
                          theorem AddCommMonCat.coe_comp {X : AddCommMonCat} {Y : AddCommMonCat} {Z : AddCommMonCat} {f : X Y} {g : Y Z} :
                          @[simp]
                          theorem CommMonCat.coe_comp {X : CommMonCat} {Y : CommMonCat} {Z : CommMonCat} {f : X Y} {g : Y Z} :
                          @[simp]
                          theorem AddCommMonCat.ext {X : AddCommMonCat} {Y : AddCommMonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                          f = g
                          theorem CommMonCat.ext {X : CommMonCat} {Y : CommMonCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                          f = g

                          Construct a bundled AddCommMonCat from the underlying type and typeclass.

                          Equations
                          Instances For

                            Construct a bundled CommMonCat from the underlying type and typeclass.

                            Equations
                            Instances For
                              theorem CommMonCat.coe_of (R : Type u) [CommMonoid R] :
                              (CommMonCat.of R) = R

                              Typecheck an AddMonoidHom as a morphism in AddCommMonCat.

                              Equations
                              Instances For

                                Typecheck a MonoidHom as a morphism in CommMonCat.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem AddCommMonCat.ofHom_apply {X : Type u} {Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : X →+ Y) (x : X) :
                                  @[simp]
                                  theorem CommMonCat.ofHom_apply {X : Type u} {Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) (x : X) :

                                  Universe lift functor for additive commutative monoids.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem AddCommMonCat.uliftFunctor.proof_2 {X : AddCommMonCat} {Y : AddCommMonCat} {Z : AddCommMonCat} (f : X Y) (g : Y Z) :
                                    { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommMonCat} (f : X Y) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommMonCat} (f : X Y) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)
                                    theorem AddCommMonCat.uliftFunctor.proof_1 (X : AddCommMonCat) :
                                    { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommMonCat} (f : X Y) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddCommMonCat) => AddCommMonCat.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommMonCat} (f : X Y) => AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)
                                    @[simp]
                                    theorem CommMonCat.uliftFunctor_map {X : CommMonCat} {Y : CommMonCat} (f : X Y) :
                                    CommMonCat.uliftFunctor.map f = CommMonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))
                                    @[simp]
                                    theorem AddCommMonCat.uliftFunctor_map {X : AddCommMonCat} {Y : AddCommMonCat} (f : X Y) :
                                    AddCommMonCat.uliftFunctor.map f = AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))

                                    Universe lift functor for commutative monoids.

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

                                      Build an isomorphism in the category AddMonCat from an AddEquiv between AddMonoids.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem MulEquiv.toMonCatIso_inv {X : Type u} {Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) :
                                        e.toMonCatIso.inv = MonCat.ofHom e.symm.toMonoidHom
                                        @[simp]
                                        theorem AddEquiv.toAddMonCatIso_inv {X : Type u} {Y : Type u} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) :
                                        e.toAddMonCatIso.inv = AddMonCat.ofHom e.symm.toAddMonoidHom
                                        @[simp]
                                        theorem AddEquiv.toAddMonCatIso_hom {X : Type u} {Y : Type u} [AddMonoid X] [AddMonoid Y] (e : X ≃+ Y) :
                                        e.toAddMonCatIso.hom = AddMonCat.ofHom e.toAddMonoidHom
                                        @[simp]
                                        theorem MulEquiv.toMonCatIso_hom {X : Type u} {Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) :
                                        e.toMonCatIso.hom = MonCat.ofHom e.toMonoidHom
                                        def MulEquiv.toMonCatIso {X : Type u} {Y : Type u} [Monoid X] [Monoid Y] (e : X ≃* Y) :

                                        Build an isomorphism in the category MonCat from a MulEquiv between Monoids.

                                        Equations
                                        • e.toMonCatIso = { hom := MonCat.ofHom e.toMonoidHom, inv := MonCat.ofHom e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
                                        Instances For

                                          Build an isomorphism in the category AddCommMonCat from an AddEquiv between AddCommMonoids.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem AddEquiv.toAddCommMonCatIso_hom {X : Type u} {Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) :
                                            e.toAddCommMonCatIso.hom = AddCommMonCat.ofHom e.toAddMonoidHom
                                            @[simp]
                                            theorem AddEquiv.toAddCommMonCatIso_inv {X : Type u} {Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) :
                                            e.toAddCommMonCatIso.inv = AddCommMonCat.ofHom e.symm.toAddMonoidHom
                                            @[simp]
                                            theorem MulEquiv.toCommMonCatIso_inv {X : Type u} {Y : Type u} [CommMonoid X] [CommMonoid Y] (e : X ≃* Y) :
                                            e.toCommMonCatIso.inv = CommMonCat.ofHom e.symm.toMonoidHom
                                            @[simp]
                                            theorem MulEquiv.toCommMonCatIso_hom {X : Type u} {Y : Type u} [CommMonoid X] [CommMonoid Y] (e : X ≃* Y) :
                                            e.toCommMonCatIso.hom = CommMonCat.ofHom e.toMonoidHom

                                            Build an isomorphism in the category CommMonCat from a MulEquiv between CommMonoids.

                                            Equations
                                            Instances For

                                              Build an AddEquiv from an isomorphism in the category AddMonCat.

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

                                                Build a MulEquiv from an isomorphism in the category MonCat.

                                                Equations
                                                Instances For

                                                  Build an AddEquiv from an isomorphism in the category AddCommMonCat.

                                                  Equations
                                                  Instances For

                                                    Build a MulEquiv from an isomorphism in the category CommMonCat.

                                                    Equations
                                                    Instances For
                                                      theorem addEquivIsoAddMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddMonoid X] [AddMonoid Y] :
                                                      (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddMonCatIso) fun (i : AddMonCat.of X AddMonCat.of Y) => i.addMonCatIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddMonCatIso) fun (i : AddMonCat.of X AddMonCat.of Y) => i.addMonCatIsoToAddEquiv

                                                      additive equivalences between AddMonoids are the same as (isomorphic to) isomorphisms in AddMonCat

                                                      Equations
                                                      • addEquivIsoAddMonCatIso = { hom := fun (e : X ≃+ Y) => e.toAddMonCatIso, inv := fun (i : AddMonCat.of X AddMonCat.of Y) => i.addMonCatIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
                                                      Instances For
                                                        theorem addEquivIsoAddMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddMonoid X] [AddMonoid Y] :
                                                        (CategoryTheory.CategoryStruct.comp (fun (i : AddMonCat.of X AddMonCat.of Y) => i.addMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMonCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddMonCat.of X AddMonCat.of Y) => i.addMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddMonCatIso
                                                        def mulEquivIsoMonCatIso {X : Type u} {Y : Type u} [Monoid X] [Monoid Y] :

                                                        multiplicative equivalences between Monoids are the same as (isomorphic to) isomorphisms in MonCat

                                                        Equations
                                                        • mulEquivIsoMonCatIso = { hom := fun (e : X ≃* Y) => e.toMonCatIso, inv := fun (i : MonCat.of X MonCat.of Y) => i.monCatIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                        Instances For
                                                          theorem addEquivIsoAddCommMonCatIso.proof_1 {X : Type u_1} {Y : Type u_1} [AddCommMonoid X] [AddCommMonoid Y] :
                                                          (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommMonCatIso) fun (i : AddCommMonCat.of X AddCommMonCat.of Y) => i.commMonCatIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommMonCatIso) fun (i : AddCommMonCat.of X AddCommMonCat.of Y) => i.commMonCatIsoToAddEquiv

                                                          additive equivalences between AddCommMonoids are the same as (isomorphic to) isomorphisms in AddCommMonCat

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            theorem addEquivIsoAddCommMonCatIso.proof_2 {X : Type u_1} {Y : Type u_1} [AddCommMonoid X] [AddCommMonoid Y] :
                                                            (CategoryTheory.CategoryStruct.comp (fun (i : AddCommMonCat.of X AddCommMonCat.of Y) => i.commMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommMonCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : AddCommMonCat.of X AddCommMonCat.of Y) => i.commMonCatIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommMonCatIso

                                                            multiplicative equivalences between CommMonoids are the same as (isomorphic to) isomorphisms in CommMonCat

                                                            Equations
                                                            • mulEquivIsoCommMonCatIso = { hom := fun (e : X ≃* Y) => e.toCommMonCatIso, inv := fun (i : CommMonCat.of X CommMonCat.of Y) => i.commMonCatIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                            Instances For

                                                              @[simp] lemmas for MonoidHom.comp and categorical identities.

                                                              @[simp]
                                                              theorem AddMonoidHom.comp_id_monCat {G : AddMonCat} {H : Type u} [AddMonoid H] (f : G →+ H) :
                                                              @[simp]
                                                              theorem MonoidHom.comp_id_monCat {G : MonCat} {H : Type u} [Monoid H] (f : G →* H) :
                                                              @[simp]