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.

TODO #

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
    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
    Instances For
      source
      @[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
      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.toPresheafedSpace
      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.toPresheafedSpace), ∃ (U : Y.Opens), x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) :
      IsAffineHom f
      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.

      Stacks Tag 04DE