English
If F preserves and reflects extensional structure and has finite limits, then C is finitary extensive whenever D is.
Русский
Если F сохраняет и отражает расширительную структуру и имеет конечные пределы, то C является финитно расширяемой тогда, когда D таковая.
LaTeX
$$$FinitaryExtensive\; C$ under preservation/reflection of extensional structure.$$
Lean4
theorem finitaryExtensive_of_preserves_and_reflects (F : C ⥤ D) [FinitaryExtensive D] [HasFiniteCoproducts C]
[HasPullbacksOfInclusions C] [PreservesPullbacksOfInclusions F] [ReflectsLimitsOfShape WalkingCospan F]
[PreservesColimitsOfShape (Discrete WalkingPair) F] [ReflectsColimitsOfShape (Discrete WalkingPair) F] :
FinitaryExtensive C := by
constructor
intro X Y c hc
refine IsVanKampenColimit.of_iso ?_ (hc.uniqueUpToIso (coprodIsCoprod X Y)).symm
have (i : Discrete WalkingPair) (Z : C) (f : Z ⟶ X ⨿ Y) :
PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app i)) F := by
rcases i with ⟨_ | _⟩ <;> dsimp <;> infer_instance
refine (FinitaryExtensive.vanKampen _ (isColimitOfPreserves F (coprodIsCoprod X Y))).of_mapCocone F
