instIsAffineHomιBasicOpen — Mathlib

English

If f is an affine morphism into Y and Y is affine, then preimage of an affine open is affine.

Русский

Если f — аффинная морфизм в Y и Y аффинна, то прообраз аффинного открытого множества является аффинным.

LaTeX

$$$\\forall f: X\\to Y, [IsAffineHom f] \\land [IsAffine Y] \\Rightarrow IsAffineOpen (\\text{preimage of affine open})$$$

Lean4

instance {X : Scheme} (r : Γ(X, ⊤)) : IsAffineHom (X.basicOpen r).ι :=
  by
  constructor
  intro U hU
  fapply (Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (X.basicOpen r).ι).mp
  convert hU.basicOpen (X.presheaf.map (homOfLE le_top).op r)
  rw [X.basicOpen_res]
  ext1
  refine Set.image_preimage_eq_inter_range.trans ?_
  simp

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