English
The shape-based creation principle for limits holds via certain shapes.
Русский
Принцип создания пределов по формам действует через указанные формы.
LaTeX
$$CreatesLimitsOfShape J G$$
Lean4
/-- (Implementation) Show the cocone constructed in `buildColimit` is colimiting,
provided the cocones used in its construction are.
-/
def buildIsColimit (t₁ : IsColimit c₁) (t₂ : IsColimit c₂) (hi : IsColimit i) : IsColimit (buildColimit s t hs ht i)
where
desc
q := by
refine hi.desc (Cofork.ofπ ?_ ?_)
· refine t₂.desc (Cofan.mk _ fun j => ?_)
apply q.ι.app j
· apply t₁.hom_ext
intro ⟨j⟩
have reassoced_s (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h :=
by
simp only [← Category.assoc]
apply eq_whisker (hs f)
have reassoced_t (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
c₁.ι.app ⟨f⟩ ≫ t ≫ h = c₂.ι.app ⟨f.fst.fst⟩ ≫ h :=
by
simp only [← Category.assoc]
apply eq_whisker (ht f)
simp [reassoced_s, reassoced_t]
uniq q m w := hi.hom_ext (i.coequalizer_ext (t₂.hom_ext fun j => by simpa using w j.1))
fac s j := by simp
