Documentation

Mathlib.CategoryTheory.Limits.Shapes.End

Ends and coends #

In this file, given a functor F : Jᵒᵖ ⥤ J ⥤ C, we define its end end_ F, which is a suitable multiequalizer of the objects (F.obj (op j)).obj j for all j : J. For this shape of limits, cones are named wedges: the corresponding type is Wedge F.

References #

TODO #

source
def CategoryTheory.Limits.multicospanIndexEnd {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) :
CategoryTheory.Limits.MulticospanIndex C

Given F : Jᵒᵖ ⥤ J ⥤ C, this is the multicospan index which shall be used to define the end of F.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_sndTo {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) :
    (CategoryTheory.Limits.multicospanIndexEnd F).sndTo f = f.right
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_R {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) :
    (CategoryTheory.Limits.multicospanIndexEnd F).R = CategoryTheory.Arrow J
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_L {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) :
    (CategoryTheory.Limits.multicospanIndexEnd F).L = J
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_left {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (j : J) :
    (CategoryTheory.Limits.multicospanIndexEnd F).left j = (F.obj (Opposite.op j)).obj j
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_fst {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) :
    (CategoryTheory.Limits.multicospanIndexEnd F).fst f = (F.obj (Opposite.op f.left)).map f.hom
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_fstTo {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) :
    (CategoryTheory.Limits.multicospanIndexEnd F).fstTo f = f.left
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_right {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) :
    (CategoryTheory.Limits.multicospanIndexEnd F).right f = (F.obj (Opposite.op f.left)).obj f.right
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanIndexEnd_snd {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : CategoryTheory.Arrow J) :
    (CategoryTheory.Limits.multicospanIndexEnd F).snd f = (F.map f.hom.op).app f.right
    source
    @[reducible, inline]
    abbrev CategoryTheory.Limits.Wedge {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) :
    Type (max (max (max u v) u') v')

    Given F : Jᵒᵖ ⥤ J ⥤ C, a wedge for F is a type of cones (specifically the type of multiforks for multicospanIndexEnd F): the point of universal of these wedges shall be the end of F.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev CategoryTheory.Limits.Wedge.mk {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) :
      CategoryTheory.Limits.Wedge F

      Constructor for wedges.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Limits.Wedge.mk_pt {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) :
        (CategoryTheory.Limits.Wedge.mk pt π hπ).pt = pt
        source
        @[simp]
        theorem CategoryTheory.Limits.Wedge.mk_ι {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) (j : J) :
        CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Wedge.mk pt π hπ) j = π j
        source
        theorem CategoryTheory.Limits.Wedge.condition {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Wedge F) {i : J} {j : J} (f : i ⟶ j) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) ((F.map f.op).app j)
        source
        theorem CategoryTheory.Limits.Wedge.condition_assoc {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Wedge F) {i : J} {j : J} (f : i ⟶ j) {Z : C} (h : (F.obj (Opposite.op i)).obj j ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c i) (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
        source
        theorem CategoryTheory.Limits.Wedge.IsLimit.hom_ext {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} {f : X ⟶ c.pt} {g : X ⟶ c.pt} (h : ∀ (j : (CategoryTheory.Limits.multicospanIndexEnd F).L), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Multifork.ι c j) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Multifork.ι c j)) :
        f = g
        source
        def CategoryTheory.Limits.Wedge.IsLimit.lift {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) :
        X ⟶ c.pt

        Construct a morphism to the end from its universal property.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Limits.Wedge.IsLimit.lift_ι {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf) (CategoryTheory.Limits.Multifork.ι c j) = f j
          source
          @[simp]
          theorem CategoryTheory.Limits.Wedge.IsLimit.lift_ι_assoc {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F} (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) {Z : C} (h : (CategoryTheory.Limits.multicospanIndexEnd F).left j ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) h) = CategoryTheory.CategoryStruct.comp (f j) h
          source
          @[reducible, inline]
          abbrev CategoryTheory.Limits.HasEnd {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) :
          Prop

          Given F : Jᵒᵖ ⥤ J ⥤ C, this property asserts the existence of the end of F.

          Equations
          Instances For
            source
            noncomputable def CategoryTheory.Limits.end_ {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [CategoryTheory.Limits.HasEnd F] :
            C

            The end of a functor F : Jᵒᵖ ⥤ J ⥤ C.

            Equations
            Instances For
              source
              noncomputable def CategoryTheory.Limits.end_.π {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [CategoryTheory.Limits.HasEnd F] (j : J) :
              CategoryTheory.Limits.end_ F ⟶ (F.obj (Opposite.op j)).obj j

              Given F : Jᵒᵖ ⥤ J ⥤ C, this is the projection end_ F ⟶ (F.obj (op j)).obj j for any j : J.

              Equations
              Instances For
                source
                theorem CategoryTheory.Limits.end_.condition {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [CategoryTheory.Limits.HasEnd F] {i : J} {j : J} (f : i ⟶ j) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F i) ((F.obj (Opposite.op i)).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j) ((F.map f.op).app j)
                source
                theorem CategoryTheory.Limits.end_.condition_assoc {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [CategoryTheory.Limits.HasEnd F] {i : J} {j : J} (f : i ⟶ j) {Z : C} (h : (F.obj (Opposite.op i)).obj j ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F i) (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j) (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
                source
                theorem CategoryTheory.Limits.hom_ext {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [CategoryTheory.Limits.HasEnd F] {X : C} {f : X ⟶ CategoryTheory.Limits.end_ F} {g : X ⟶ CategoryTheory.Limits.end_ F} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.end_.π F j) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.end_.π F j)) :
                f = g
                source
                noncomputable def CategoryTheory.Limits.end_.lift {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [CategoryTheory.Limits.HasEnd F] {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) :
                X ⟶ CategoryTheory.Limits.end_ F

                Constructor for morphisms to the end of a functor.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Limits.end_.lift_π {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [CategoryTheory.Limits.HasEnd F] {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.lift f hf) (CategoryTheory.Limits.end_.π F j) = f j
                  source
                  @[simp]
                  theorem CategoryTheory.Limits.end_.lift_π_assoc {J : Type u} [CategoryTheory.Category.{v, u} J] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [CategoryTheory.Limits.HasEnd F] {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) = CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) (j : J) {Z : C} (h : (F.obj (Opposite.op j)).obj j ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.lift f hf) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j) h) = CategoryTheory.CategoryStruct.comp (f j) h