Lean4
/-- Auxiliary definition for `Functor.Monoidal.transport`
-/
def coreMonoidalTransport {F G : C ⥤ D} [F.Monoidal] (i : F ≅ G) : G.CoreMonoidal
where
εIso := εIso F ≪≫ i.app _
μIso X Y := tensorIso (i.symm.app _) (i.symm.app _) ≪≫ μIso F X Y ≪≫ i.app _
μIso_hom_natural_left _ _ := by simp [NatTrans.whiskerRight_app_tensor_app_assoc]
μIso_hom_natural_right _ _ := by simp [NatTrans.whiskerLeft_app_tensor_app_assoc]
associativity X Y
Z :=
by
simp only [Iso.trans_hom, tensorIso_hom, Iso.app_hom, Iso.symm_hom, μIso_hom, comp_whiskerRight, Category.assoc,
MonoidalCategory.whiskerLeft_comp]
rw [← i.hom.naturality, map_associator_assoc, Functor.OplaxMonoidal.associativity_assoc, whiskerLeft_δ_μ_assoc,
δ_μ_assoc]
simp only [← Category.assoc]
congr 1
slice_lhs 3 4 =>
rw [← tensorHom_id, tensorHom_comp_tensorHom]
simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]
simp only [Category.assoc]
rw [← whisker_exchange_assoc]
simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc, Iso.inv_hom_id_assoc]
rw [← tensorHom_id, associator_naturality_assoc]
simp [← id_tensorHom, -tensorHom_id]
left_unitality
X :=
by
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom, μIso_hom,
Category.assoc, tensorHom_comp_tensorHom_assoc, Iso.hom_inv_id_app, Category.comp_id, Category.id_comp]
rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X), ← Category.id_comp (Functor.LaxMonoidal.ε F), ←
tensorHom_comp_tensorHom]
simp
right_unitality
X :=
by
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom, μIso_hom,
Category.assoc, tensorHom_comp_tensorHom_assoc, Category.id_comp, Iso.hom_inv_id_app, Category.comp_id]
rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X), ← Category.id_comp (Functor.LaxMonoidal.ε F), ←
tensorHom_comp_tensorHom]
simp
