limitConeLift — Mathlib

Lean4
/-- Auxiliary definition: the universal morphism to the proposed limit cone. -/
@[simps]
def limitConeLift (F : J ⥤ Cat.{v, v}) (s : Cone F) : s.pt ⟶ limitConeX F
    where
  obj :=
    limit.lift (F ⋙ Cat.objects)
      { pt := s.pt
        π :=
          { app := fun j => (s.π.app j).obj
            naturality := fun _ _ f => objects.congr_map (s.π.naturality f) } }
  map
    f := by
    fapply Types.Limit.mk.{v, v}
    · intro j
      refine eqToHom ?_ ≫ (s.π.app j).map f ≫ eqToHom ?_ <;> simp
    · intro j j' h
      dsimp
      simp only [Category.assoc, Functor.map_comp, eqToHom_map, eqToHom_trans, eqToHom_trans_assoc, ← Functor.comp_map]
      have := (s.π.naturality h).symm
      dsimp at this
      rw [Category.id_comp] at this
      erw [Functor.congr_hom this f]
      simp
Похожие утверждения