Documentation

Mathlib.Algebra.Category.Grp.Yoneda

Yoneda embeddings #

This file defines a few Yoneda embeddings for the category of commutative groups.

source
def CommGrpCat.coyoneda :
CategoryTheory.Functor CommGrpCatᵒᵖ (CategoryTheory.Functor CommGrpCat CommGrpCat)

The CommGrpCat-valued coyoneda embedding.

Equations
    Instances For
      source
      def AddCommGrpCat.coyoneda :
      CategoryTheory.Functor AddCommGrpCatᵒᵖ (CategoryTheory.Functor AddCommGrpCat AddCommGrpCat)

      The AddCommGrpCat-valued coyoneda embedding.

      Equations
        Instances For
          source
          @[simp]
          theorem AddCommGrpCat.coyoneda_map_app {X✝ Y✝ : AddCommGrpCatᵒᵖ} (f : X✝ ⟶ Y✝) (N : AddCommGrpCat) :
          (coyoneda.map f).app N = ofHom (Hom.hom f.unop).compHom'
          source
          @[simp]
          theorem CommGrpCat.coyoneda_map_app {X✝ Y✝ : CommGrpCatᵒᵖ} (f : X✝ ⟶ Y✝) (N : CommGrpCat) :
          (coyoneda.map f).app N = ofHom (Hom.hom f.unop).compHom'
          source
          @[simp]
          theorem CommGrpCat.coyoneda_obj_map (M : CommGrpCatᵒᵖ) {X✝ Y✝ : CommGrpCat} (f : X✝ ⟶ Y✝) :
          (coyoneda.obj M).map f = ofHom (MonoidHom.compHom (Hom.hom f))
          source
          @[simp]
          theorem AddCommGrpCat.coyoneda_obj_obj_coe (M : AddCommGrpCatᵒᵖ) (N : AddCommGrpCat) :
          ↑((coyoneda.obj M).obj N) = (↑(Opposite.unop M) →+ ↑N)
          source
          @[simp]
          theorem CommGrpCat.coyoneda_obj_obj_coe (M : CommGrpCatᵒᵖ) (N : CommGrpCat) :
          ↑((coyoneda.obj M).obj N) = (↑(Opposite.unop M) →* ↑N)
          source
          @[simp]
          theorem AddCommGrpCat.coyoneda_obj_map (M : AddCommGrpCatᵒᵖ) {X✝ Y✝ : AddCommGrpCat} (f : X✝ ⟶ Y✝) :
          (coyoneda.obj M).map f = ofHom (AddMonoidHom.compHom (Hom.hom f))
          source
          def CommGrpCat.coyonedaForget :
          coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommGrpCat CommGrpCat (Type u_1)).obj (CategoryTheory.forget CommGrpCat)) ≅ CategoryTheory.coyoneda

          The CommGrpCat-valued coyoneda embedding composed with the forgetful functor is the usual coyoneda embedding.

          Equations
            Instances For
              source
              def AddCommGrpCat.coyonedaForget :
              coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommGrpCat AddCommGrpCat (Type u_1)).obj (CategoryTheory.forget AddCommGrpCat)) ≅ CategoryTheory.coyoneda

              The AddCommGrpCat-valued coyoneda embedding composed with the forgetful functor is the usual coyoneda embedding.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem AddCommGrpCat.coyonedaForget_inv_app_app (X : AddCommGrpCatᵒᵖ) (X✝ : AddCommGrpCat) (a✝ : (CategoryTheory.coyoneda.obj X).obj X✝) :
                  (coyonedaForget.inv.app X).app X✝ a✝ = Hom.hom a✝
                  source
                  @[simp]
                  theorem CommGrpCat.coyonedaForget_hom_app_app_hom (X : CommGrpCatᵒᵖ) (X✝ : CommGrpCat) (a✝ : ((coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommGrpCat CommGrpCat (Type u_1)).obj (CategoryTheory.forget CommGrpCat))).obj X).obj X✝) :
                  Hom.hom ((coyonedaForget.hom.app X).app X✝ a✝) = a✝
                  source
                  @[simp]
                  theorem AddCommGrpCat.coyonedaForget_hom_app_app_hom (X : AddCommGrpCatᵒᵖ) (X✝ : AddCommGrpCat) (a✝ : ((coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommGrpCat AddCommGrpCat (Type u_1)).obj (CategoryTheory.forget AddCommGrpCat))).obj X).obj X✝) :
                  Hom.hom ((coyonedaForget.hom.app X).app X✝ a✝) = a✝
                  source
                  @[simp]
                  theorem CommGrpCat.coyonedaForget_inv_app_app (X : CommGrpCatᵒᵖ) (X✝ : CommGrpCat) (a✝ : (CategoryTheory.coyoneda.obj X).obj X✝) :
                  (coyonedaForget.inv.app X).app X✝ a✝ = Hom.hom a✝
                  source
                  def CommGrpCat.coyonedaType :
                  CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor CommGrpCat CommGrpCat)

                  The Hom bifunctor sending a type X and a commutative group G to the commutative group X → G with pointwise operations.

                  This is also the coyoneda embedding of Type into CommGrpCat-valued presheaves of commutative groups.

                  Equations
                    Instances For
                      source
                      def AddCommGrpCat.coyonedaType :
                      CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor AddCommGrpCat AddCommGrpCat)

                      The Hom bifunctor sending a type X and a commutative group G to the commutative group X → G with pointwise operations.

                      This is also the coyoneda embedding of Type into AddCommGrpCat-valued presheaves of commutative groups.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CommGrpCat.coyonedaType_obj_obj_coe (X : Type uᵒᵖ) (G : CommGrpCat) :
                          ↑((coyonedaType.obj X).obj G) = (Opposite.unop X → ↑G)
                          source
                          @[simp]
                          theorem AddCommGrpCat.coyonedaType_map_app {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (G : AddCommGrpCat) :
                          (coyonedaType.map f).app G = ofHom (Pi.addMonoidHom fun (i : Opposite.unop Y✝) => Pi.evalAddMonoidHom (fun (a : Opposite.unop X✝) => ↑G) (f.unop i))
                          source
                          @[simp]
                          theorem AddCommGrpCat.coyonedaType_obj_map (X : Type uᵒᵖ) {X✝ Y✝ : AddCommGrpCat} (f : X✝ ⟶ Y✝) :
                          (coyonedaType.obj X).map f = ofHom (Pi.addMonoidHom fun (i : Opposite.unop X) => (Hom.hom f).comp (Pi.evalAddMonoidHom (fun (a : Opposite.unop X) => ↑X✝) i))
                          source
                          @[simp]
                          theorem AddCommGrpCat.coyonedaType_obj_obj_coe (X : Type uᵒᵖ) (G : AddCommGrpCat) :
                          ↑((coyonedaType.obj X).obj G) = (Opposite.unop X → ↑G)
                          source
                          @[simp]
                          theorem CommGrpCat.coyonedaType_obj_map (X : Type uᵒᵖ) {X✝ Y✝ : CommGrpCat} (f : X✝ ⟶ Y✝) :
                          (coyonedaType.obj X).map f = ofHom (Pi.monoidHom fun (i : Opposite.unop X) => (Hom.hom f).comp (Pi.evalMonoidHom (fun (a : Opposite.unop X) => ↑X✝) i))
                          source
                          @[simp]
                          theorem CommGrpCat.coyonedaType_map_app {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (G : CommGrpCat) :
                          (coyonedaType.map f).app G = ofHom (Pi.monoidHom fun (i : Opposite.unop Y✝) => Pi.evalMonoidHom (fun (a : Opposite.unop X✝) => ↑G) (f.unop i))