preimage — Mathlib

English

If f: X → Y is affine, then the preimage of any affine open in Y is affine in X.

Русский

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

LaTeX

$$$IsAffineOpen U \\to IsAffineOpen (f^{-1}_{\\text{op}} U)$$$

Lean4

theorem preimage {X Y : Scheme} {U : Y.Opens} (hU : IsAffineOpen U) (f : X ⟶ Y) [IsAffineHom f] :
    IsAffineOpen (f ⁻¹ᵁ U) :=
  IsAffineHom.isAffine_preimage _ hU

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