English
There is a construction that, given a family of isomorphisms app: F.obj i ≅ G.obj i, and a naturality condition, yields an isomorphism F ≅ G.
Русский
Существует конструктор, который по заданной семье изоморфизмов app: F.obj i ≅ G.obj i и условию естественности получает изomорфизм F ≅ G.
LaTeX
$$$\text{isoMk} : (\forall i, F.obj i \cong G.obj i) \to (\forall i hi, F.map' i (i+1) ≫ (app_i).hom = (app_i).hom ≫ G.map' i (i+1)) \to (F \cong G)$$$
Lean4
/-- Constructor for isomorphisms `F ≅ G` in `ComposableArrows C n` which takes as inputs
a family of isomorphisms `F.obj i ≅ G.obj i` and the naturality condition only for the
maps in `Fin (n + 1)` given by inequalities of the form `i ≤ i + 1`. -/
@[simps]
def isoMk {F G : ComposableArrows C n} (app : ∀ i, F.obj i ≅ G.obj i)
(w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ≫ (app _).hom = (app _).hom ≫ G.map' i (i + 1)) : F ≅ G
where
hom := homMk (fun i => (app i).hom) w
inv :=
homMk (fun i => (app i).inv)
(fun i hi => by
dsimp only
rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc])
