coproductCofanIsColimit — Mathlib

English

The forgetful functor from LocallyRingedSpace to SheafedSpace preserves colimits of shape WalkingParallelPair; consequently, colimits in LocallyRingedSpace are computed by transferring to the forgetful setting.

Русский

Функтор забывания из LocallyRingedSpace в SheafedSpace сохраняет колимиты формы WalkingParallelPair; следовательно, колимиты в LocallyRingedSpace получаются через переход к забывающему контексту.

LaTeX

$$PreservesColimitsOfShape\(WalkingParallelPair\, forgetToSheafedSpace$$

Lean4

/-- The explicit coproduct cofan constructed in `coproductCofan` is indeed a colimit. -/
noncomputable def coproductCofanIsColimit : IsColimit (coproductCofan F)
    where
  desc
    s :=
    ⟨colimit.desc (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (F ⋙ forgetToSheafedSpace)
        (forgetToSheafedSpace.mapCocone s),
      by
      intro x
      obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
      have :=
        PresheafedSpace.stalkMap.comp
          (colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (F ⋙ forgetToSheafedSpace) i)
          (colimit.desc (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (F ⋙ forgetToSheafedSpace)
            (forgetToSheafedSpace.mapCocone s))
          y
      rw [← IsIso.comp_inv_eq] at this
      erw [← this,
        PresheafedSpace.stalkMap.congr_hom _ _
          (colimit.ι_desc (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (forgetToSheafedSpace.mapCocone s) i :)]
      haveI : IsLocalHom (((forgetToSheafedSpace.mapCocone s).ι.app i).stalkMap y).hom := (s.ι.app i).2 y
      infer_instance⟩
  fac _ _ := LocallyRingedSpace.Hom.ext' (colimit.ι_desc (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) _ _)
  uniq s f
    h :=
    LocallyRingedSpace.Hom.ext'
      (IsColimit.uniq _ (forgetToSheafedSpace.mapCocone s) f.toShHom fun j =>
        congr_arg LocallyRingedSpace.Hom.toShHom (h j))

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