preservesColimit_Γ — Mathlib

English

The functor Scheme.Γ preserves colimits of diagrams of affine schemes.

Русский

Функтор Scheme.Γ сохраняет пределы колимитов диаграмм из аффинных схем.

LaTeX

$$PreservesColimit D Scheme.Γ$$

Lean4

/-- `Scheme.Γ : Schemeᵒᵖ ⥤ CommRingCat` preserves colimits of diagrams consisting of
affine schemes. -/
instance preservesColimit_Γ.{v, w} {I : Type w} [Category.{v} I] (D : I ⥤ Scheme.{u}ᵒᵖ) [∀ i, IsAffine (D.obj i).unop] :
    PreservesColimit D Scheme.Γ :=
  by
  have (i : _) : IsAffine (D.leftOp.obj i) := Functor.leftOp_obj D _ ▸ inferInstance
  exact preservesColimit_of_rightOp D Scheme.Γ

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