arrowMap_ofCocone — Mathlib

English

There is a canonical isomorphism between the restriction of the extended system to Set.Iic j and the original inductive system built from F, preserving the object components.

Русский

Существует каноническое изоморфизм ограниченного расширенного системы до Set.Iic j и исходной индуктивной системы, построенной из F, сохраняющее объектные компоненты.

LaTeX

$$$\\mathrm{restrictionLTOfCoconeIso} : \\mathrm{restrictionLT}(\\mathrm{ofCocone} c) \\cong F$$$

Lean4

theorem arrowMap_ofCocone (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) :
    arrowMap (ofCocone c) i₁ i₂ h₁₂ h₂.le = Arrow.mk (F.map (homOfLE h₁₂ : ⟨i₁, lt_of_le_of_lt h₁₂ h₂⟩ ⟶ ⟨i₂, h₂⟩)) :=
  Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq _ _ _) (ofCocone_map _ _ _ _ _)

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