diagonal_isStableUnderComposition

English

Let P be a morphism property that is stable under composition, stable under base change, and respects isomorphisms. Then the diagonal construction P.diagonal is stable under composition.

Русский

Пусть P — свойство морфизмов, устойчивое к композиции и изменению основания, а также сохраняющее эквивалентности. Тогда диагональная конструкция P.diagonal устойчива по отношению к композиции.

LaTeX

$$$IsStableUnderComposition(P_{\mathrm{diag}})$$$

Lean4

instance diagonal_isStableUnderComposition [P.IsStableUnderComposition] [RespectsIso P] [IsStableUnderBaseChange P] :
    P.diagonal.IsStableUnderComposition where
  comp_mem _ _ h₁
    h₂ := by
    rw [diagonal_iff, pullback.diagonal_comp]
    exact P.comp_mem _ _ h₁ (by simpa only [cancel_left_of_respectsIso] using P.pullback_snd _ _ h₂)

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