Documentation

Mathlib.AlgebraicGeometry.Morphisms.Affine

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 #

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

source
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.

Instances
    source
    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)
    source
    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)
    source
    @[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.

    source
    @[instance 900]
    instance AlgebraicGeometry.instIsAffineHomOfIsIsoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
    IsAffineHom f
    source
    @[instance 900]
    instance AlgebraicGeometry.instQuasiCompactOfIsAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] :
    QuasiCompact f
    source
    instance AlgebraicGeometry.instIsAffineHomCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsAffineHom f] [IsAffineHom g] :
    IsAffineHom (CategoryTheory.CategoryStruct.comp f g)
    source
    instance AlgebraicGeometry.instIsMultiplicativeSchemeIsAffineHom :
    CategoryTheory.MorphismProperty.IsMultiplicative @IsAffineHom
    source
    instance AlgebraicGeometry.instIsAffineHomιBasicOpen {X : Scheme} (r : ↑(X.presheaf.obj (Opposite.op ⊤))) :
    IsAffineHom (X.basicOpen r).ι
    source
    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
    source
    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
    source
    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.

    source
    instance AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine :
    HasAffineProperty @IsAffineHom fun (X x : Scheme) (x_1 : X ⟶ x) (x : IsAffine x) => IsAffine X
    source
    instance AlgebraicGeometry.isAffineHom_isStableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsAffineHom
    source
    @[instance 100]
    instance AlgebraicGeometry.isAffineHom_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine X] [IsAffine Y] :
    IsAffineHom f
    source
    theorem AlgebraicGeometry.isAffine_of_isAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] [IsAffine Y] :
    IsAffine X
    source
    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
    source
    instance AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffineHom f] [IsAffine Y] :
    IsAffine (CategoryTheory.Limits.pullback f g)
    source
    instance AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom_1 {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffineHom g] [IsAffine X] :
    IsAffine (CategoryTheory.Limits.pullback f g)
    source
    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.