mk' — Mathlib

English

If W1 ≤ W2 as morphism properties, then for any index category J, W1.colimitsOfShape J ≤ W2.colimitsOfShape J.

Русский

Если W1 ≤ W2 как свойства морфизмов, то для любого индекса J выполняется W1.colimitsOfShape J ≤ W2.colimitsOfShape J.

LaTeX

$$W1.colimitsOfShape J ≤ W2.colimitsOfShape J$$

Lean4

theorem mk' (X₁ X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₂ : IsColimit c₂) (f : X₁ ⟶ X₂)
    (hf : W.functorCategory J f) (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ j, c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) :
    W.colimitsOfShape J φ :=
  by
  obtain rfl : φ = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) := h₁.hom_ext (fun j ↦ by simp [hφ])
  exact ⟨_, _, _, _, _, h₂, _, hf⟩

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