English
With F additive as above, the inverse component of the additive biproduct isomorphism also respects the matrix decomposition: (additiveObjIsoBiproduct F M).inv ≫ F.map f = biproduct.matrix (λ i j => F.map ((embedding C).map (f i j)) ) ≫ (additiveObjIsoBiproduct F N).inv.
Русский
Для того же F и f, обратная часть изоморфизма биопродукта также согласуется с разложением по матрице: (additiveObjIsoBiproduct F M).inv ≫ F.map f = biproduct.matrix(λ i j, F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv.
LaTeX
$$$(\text{additiveObjIsoBiproduct } F M).inv \;\circ F.map f = \; \mathrm{biproduct.matrix}\left(\lambda i j \;=>\; F.map((\mathrm{embedding}\, C).map(f_{i j}))\right) \;\circ (\text{additiveObjIsoBiproduct } F N).inv$$$
Lean4
@[reassoc]
theorem additiveObjIsoBiproduct_naturality' (F : Mat_ C ⥤ D) [Functor.Additive F] {M N : Mat_ C} (f : M ⟶ N) :
(additiveObjIsoBiproduct F M).inv ≫ F.map f =
biproduct.matrix (fun i j => F.map ((embedding C).map (f i j)) :) ≫ (additiveObjIsoBiproduct F N).inv :=
by rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]
