English
If ι: J → I is injective and a suitable diagram X, c, c1, c2 exist with colimits, then a certain map desc is mono.
Русский
Если ι: J → I инъективно и существуют диаграммы X, c, c1, c2 с пределами, то отображение desc моно.
LaTeX
$$$\\text{mono\_of\_injective\_aux}(X,ι,hι,c,c_1,c_2,hc,hc_1,hc_2):\\ Mono(Cofan.IsColimit.desc hc_1 (\\lambda i. c.inj (ι i))).$$$
Lean4
theorem mono_of_injective_aux (hι : Function.Injective ι) (c : Cofan X) (c₁ : Cofan (X ∘ ι)) (hc : IsColimit c)
(hc₁ : IsColimit c₁) (c₂ : Cofan (fun (k : ((Set.range ι)ᶜ : Set I)) => X k.1)) (hc₂ : IsColimit c₂) :
Mono (Cofan.IsColimit.desc hc₁ (fun i => c.inj (ι i))) := by
classical
let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_ hc₁ hc₂ _ (by simp [e])
exact
IsColimit.ofIsoColimit
((IsColimit.ofCoconeEquiv (Cocones.equivalenceOfReindexing (Discrete.equivalence e) (Iso.refl _))).symm hc)
(Cocones.ext (Iso.refl _))
