Quasi-affine schemes

Main results

• IsQuasiAffine: A scheme X is quasi-affine if it is quasi-compact and 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.PresheafedSpace.IsOpenImmersion (AlgebraicGeometry.Scheme.Hom.toLRSHom X.toSpecΓ).toHom : Prop

A scheme X is quasi-affine if it is quasi-compact and X ⟶ Spec Γ(X, ⊤) is an open immersion. Despite the definition, any quasi-compact locally closed subscheme of an affine scheme is quasi-affine. See IsQuasiAffine.of_isImmersion

• isCompact_univ : IsCompact Set.univ
• base_open : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.toLRSHom X.toSpecΓ).base)
• c_iso (U : TopologicalSpace.Opens ↥X) : CategoryTheory.IsIso ((Scheme.Hom.toLRSHom X.toSpecΓ).c.app (Opposite.op (⋯.functor.obj U)))

@[instance 100]

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

@[instance 100]

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

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 an quasi-affine scheme is quasi-affine.