affineOpensEquiv — Mathlib

English

For an affine open U, the appTop of hU.isoSpec.hom equals the map induced by the Γ-spec isomorphism, i.e., hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv.

Русский

Для аффинного открытого множества U appTop гомоморфизма hU.isoSpec.hom равен отображению, индуцированному Γ-специзом, то есть hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ∘ U.topIso.inv.

LaTeX

$$hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv$$

Lean4

/-- The affine open sets of an open subscheme corresponds to
the affine open sets containing in the image. -/
@[simps]
def _root_.AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv (f : X ⟶ Y) [H : IsOpenImmersion f] :
    X.affineOpens ≃ { U : Y.affineOpens // U ≤ f.opensRange }
    where
  toFun U := ⟨⟨f ''ᵁ U, U.2.image_of_isOpenImmersion f⟩, Set.image_subset_range _ _⟩
  invFun
    U :=
    ⟨f ⁻¹ᵁ U,
      f.isAffineOpen_iff_of_isOpenImmersion.mp
        (by rw [show f ''ᵁ f ⁻¹ᵁ U = U from Opens.ext (Set.image_preimage_eq_of_subset U.2)]; exact U.1.2)⟩
  left_inv _ := Subtype.ext (Opens.ext (Set.preimage_image_eq _ H.base_open.injective))
  right_inv U := Subtype.ext (Subtype.ext (Opens.ext (Set.image_preimage_eq_of_subset U.2)))

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