extendToSuccRestrictionLEIso — Mathlib

English

A naturality condition expresses compatibility of the map with objIso and F.map.

Русский

Условие натуральности выражает совместимость отображения с objIso и F.map.

LaTeX

$$$(extendToSucc hj F τ).map (homOfLE hi) \\; ≫ (extendToSuccObjIso hj F τ i_2 hi_2).hom = (extendToSuccObjIso hj F τ i_1 (hi.trans hi_2)).hom ≫ F.map (homOfLE hi)$$$

Lean4

/-- The isomorphism expressing that `extendToSucc hj F τ` extends `F`. -/
@[simps!]
def extendToSuccRestrictionLEIso : SmallObject.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F :=
  NatIso.ofComponents (fun i ↦ extendToSuccObjIso hj F τ i.1 i.2)
    (by
      rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
      apply extendToSuccObjIso_hom_naturality)

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