respectsIso_mk — Mathlib

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⟩

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