of_isLocalization — Mathlib

English

There is a simple identity linking appIso inverse with app on the image of a subset, expressing the compatibility of the two ways to move sections along f.

Русский

Существуют простые тождества, связывающие обратную часть appIso и app на образе подмножества, отражающие совместимость способов перемещения секций по f.

LaTeX

$$$$ (f.appIso U).inv \;≫ \; f.app (f''^\!U) = X.presheaf.map (eqToHom (preimage_image_eq f U)).op $$$$

Lean4

theorem _root_.AlgebraicGeometry.IsOpenImmersion.of_isLocalization {R S} [CommRing R] [CommRing S] [Algebra R S] (f : R)
    [IsLocalization.Away f S] : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S))) :=
  by
  have e := (IsLocalization.algEquiv (.powers f) S (Localization.Away f)).symm.toAlgHom.comp_algebraMap
  rw [← e, CommRingCat.ofHom_comp, Spec.map_comp]
  have H :
    IsIso
      (CommRingCat.ofHom
        (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm.toAlgHom.toRingHom) :=
    by
    exact
      inferInstanceAs
        (IsIso <|
          (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)
  simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.toRingHom_eq_coe, AlgEquiv.toAlgHom_toRingHom] at H ⊢
  infer_instance

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