English
Let F: C → D be a functor and P a morphism property on C. Then the class of morphisms X ⟶ Y in D that are relatively representable with respect to F is stable under base change: if a pullback of a relatively representable morphism exists, the pulled-back morphism is again relatively representable (with respect to F).
Русский
Пусть F: C → D — функтор, и P — свойство морфизмов в C. Тогда множество морфизмов X ⟶ Y в D, которые относительно представимы по F, устойчиво при базовом изменении: если существует вытяжка по базовому изменению, вытянутый морфизм снова относительно представим по F.
LaTeX
$$$\text{IsStableUnderBaseChange}(F.\text{relativelyRepresentable})$$$
Lean4
instance isStableUnderBaseChange : IsStableUnderBaseChange F.relativelyRepresentable where
of_isPullback {X Y Y' X' f g f' g'} P₁ hg a
h := by
refine ⟨hg.pullback (h ≫ f), hg.snd (h ≫ f), ?_, ?_⟩
· apply P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) (by simpa using hg.w (h ≫ f))
· apply IsPullback.of_right' (hg.isPullback (h ≫ f)) P₁
