Lean4
/-- `Mat_.lift F` is the unique additive functor `L : Mat_ C ⥤ D` such that `F ≅ embedding C ⋙ L`.
-/
def liftUnique (F : C ⥤ D) [Functor.Additive F] (L : Mat_ C ⥤ D) [Functor.Additive L] (α : embedding C ⋙ L ≅ F) :
L ≅ lift F :=
NatIso.ofComponents
(fun M =>
additiveObjIsoBiproduct L M ≪≫
(biproduct.mapIso fun i => α.app (M.X i)) ≪≫
(biproduct.mapIso fun i => (embeddingLiftIso F).symm.app (M.X i)) ≪≫
(additiveObjIsoBiproduct (lift F) M).symm)
fun f => by
dsimp only [Iso.trans_hom, Iso.symm_hom, biproduct.mapIso_hom]
simp only [additiveObjIsoBiproduct_naturality_assoc]
simp only [biproduct.matrix_map_assoc, Category.assoc]
simp only [additiveObjIsoBiproduct_naturality']
simp only [biproduct.map_matrix_assoc]
congr 3
ext j k
apply biproduct.hom_ext
rintro ⟨⟩
dsimp
simpa using
α.hom.naturality
(f j k)
-- TODO is there some uniqueness statement for the natural isomorphism in `liftUnique`?
