instComonObj — Mathlib

Lean4
/-- The image of a comonoid object under a oplax monoidal functor is a comonoid object. -/
abbrev instComonObj (A : C) [ComonObj A] (F : C ⥤ D) [F.OplaxMonoidal] : ComonObj (F.obj A)
    where
  counit := F.map ε[A] ≫ η F
  comul := F.map Δ[A] ≫ δ F _ _
  counit_comul := by
    simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality, ← F.map_comp_assoc, counit_comul]
  comul_counit := by
    simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc, right_unitality, ←
      F.map_comp_assoc, comul_counit]
  comul_assoc := by
    simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, MonoidalCategory.whiskerLeft_comp,
      δ_natural_right_assoc, ← F.map_comp_assoc, comul_assoc, F.map_comp, Category.assoc, associativity]
Похожие утверждения