Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.isAffine_of_isLimit

∀ {I : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} I] {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme}
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c)
  [∀ (i : I), AlgebraicGeometry.IsAffine (D.obj i)], AlgebraicGeometry.IsAffine c.pt

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.IsAffine