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)

@[deprecated AlgebraicGeometry.IsAffineOpen.preimage (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.IsAffineOpen.preimage.

@[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.isRetrocompact_basicOpen {X : Scheme} (s : ↑(X.presheaf.obj (Opposite.op ⊤))) : IsRetrocompact ↑(X.basicOpen s)

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

Stacks Tag 01QF

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_2 : 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)

instance AlgebraicGeometry.instIsAffineHomDescScheme {U V X : Scheme} (f : U ⟶ X) (g : V ⟶ X) [IsAffineHom f] [IsAffineHom g] : IsAffineHom (CategoryTheory.Limits.coprod.desc f g)

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

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

theorem AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} {U : X.Opens} (hU : IsAffineOpen U) {V : Y.Opens} (hV : IsCompact ↑V) {W : Z.Opens} (hW : IsAffineOpen W) (hUW : U ≤ (TopologicalSpace.Opens.map f.base).obj W) (hVW : V ≤ (TopologicalSpace.Opens.map g.base).obj W) : IsCompact (↑((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst f g).base).obj U) ⊓ ↑((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.snd f g).base).obj V))

theorem AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] {U : Y.Opens} (hU : IsAffineOpen U) : CategoryTheory.IsIso (f ∣_ U) ↔ CategoryTheory.IsIso (Scheme.Hom.app f U)

theorem AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_inf {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : AffineTargetMorphismProperty.diagonal (fun (X x : Scheme) (x_1 : X ⟶ x) (x_2 : IsAffine x) => IsAffine X) f ↔ ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

theorem AlgebraicGeometry.isAffineHom_diagonal_iff {X Y : Scheme} {f : X ⟶ Y} : IsAffineHom (CategoryTheory.Limits.pullback.diagonal f) ↔ ∀ (U : Y.Opens), IsAffineOpen U → ∀ V₁ ≤ (TopologicalSpace.Opens.map f.base).obj U, ∀ V₂ ≤ (TopologicalSpace.Opens.map f.base).obj U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

theorem AlgebraicGeometry.IsAffineOpen.inf {X : Scheme} [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) : IsAffineOpen (U ⊓ V)

If X ⟶ Spec ℤ has affine diagonal (in particular when X is separated), then intersections of affine opens of X are also affine.

theorem AlgebraicGeometry.IsAffineOpen.iInf {X : Scheme} [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] {ι : Sort u_1} [Finite ι] [Nonempty ι] {U : ι → X.Opens} (hU : ∀ (i : ι), IsAffineOpen (U i)) : IsAffineOpen (⨅ (i : ι), U i)

theorem AlgebraicGeometry.IsAffineOpen.biInf {X : Scheme} [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] {ι : Type u_1} (s : Set ι) (hs : s.Finite) (hs' : s.Nonempty) {U : ι → X.Opens} (hU : ∀ i ∈ s, IsAffineOpen (U i)) : IsAffineOpen (⨅ i ∈ s, U i)