diagonal_respectsIso — Mathlib

English

If P is a morphism property of schemes that respects isomorphisms, then the diagonal construction P.diagonal also respects isomorphisms.

Русский

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

LaTeX

$$$(P.diagonal).toProperty.RespectsIso$$

Lean4

instance diagonal_respectsIso (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] :
    P.diagonal.toProperty.RespectsIso :=
  by
  delta AffineTargetMorphismProperty.diagonal
  apply AffineTargetMorphismProperty.respectsIso_mk
  · introv H _ _
    rw [pullback.mapDesc_comp, P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
    apply H
  · introv H _ _
    rw [pullback.mapDesc_comp, P.cancel_right_of_respectsIso]
    apply H

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