English
If F preserves and reflects the relevant colimits and limits, then C is finitary extensive whenever D is; i.e., finitaryExtensive C follows from the corresponding property in D via F.
Русский
Если F сохраняет и отражает соответствующие пределы и копродукты, тогда C является конечной расширяемой, если D такова; то есть финитная расширяемость C следует из аналогичного свойства в D через F.
LaTeX
$$$FinitaryExtensive\; C$ under assumptions on $F$ that preserve/reflect limits and colimits.$$
Lean4
instance {C} [Category C] {D} [Category D] (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] :
PreservesLimit (cospan f g) F :=
have := hasPullback_of_left_iso f g
preservesLimit_of_preserves_limit_cone (IsPullback.of_hasPullback f g).isLimit
((isLimitMapConePullbackConeEquiv _ pullback.condition).symm
(IsPullback.of_vert_isIso ⟨by simp only [← F.map_comp, pullback.condition]⟩).isLimit)
