theorem affineVariety_isIso_toSpecΓ (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)) [Definition3_AlgebraicVariety k X f] [AlgebraicGeometry.IsAffine X] : CategoryTheory.IsIso X.toSpecΓ

For an affine algebraic variety X over k, the canonical map X → Spec Γ(X, O_X) is an isomorphism.

theorem affineVariety_globalSections_isReduced (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)) [hvar : Definition3_AlgebraicVariety k X f] [AlgebraicGeometry.IsAffine X] : IsReduced ↑(X.presheaf.obj (Opposite.op ⊤))

The global sections ring Γ(X, O_X) of an affine algebraic variety is reduced.

theorem affineVariety_globalSections_finiteType (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)) [hvar : Definition3_AlgebraicVariety k X f] [AlgebraicGeometry.IsAffine X] : (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).FiniteType

The structure map k → Γ(X, O_X) of an affine algebraic variety is of finite type, i.e. Γ(X, O_X) is a finitely generated k-algebra.

theorem affineVariety_forward (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)) [hvar : Definition3_AlgebraicVariety k X f] [AlgebraicGeometry.IsAffine X] : CategoryTheory.IsIso X.toSpecΓ ∧ IsReduced ↑(X.presheaf.obj (Opposite.op ⊤)) ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).FiniteType

Forward direction of Theorem 3.1: an affine algebraic variety X satisfies X ≅ Spec Γ(X), its global sections form a reduced finitely-generated k-algebra.

theorem affineVariety_backward (k : Type u) [Field k] (A : Type u) [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [IsReduced A] : Definition3_AlgebraicVariety k (AlgebraicGeometry.Spec (CommRingCat.of A)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k A)))

Converse direction: if A is a reduced finitely-generated k-algebra, then Spec A is an affine algebraic variety over k.

theorem affineVariety_iff_spec_fg_reduced (k : Type u) [Field k] : (∀ (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)) [Definition3_AlgebraicVariety k X f] [AlgebraicGeometry.IsAffine X], CategoryTheory.IsIso X.toSpecΓ ∧ IsReduced ↑(X.presheaf.obj (Opposite.op ⊤)) ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).FiniteType) ∧ ∀ (A : Type u) [inst : CommRing A] [inst_1 : Algebra k A] [Algebra.FiniteType k A] [IsReduced A], Definition3_AlgebraicVariety k (AlgebraicGeometry.Spec (CommRingCat.of A)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k A)))

Combined two directions of Theorem 3.1: an algebraic variety X over k is affine if and only if it is Spec A for some reduced finitely-generated k-algebra A.

theorem Theorem3_1_affineVariety_iff_fg_reduced_algebra (k : Type u) [Field k] [IsAlgClosed k] : (∀ (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)) [Definition3_AlgebraicVariety k X f] [AlgebraicGeometry.IsAffine X], CategoryTheory.IsIso X.toSpecΓ ∧ IsReduced ↑(X.presheaf.obj (Opposite.op ⊤)) ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).FiniteType) ∧ ∀ (A : Type u) [inst : CommRing A] [inst_1 : Algebra k A] [Algebra.FiniteType k A] [IsReduced A], Definition3_AlgebraicVariety k (AlgebraicGeometry.Spec (CommRingCat.of A)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k A)))

Theorem 3.1 (Lec 2/3): Over an algebraically closed field k, an algebraic variety is affine iff it is Spec A for some reduced finitely-generated k-algebra A.