English
If a cofan X → isColimit with each leg mono, plus a system of pullbacks indexed by pairs converging to X, then X forms a CoproductDisjoint family; concretely the family of injections into the coproduct X is jointly mono.
Русский
Если кофан является колимитом и все иньекции моно, то семействоkoproduct раздельно по отношению к X; инъекции в копродукт образуют совместное моно.
LaTeX
$$$\\text{CoproductDisjoint}\\ X$$$
Lean4
theorem of_cofan {c : Cofan X} (hc : IsColimit c) [∀ i, Mono (c.inj i)]
(s : ∀ {i j : ι} (_ : i ≠ j), PullbackCone (c.inj i) (c.inj j)) (hs : ∀ {i j : ι} (hij : i ≠ j), IsLimit (s hij))
(H : ∀ {i j : ι} (hij : i ≠ j), IsInitial (s hij).pt) : CoproductDisjoint X
where
nonempty_isInitial_of_ne {d} hd {i j} hij t
ht := by
let e := hd.uniqueUpToIso hc
have heq (i) : d.inj i ≫ e.hom.hom = c.inj i := e.hom.w ⟨i⟩
let u : t.pt ⟶ (s hij).pt := by
refine PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ?_
simp [← heq, t.condition_assoc]
refine ⟨(H hij).ofIso ⟨(H hij).to t.pt, u, (H hij).hom_ext _ _, ?_⟩⟩
refine PullbackCone.IsLimit.hom_ext ht ?_ ?_
· simp [show (H hij).to (X i) = (s hij).fst from (H hij).hom_ext _ _, u]
· simp [show (H hij).to (X j) = (s hij).snd from (H hij).hom_ext _ _, u]
mono_inj {d} hd
i := by
rw [show d.inj i = c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom by simp]
infer_instance
