English
Let C and D be categories with finite biproducts and Preadditive structure. If F : Mat_C ⥤ D is an additive functor and f : M ⟶ N is a morphism in Mat_C, then F.map f is represented, with respect to the biproduct decompositions of M and N, by the matrix whose (i,j)-entry is F.map (f i j). Equivalently, the map F.map f factors through the additive biproducts via the biproduct matrix of entries F.map (embedding i j) and the corresponding biproduct homs.
Русский
Пусть C и D — категории с конечными би-произведениями и предадпитивной структурой. Пусть F : Mat_C ⥤ D — добавитная функтор. Для любого морфизма f : M ⟶ N в категории матриц над C, отображение F.map f от F(M) к F(N) выражается в терминах биопроизвольной декомпозиции: он задаётся матрицей элементов F.map (f i j) относительно биопроизводного разложения. Иными словами, F.map f определяется матрицей из F.map (f i j) через соответствующие проекции и вложения биопродукта.
LaTeX
$$$\displaystyle F.map f \;\;\;\; \text{and} \;\;\;\; (\text{additiveObjIsoBiproduct } F N).hom = \;\; (\text{additiveObjIsoBiproduct } F M).hom \;\circ \mathrm{biproduct.matrix}\left(\lambda i j \;=>\; F.map((\mathrm{embedding}\, C).map(f_{i j}))\right) \,,$$$
Lean4
@[reassoc]
theorem additiveObjIsoBiproduct_naturality (F : Mat_ C ⥤ D) [Functor.Additive F] {M N : Mat_ C} (f : M ⟶ N) :
F.map f ≫ (additiveObjIsoBiproduct F N).hom =
(additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j => F.map ((embedding C).map (f i j)) :=
by
classical
ext i : 1
simp only [Category.assoc, additiveObjIsoBiproduct_hom_π, isoBiproductEmbedding_hom, embedding_obj_ι, embedding_obj_X,
biproduct.lift_π, biproduct.matrix_π, ← cancel_epi (additiveObjIsoBiproduct F M).inv, Iso.inv_hom_id_assoc]
ext j : 1
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv, biproduct.ι_desc, ← F.map_comp]
congr 1
funext ⟨⟩ ⟨⟩
simp [comp_apply, dite_comp, comp_dite]
