English
If W.colimitsOfShape J .RespectsIso, then the underObj construction is closed under isomorphisms, i.e., isomorphisms preserve the property.
Русский
Если W.colimitsOfShape J .RespectsIso, то underObj сохраняет изоморфизм; изоморфизмы сохраняют свойство.
LaTeX
$$W.colimitsOfShape J .IsClosedUnderIsomorphisms$$
Lean4
instance : (W.colimitsOfShape J).RespectsIso :=
RespectsIso.of_respects_arrow_iso _
(by
rintro ⟨_, _, f⟩ ⟨Y₁, Y₂, g⟩ e ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩
let e₁ := Arrow.leftFunc.mapIso e
let e₂ := Arrow.rightFunc.mapIso e
have fac : e₁.hom ≫ g = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) ≫ e₂.hom := e.hom.w
let c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const _).map e₁.hom }
let c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const _).map e₂.hom }
have h₁' : IsColimit c₁' := IsColimit.ofIsoColimit h₁ (Cocones.ext e₁)
have h₂' : IsColimit c₂' := IsColimit.ofIsoColimit h₂ (Cocones.ext e₂)
obtain hg : h₁'.desc (Cocone.mk _ (f ≫ c₂'.ι)) = g :=
h₁'.hom_ext
(fun j ↦ by
rw [h₁'.fac]
simp [fac, c₁', c₂'])
rw [← hg]
exact ⟨_, _, _, _, _, h₂', _, hf⟩)
