English
If a functor preserves coequalizers and coproducts, it preserves colimits.
Русский
Если функтор сохраняет коэквалайзеры и копроизведения, он сохраняет колимиты.
LaTeX
$$PreservesColimitsOfShape J G$$
Lean4
/-- If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits. -/
theorem preservesColimit_of_preservesCoequalizers_and_coproduct : PreservesColimitsOfShape J G where
preservesColimit
{K} := by
let P := ∐ K.obj
let Q := ∐ fun f : Σ p : J × J, p.fst ⟶ p.snd => K.obj f.1.1
let s : Q ⟶ P := Sigma.desc fun f => K.map f.2 ≫ colimit.ι (Discrete.functor K.obj) ⟨_⟩
let t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) ⟨f.1.1⟩
let I := coequalizer s t
let i : P ⟶ I := coequalizer.π s t
apply
preservesColimit_of_preserves_colimit_cocone
(buildIsColimit s t (by simp [P, s]) (by simp [P, t]) (colimit.isColimit _) (colimit.isColimit _)
(colimit.isColimit _))
apply IsColimit.ofIsoColimit (buildIsColimit _ _ _ _ _ _ _) _
· refine Cofan.mk (G.obj Q) fun j => G.map ?_
apply Sigma.ι _ j
· exact Cofan.mk _ fun f => G.map (Sigma.ι _ f)
· apply G.map s
· apply G.map t
· intro f
dsimp [P, Q, s, Cofan.mk]
simp only [← G.map_comp, colimit.ι_desc]
congr
· intro f
dsimp [P, Q, t, Cofan.mk]
simp only [← G.map_comp, colimit.ι_desc]
dsimp
· refine Cofork.ofπ (G.map i) ?_
rw [← G.map_comp, ← G.map_comp]
apply congrArg G.map
apply coequalizer.condition
· apply isColimitOfHasCoproductOfPreservesColimit
· apply isColimitOfHasCoproductOfPreservesColimit
· apply isColimitCoforkMapOfIsColimit
apply coequalizerIsCoequalizer
refine Cocones.ext (Iso.refl _) ?_
intro j
dsimp [P, Q, I, i]
simp
