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).

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.

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

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

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.

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

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

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.

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

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

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.

@[simp]

theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_inv {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : (Functor.const J).obj X ⟶ F) : (limitCompCoyonedaIsoCone F X).inv a✝ = (Types.limitEquivSections (F.comp (coyoneda.obj (Opposite.op X)))).symm ((compCoyonedaSectionsEquiv F X).symm a✝)

@[simp]

theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_hom_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : limit (F.comp (coyoneda.obj (Opposite.op X)))) (j : J) : ((limitCompCoyonedaIsoCone F X).hom a✝).app j = limit.π (F.comp (coyoneda.obj (Opposite.op X))) j a✝

noncomputable def CategoryTheory.Limits.coyonedaCompLimIsoCones {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) : coyoneda.comp (((Functor.whiskeringLeft J C (Type v)).obj F).comp lim) ≅ F.cones

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

Equations

• CategoryTheory.Limits.coyonedaCompLimIsoCones F = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => CategoryTheory.Limits.limitCompCoyonedaIsoCone F (Opposite.unop X)) ⋯

@[simp]

theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_hom_app_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : Cᵒᵖ) (a✝ : (coyoneda.comp (((Functor.whiskeringLeft J C (Type v)).obj F).comp lim)).obj X) (j : J) : ((coyonedaCompLimIsoCones F).hom.app X a✝).app j = limit.π (F.comp (coyoneda.obj X)) j a✝

@[simp]

theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_inv_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : Cᵒᵖ) (a✝ : F.cones.obj X) : (coyonedaCompLimIsoCones F).inv.app X a✝ = (Types.limitEquivSections (F.comp (coyoneda.obj X))).symm ((compCoyonedaSectionsEquiv F (Opposite.unop X)).symm a✝)

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

• CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C = CategoryTheory.NatIso.ofComponents CategoryTheory.Limits.coyonedaCompLimIsoCones ⋯

@[simp]

theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : Functor J C) (X✝ : Cᵒᵖ) (a✝ : X.cones.obj X✝) : ((whiskeringLimYonedaIsoCones J C).inv.app X).app X✝ a✝ = (Types.limitEquivSections (X.comp (coyoneda.obj X✝))).symm ((compCoyonedaSectionsEquiv X (Opposite.unop X✝)).symm a✝)

@[simp]

theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_app (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : Functor J C) (X✝ : Cᵒᵖ) (a✝ : (coyoneda.comp (((Functor.whiskeringLeft J C (Type v)).obj X).comp lim)).obj X✝) (j : J) : (((whiskeringLimYonedaIsoCones J C).hom.app X).app X✝ a✝).app j = limit.π (X.comp (coyoneda.obj X✝)) j a✝

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.

@[simp]

theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_hom_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : limit (F.op.comp (yoneda.obj X))) (j : J) : ((limitCompYonedaIsoCocone F X).hom a✝).app j = limit.π (F.op.comp (yoneda.obj X)) (Opposite.op j) a✝

@[simp]

theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_inv {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : F ⟶ (Functor.const J).obj X) : (limitCompYonedaIsoCocone F X).inv a✝ = (Types.limitEquivSections (F.op.comp (yoneda.obj X))).symm ((opCompYonedaSectionsEquiv F X).symm a✝)

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

• CategoryTheory.Limits.yonedaCompLimIsoCocones F = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.limitCompYonedaIsoCocone F) ⋯

@[simp]

theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_hom_app_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : (yoneda.comp (((Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp lim)).obj X) (j : J) : ((yonedaCompLimIsoCocones F).hom.app X a✝).app j = limit.π (F.op.comp (yoneda.obj X)) (Opposite.op j) a✝

@[simp]

theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_inv_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : F.cocones.obj X) : (yonedaCompLimIsoCocones F).inv.app X a✝ = (Types.limitEquivSections (F.op.comp (yoneda.obj X))).symm ((opCompYonedaSectionsEquiv F X).symm a✝)

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.

@[simp]

theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : (Functor J C)ᵒᵖ) (X✝ : C) (a✝ : (yoneda.comp (((Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj (Opposite.unop X).op).comp lim)).obj X✝) (j : J) : (((opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X✝ a✝).app j = limit.π ((Opposite.unop X).op.comp (yoneda.obj X✝)) (Opposite.op j) a✝

@[simp]

theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app (J : Type v) [SmallCategory J] (C : Type u) [Category.{v, u} C] (X : (Functor J C)ᵒᵖ) (X✝ : C) (a✝ : (Opposite.unop X).cocones.obj X✝) : ((opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X).app X✝ a✝ = (Types.limitEquivSections ((Opposite.unop X).op.comp (yoneda.obj X✝))).symm ((opCompYonedaSectionsEquiv (Opposite.unop X) X✝).symm a✝)