English
If F is a faithful functor that preserves the shift and acts on triangles by mapping components, then F.mapTriangle is faithful; i.e., F detects equality of triangle morphisms by their components.
Русский
Если F — внимательный функтор, сохраняющий сдвиг и действующий на треугольники по компонентам, то F.mapTriangle является верным; то есть F обнаруживает равенство треугольников по компонентам.
LaTeX
$$F.mapTriangle.Faithful$$
Lean4
/-- The functor `Triangle C ⥤ Triangle D` that is induced by a functor `F : C ⥤ D`
which commutes with shift by `ℤ`. -/
@[simps]
def mapTriangle : Triangle C ⥤ Triangle D
where
obj T := Triangle.mk (F.map T.mor₁) (F.map T.mor₂) (F.map T.mor₃ ≫ (F.commShiftIso (1 : ℤ)).hom.app T.obj₁)
map
f :=
{ hom₁ := F.map f.hom₁
hom₂ := F.map f.hom₂
hom₃ := F.map f.hom₃
comm₁ := by dsimp; simp only [← F.map_comp, f.comm₁]
comm₂ := by dsimp; simp only [← F.map_comp, f.comm₂]
comm₃ := by
dsimp [Functor.comp]
simp only [Category.assoc, ← NatTrans.naturality, ← F.map_comp_assoc, f.comm₃] }
