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
• surj_on_stalks (x : ↥X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap X.toSpecΓ x))
• base_embedding : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom X.toSpecΓ.base)
• isLocallyClosed_range : IsLocallyClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom X.toSpecΓ.base))

@[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