class AlgebraicGeometry.Scheme.IsAffineVariety (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : Prop

An affine variety over a field k (Def 2, Lec 2): a scheme X over Spec k that is isomorphic to Spec Γ(X, O_X), is locally of finite type over k, and is reduced.

• toSpecΓ_isIso : CategoryTheory.IsIso X.toSpecΓ
• locallyOfFiniteType : LocallyOfFiniteType (X ↘ Spec (CommRingCat.of k))
• isReduced : IsReduced X

theorem AlgebraicGeometry.Scheme.IsAffineVariety.isAffine {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [h : IsAffineVariety k X] : IsAffine X

Any affine variety is in particular an affine scheme.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.specOverSpec (k : Type u) [Field k] (A : Type u) [CommRing A] [Algebra k A] : (Spec (CommRingCat.of A)).Over (Spec (CommRingCat.of k))

A k-algebra A gives Spec A the structure of a scheme over Spec k via the structure map of the algebra.

instance AlgebraicGeometry.Scheme.specIsAffineVariety (k : Type u) [Field k] (A : Type u) [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [_root_.IsReduced A] : IsAffineVariety k (Spec (CommRingCat.of A))

For A a reduced finitely-generated k-algebra, Spec A is an affine variety over k.