relative_isStableUnderComposition

English

If P is stable under composition, then so is P.relative F; composing two relative morphisms preserves the relative property.

Русский

Если P устойчива к композициям, то и P.relative F устойчива; композиция двух относительных морфизмов сохраняет относительное свойство.

LaTeX

$$$\text{IsStableUnderComposition}(P) \Rightarrow \text{IsStableUnderComposition}(P.relative F)$$$

Lean4

instance relative_isStableUnderComposition [F.Faithful] [F.Full] [P.IsStableUnderComposition] :
    IsStableUnderComposition (P.relative F) where
  comp_mem {F G H} f g hf
    hg := by
    refine ⟨comp_mem _ _ _ hf.1 hg.1, fun Z X p fst snd h ↦ ?_⟩
    rw [← hg.1.lift_snd (fst ≫ f) snd (by simpa using h.w)]
    refine
      comp_mem _ _ _ (hf.property (hg.1.fst p) fst _ (IsPullback.of_bot ?_ ?_ (hg.1.isPullback p))) (hg.property_snd p)
    · rw [← Functor.map_comp, lift_snd]
      exact h
    · symm
      apply hg.1.lift_fst

Похожие утверждения