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.multicospanShapeEnd (J : Type u) [Category.{v, u} J] :
MulticospanShape

The shape of multiequalizer diagrams involved in the definition of ends.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanShapeEnd_R (J : Type u) [Category.{v, u} J] :
    (multicospanShapeEnd J).R = Arrow J
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanShapeEnd_fst (J : Type u) [Category.{v, u} J] (f : Arrow J) :
    (multicospanShapeEnd J).fst f = f.left
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanShapeEnd_L (J : Type u) [Category.{v, u} J] :
    (multicospanShapeEnd J).L = J
    source
    @[simp]
    theorem CategoryTheory.Limits.multicospanShapeEnd_snd (J : Type u) [Category.{v, u} J] (f : Arrow J) :
    (multicospanShapeEnd J).snd f = f.right
    source
    def CategoryTheory.Limits.multicospanIndexEnd {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) :
    MulticospanIndex (multicospanShapeEnd J) 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_left {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (j : (multicospanShapeEnd J).L) :
      (multicospanIndexEnd F).left j = (F.obj (Opposite.op j)).obj j
      source
      @[simp]
      theorem CategoryTheory.Limits.multicospanIndexEnd_right {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multicospanShapeEnd J).R) :
      (multicospanIndexEnd F).right f = (F.obj (Opposite.op f.left)).obj f.right
      source
      @[simp]
      theorem CategoryTheory.Limits.multicospanIndexEnd_snd {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multicospanShapeEnd J).R) :
      (multicospanIndexEnd F).snd f = (F.map f.hom.op).app f.right
      source
      @[simp]
      theorem CategoryTheory.Limits.multicospanIndexEnd_fst {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (Functor J C)) (f : (multicospanShapeEnd J).R) :
      (multicospanIndexEnd F).fst f = (F.obj (Opposite.op f.left)).map f.hom
      source
      @[reducible, inline]
      abbrev CategoryTheory.Limits.Wedge {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor Jᵒᵖ (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} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {F : Functor Jᵒᵖ (Functor J C)} (pt : C) (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) (hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) = CategoryStruct.comp (π j) ((F.map f.op).app j)) :
        Wedge F

        Constructor for wedges.

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

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

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

                  Constructor for morphisms to the end of a functor.

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