English
A variant stating that if F preserves the shape WalkingCospan and J is stable under base change, then the comap J.comap F is stable under base change.
Русский
Вариант того же утверждения: если F сохраняет форму WalkingCospan и J стабильно относительно изменения базы, то J.comap F стабильно по базовому изменению.
LaTeX
$$$ (J.comap F) \\text{ IsStableUnderBaseChange}$$$
Lean4
instance [PreservesLimitsOfShape WalkingCospan F] [IsStableUnderBaseChange.{w} J] :
IsStableUnderBaseChange.{w} (J.comap F) where
mem_coverings_of_isPullback {ι} S Y f hf Z g P p₁ p₂
h := by
simp only [mem_comap_iff, Presieve.map_ofArrows] at hf ⊢
exact mem_coverings_of_isPullback _ hf _ _ _ fun i ↦ CategoryTheory.Functor.map_isPullback F (h i)
