Quasi-affine schemes

Main results

• IsQuasiAffine: A scheme X is quasi-affine if it is quasi-compact and X ⟶ Spec Γ(X, ⊤) is an immersion. This actually implies that X ⟶ Spec Γ(X, ⊤) is an open immersion.
• IsQuasiAffine.of_isImmersion: Any quasi-compact locally closed subscheme of a quasi-affine scheme is quasi-affine.

class AlgebraicGeometry.Scheme.IsQuasiAffine (X : Scheme) extends CompactSpace ↥X, AlgebraicGeometry.IsImmersion X.toSpecΓ : Prop

A scheme X is quasi-affine if it is quasi-compact and X ⟶ Spec Γ(X, ⊤) is an immersion. This actually implies that X ⟶ Spec Γ(X, ⊤) is an open immersion.

• isCompact_univ : IsCompact Set.univ
• stalkMap_surjective (x : ↥X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap X.toSpecΓ x))
• isEmbedding : Topology.IsEmbedding ⇑X.toSpecΓ
• isLocallyClosed_range : IsLocallyClosed (Set.range ⇑X.toSpecΓ)

@[instance 100]

instance AlgebraicGeometry.Scheme.instIsQuasiAffineOfIsAffine {X : Scheme} [IsAffine X] : X.IsQuasiAffine

@[instance 100]

instance AlgebraicGeometry.Scheme.instIsSeparatedOfIsQuasiAffine {X : Scheme} [X.IsQuasiAffine] : X.IsSeparated

instance AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine {X : Scheme} [X.IsQuasiAffine] : IsOpenImmersion X.toSpecΓ

theorem AlgebraicGeometry.Scheme.IsQuasiAffine.of_isImmersion {X Y : Scheme} (f : X ⟶ Y) [Y.IsQuasiAffine] [IsImmersion f] [CompactSpace ↥X] : X.IsQuasiAffine

Any quasicompact locally closed subscheme of a quasi-affine scheme is quasi-affine.

theorem AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen (X : Scheme) [X.IsQuasiAffine] : TopologicalSpace.Opens.IsBasis {x : TopologicalSpace.Opens ↥X | ∃ (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}

theorem AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpen (X : Scheme) [CompactSpace ↥X] (H : ∀ (x : ↥X), ∃ (r : ↑(X.presheaf.obj (Opposite.op ⊤))), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r) : X.IsQuasiAffine

A quasi-compact scheme is quasi-affine if it can be covered by affine basic opens of global sections.

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

def AlgebraicGeometry.Scheme.openCoverBasicOpenTop (X : Scheme) [X.IsQuasiAffine] : X.OpenCover

The affine basic opens of a quasi-affine scheme form an open cover.

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f (X : Scheme) [X.IsQuasiAffine] (i : { r : ↑(X.presheaf.obj (Opposite.op ⊤)) // IsAffineOpen (X.basicOpen r) }) : X.openCoverBasicOpenTop.f i = (X.basicOpen ↑i).ι

theorem AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] [Y.IsQuasiAffine] : CategoryTheory.IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))

If f : X ⟶ Y is an affine morphism between quasi-affine schemes, then it is the pullback of Spec Γ(X, ⊤) ⟶ Spec Γ(Y, ⊤) along the open immersion Y ⟶ Spec Γ(Y, ⊤).

theorem AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] [X.IsQuasiAffine] [Y.IsQuasiAffine] : (TopologicalSpace.Opens.map (Spec.map (Hom.appTop f)).base).obj (Hom.opensRange Y.toSpecΓ) = Hom.opensRange X.toSpecΓ