ofCoconeObjIso_hom_naturality — Mathlib

English

A second naturality property holds between different formulations of the isomorphisms relating the extended cocone to F, ensuring the two routes around a square agree.

Русский

Соблюдается вторая естественность между разными формулациями изоморфизмов, связывающих расширённый кокон с F, так что верхний и нижний маршруты дают одинаковый результат.

LaTeX

$$$(\\mathrm{ofCoconeObjIso}\\,i) \\circ F.map(\\mathrm{homOfLE}) = \\mathrm{ofCoconeObjIso}(i') \\circ (\\mathrm{map}\\, i,i')$$$

Lean4

@[reassoc]
theorem ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) :=
  by rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

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