feat(CategoryTheory): the universal property of localized monoidal categories

[dagurtomas]

This PR provides a monoidal structure on any functor out of a localized monoidal category whose precomposition with the localization functor is monoidal

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Monoidal): more natural constructors for monoidal functors #29564

---

This PR continues the work from #24727.

Original PR: #24727

[github-actions]

PR summary dde1cfffb6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Localization.Monoidal.Functor (new file)	479

---

Declarations diff

+ Functor.curriedTensorPreIsoPost
+ Lifting₂.compRight
+ curriedTensorPostFunctor
+ curriedTensorPreFunctor
+ curriedTensorPreIsoPost
+ curriedTensorPreIsoPost_hom_app_app
+ curriedTensorPreIsoPost_hom_app_app'
+ functorCoreMonoidalOfComp
+ functorMonoidalOfComp
+ functorMonoidalOfComp_ε
+ functorMonoidalOfComp_μ
+ lifting₂CurriedTensorPost
+ lifting₂CurriedTensorPre
+ map_associator'
+ map_associator_inv'
+ natTrans_isMonoidal
+ transport_iso_isMonoidal
+ transport_δ
+ transport_ε
+ transport_η
+ transport_μ

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joelriou]

This is a very nice result. I think there is a way to simplify the proofs in a significant manner by introducing more constructors both for MonoidalCategory, and Functor.Lax/Oplax/Monoidal.
For example, the pentagon axiom for monoidal categories can be phrased as a property of a natural transformation between quadrifunctors, see the file https://github.com/joelriou/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Monoidal/Pentagon.lean
I have used this to construct the left derived monoidal structure, see https://github.com/joelriou/mathlib4/blob/2cc368b3e6ba0651e7e8dcc70429a4761cb4ff66/Mathlib/CategoryTheory/Monoidal/Derived.lean#L220 where the extensionality property for left derived functors is applied in order to reduce to pentagon property in the original category (the same strategy would work in order to simplify some proofs in the construction of the localized monoidal category).
Similarly (but I have not worked on this), in order to construct op/lax/monoidal functors, we could use the data of an (iso)morphism between bifunctors along with compatibilities phrased in terms of natural transformations instead of individual objects: for example, the associativity compatibility for a lax/oplax would be expressed as an identity of natural transformations between trifunctors. In order to prove it, we may use the extensionality property for natural transformations via localization functors (one still needs to do some rewrites after applying the lemma, but it does simplify the proofs!).
I believe we should develop this approach. What would you think about it? If you agree, we can plan how to proceed.

[dagurtomas]

I agree that there is room for improvement and generalization here. I'm working on it!

[dagurtomas]

I have obtained significantly simpler proofs of the main result in this PR using your suggested approach. I will split this up into two PRs and attempt something similar for the construction of localized monoidal categories

[dagurtomas]

#29564 creates a new file CategoryTheory/Monoidal/Multifunctor.lean with these constructors for (op/lax) monoidal functors. Once the relevant API for quadrifunctors is in, you can add the constructor for monoidal categories where the pentagon axiom is an equality of natural transformations between quadrifunctors, to that file, and we can simplify the construction of the localized monoidal category.

[mathlib4-merge-conflict-bot]

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

[joelriou]

I am not very happy with the line letI : (L ⋙ F).Monoidal := Functor.Monoidal.transport e.symm. I believe this should be phrased in terms of Functor.LaxMonoidal.μ G. The chunks of code I have given before show that the proofs have a similar length when using G instead of L ⋙ F.

[dagurtomas]

The letI : (L ⋙ F).Monoidal := Functor.Monoidal.transport e.symm line is just a way of avoiding to have to carry around the isomorphism e in proofs. Your suggested curriedTensorPreIsoPost_hom_app_app just writes that out explicitly. Although your proofs have similar length, they rely more on big rw blocks which indicates that automation doesn't work as well in them, also making them harder to maintain.

[dagurtomas]

I've added explicit rewrite lemmas functorMonoidalOfComp_ε and functorMonoidalOfComp_μ

[dagurtomas]

Just to summarize the situation, below is the approach suggested by @joelriou. It might be good to get a second opinion. I'm happy to change to this approach if a second reviewer agrees with Joël, but I prefer my approach. The advantage of Joël's approach is that it avoids temporarily transporting the monoidal structure on G to the isomorphic functor L ⋙ F, while the advantage of mine is (in my opinion) more straightforward proofs.

@[reassoc]
noncomputable def curriedTensorPreIsoPost_hom_app_app (X₁ X₂ : C) :
    letI e := Lifting.iso L W G F
    ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂) =
      (e.hom.app _ ⊗ₘ e.hom.app _) ≫ LaxMonoidal.μ G X₁ X₂ ≫ e.inv.app _ ≫
        F.map (OplaxMonoidal.δ L _ _) := by
  simp [curriedTensorPreIsoPost]


lemma curriedTensorPreIsoPost_hom_app_app' {X₁ X₂ : C} {Y₁ Y₂ : D}
    (e₁ : Y₁ ≅ L.obj X₁) (e₂ : Y₂ ≅ L.obj X₂) :
    letI e := Lifting.iso L W G F
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
      ((F.map e₁.hom ≫ e.hom.app _) ⊗ₘ (F.map e₂.hom ≫ e.hom.app _)) ≫
        LaxMonoidal.μ G X₁ X₂ ≫ e.inv.app _ ≫
        F.map (OplaxMonoidal.δ L _ _≫ (e₁.inv ⊗ₘ e₂.inv)) := by
  have h₁ := ((curriedTensorPreIsoPost L W F G).hom.app Y₁).naturality e₂.hom
  have h₂ := congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality e₁.hom)
  dsimp at h₁ h₂ ⊢
  rw [← cancel_mono (F.map (Y₁ ◁ e₂.hom)), ← h₁, ← cancel_mono (F.map (e₁.hom ▷ L.obj X₂)),
    Category.assoc, ← h₂, curriedTensorPreIsoPost_hom_app_app, Category.assoc, Category.assoc,
    Category.assoc, Category.assoc, ← tensorHom_def'_assoc, tensorHom_comp_tensorHom_assoc,
    ← Functor.map_comp, ← tensorHom_def', ← Functor.map_comp, Category.assoc,
    tensorHom_comp_tensorHom, Iso.inv_hom_id, Iso.inv_hom_id, tensorHom_id, id_whiskerRight,
    Category.comp_id]

/--
Monoidal structure on `F`, given that `L ⋙ F` is monoidal, where `L` is a localization functor.
-/
@[simps!]
noncomputable def functorCoreMonoidalOfComp : F.CoreMonoidal := by
  letI e := Lifting.iso L W G F
  refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_
  · refine natTrans₃_ext L L L W W W (fun X₁ X₂ X₃ ↦ ?_)
    dsimp
    rw [curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app,
      curriedTensorPreIsoPost_hom_app_app' L W F G (μIso L _ _) (Iso.refl _),
      curriedTensorPreIsoPost_hom_app_app' L W F G (Iso.refl _) (μIso L _ _)]
    dsimp
    simp only [comp_whiskerRight, map_id, Category.id_comp, tensorHom_id, map_comp, Category.assoc,
      MonoidalCategory.whiskerLeft_comp, id_tensorHom]
    rw [tensorHom_def', comp_whiskerRight_assoc,
      tensorHom_def (e.hom.app X₂), whisker_assoc_assoc,
      MonoidalCategory.whiskerLeft_comp_assoc,
      tensorHom_def'_assoc, ← whisker_exchange_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← whisker_exchange_assoc,
      tensor_whiskerLeft_assoc, Iso.inv_hom_id_assoc,
      ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc,
      ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc,
      Category.assoc, Category.assoc, Category.assoc, map_δ_μ_assoc,
      Iso.inv_hom_id_app, Category.comp_id,
      ← map_comp, ← map_comp, OplaxMonoidal.associativity,
      tensorHom_def_assoc, whisker_exchange_assoc, whisker_exchange_assoc,
      whisker_exchange_assoc, whiskerRight_tensor_assoc,
      comp_whiskerRight_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc (G.obj X₁),
      ← MonoidalCategory.whiskerLeft_comp_assoc (G.obj X₁),
      ← MonoidalCategory.whiskerLeft_comp_assoc (G.obj X₁),
      Category.assoc, Category.assoc, ← Functor.map_comp_assoc,
      δ_μ, map_id, Category.id_comp, Iso.inv_hom_id_app,
      Category.comp_id, ← LaxMonoidal.associativity_assoc, NatTrans.naturality_assoc,
      Functor.map_comp, Functor.map_comp]
    dsimp
  · refine natTrans_ext L W (fun X₂ ↦ ?_)
    have := NatTrans.congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality (εIso L).inv)
      (L.obj X₂)
    dsimp at this ⊢
    rw [comp_whiskerRight_assoc, comp_whiskerRight_assoc,
      reassoc_of% this,
      curriedTensorPreIsoPost_hom_app_app_assoc, tensorHom_def_assoc,
      ← comp_whiskerRight_assoc _ (e.hom.app _),
      Iso.inv_hom_id_app, id_whiskerRight, Category.id_comp, ← whisker_exchange_assoc,
      id_whiskerLeft_assoc, OplaxMonoidal.left_unitality_assoc,
      whiskerRight_η_ε_assoc, δ_μ_assoc, NatTrans.naturality_assoc,
      Iso.hom_inv_id_app_assoc]
    dsimp
    rw [← map_comp, ← map_comp, ← map_comp,
      LaxMonoidal.left_unitality L, whiskerRight_η_ε_assoc, δ_μ_assoc, Iso.map_inv_hom_id,
      Functor.map_id, Category.comp_id]
  · refine natTrans_ext L W (fun X₁ ↦ ?_)
    dsimp
    have := ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).naturality (εIso L).inv
    dsimp at this
    rw [MonoidalCategory.whiskerLeft_comp_assoc,
      MonoidalCategory.whiskerLeft_comp_assoc, reassoc_of% this,
      curriedTensorPreIsoPost_hom_app_app_assoc, tensorHom_def'_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc _ (e.inv.app _), Iso.inv_hom_id_app,
      MonoidalCategory.whiskerLeft_id_assoc, whisker_exchange_assoc,
      MonoidalCategory.whiskerRight_id_assoc, OplaxMonoidal.right_unitality_assoc,
      whiskerLeft_η_ε_assoc, δ_μ_assoc, NatTrans.naturality_assoc, Iso.hom_inv_id_app_assoc]
    dsimp
    rw [← map_comp, ← map_comp, ← map_comp,
      LaxMonoidal.right_unitality L, whiskerLeft_η_ε_assoc, δ_μ_assoc, Iso.map_inv_hom_id,
      Functor.map_id, Category.comp_id]

[mathlib4-merge-conflict-bot]

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