instFaithfulGradedObjectProdToGradedObjectFunctor

English

The functor toGradedObjectFunctor is faithful; i.e., if two morphisms of bicomplexes have the same image under this functor, they are equal.

Русский

Функтор toGradedObjectFunctor верен; то есть если два морфизма биокомплексoв имеют одинаковое изображение под этим функтором, то они равны.

LaTeX

$$$\\forall X,Y:\\, \\mathrm{HomologicalComplex}_2(C;c_1,c_2),\\; f,g: X \\to Y,\quad \\mathrm{toGradedObjectMap}(f) = \\mathrm{toGradedObjectMap}(g) \\Rightarrow f = g$$$

Lean4

instance : (toGradedObjectFunctor C c₁ c₂).Faithful where
  map_injective {_ _ φ₁ φ₂}
    h := by
    ext i₁ i₂
    exact congr_fun h ⟨i₁, i₂⟩

Похожие утверждения