Lean4
/-- Induce the lawfulness of the monoidal structure along an faithful functor of (plain) categories,
where the operations are already defined on the destination type `D`.
The functor `F` must preserve all the data parts of the monoidal structure between the two
categories.
-/
def induced [MonoidalCategoryStruct D] (F : D ⥤ C) [F.Faithful] (fData : InducingFunctorData F) :
MonoidalCategory.{v₂} D
where
tensorHom_def {X₁ Y₁ X₂ Y₂} f
g :=
F.map_injective <|
by
rw [fData.tensorHom_eq, Functor.map_comp, fData.whiskerRight_eq, fData.whiskerLeft_eq]
simp only [tensorHom_def, assoc, Iso.hom_inv_id_assoc]
id_tensorHom_id X₁ X₂ := F.map_injective <| by cases fData; cat_disch
tensorHom_comp_tensorHom f₁ f₂ g₁ g₂ := F.map_injective <| by cases fData; cat_disch
whiskerLeft_id X Y := F.map_injective <| by simp [fData.whiskerLeft_eq]
id_whiskerRight X Y := F.map_injective <| by simp [fData.whiskerRight_eq]
triangle X Y := F.map_injective <| by cases fData; cat_disch
pentagon W X Y
Z :=
F.map_injective <|
by
simp only [Functor.map_comp, fData.whiskerRight_eq, fData.associator_eq, Iso.trans_assoc, Iso.trans_hom,
Iso.symm_hom, tensorIso_hom, Iso.refl_hom, tensorHom_id, id_tensorHom, comp_whiskerRight, whisker_assoc, assoc,
fData.whiskerLeft_eq, whiskerLeft_comp, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc,
hom_inv_whiskerRight_assoc, Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]
slice_lhs 5 6 => rw [← whiskerLeft_comp, hom_inv_whiskerRight]
rw [whisker_exchange_assoc]
simp
leftUnitor_naturality {X Y : D}
f := F.map_injective <| by simp [fData.leftUnitor_eq, fData.whiskerLeft_eq, whisker_exchange_assoc]
rightUnitor_naturality {X Y : D}
f := F.map_injective <| by simp [fData.rightUnitor_eq, fData.whiskerRight_eq, ← whisker_exchange_assoc]
associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃} f₁ f₂
f₃ := F.map_injective <| by simp [fData.tensorHom_eq, fData.associator_eq, tensorHom_def, whisker_exchange_assoc]
