18.4. Affine schemes🔗

Among all schemes, the affine schemes take an important role and we use the predicate IsAffine to say a scheme is affine. For example, Spec R is affine:

example (R : CommRingCat) : IsAffine (Spec R) :=
  inferInstance

If X is an affine scheme, it is isomorphic to Spec Γ(X, ⊤).

example [IsAffine X] : X ≅ Spec Γ(X, ⊤) :=
  X.isoSpec

Some proofs of being affine can be found by instance synthesis.

example (f : X ⟶ Z) (g : Y ⟶ Z)
    [IsAffine X] [IsAffine Y] [IsAffine Z] :
    IsAffine (pullback f g) :=
  inferInstance