preservesZeroMorphisms_of_isLeftAdjoint

English

If F is a functor that is left adjoint, then F preserves zero morphisms.

Русский

Если F является левым сопряженным, то F сохраняет нулевые морфизмы.

LaTeX

$$$\text{IsLeftAdjoint } F \Rightarrow \PreservesZeroMorphisms F$$$

Lean4

instance (priority := 100) preservesZeroMorphisms_of_isLeftAdjoint (F : C ⥤ D) [IsLeftAdjoint F] :
    PreservesZeroMorphisms F where
  map_zero X
    Y := by
    let adj := Adjunction.ofIsLeftAdjoint F
    calc
      F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
    · rw [Adjunction.left_triangle_components]
      exact (Category.comp_id _).symm
    · simp only [← Category.assoc, ← F.map_comp, zero_comp]
    · simp only [Adjunction.counit_naturality, comp_zero]

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