pushforward of tensor presheaves

Stream: maths

[Zhong TengXun]

I'm trying to prove "restriction of tensor presheaves is the tensor of presheaves' restriction". restriction is threat as pushforward throuth immersion. So I write sth like

theorem tensor_comm_with_over {C : Type u_1} [Category.{u_2, u_1} C] {R : Functor Cᵒᵖ CommRingCat}
(M₁ M₂ : PresheafOfModules (R.comp (forget₂ CommRingCat RingCat))) (X : C) :
(@PresheafOfModules.monoidalCategoryStruct (Over X) _ ((Over.forget X).op ⋙ R)).tensorObj (M₁.over X) (M₂.over X)=(tensorObj M₁ M₂).over X:=sorry
--over just the presheaf version of  SheafOfModules.over

the tensorObj on the left is due to lean can't figure out (Over.forget X).op ⋙ R ⋙ (forget₂ CommRingCat RingCat) represent somthing likeR' ⋙ (forget₂ CommRingCat RingCat) due to the associativity of ⋙. thus fail to see the tensor by default.
I'm quite sure this is an equal by definition, but rfl failed. Then I want to try proving obj and map are each equal but failed to find a way to transist the equality of obj and map into equality of hole presheaves. or I'm wrong, that they're just isomorphic?

[Joël Riou]

It seems that what you are trying to prove would be a particular case of:

import Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

universe u

open CategoryTheory MonoidalCategory

namespace PresheafOfModules

variable {C D : Type*} [Category C] [Category D] {F : C ⥤ D}

abbrev toRingCatPresheafMap
    {R : Dᵒᵖ ⥤ CommRingCat.{u}} {S : Cᵒᵖ ⥤ CommRingCat.{u}} (φ : S ⟶ F.op ⋙ R) :
    S ⋙ forget₂ _ RingCat ⟶ F.op ⋙ (R ⋙ forget₂ _ RingCat) :=
  whiskerRight φ (forget₂ _ _)

variable (R : Dᵒᵖ ⥤ CommRingCat.{u})

noncomputable def pushforwardCoreMonoidal :
    (pushforward (toRingCatPresheafMap (𝟙 (F.op ⋙ R)))).CoreMonoidal where
  εIso := Iso.refl _
  μIso M₁ M₂ := isoMk (fun X ↦ by
    -- `exact` fails without the `dsimp`
    dsimp [pushforward, pushforward₀, restrictScalarsObj, ModuleCat.restrictScalars,
      tensorObj, ModuleCat.RestrictScalars.obj']
    exact Iso.refl _) sorry
  μIso_hom_natural_left := sorry
  μIso_hom_natural_right := sorry
  associativity := sorry
  left_unitality := sorry
  right_unitality := sorry

noncomputable instance : (pushforward (toRingCatPresheafMap (𝟙 (F.op ⋙ R)))).Monoidal :=
  Functor.CoreMonoidal.toMonoidal (pushforwardCoreMonoidal _)

end PresheafOfModules

A better approach could be to show that for a general morphism φ : S ⟶ F.op ⋙ R of categories equipped with a presheaf of commutative rings, the pushforward functor is (op?)lax monoidal, and then show that if φ is an isomorphism, it is monoidal. (Using Iso.refl above is very much an abuse as it seems we use a restriction of scalars via the identity ring morphism...)
I am not even sure that mathlib has the fact that the restriction of scalars for a morphism of commutative rings is (op?)lax monoidal, so that is something which should be done first, and then it may be extended to the case of presheaves of modules.

[Joël Riou]

Actually, the following works:

variable {C D : Type*} [Category C] [Category D]
  (F : C ⥤ D) (R : Dᵒᵖ ⥤ CommRingCat.{u})

abbrev pushforward₀Comm (F : C ⥤ D) (R : Dᵒᵖ ⥤ CommRingCat.{u}) :
    PresheafOfModules (R ⋙ forget₂ _ _) ⥤ PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ _ _) :=
  pushforward₀ F (R ⋙ forget₂ _ _)

noncomputable def pushforward₀CommCoreMonoidal :
    (pushforward₀Comm F R).CoreMonoidal where
  εIso := Iso.refl _
  μIso M₁ M₂ := Iso.refl _
  μIso_hom_natural_left := sorry
  μIso_hom_natural_right := sorry
  associativity := sorry
  left_unitality := sorry
  right_unitality := sorry

noncomputable instance : (pushforward₀Comm F R).Monoidal :=
  Functor.CoreMonoidal.toMonoidal (pushforward₀CommCoreMonoidal F R)

[Zhong TengXun]

Is this show we don't need φ to be isomorphism to let pushforward functor monodial?
Lemma 17.16.4

[Joël Riou]

For the pushforward, we need an assumption, but for the pullback, it holds in general. (Note that the pullback of (pre)sheaves of modules is not yet in mathlib, cf. #17366)

[Zhong TengXun]

wait, I just realized the restiction of sheaf to an open set X should defines as pullback whose map Y to Y ⊓ X, is this a easier approach?(Even not I guess still need to prove this since covers of schemes give fuctors above And Over.forget X can't induce by any continue map of topological spaces)

[Joël Riou]

There are two ways to describe the pullback functor for sheaves (of modules) by an open immersion j : U ⟶ X.

1. As a particular case of a pullback by a map, j^* is the left adjoint to the direct image functor j_*, where for any V open in X, (j_*F)(V) identify toF(U ⊓ V).
2. Directly, as the functor defined by (j^*G)(W) = G(W) where any open subset W of U is identified to an open subset of X. Then, this is a particular case of the construction pushforward(₀) in my code. This approach has better definitional properties.

[Zhong TengXun]

Another question, to show something like $(\mathcal{F}|_U)|_V=\mathcal{F}|_V$ for $V \subset U$ we can't use Over.forget right? Is it not the right fuctor since it map all $f : Y \to X$ to $Y$ so we can't get the right composition relation?

[Joël Riou]

If j : U ⟶ X is the inclusion of an open subset, then the category of opens of U is equivalent (but not equal) to the category Over U' where U' is U considered as an object in the category of opens of X.

[Zhong TengXun]

If we have inclusion $j_1:V\to U$ and $j_2:W\to V$, and I want to show category of open of W as a open subset of V via Over. Then which object in Over V'should I pick?

[Joël Riou]

I would suggest you look at certain references and textbooks in order to clarify the mathematical aspects, and then you may try to formalise some definitions.