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_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
          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
                  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) :

                              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_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
                                @[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
                                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 MulEquiv.toCommMonCatIso_hom {X : Type u} {Y : Type u} [CommMonoid X] [CommMonoid Y] (e : X ≃* Y) :
                                    e.toCommMonCatIso.hom = CommMonCat.ofHom e.toMonoidHom
                                    @[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 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 AddEquiv.toAddCommMonCatIso_hom {X : Type u} {Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (e : X ≃+ Y) :
                                    e.toAddCommMonCatIso.hom = AddCommMonCat.ofHom e.toAddMonoidHom

                                    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
                                              • 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
                                                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
                                                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
                                                  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

                                                  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

                                                      @[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]