isColimit_eq_iff' — Mathlib

English

If t is a colimit cocone for F and x,y ∈ F(i), then t.ι.app i x = t.ι.app i y iff there exists j and f:i→j with F.map f x = F.map f y.

Русский

Если t — колимитный кокон для F и x,y ∈ F(i), то t.ι.app i x = t.ι.app i y тогда и только тогда, когда существует j и f:i→j с F.map f x = F.map f y.

LaTeX

$$$t.ι.app i x = t.ι.app i y \\iff \\exists j\\, f:i \\to j,\\ F.map f x = F.map f y$$$

Lean4

theorem isColimit_eq_iff' {t : Cocone F} (ht : IsColimit t) {i : J} (x y : F.obj i) :
    t.ι.app i x = t.ι.app i y ↔ ∃ (j : _) (f : i ⟶ j), F.map f x = F.map f y :=
  by
  rw [isColimit_eq_iff _ ht]
  constructor
  · rintro ⟨k, f, g, h⟩
    refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
    conv_rhs => rw [IsFiltered.coeq_condition]
    simp only [FunctorToTypes.map_comp_apply, h]
  · rintro ⟨j, f, h⟩
    exact ⟨j, f, f, h⟩

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