fromInducedCoreMonoidal — Mathlib

Lean4

/-- A faithful functor equipped with a `InducingFunctorData` structure is monoidal. -/
def fromInducedCoreMonoidal [MonoidalCategoryStruct D] (F : D ⥤ C) [F.Faithful] (fData : InducingFunctorData F) :
    letI := induced F fData
    F.CoreMonoidal :=
  by
  letI := induced F fData
  exact
    { εIso := fData.εIso
      μIso := fData.μIso
      μIso_hom_natural_left := fun _ ↦ by simp [fData.whiskerRight_eq]
      μIso_hom_natural_right := fun _ ↦ by simp [fData.whiskerLeft_eq]
      associativity := fun _ _ _ ↦ by simp [fData.associator_eq]
      left_unitality := fun _ ↦ by simp [fData.leftUnitor_eq]
      right_unitality := fun _ ↦ by simp [fData.rightUnitor_eq] }

Похожие утверждения