Theorems · Theorem · algebraic geometry

AlgebraicGeometry.essentiallySmall_costructuredArrow_Spec

∀ {X : AlgebraicGeometry.Scheme},
  ∀ P ≤ @AlgebraicGeometry.LocallyOfFiniteType,
    ∀ [P.RespectsIso],
      CategoryTheory.EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ AlgebraicGeometry.Scheme.Spec X)

The category of affine schemes locally of finite type over a fixed base scheme is essentially small. TODO: extend this to (relatively) quasi-compact schemes.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Cited by

0 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.RespectsIso