hasLimits — Mathlib

English

The category of affine schemes has all limits.

Русский

Категория аффинных схем имеет все пределы.

LaTeX

$$$$ \text{HasLimits}(\text{AffineScheme}). $$$$

Lean4

instance hasLimits : HasLimits AffineScheme.{u} :=
  by
  haveI := Adjunction.has_colimits_of_equivalence Γ.{u}
  haveI : HasLimits AffineScheme.{u}ᵒᵖᵒᵖ := Limits.hasLimits_op_of_hasColimits
  exact Adjunction.has_limits_of_equivalence (opOpEquivalence AffineScheme.{u}).inverse

Похожие утверждения