feat(CategoryTheory/Monoidal): MulAction induced by a ModObj

[chrisflav]

We define the MulAction on hom types induced by a monoid object M action on X in a cartesian monoidal category.

---

• depends on: [Merged by Bors] - chore(CategoryTheory/Monoidal): rename Mod_ to Mod #38342

Given that Mathlib.CategoryTheory.Monoidal.Cartesian.Mod, I think the import increase is fine.

[github-actions]

PR summary ea11ccc0c5

Import changes exceeding 2%

%	File
+8.45%	Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Monoidal.Cartesian.Mod	663	719	+56 (+8.45%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mod	56

---

Declarations diff

+ IsModHom.map_smul
+ IsModHom.mulActionHom
+ ModObj.comp_smul
+ instance (Y : C) : SMul (Y ⟶ M) (Y ⟶ X)
+ isIso_leftSMul_iff
+ leftSMul
+ leftSMul_fst
+ leftSMul_snd
+ liftEquiv
+ lift_leftSMul
+ lift_leftSMul_eq_lift_iff
+ mulAction
+ mul_smul_self
+ mul_smul_self_flip
+ ofIso
+ one_smul_self

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[robin-carlier]

We already have something more general in Mathlib/CategoryTheory/Monoidal/Mod_.lean: this definition seems to be an instance of the notion of ModObj, which is the more general case where C is just monoidal (not necessarily cartesian monoidal) and acts on the left on a different category D. I think the results here that specializes to a cartesian monoidal category acting on itself should use ModObj instead. We might need a an additivization of them though.

[chrisflav]

Oh, thanks! (This is very clearly not an area of mathlib I am familiar with).

As far as I can tell, the only thing from this PR that is not yet in mathlib is the bit about the induced MulAction on Hom types. Is this correct? Is it in the correct generality (after replacing everything with ModObj)?

[robin-carlier]

Well we still need to to_additivize the module objects AddModObj and the IsMod_Hom (this name should be changed...).
I can see a few things here that we don’t have: I don’t think we have transport of structure along isomorphisms for ModObj (this is true in the generality of ModObj for sure). Also a slight difference I can see is that for ModObj the regular action of M on itself is not a global instance (I can’t exactly remember if there is a reason for this...)

The SMul on hom-types "as is" requires a cartesian monoidal category acting on itself I would say: you want to use lift in the definition, and having both Y ⟶ M Y ⟶ X well-defined requires everything to be in the same category (but maybe I’m missing some general setup... I’ll think about it, but I think for now it’s probably safe to go with this and to avoid attempting too much generalization of this part.)

[chrisflav]

Thanks, I will update this PR along these lines.

[chrisflav]

I have now updated this PR (hopefully) following your suggestions.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore(CategoryTheory/Monoidal): rename Mod_ to Mod #38342
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[dagurtomas]

Changing this and line 67 to

attribute [to_additive existing (attr := simp, reassoc)] ModObj.mul_smul ModObj.one_smul
attribute [to_additive existing (attr := simp)] ModObj.one_smul_assoc ModObj.mul_smul_assoc

achieves what you want to do without the warning, I think

[dagurtomas]

But I don't understand why the previous line doesn't do the same thing as these two lines

[chrisflav]

This is fixed in #38994 (see also #38336 (comment), where I asked Jovan a similar question). With that fix, these two lines can just be removed again and line 67 can stay as is.

I think it is slightly nicer to have the set_option version as is for now as a reminder that it should be cleaned up when #38994 lands, but if you prefer your version in the meantime I am happy to change it.