ofArrowIso — Mathlib

English

If two arrows f and f′ are isomorphic, and f is a transfinite composition of shape J, then f′ is also a transfinite composition of shape J.

Русский

Если два морфизма f и f′ изоморфны и f — трансфинитная композиция формы J, то и f′ — трансфинитная композиция формы J.

LaTeX

$$$\text{TransfiniteCompositionOfShape}(J, f) \Rightarrow \text{TransfiniteCompositionOfShape}(J, f')$ under an Arrow isomorphism$$

Lean4

/-- If `f` and `f'` are two isomorphic morphisms, and `f` is a transfinite composition
of shape `J`, then `f'` also is. -/
@[simps]
def ofArrowIso {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : TransfiniteCompositionOfShape J f'
    where
  F := c.F
  isoBot := c.isoBot ≪≫ Arrow.leftFunc.mapIso e
  incl := c.incl ≫ (Functor.const J).map e.hom.right
  isColimit := IsColimit.ofIsoColimit c.isColimit (Cocones.ext (Arrow.rightFunc.mapIso e))

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