mono_of_cofan_isVanKampen — Mathlib

English

If c is a Van Kampen cocone on a diagram F, then every leg c.ι.app i is a mono in C.

Русский

Если когон c является когоном ван-Кемпена, то каждая ножка c.ι.app i является монообразной в C.

LaTeX

$$$\\forall i,\\; \\mathrm{Mono}(c.\\!ι.app i)$$$

Lean4

theorem mono_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C} {c : Cocone F}
    (hc : IsVanKampenColimit c) (i : Discrete ι) : Mono (c.ι.app i) := by
  classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f := Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
  nth_rw 1 [← Category.id_comp (c.ι.app i)]
  convert IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
  swap
  · exact (eqToHom (if_pos rfl).symm)
  · simp
  · exact IsPullback.of_vert_isIso ⟨by simp⟩

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