English
If X is κ-presentable and F: C → C' is an equivalence, then F.obj X is κ-presentable.
Русский
Если X κ-представим и F: C → C' — эквивалентность, то F.obj X κ-представим.
LaTeX
$$$[IsCardinalPresentable X \kappa] (F : C \to C') [F.IsEquivalence] : IsCardinalPresentable (F.obj X) \kappa$$$
Lean4
theorem isCardinalPresentable_of_equivalence {C' : Type u₃} [Category.{v₃} C'] [IsCardinalPresentable X κ]
(e : C ≌ C') : IsCardinalPresentable (e.functor.obj X) κ :=
by
refine ⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩
have := preservesColimitsOfShape_of_isCardinalPresentable X κ J
suffices PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) from
⟨fun {c} hc ↦
⟨isColimitOfReflects uliftFunctor.{v₁}
(isColimitOfPreserves (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) hc)⟩⟩
have iso :
coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁} ≅ e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃} :=
NatIso.ofComponents (fun Z ↦ (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso)
(by
intro _ _ f
ext ⟨g⟩
apply Equiv.ulift.injective
simp [Adjunction.homEquiv_unit])
exact preservesColimit_of_natIso Y iso.symm
