Documentation

Mathlib.Algebra.Category.Grp.Yoneda

Yoneda embeddings #

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

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

The CommGrp-valued coyoneda embedding.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AddCommGrp.coyoneda :
    CategoryTheory.Functor AddCommGrpᵒᵖ (CategoryTheory.Functor AddCommGrp AddCommGrp)

    The AddCommGrp-valued coyoneda embedding.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AddCommGrp.coyoneda_obj_map (M : AddCommGrpᵒᵖ) {X✝ Y✝ : AddCommGrp} (f : X✝ ⟶ Y✝) :
      (coyoneda.obj M).map f = ofHom (AddMonoidHom.compHom (Hom.hom f))
      source
      @[simp]
      theorem CommGrp.coyoneda_map_app {X✝ Y✝ : CommGrpᵒᵖ} (f : X✝ ⟶ Y✝) (N : CommGrp) :
      (coyoneda.map f).app N = ofHom (Hom.hom f.unop).compHom'
      source
      @[simp]
      theorem CommGrp.coyoneda_obj_map (M : CommGrpᵒᵖ) {X✝ Y✝ : CommGrp} (f : X✝ ⟶ Y✝) :
      (coyoneda.obj M).map f = ofHom (MonoidHom.compHom (Hom.hom f))
      source
      @[simp]
      theorem AddCommGrp.coyoneda_map_app {X✝ Y✝ : AddCommGrpᵒᵖ} (f : X✝ ⟶ Y✝) (N : AddCommGrp) :
      (coyoneda.map f).app N = ofHom (Hom.hom f.unop).compHom'
      source
      @[simp]
      theorem AddCommGrp.coyoneda_obj_obj_coe (M : AddCommGrpᵒᵖ) (N : AddCommGrp) :
      ↑((coyoneda.obj M).obj N) = (↑(Opposite.unop M) →+ ↑N)
      source
      @[simp]
      theorem CommGrp.coyoneda_obj_obj_coe (M : CommGrpᵒᵖ) (N : CommGrp) :
      ↑((coyoneda.obj M).obj N) = (↑(Opposite.unop M) →* ↑N)
      source
      def CommGrp.coyonedaForget :
      coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommGrp CommGrp (Type u_1)).obj (CategoryTheory.forget CommGrp)) ≅ CategoryTheory.coyoneda

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def AddCommGrp.coyonedaForget :
        coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommGrp AddCommGrp (Type u_1)).obj (CategoryTheory.forget AddCommGrp)) ≅ CategoryTheory.coyoneda

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CommGrp.coyonedaForget_inv_app_app (X : CommGrpᵒᵖ) (X✝ : CommGrp) (a✝ : (CategoryTheory.coyoneda.obj X).obj X✝) :
          (coyonedaForget.inv.app X).app X✝ a✝ = Hom.hom a✝
          source
          @[simp]
          theorem AddCommGrp.coyonedaForget_hom_app_app_hom (X : AddCommGrpᵒᵖ) (X✝ : AddCommGrp) (a✝ : ((coyoneda.comp ((CategoryTheory.Functor.whiskeringRight AddCommGrp AddCommGrp (Type u_1)).obj (CategoryTheory.forget AddCommGrp))).obj X).obj X✝) :
          Hom.hom ((coyonedaForget.hom.app X).app X✝ a✝) = a✝
          source
          @[simp]
          theorem CommGrp.coyonedaForget_hom_app_app_hom (X : CommGrpᵒᵖ) (X✝ : CommGrp) (a✝ : ((coyoneda.comp ((CategoryTheory.Functor.whiskeringRight CommGrp CommGrp (Type u_1)).obj (CategoryTheory.forget CommGrp))).obj X).obj X✝) :
          Hom.hom ((coyonedaForget.hom.app X).app X✝ a✝) = a✝
          source
          @[simp]
          theorem AddCommGrp.coyonedaForget_inv_app_app (X : AddCommGrpᵒᵖ) (X✝ : AddCommGrp) (a✝ : (CategoryTheory.coyoneda.obj X).obj X✝) :
          (coyonedaForget.inv.app X).app X✝ a✝ = Hom.hom a✝
          source
          def CommGrp.coyonedaType :
          CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor CommGrp CommGrp)

          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 CommGrp-valued presheaves of commutative groups.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def AddCommGrp.coyonedaType :
            CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor AddCommGrp AddCommGrp)

            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 AddCommGrp-valued presheaves of commutative groups.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CommGrp.coyonedaType_obj_map (X : Type uᵒᵖ) {X✝ Y✝ : CommGrp} (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 CommGrp.coyonedaType_map_app {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (G : CommGrp) :
              (coyonedaType.map f).app G = ofHom (Pi.monoidHom fun (i : Opposite.unop Y✝) => Pi.evalMonoidHom (fun (a : Opposite.unop X✝) => ↑G) (f.unop i))
              source
              @[simp]
              theorem CommGrp.coyonedaType_obj_obj_coe (X : Type uᵒᵖ) (G : CommGrp) :
              ↑((coyonedaType.obj X).obj G) = (Opposite.unop X → ↑G)
              source
              @[simp]
              theorem AddCommGrp.coyonedaType_obj_obj_coe (X : Type uᵒᵖ) (G : AddCommGrp) :
              ↑((coyonedaType.obj X).obj G) = (Opposite.unop X → ↑G)
              source
              @[simp]
              theorem AddCommGrp.coyonedaType_obj_map (X : Type uᵒᵖ) {X✝ Y✝ : AddCommGrp} (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 AddCommGrp.coyonedaType_map_app {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (G : AddCommGrp) :
              (coyonedaType.map f).app G = ofHom (Pi.addMonoidHom fun (i : Opposite.unop Y✝) => Pi.evalAddMonoidHom (fun (a : Opposite.unop X✝) => ↑G) (f.unop i))