Lean4
/-- When `M` is a `B`-module in `D` and `f : A ⟶ B` is a morphism of internal
monoid objects, `M` inherits an `A`-module structure via
"restriction of scalars", i.e `γ[A, M] = f.hom ⊵ₗ M ≫ γ[B, M]`. -/
@[simps!]
def scalarRestriction (M : D) [ModObj B M] : ModObj A M
where
smul := f ⊵ₗ M ≫ γ[B,M]
one_smul' := by
rw [← comp_actionHomLeft_assoc]
rw [IsMonHom.one_hom, ModObj.one_smul]
mul_smul' := by
-- oh, for homotopy.io in a widget!
slice_rhs 2 3 => rw [action_exchange]
simp only [actionHomLeft_action_assoc, Category.assoc, Iso.hom_inv_id_assoc, actionHomRight_comp]
slice_rhs 4 6 => rw [ModObj.assoc_flip]
slice_rhs 2 4 => rw [← whiskerLeft_actionHomLeft]
slice_rhs 1 2 => rw [← comp_actionHomLeft]
rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc, IsMonHom.mul_hom, tensorHom_def,
Category.assoc]
