theorem AlgebraicGeometry.Scheme.IsAffineVariety.globalSections_isReduced {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [h : IsAffineVariety k X] : _root_.IsReduced ↑(X.presheaf.obj (Opposite.op ⊤))

For an affine variety X over k, the global sections Γ(X, O_X) form a reduced ring.

theorem AlgebraicGeometry.Scheme.IsAffineVariety.appTop_finiteType {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [h : IsAffineVariety k X] : (CommRingCat.Hom.hom (Hom.appTop (X ↘ Spec (CommRingCat.of k)))).FiniteType

For an affine variety X over k, the structure map k → Γ(X, O_X) is of finite type.

theorem AlgebraicGeometry.Scheme.Theorem2_2_affineVariety_iff_spec_IsAffineVariety (k : Type u) [Field k] : (∀ (X : Scheme) [inst : X.Over (Spec (CommRingCat.of k))] [IsAffineVariety k X], CategoryTheory.IsIso X.toSpecΓ ∧ _root_.IsReduced ↑(X.presheaf.obj (Opposite.op ⊤)) ∧ (CommRingCat.Hom.hom (Hom.appTop (X ↘ Spec (CommRingCat.of k)))).FiniteType) ∧ ∀ (A : Type u) [inst : CommRing A] [inst_1 : Algebra k A] [Algebra.FiniteType k A] [_root_.IsReduced A], IsAffineVariety k (Spec (CommRingCat.of A))

Theorem 2.2 (Lec 2): the two equivalent characterizations of affine varieties — every affine variety X over k satisfies X ≅ Spec Γ(X) with reduced finitely-generated coordinate ring, and conversely Spec A for any such A is an affine variety.