English
The functor Scheme.Γ.rightOp preserves limits along diagrams consisting of affine schemes.
Русский
Функтор Scheme.Γ.rightOp сохраняет пределы диаграмм, состоящих из аффинных схем.
LaTeX
$$PreservesLimit D Scheme.Γ.rightOp$$
Lean4
/-- `Scheme.Γ.rightOp : Scheme ⥤ CommRingCatᵒᵖ` preserves limits of diagrams consisting of
affine schemes. -/
instance preservesLimit_rightOp_Γ.{v, w} {I : Type w} [Category.{v} I] (D : I ⥤ Scheme.{u}) [∀ i, IsAffine (D.obj i)] :
PreservesLimit D Scheme.Γ.rightOp :=
by
let α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
have (i : _) : IsIso (α.app i) := IsAffine.affine
have : IsIso α := NatIso.isIso_of_isIso_app α
suffices PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp from
preservesLimit_of_iso_diagram _ (asIso α).symm
have := monadicCreatesLimits.{v, w} Scheme.Spec.{u}
suffices PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp) from
preservesLimit_comp_of_createsLimit _ _
exact preservesLimit_of_natIso _ (NatIso.op Scheme.SpecΓIdentity)
