feat(CategoryTheory/Monoidal/DayConvolution): left and right unitors for Day convolution

[robin-carlier]

Given a DayConvolutionUnit U a functor F : C ⥤ V and a Day convolution of U and F, we construct the left unitor isomorphism. U ⊛ F ≅ F. Similarly, given a Day convolution of F and U, we construct the right unitor.

We characterize the isomorphisms, show their naturality, and show that the triangle identity is satisfied.

---

• depends on: feat(CategoryTheory/Monoidal/DayConvolution): Associators and pentagon for Day Convolution #24992

[github-actions]

PR summary a9d7ae146f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic (new file)	446
Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (new file)	640
Mathlib.CategoryTheory.Monoidal.DayConvolution (new file)	642

---

Declarations diff

+ DayConvolution
+ DayConvolution.triangle
+ DayConvolutionUnit
+ associator
+ associatorCorepresentingIso
+ associator_hom_unit_unit
+ associator_inv_unit_unit
+ associator_naturality
+ convolution_hom_ext_at
+ corepresentable
+ corepresentableIso
+ corepresentableIsoLeft
+ corepresentableIsoRight
+ corepresentableIso₂
+ corepresentableIso₂'
+ corepresentableLeft
+ corepresentableRight
+ corepresentable₂
+ corepresentable₂'
+ extensionUnitLeft
+ extensionUnitRight
+ externalProduct
+ externalProductBifunctor
+ externalProductBifunctorUncurried
+ externalProductCompDiagIso
+ externalProductFlip
+ externalProductSwap
+ hom_ext
+ instance : ((F ⊛ G) ⊠ H).IsLeftKanExtension <|
+ instance : (F ⊠ G ⊛ H).IsLeftKanExtension <|
+ instance : (F ⊠ U).IsLeftKanExtension <| extensionUnitRight U (φ U) F
+ instance : (U ⊠ F).IsLeftKanExtension <| extensionUnitLeft U (φ U) F
+ leftKanExtension
+ leftUnitor
+ leftUnitorCorepresentingIso
+ leftUnitor_hom_unit_app
+ leftUnitor_inv_app
+ leftUnitor_naturality
+ map
+ map_unit_app
+ pentagon
+ pointwiseLeftKanExtensionAtLeft
+ pointwiseLeftKanExtensionAtRight
+ pointwiseLeftKanExtensionLeft
+ pointwiseLeftKanExtensionRight
+ prodCompExternalProduct
+ rightUnitor
+ rightUnitorCorepresentingIso
+ rightUnitor_hom_unit_app
+ rightUnitor_inv_app
+ rightUnitor_naturality
+ uniqueUpToIso
+ uniqueUpToIso_hom_unit
+ uniqueUpToIso_inv_unit
+ unit_naturality
+ unit_naturality_id_left
+ unit_naturality_id_right
+ φ

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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(CategoryTheory/Monoidal/DayConvolution): Associators and pentagon for Day Convolution #24992
  By Dependent Issues (🤖). Happy coding!