Documentation

Mathlib.CategoryTheory.Limits.Types.Yoneda

Cones and limits #

In this file, we give the natural isomorphism between cones on F with cone point X and the type lim Hom(X, F·), and similarly the natural isomorphism between cocones on F with cocone point X and the type lim Hom(F·, X).

source
def CategoryTheory.Limits.compCoyonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J C) (X : C) :
↑(F.comp (coyoneda.obj (Opposite.op X))).sections ≃ ((Functor.const J).obj X ⟶ F)

Sections of F ⋙ coyoneda.obj (op X) identify to natural transformations (const J).obj X ⟶ F.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J C) (X : C) (s : ↑(F.comp (coyoneda.obj (Opposite.op X))).sections) (j : J) :
    ((compCoyonedaSectionsEquiv F X) s).app j = ↑s j
    source
    @[simp]
    theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J C) (X : C) (τ : (Functor.const J).obj X ⟶ F) (X✝ : J) :
    ↑((compCoyonedaSectionsEquiv F X).symm τ) X✝ = τ.app X✝
    source
    def CategoryTheory.Limits.opCompYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J C) (X : C) :
    ↑(F.op.comp (yoneda.obj X)).sections ≃ (F ⟶ (Functor.const J).obj X)

    Sections of F.op ⋙ yoneda.obj X identify to natural transformations F ⟶ (const J).obj X.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J C) (X : C) (τ : F ⟶ (Functor.const J).obj X) (j : Jᵒᵖ) :
      ↑((opCompYonedaSectionsEquiv F X).symm τ) j = τ.app (Opposite.unop j)
      source
      @[simp]
      theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J C) (X : C) (s : ↑(F.op.comp (yoneda.obj X)).sections) (j : J) :
      ((opCompYonedaSectionsEquiv F X) s).app j = ↑s (Opposite.op j)
      source
      def CategoryTheory.Limits.compYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J Cᵒᵖ) (X : C) :
      ↑(F.comp (yoneda.obj X)).sections ≃ ((Functor.const J).obj (Opposite.op X) ⟶ F)

      Sections of F ⋙ yoneda.obj X identify to natural transformations (const J).obj X ⟶ F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Limits.compYonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J Cᵒᵖ) (X : C) (τ : (Functor.const J).obj (Opposite.op X) ⟶ F) (j : J) :
        ↑((compYonedaSectionsEquiv F X).symm τ) j = (τ.app j).unop
        source
        @[simp]
        theorem CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] (F : Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (yoneda.obj X)).sections) (j : J) :
        ((compYonedaSectionsEquiv F X) s).app j = Quiver.Hom.op (↑s j)
        source
        noncomputable def CategoryTheory.Limits.limitCompCoyonedaIsoCone {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) :
        limit (F.comp (coyoneda.obj (Opposite.op X))) ≅ (Functor.const J).obj X ⟶ F

        A cone on F with cone point X is the same as an element of lim Hom(X, F·).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_inv {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) :
          (limitCompCoyonedaIsoCone F X).inv = TypeCat.ofHom fun (t : (Functor.const J).obj X ⟶ F) => (ConcreteCategory.hom (limit.lift (F.comp (coyoneda.obj (Opposite.op X))) (Types.coneOfSection ⋯))) PUnit.unit
          source
          @[simp]
          theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_hom {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) :
          (limitCompCoyonedaIsoCone F X).hom = TypeCat.ofHom fun (a : limit (F.comp (coyoneda.obj (Opposite.op X)))) => { app := fun (j : J) => (ConcreteCategory.hom (limit.π (F.comp (coyoneda.obj (Opposite.op X))) j)) a, naturality := ⋯ }
          source
          noncomputable def CategoryTheory.Limits.whiskeringLimYonedaIsoCones (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] :
          (Functor.whiskeringLeft J C (Type v)).comp (((Functor.whiskeringRight (Functor C (Type v)) (Functor J (Type v)) (Type v)).obj lim).comp ((Functor.whiskeringLeft Cᵒᵖ (Functor C (Type v)) (Type v)).obj coyoneda)) ≅ cones J C

          A cone on F with cone point X is the same as an element of lim Hom(X, F·), naturally in F and X.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_hom_apply_app (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : Functor J C) (X✝ : Cᵒᵖ) (a : limit (X.comp (coyoneda.obj (Opposite.op (Opposite.unop X✝))))) (j : J) :
            ((ConcreteCategory.hom (((whiskeringLimYonedaIsoCones J C).hom.app X).app X✝)) a).app j = (ConcreteCategory.hom (limit.π (X.comp (coyoneda.obj X✝)) j)) a
            source
            @[simp]
            theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app_hom_apply (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : Functor J C) (X✝ : Cᵒᵖ) (t : (Functor.const J).obj (Opposite.unop X✝) ⟶ X) :
            (ConcreteCategory.hom (((whiskeringLimYonedaIsoCones J C).inv.app X).app X✝)) t = (ConcreteCategory.hom (limit.lift (X.comp (coyoneda.obj X✝)) (Types.coneOfSection ⋯))) PUnit.unit
            source
            noncomputable def CategoryTheory.Limits.limitCompYonedaIsoCocone {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) :
            limit (F.op.comp (yoneda.obj X)) ≅ F ⟶ (Functor.const J).obj X

            A cocone on F with cocone point X is the same as an element of lim Hom(F·, X).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_hom {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) :
              (limitCompYonedaIsoCocone F X).hom = TypeCat.ofHom fun (a : limit (F.op.comp (yoneda.obj X))) => { app := fun (j : J) => (ConcreteCategory.hom (limit.π (F.op.comp (yoneda.obj X)) (Opposite.op j))) a, naturality := ⋯ }
              source
              @[simp]
              theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_inv {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) :
              (limitCompYonedaIsoCocone F X).inv = TypeCat.ofHom fun (t : F ⟶ (Functor.const J).obj X) => (ConcreteCategory.hom (limit.lift (F.op.comp (yoneda.obj X)) (Types.coneOfSection ⋯))) PUnit.unit
              source
              noncomputable def CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] :
              (Functor.opHom J C).comp ((Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).comp (((Functor.whiskeringRight (Functor Cᵒᵖ (Type v)) (Functor Jᵒᵖ (Type v)) (Type v)).obj lim).comp ((Functor.whiskeringLeft C (Functor Cᵒᵖ (Type v)) (Type v)).obj yoneda))) ≅ cocones J C

              A cocone on F with cocone point X is the same as an element of lim Hom(F·, X), naturally in F and X.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app_hom_apply (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : (Functor J C)ᵒᵖ) (X✝ : C) (t : Opposite.unop X ⟶ (Functor.const J).obj X✝) :
                (ConcreteCategory.hom (((opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X).app X✝)) t = (ConcreteCategory.hom (limit.lift ((Opposite.unop X).op.comp (yoneda.obj X✝)) (Types.coneOfSection ⋯))) PUnit.unit
                source
                @[simp]
                theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_hom_apply_app (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : (Functor J C)ᵒᵖ) (X✝ : C) (a : limit ((Opposite.unop X).op.comp (yoneda.obj X✝))) (j : J) :
                ((ConcreteCategory.hom (((opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X✝)) a).app j = (ConcreteCategory.hom (limit.π ((Opposite.unop X).op.comp (yoneda.obj X✝)) (Opposite.op j))) a
                source
                @[deprecated "Use `(opHomCompWhiskeringLimYonedaIsoCocones _ _).app _` instead" (since := "2026-04-08")]
                noncomputable def CategoryTheory.Limits.yonedaCompLimIsoCocones {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) :
                yoneda.comp (((Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp lim) ≅ F.cocones

                A cocone on F with cocone point X is the same as an element of lim Hom(F·, X), naturally in X.

                Equations
                Instances For