Lean4
/-- The structure which allows to construct the monoidal category structure
on `HomologicalComplex C c` from the monoidal category structure on
graded objects. -/
noncomputable def inducingFunctorData : Monoidal.InducingFunctorData (forget C c)
where
μIso _ _ := Iso.refl _
εIso := tensorUnitIso C c
whiskerLeft_eq K₁ K₂ L₂
g := by
dsimp [forget]
rw [comp_id]
erw [id_comp]
rfl
whiskerRight_eq {K₁ L₁} f
K₂ := by
dsimp [forget]
rw [comp_id]
erw [id_comp]
rfl
tensorHom_eq {K₁ L₁ K₂ L₂} f
g := by
dsimp [forget]
rw [comp_id]
erw [id_comp]
rfl
associator_eq K₁ K₂
K₃ := by
dsimp [forget]
simp only [tensorHom_id, whiskerRight_tensor, id_whiskerRight, id_comp, Iso.inv_hom_id, comp_id, assoc]
erw [id_whiskerRight]
rw [id_comp]
erw [id_comp]
rfl
leftUnitor_eq
K := by
dsimp
erw [id_comp]
rfl
rightUnitor_eq
K := by
dsimp
rw [assoc]
erw [id_comp]
rfl
