cocone — Mathlib

Lean4
/-- A choice of cocone for a functor `F : A ⥤ J` such that `HasCardinalLT (Arrow A) κ`
when `J` is a `κ`-filtered category, and `Arrow A` has cardinality `< κ`. -/
noncomputable def cocone {A : Type v'} [Category.{u'} A] (F : A ⥤ J) (hA : HasCardinalLT (Arrow A) κ) : Cocone F :=
  by
  have := hA.small
  have := small_of_small_arrow.{w} A
  have := locallySmall_of_small_arrow.{w} A
  let e := (Shrink.equivalence.{w} A).trans (ShrinkHoms.equivalence.{w} (Shrink.{w} A))
  exact
    (Cocones.equivalenceOfReindexing e.symm (Iso.refl _)).inverse.obj
      (nonempty_cocone (κ := κ) (e.inverse ⋙ F) (by simpa)).some
Похожие утверждения