preservesZeroMorphisms_of_isRightAdjoint

English

If G is a right adjoint, then G preserves zero morphisms.

Русский

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

LaTeX

$$$\text{IsRightAdjoint } G \Rightarrow \PreservesZeroMorphisms G$$$

Lean4

instance (priority := 100) preservesZeroMorphisms_of_isRightAdjoint (G : C ⥤ D) [IsRightAdjoint G] :
    PreservesZeroMorphisms G where
  map_zero X
    Y := by
    let adj := Adjunction.ofIsRightAdjoint G
    calc
      G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
      _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
      _ = 0 := ?_
    · rw [Adjunction.right_triangle_components_assoc]
    · simp only [← G.map_comp, comp_zero]
    · simp only [id_obj, comp_obj, Adjunction.unit_naturality_assoc, zero_comp]

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