Affine morphisms of schemes

A morphism of schemes f : X ⟶ Y is affine if the preimage of an arbitrary affine open subset of Y is affine.

It is equivalent to ask only that Y is covered by affine opens whose preimage is affine.

Main results

• AlgebraicGeometry.IsAffineHom: The class of affine morphisms.
• AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen: If s is a spanning set of Γ(X, U), such that each X.basicOpen i is affine, then U is also affine.
• AlgebraicGeometry.isAffineHom_isStableUnderBaseChange: Affine morphisms are stable under base change.

We also provide the instance HasAffineProperty @IsAffineHom fun X _ _ _ ↦ IsAffine X.

class AlgebraicGeometry.IsAffineHom {X Y : Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes X ⟶ Y is affine if the preimage of any affine open subset of Y is affine.

• isAffine_preimage (U : Y.Opens) : IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)

theorem AlgebraicGeometry.isAffineHom_iff {X Y : Scheme} (f : X ⟶ Y) : IsAffineHom f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)

theorem AlgebraicGeometry.IsAffineOpen.preimage {X Y : Scheme} {U : Y.Opens} (hU : IsAffineOpen U) (f : X ⟶ Y) [IsAffineHom f] : IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)

def AlgebraicGeometry.affinePreimage {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] (U : ↑Y.affineOpens) : ↑X.affineOpens

The preimage of an affine open as an Scheme.affine_opens.

Equations

• AlgebraicGeometry.affinePreimage f U = ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, ⋯⟩

@[simp]

theorem AlgebraicGeometry.affinePreimage_coe {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] (U : ↑Y.affineOpens) : ↑(affinePreimage f U) = (TopologicalSpace.Opens.map f.base).obj ↑U

@[instance 900]

instance AlgebraicGeometry.instIsAffineHomOfIsIsoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsAffineHom f

@[instance 900]

instance AlgebraicGeometry.instQuasiCompactOfIsAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] : QuasiCompact f

instance AlgebraicGeometry.instIsAffineHomCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsAffineHom f] [IsAffineHom g] : IsAffineHom (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.instIsMultiplicativeSchemeIsAffineHom : CategoryTheory.MorphismProperty.IsMultiplicative @IsAffineHom

instance AlgebraicGeometry.instIsAffineHomιBasicOpen {X : Scheme} (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : IsAffineHom (X.basicOpen r).ι

theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen_aux {X : Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) : QuasiSeparatedSpace ↥X

theorem AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen {X : Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) : IsAffine X

theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen {X : Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))) (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) : IsAffineOpen U

If s is a spanning set of Γ(X, U), such that each X.basicOpen i is affine, then U is also affine.

instance AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine : HasAffineProperty @IsAffineHom fun (X x : Scheme) (x_1 : X ⟶ x) (x : IsAffine x) => IsAffine X

instance AlgebraicGeometry.isAffineHom_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsAffineHom

@[instance 100]

instance AlgebraicGeometry.isAffineHom_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine X] [IsAffine Y] : IsAffineHom f

theorem AlgebraicGeometry.isAffine_of_isAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] [IsAffine Y] : IsAffine X

theorem AlgebraicGeometry.isAffineHom_of_forall_exists_isAffineOpen {X Y : Scheme} (f : X ⟶ Y) (H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) : IsAffineHom f

instance AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffineHom f] [IsAffine Y] : IsAffine (CategoryTheory.Limits.pullback f g)

instance AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom_1 {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffineHom g] [IsAffine X] : IsAffine (CategoryTheory.Limits.pullback f g)

theorem AlgebraicGeometry.isAffineHom_of_isInducing {X Y : Scheme} (f : X ⟶ Y) (hf₁ : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (hf₂ : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))) : IsAffineHom f

If the underlying map of a morphism is inducing and has closed range, then it is affine.