Refactoring Mod_?

Stream: mathlib4

[Robin Carlier]

In #25499, I introduce the notion of a left action of a monoidal category on a category. Given such an action of C on D, I intend to define modules in D on an internal monoid object of C. In terms of generality, this should completely supercedes Mathlib.CategoryTheory.Monoidal.Mod_ , which is the special case where C acts on itself via the tensor product.
Should I do this construction in a separate definition, and leave the current Mod_ as is (and of course provide an equivalence between the two), or should I rather refactor Mod_ into the more general construction?
My gut feeling is to go for the refactor, because otherwise this is just going to end up with duplicated code/API, but I’d rather ask maintainers what they think of this.

[Joël Riou]

I would think it would be fine to refactor Mod_. You should coordinate with @Yuma Mizuno because #24646 refactors Mon_ by making the unbundled version Mon_Class the preferred API. We probably want that Mod_ be changed accordingly.

[Yuma Mizuno]

I'm not working on Mod_ right now, but what I have in mind (for the current definition) is the following:

structure Mod_ (A : C) [Mon_Class A] where
  X : C
  [mod : Mod_Class A X]

[Yuma Mizuno]

By the way, is #24599 the intended PR?

[Joël Riou]

#25499

[Robin Carlier]

Oh, right, sorry for the wrong number...

[Robin Carlier]

Yuma Mizuno said:

I'm not working on Mod_ right now, but what I have in mind (for the current definition) is the following:

structure Mod_ (A : C) [Mon_Class A] where
  X : C
  [mod : Mod_Class A X]

I guess then this means thatMod_Class should also be refactored so that X can be in D where C acts on D.

[Robin Carlier]

@Yuma Mizuno Is there a rationale behind the fact that Mon_ has been redefined as

structure Mon_ where
  /-- The underlying object in the ambient monoidal category -/
  X : C
  [mon : Mon_Class X]

but the Mon_.Hom structure remains

@[ext]
structure Hom (M N : Mon_ C) where
  /-- The underlying morphism -/
  hom : M.X ⟶ N.X
  one_hom : η ≫ hom = η := by aesop_cat
  mul_hom : μ ≫ hom = (hom ⊗ hom) ≫ μ := by aesop_cat

and is not e.g

/-- A morphism of monoid objects. -/
@[ext]
structure Hom (M N : Mon_ C) where
  /-- The underlying morphism -/
  hom : M.X ⟶ N.X
  [isMon_Hom: IsMon_Hom hom]

?

[Robin Carlier]

The refactor is at #25545. I went with this definition for morphisms

/-- A morphism of monoid objects. -/
@[ext]
structure Hom (M N : Mod_ D A) where
  /-- The underlying morphism -/
  hom : M.X ⟶ N.X
  [isMod_Hom : IsMod_Hom A hom]

but this can be easily change if we want something more aligned with the current Hom-types in Mon_.

[Yuma Mizuno]

For Hom, I don't think it makes much difference. I think it's just the difference in the default constructor. For Mon_, the difference is more serious because Mon_Class contains data (μ and η).

[Robin Carlier]

So you’d suggest aligning the Hom structure for Mod_ with the one for Mon_?

[Yuma Mizuno]

No. I think either is fine. In particular, it would be fine to change the Mon_.Hom definition to the latter (one using isMon_Hom).

[Robin Carlier]

Given that Mod_ is way less used than Mon_, it’s probably more of a pain to change Mon_.Hom than to just align Mod_ on Mon_, if you say it doesn’t matter much anyway (which I agree). At least things would feel more coherent and would save an extra refactor PR if I just make Mod_.Hom without isMod_hom.

[Yuma Mizuno]

I'm willing to do the refactoring about Mon_.Hom, which doesn't look hard if I introduce a new constructor like

abbrev Hom.mk' {M N : Mon_ C} (f : M.X ⟶ N.X)
    (one_f : η ≫ f = η := by aesop_cat)
    (mul_f : μ ≫ f = (f ⊗ f) ≫ μ := by aesop_cat) : Hom M N :=
  have : IsMon_Hom f := ⟨one_f, mul_f⟩
  .mk f

and just replace the current use of Hom.mk with Hom.mk'.

[Robin Carlier]

Well, too late as I have already replaced the definition in #25545 to match the current Mon_ :D. It’s your call really. I just find that it’s better if the two definition align, whichever we pick.

[Yuma Mizuno]

If it doesn't make a big difference, I would prefer IsMon_Hom to be the default.

[Robin Carlier]

Ok! I’ll revert the commit in #25545 then.

[Yuma Mizuno]

Thanks!

[Yuma Mizuno]

refactor(CategoryTheory/Monoidal): define Mon_.Hom using type class IsMon_Hom #25549