instMonoidalDiscreteFunctorFunctorF

Lean4
instance (h : ShiftMkCore C A) : (Discrete.functor h.F).Monoidal :=
  Functor.CoreMonoidal.toMonoidal
    { εIso := h.zero.symm
      μIso := fun m n ↦ (h.add m.as n.as).symm
      μIso_hom_natural_left := by
        rintro ⟨X⟩ ⟨Y⟩ ⟨⟨⟨rfl⟩⟩⟩ ⟨X'⟩
        ext
        simp
      μIso_hom_natural_right := by
        rintro ⟨X⟩ ⟨Y⟩ ⟨X'⟩ ⟨⟨⟨rfl⟩⟩⟩
        ext
        simp
      associativity := by
        rintro ⟨m₁⟩ ⟨m₂⟩ ⟨m₃⟩
        ext X
        simp [endofunctorMonoidalCategory, h.assoc_inv_app_assoc]
      left_unitality := by
        rintro ⟨n⟩
        ext X
        simp [endofunctorMonoidalCategory, h.zero_add_inv_app, ← Functor.map_comp]
      right_unitality := by
        rintro ⟨n⟩
        ext X
        simp [endofunctorMonoidalCategory, h.add_zero_inv_app] }
Похожие утверждения