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 #
- define coends
def
CategoryTheory.Limits.multicospanIndexEnd
{J : Type u}
[Category.{v, u} J]
{C : Type u'}
[Category.{v', u'} C]
(F : Functor Jᵒᵖ (Functor 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
@[simp]
theorem
CategoryTheory.Limits.multicospanIndexEnd_sndTo
{J : Type u}
[Category.{v, u} J]
{C : Type u'}
[Category.{v', u'} C]
(F : Functor Jᵒᵖ (Functor J C))
(f : Arrow J)
:
(multicospanIndexEnd F).sndTo f = f.right
@[simp]
theorem
CategoryTheory.Limits.multicospanIndexEnd_R
{J : Type u}
[Category.{v, u} J]
{C : Type u'}
[Category.{v', u'} C]
(F : Functor Jᵒᵖ (Functor J C))
:
(multicospanIndexEnd F).R = Arrow J
@[simp]
theorem
CategoryTheory.Limits.multicospanIndexEnd_L
{J : Type u}
[Category.{v, u} J]
{C : Type u'}
[Category.{v', u'} C]
(F : Functor Jᵒᵖ (Functor J C))
:
(multicospanIndexEnd F).L = J
@[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 : J)
:
(multicospanIndexEnd F).left j = (F.obj (Opposite.op j)).obj j
@[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 : Arrow J)
:
(multicospanIndexEnd F).fst f = (F.obj (Opposite.op f.left)).map f.hom
@[simp]
theorem
CategoryTheory.Limits.multicospanIndexEnd_fstTo
{J : Type u}
[Category.{v, u} J]
{C : Type u'}
[Category.{v', u'} C]
(F : Functor Jᵒᵖ (Functor J C))
(f : Arrow J)
:
(multicospanIndexEnd F).fstTo f = f.left
@[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 : Arrow J)
:
(multicospanIndexEnd F).right f = (F.obj (Opposite.op f.left)).obj f.right
@[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 : Arrow J)
:
(multicospanIndexEnd F).snd f = (F.map f.hom.op).app f.right
@[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
@[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
@[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))
:
@[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
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)
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)
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 : (multicospanIndexEnd F).L), CategoryStruct.comp f (Multifork.ι c j) = CategoryStruct.comp g (Multifork.ι c j))
:
f = g
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
@[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
@[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
@[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))
:
Given F : Jᵒᵖ ⥤ J ⥤ C, this property asserts the existence of the end of F.
Equations
Instances For
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
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
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)
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)
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
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))
:
Constructor for morphisms to the end of a functor.
Equations
Instances For
@[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
@[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