English
Construct an isomorphism F ≅ G from α: F.obj'0 ≅ G.obj'0 and β: F.δ₀ ≅ G.δ₀ provided the compatibility condition holds.
Русский
Построить изоморфизм F ≅ G из α и β с условием совместимости.
LaTeX
$$$$ \\text{isoMkSucc}: (α: F.obj'0 \\cong G.obj'0) \\to (β: F.δ_0 \\cong G.δ_0) \\to (w: F.map' 0 1 ≫ app' β.hom = α.hom ≫ G.map' 0 1) \\to F \\cong G $$$$
Lean4
/-- Inductive construction of isomorphisms in `ComposableArrows C (n + 1)`: in order to
construct an isomorphism `F ≅ G`, it suffices to provide `α : F.obj' 0 ≅ G.obj' 0` and
`β : F.δ₀ ≅ G.δ₀` such that `F.map' 0 1 ≫ app' β.hom 0 = α.hom ≫ G.map' 0 1`. -/
@[simps]
def isoMkSucc {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ≅ G.obj' 0) (β : F.δ₀ ≅ G.δ₀)
(w : F.map' 0 1 ≫ app' β.hom 0 = α.hom ≫ G.map' 0 1) : F ≅ G
where
hom := homMkSucc α.hom β.hom w
inv :=
homMkSucc α.inv β.inv
(by
rw [← cancel_epi α.hom, ← reassoc_of% w, α.hom_inv_id_assoc, β.hom_inv_id_app]
dsimp
rw [comp_id])
hom_inv_id := by
apply hom_ext_succ
· simp
· ext ⟨i, hi⟩
simp
inv_hom_id := by
apply hom_ext_succ
· simp
· ext ⟨i, hi⟩
simp
