English
The natural isomorphism respects the components at each object of walking multispans.
Русский
Естественный изоморфизм согласуется с компонентами на каждом объекте в WalkingMultispan.
LaTeX
$$$\\mathrm{diagramIso}$ is a natural isomorphism with components $(\\mathrm{left},\\mathrm{right})$ being identities on appropriate objects.$$
Lean4
/-- The diagram of the image of a `GlueData` under a functor `F` is naturally isomorphic to the
original diagram of the `GlueData` via `F`.
-/
def diagramIso : D.diagram.multispan ⋙ F ≅ (D.mapGlueData F).diagram.multispan :=
NatIso.ofComponents
(fun x =>
match x with
| WalkingMultispan.left _ => Iso.refl _
| WalkingMultispan.right _ => Iso.refl _)
(by
rintro (⟨_, _⟩ | _) _ (_ | _ | _)
· erw [Category.comp_id, Category.id_comp, Functor.map_id]
rfl
· erw [Category.comp_id, Category.id_comp]
rfl
· erw [Category.comp_id, Category.id_comp, Functor.map_comp]
rfl
· erw [Category.comp_id, Category.id_comp, Functor.map_id]
rfl)
