English
For each X, the X-component of the natural transformation natTrans φ is given by composing the inverse of a canonical map with φ.app X.
Русский
Для каждого X компонент natTrans φ задаётся через композицию обратного канонического отображения и φ.app X.
LaTeX
$$$$ (natTrans.{w} φ).app (uliftYoneda.{max w v₂}.obj X) = (compULiftYonedaIsoULiftYonedaCompLan.{w} F).inv.app X \;\gg\; φ.app X $$$$
Lean4
instance {J : Type w} [Category.{w'} J] {X : Type u} [IsFilteredOrEmpty J] :
PreservesColimitsOfShape J (functorToTypes (X := X)) where
preservesColimit
{F} := by
apply preservesColimit_of_preserves_colimit_cocone (colimitCocone F).isColimit
apply Types.FilteredColimit.isColimitOf
· rintro ⟨x, hx⟩
simp only [colimitCocone_cocone_pt, iSup_eq_iUnion, mem_iUnion] at hx
obtain ⟨i, hi⟩ := hx
exact ⟨i, ⟨x, hi⟩, rfl⟩
· intro i j ⟨x, hx⟩ ⟨y, hy⟩ h
obtain rfl : x = y := by simpa using h
exact ⟨IsFiltered.max i j, IsFiltered.leftToMax i j, IsFiltered.rightToMax i j, rfl⟩
