ofTensorHom — Mathlib

Lean4
/-- A constructor for lax monoidal functors whose axioms are described by `tensorHom` instead of
`whiskerLeft` and `whiskerRight`.
-/
def ofTensorHom : F.LaxMonoidal where
  ε := ε
  μ := μ
  μ_natural_left := fun f X' => by simp_rw [← tensorHom_id, ← F.map_id, μ_natural]
  μ_natural_right := fun X' f => by simp_rw [← id_tensorHom, ← F.map_id, μ_natural]
  associativity := fun X Y Z => by simp_rw [← tensorHom_id, ← id_tensorHom, associativity]
  left_unitality := fun X => by simp_rw [← tensorHom_id, left_unitality]
  right_unitality := fun X => by simp_rw [← id_tensorHom, right_unitality]
Похожие утверждения