diagonal — Mathlib

English

If P respects isomorphisms, then the diagonal construction P.diagonal also respects isomorphisms.

Русский

Если свойство P сохраняет изоморфизмы, тогда диагональная конструкция P.diagonal также сохраняет изоморфизмы.

LaTeX

$$[P.RespectsIso] ⇒ P.diagonal.RespectsIso$$

Lean4

instance diagonal [P.RespectsIso] : P.diagonal.RespectsIso :=
  by
  apply RespectsIso.mk
  · introv H
    rwa [diagonal_iff, pullback.diagonal_comp, P.cancel_left_of_respectsIso, P.cancel_left_of_respectsIso, ←
      P.cancel_right_of_respectsIso _ (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)),
      ← pullback.condition, P.cancel_left_of_respectsIso]
  · introv H
    delta diagonal
    rwa [pullback.diagonal_comp, P.cancel_right_of_respectsIso]

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