English
In the costructured arrow over a product of functors S.prod S', the left component of a morphism f satisfies the equation S.map f.left.1 ≫ B.hom.1 = A.hom.1.
Русский
В стрелке CostructuredArrow над произведением S и S' левые координаты морфизма удовлетворяют равенству S.map f.left.1 ≫ B.hom.1 = A.hom.1.
LaTeX
$$$ S.map f.left.1 \; \circ \; B.hom.1 = A.hom.1 $$$
Lean4
instance full_map [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (map α β).Full where
map_surjective {X Y}
φ :=
⟨{ left := F₁.preimage φ.left
right := F₂.preimage φ.right
w :=
F.map_injective
(by
rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp, assoc, assoc]
erw [← α.naturality_assoc, β.naturality]
dsimp
rw [F₁.map_preimage, F₂.map_preimage]
simpa using φ.w) },
by cat_disch⟩
