feat(CategoryTheory): some API for transporting monoidal morphism properties (#31345)

Author: dagurtomas

Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean

@@ -40,6 +40,14 @@ class IsMonoidal : Prop extends W.IsMultiplicative where
   whiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (X ◁ g)
   whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : W f) (Y : C) : W (f ▷ Y)
 
+/-- Alternative constructor for `W.IsMonoidal` given that `W` is multiplicative and stable under
+tensoring morphisms. -/
+lemma IsMonoidal.mk' [W.IsMultiplicative]
+    (h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (_ : W f) (_ : W g), W (f ⊗ₘ g)) :
+    W.IsMonoidal where
+  whiskerLeft X _ _ g hg := by simpa using h (𝟙 X) g (W.id_mem _) hg
+  whiskerRight f hf Y := by simpa using h f (𝟙 Y) hf (W.id_mem _)
+
 variable [W.IsMonoidal]
 
 lemma whiskerLeft_mem (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : W g) : W (X ◁ g) :=
@@ -53,6 +61,16 @@ lemma tensorHom_mem {X₁ X₂ : C} (f : X₁ ⟶ X₂) {Y₁ Y₂ : C} (g : Y
   rw [tensorHom_def]
   exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)
 
+/-- The inverse image under a monoidal functor of a monoidal morphism property which respects
+isomorphisms is monoidal. -/
+instance {C' : Type*} [Category C'] [MonoidalCategory C'] (F : C' ⥤ C) [F.Monoidal]
+    [W.RespectsIso] : (W.inverseImage F).IsMonoidal := .mk' _ fun f g hf hg ↦ by
+  simp only [inverseImage_iff] at hf hg ⊢
+  rw [Functor.Monoidal.map_tensor _ f g]
+  apply MorphismProperty.RespectsIso.precomp
+  apply MorphismProperty.RespectsIso.postcomp
+  exact tensorHom_mem _ _ _ hf hg
+
 end MorphismProperty
 
 /-- Given a monoidal category `C`, a localization functor `L : C ⥤ D` with respect

Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

@@ -225,4 +225,9 @@ instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategor
 @[deprecated (since := "2025-11-06")] alias η_app := Functor.OplaxMonoidal.whiskeringRight_η_app
 @[deprecated (since := "2025-11-06")] alias δ_app := Functor.OplaxMonoidal.whiskeringRight_δ_app
 
+@[simps!]
+instance Functor.Monoidal.whiskeringLeft (E : Type*) [Category E] [MonoidalCategory E] (F : C ⥤ D) :
+    ((whiskeringLeft _ _ E).obj F).Monoidal :=
+  CoreMonoidal.toMonoidal { εIso := Iso.refl _, μIso _ _ := Iso.refl _ }
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Monoidal.lean

@@ -6,7 +6,7 @@ Authors: Joël Riou
 
 import Mathlib.CategoryTheory.Closed.FunctorCategory.Basic
 import Mathlib.CategoryTheory.Localization.Monoidal.Braided
-import Mathlib.CategoryTheory.Sites.Localization
+import Mathlib.CategoryTheory.Sites.Equivalence
 import Mathlib.CategoryTheory.Sites.SheafHom
 
 /-!
@@ -29,12 +29,12 @@ chosen finite products.
 
 -/
 
-universe v v' u u'
+universe v₁ v₂ v₃ u₁ u₂ u₃
 
 namespace CategoryTheory
 
-variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C}
-  {A : Type u} [Category.{v} A] [MonoidalCategory A]
+variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
+  {A : Type u₃} [Category.{v₃} A] [MonoidalCategory A]
 
 open Opposite Limits MonoidalCategory MonoidalClosed Enriched.FunctorCategory
 
@@ -107,12 +107,20 @@ end Presheaf
 
 namespace GrothendieckTopology
 
+namespace W
+
+variable (J A) in
+lemma transport_isMonoidal {D : Type u₂} [Category.{v₂} D] (K : GrothendieckTopology D)
+    (G : D ⥤ C) [G.IsCoverDense J] [G.Full] [G.IsContinuous K J]
+    [(G.sheafPushforwardContinuous A K J).EssSurj] [(K.W (A := A)).IsMonoidal] :
+    (J.W (A := A)).IsMonoidal := by
+  rw [← J.W_inverseImage_whiskeringLeft K G]
+  infer_instance
+
 variable [MonoidalClosed A]
   [∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂]
   [∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂]
 
-namespace W
-
 open MonoidalClosed.FunctorCategory
 
 lemma whiskerLeft {G₁ G₂ : Cᵒᵖ ⥤ A} {g : G₁ ⟶ G₂} (hg : J.W g) (F : Cᵒᵖ ⥤ A) :