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
theorem AlgebraicGeometry.isAffineHom_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
AlgebraicGeometry.IsAffineHom f ↔ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
source
class AlgebraicGeometry.IsAffineHom {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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.isAffine_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsAffineHom f] (U : Y.Opens) :
    AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
    source
    theorem AlgebraicGeometry.isAffineOpen.preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] :
    AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
    source
    @[simp]
    theorem AlgebraicGeometry.affinePreimage_coe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (U : ↑Y.affineOpens) :
    ↑(AlgebraicGeometry.affinePreimage f U) = (TopologicalSpace.Opens.map f.val.base).obj ↑U
    source
    def AlgebraicGeometry.affinePreimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (U : ↑Y.affineOpens) :
    ↑X.affineOpens

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

    Equations
    Instances For
      source
      @[instance 900]
      instance AlgebraicGeometry.instIsAffineHomOfIsIsoScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
      AlgebraicGeometry.IsAffineHom f
      Equations
      • ⋯ = ⋯
      source
      @[instance 900]
      instance AlgebraicGeometry.instQuasiCompactOfIsAffineHom {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] :
      AlgebraicGeometry.QuasiCompact f
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.instIsAffineHomCompScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsAffineHom f] [AlgebraicGeometry.IsAffineHom g] :
      AlgebraicGeometry.IsAffineHom (CategoryTheory.CategoryStruct.comp f g)
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.instIsMultiplicativeSchemeIsAffineHom :
      CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsAffineHom
      Equations
      source
      instance AlgebraicGeometry.instIsAffineHomιBasicOpen {X : AlgebraicGeometry.Scheme} (r : ↑(X.presheaf.obj (Opposite.op ⊤))) :
      AlgebraicGeometry.IsAffineHom (X.basicOpen r).ι
      Equations
      • ⋯ = ⋯
      source
      theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen_aux {X : AlgebraicGeometry.Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) :
      QuasiSeparatedSpace ↑↑X.toPresheafedSpace
      source
      theorem AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen {X : AlgebraicGeometry.Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) :
      AlgebraicGeometry.IsAffine X
      source
      theorem AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))) (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) :
      AlgebraicGeometry.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 :
      AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsAffineHom fun (X x : AlgebraicGeometry.Scheme) (x_1 : X ⟶ x) (x : AlgebraicGeometry.IsAffine x) => AlgebraicGeometry.IsAffine X
      Equations
      source
      theorem AlgebraicGeometry.isAffineHom_stableUnderBaseChange :
      CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.IsAffineHom
      source
      @[instance 100]
      instance AlgebraicGeometry.isAffineHom_of_isAffine {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] :
      AlgebraicGeometry.IsAffineHom f
      Equations
      • ⋯ = ⋯
      source
      theorem AlgebraicGeometry.isAffine_of_isAffineHom {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] [AlgebraicGeometry.IsAffine Y] :
      AlgebraicGeometry.IsAffine X