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
        @[inline, reducible]
        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_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.
          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
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          instance MonCat.instMonoidα (X : MonCat) :
          Monoid X
          Equations
          Equations
          • AddMonCat.instCoeFunHomMonCatToQuiverToCategoryStructInstMonCatLargeCategoryForAllαAddMonoid = { coe := fun (f : X →+ Y) => f }
          Equations
          • MonCat.instCoeFunHomMonCatToQuiverToCategoryStructInstMonCatLargeCategoryForAllα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
                  @[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αAddMonoidOfToAddMonoidToSubNegAddMonoid = inst
                  Equations
                  • MonCat.instGroupαMonoidOfToMonoidToDivInvMonoid = inst
                  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
                      • AddCommMonCat.instCoeFunHomCommMonCatToQuiverToCategoryStructInstCommMonCatLargeCategoryForAllαAddCommMonoid = { coe := fun (f : X →+ Y) => f }
                      Equations
                      • CommMonCat.instCoeFunHomCommMonCatToQuiverToCategoryStructInstCommMonCatLargeCategoryForAllαCommMonoid = { coe := fun (f : X →* Y) => f }
                      instance AddCommMonCat.instFunLike (X : AddCommMonCat) (Y : AddCommMonCat) :
                      FunLike (X Y) X Y
                      Equations
                      instance CommMonCat.instFunLike (X : CommMonCat) (Y : CommMonCat) :
                      FunLike (X Y) X Y
                      Equations
                      @[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 AddCommMon 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) :

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

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

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

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

                                    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

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

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                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
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  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

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    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.