English
Constructor for isomorphisms in ComposableArrows C 5: given isomorphisms between corresponding vertices and commuting relations for each step, build f ≅ g.
Русский
Конструктор изоморфизмов в ComposableArrows C 5: при наличии изоморфизмов между вершинами и коммутирующих условий на каждом шаге строится изоморфизм f ≅ g.
LaTeX
$$$\forall f,g : ComposableArrows C 5\; (app_0 : f.obj' 0 ≅ g.obj' 0) \dots (app_5 : f.obj' 5 ≅ g.obj' 5)\; (w_0: f.map' 0 1 ≫ app_1.hom = app_0.hom ≫ g.map' 0 1) \dots (w_4: f.map' 4 5 ≫ app_5.hom = app_4.hom ≫ g.map' 4 5) \Rightarrow f \cong g$$$
Lean4
/-- Constructor for isomorphisms in `ComposableArrows C 5`. -/
@[simps]
def isoMk₅ {f g : ComposableArrows C 5} (app₀ : f.obj' 0 ≅ g.obj' 0) (app₁ : f.obj' 1 ≅ g.obj' 1)
(app₂ : f.obj' 2 ≅ g.obj' 2) (app₃ : f.obj' 3 ≅ g.obj' 3) (app₄ : f.obj' 4 ≅ g.obj' 4) (app₅ : f.obj' 5 ≅ g.obj' 5)
(w₀ : f.map' 0 1 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1) (w₁ : f.map' 1 2 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2)
(w₂ : f.map' 2 3 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3) (w₃ : f.map' 3 4 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4)
(w₄ : f.map' 4 5 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5) : f ≅ g
where
hom := homMk₅ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom app₅.hom w₀ w₁ w₂ w₃ w₄
inv :=
homMk₅ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv app₅.inv (by rw [map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀])
(by rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]) (by rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂])
(by rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]) (by rw [map'_inv_eq_inv_map' (by valid) app₄ app₅ w₄])
