instFullTriangleMapTriangleOfFaithful

English

Let F: C → D be a functor that is full and faithful. Then the induced functor on triangles, mapTriangle, is full: every morphism of triangles between F.mapTriangle(X) and F.mapTriangle(Y) lifts to a morphism of triangles X → Y in C.

Русский

Пусть F: C → D — полное и полнофункциональное отображение. Тогда на треугольниках существует полнота: любой морфизм между F.mapTriangle(X) и F.mapTriangle(Y) поднимается до морфизма между X и Y.

LaTeX

$$$\\mathrm{Full}(F.mapTriangle)$$$

Lean4

instance [Full F] [Faithful F] : Full F.mapTriangle where
  map_surjective {X Y}
    f :=
    ⟨{  hom₁ := F.preimage f.hom₁
        hom₂ := F.preimage f.hom₂
        hom₃ := F.preimage f.hom₃
        comm₁ := F.map_injective (by simpa only [mapTriangle_obj, map_comp, map_preimage] using f.comm₁)
        comm₂ := F.map_injective (by simpa only [mapTriangle_obj, map_comp, map_preimage] using f.comm₂)
        comm₃ :=
          F.map_injective
            (by
              rw [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app Y.obj₁)]
              simpa only [mapTriangle_obj, map_comp, assoc, commShiftIso_hom_naturality, map_preimage,
                Triangle.mk_mor₃] using f.comm₃) },
      by cat_disch⟩

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