English
Given two construction schemes for turning a morphism-property into a property on schemes, if both preserve isomorphisms appropriately, then the resulting property respects isomorphisms.
Русский
Пусть две конструкторские схемы перехода свойства морфизмов в свойства схем сохраняют изоморфизмы согласованно; тогда полученное свойство сохраняет изоморфизмы.
LaTeX
$$A formal statement about assembling RespectsIso via mk construction.$$
Lean4
theorem respectsIso_mk {P : AffineTargetMorphismProperty}
(h₁ : ∀ {X Y Z} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], P f → P (e.hom ≫ f))
(h₂ : ∀ {X Y Z} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], P f → @P _ _ (f ≫ e.hom) (.of_isIso e.inv)) :
P.toProperty.RespectsIso := by
apply MorphismProperty.RespectsIso.mk
· rintro X Y Z e f ⟨a, h⟩; exact ⟨a, h₁ e f h⟩
· rintro X Y Z e f ⟨a, h⟩; exact ⟨.of_isIso e.inv, h₂ e f h⟩