English
The total functor total β C: GradedObject β C ⥤ Type (or appropriate target) is faithful; i.e., it reflects distinct morphisms between graded objects via their total images in the coproduct.
Русский
Полный функтор total β C: GradedObject β C ⥤ Type сохраняет верность; то есть различающие морфизмы между градуированными объектами различимо по их образам под общий копрокон.
LaTeX
$$$ (total \ β C).\mathrm{Faithful} $$$
Lean4
/-- The `total` functor taking a graded object to the coproduct of its graded components is faithful.
To prove this, we need to know that the coprojections into the coproduct are monomorphisms,
which follows from the fact we have zero morphisms and decidable equality for the grading.
-/
instance : (total β C).Faithful where
map_injective {X Y} f g
w := by
ext i
replace w := Sigma.ι (fun i : β => X i) i ≫= w
erw [colimit.ι_map, colimit.ι_map] at w
replace w : f i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ = g i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ := by simpa
exact Mono.right_cancellation _ _ w
