instFaithfulSingleFunctor — Mathlib

English

The functor singleFunctor is faithful: distinct morphisms remain distinct after applying the functor.

Русский

Функтор singleFunctor верен: разные морфизмы сохраняются различными под действием функторa.

LaTeX

$$faithful((singleFunctor C n))$$

Lean4

instance (n : ℤ) : (singleFunctor C n).Faithful where
  map_injective {_ _ f₁ f₂}
    h := by
    have eq₁ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₁
    have eq₂ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₂
    dsimp at eq₁ eq₂
    rw [← eq₁, ← eq₂, h]

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