comp_of_isOpenImmersion — Mathlib

English

A property P on Scheme morphisms corresponds to Q on ring homomorphisms after passing to Spec.

Русский

Свойство P для морфизмов схем соответствует свойству Q для колец после перехода к Spec.

LaTeX

$$Spec.map φ property equivalence with Q φ.hom$$

Lean4

theorem comp_of_isOpenImmersion [IsOpenImmersion f] (H : P g) : P (f ≫ g) :=
  by
  rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H ⊢
  intro U V e
  have : IsIso (f.appLE (f ''ᵁ V) V.1 (f.preimage_image_eq _).ge) :=
    inferInstanceAs (IsIso (f.app _ ≫ X.presheaf.map (eqToHom (f.preimage_image_eq _).symm).op))
  rw [← Scheme.appLE_comp_appLE _ _ _ (f ''ᵁ V) V.1 (Set.image_subset_iff.mpr e) (f.preimage_image_eq _).ge,
    CommRingCat.hom_comp, (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso]
  exact H _ ⟨_, V.2.image_of_isOpenImmersion _⟩ _

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