instRespectsIsoInd — Mathlib

English

If P respects isomorphisms, then P.ind respects isomorphisms; closure under isomorphisms transfers through ind.

Русский

Если P сохраняет изоморфизмы, то P.ind сохраняет их; свойство переносится через индукцию.

LaTeX

$$$ [P.\mathrm{RespectsIso}] \Rightarrow P.ind.\mathrm{RespectsIso} $$$

Lean4

instance [P.RespectsIso] : P.ind.RespectsIso where
  postcomp {X Y Z} i (hi : IsIso i)
    f := fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦
    by
    refine ⟨J, ‹_›, ‹_›, D, t, s ≫ (Functor.const J).map i, ?_, fun j ↦ ⟨(hst j).1, ?_⟩⟩
    · exact (IsColimit.equivIsoColimit (Cocones.ext (asIso i))) hs
    · simp [reassoc_of% (hst j).2]

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