Documentation

Mathlib.Algebra.Category.MonCat.Basic

Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid. #

We introduce the bundled categories:

def AddMonCat :
Type (u + 1)

The category of additive monoids and monoid morphisms.

Instances For
    def MonCat :
    Type (u + 1)

    The category of monoids and monoid morphisms.

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

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

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

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

        Instances For
          theorem AddMonCat.bundledHom.proof_2 {α : Type u_1} (I : AddMonoid α) :
          (fun {X Y} x x_1 f => f) I I ((fun {α} x => 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} x x_1 f => f) a₁ = (fun {X Y} x x_1 f => f) a₂) :
          a₁ = a₂
          instance AddMonCat.Hom_FunLike (X : AddMonCat) (Y : AddMonCat) :
          FunLike (X Y) X fun x => Y
          instance MonCat.Hom_FunLike (X : MonCat) (Y : MonCat) :
          FunLike (X Y) X fun x => Y
          @[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.

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

            Construct a bundled MonCat from the underlying type and typeclass.

            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.

              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.

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

                  The category of additive commutative monoids and monoid morphisms.

                  Instances For
                    def CommMonCat :
                    Type (u + 1)

                    The category of commutative monoids and monoid morphisms.

                    Instances For
                      instance AddCommMonCat.Hom_FunLike (X : AddCommMonCat) (Y : AddCommMonCat) :
                      FunLike (X Y) X fun x => Y
                      instance CommMonCat.Hom_FunLike (X : CommMonCat) (Y : CommMonCat) :
                      FunLike (X Y) X fun x => Y
                      @[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.

                      Instances For

                        Construct a bundled CommMonCat from the underlying type and typeclass.

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

                          Typecheck an AddMonoidHom as a morphism in AddCommMonCat.

                          Instances For

                            Typecheck a MonoidHom as a morphism in CommMonCat.

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

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

                              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.

                                Instances For

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

                                  Instances For

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

                                    Instances For

                                      Build an AddEquiv from an isomorphism in the category AddMonCat.

                                      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.

                                        Instances For

                                          Build an AddEquiv from an isomorphism in the category AddCommMonCat.

                                          Instances For

                                            Build a MulEquiv from an isomorphism in the category CommMonCat.

                                            Instances For

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

                                              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

                                                Instances For

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

                                                  Instances For

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

                                                    Instances For