Morphisms out of the tensor product with a free presheaf on a representable

Let R be a presheaf of commutative rings on a category C, let M and N be presheaves of R-modules, and let U be an object of C. This file establishes the restriction--extension correspondence: morphisms M ⊗ freeYoneda R U ⟶ N out of the tensor product with the free presheaf of modules TauCeti.PresheafOfModules.freeYoneda R U on the presheaf represented by U are the same as morphisms of restrictions M|_U ⟶ N|_U on the slice over U, where restriction to the slice is PresheafOfModulesOfCommRing.pushforward₀ (Over.forget U) R.

A morphism ψ out of the tensor product restricts to the map sending a section m over g : V ⟶ U to ψ (m ⊗ g); conversely a morphism of restrictions φ extends to the map sending a pure tensor m ⊗ g to the value of the component of φ at g on m. The correspondence is natural in both arguments. Combined with the tensor--Hom adjunction it computes the sections of the internal Hom of presheaves of modules, in TauCeti.Algebra.Category.ModuleCat.Presheaf.InternalHom.

Main declarations

• TauCeti.PresheafOfModules.restrictOfTensorFreeYoneda and TauCeti.PresheafOfModules.tensorFreeYonedaOfRestrict: the two directions of the correspondence, characterized by TauCeti.PresheafOfModules.restrictOfTensorFreeYoneda_app_apply and TauCeti.PresheafOfModules.tensorFreeYonedaOfRestrict_app_tmul_freeMk;
• TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv: the correspondence (M ⊗ freeYoneda R U ⟶ N) ≃ (M|_U ⟶ N|_U), natural in the target by TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv_comp and in the source by TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv_whiskerRight_comp.

noncomputable def TauCeti.PresheafOfModules.restrictOfTensorFreeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (ψ : CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N) : (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N

The morphism of restrictions to the slice over U induced by a morphism out of the tensor product with the free presheaf represented by U: over g : V ⟶ U, it tensors a section with the basis element indexed by g.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.PresheafOfModules.restrictOfTensorFreeYoneda_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (ψ : CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N) (X : CategoryTheory.Over U) (m : ↑(((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M).obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (restrictOfTensorFreeYoneda U M N ψ) (Opposite.op X))) m = (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ψ (Opposite.op X.left))) (m ⊗ₜ[↑(R.obj (Opposite.op X.left))] ModuleCat.freeMk X.hom)

The component at X : Over U of the morphism of restrictions induced by ψ sends a section m over X.left to ψ (m ⊗ X.hom).

The section is taken in the domain of the component, the restriction of M to the slice evaluated at X, so that the lemma rewrites goals about components of morphisms of restrictions; a section of M over X.left may be passed as well, since the two modules are definitionally equal.

This is not a simp lemma: the component is a morphism of modules over the ring of the slice presheaf (Over.forget U).op ⋙ R at X, and simp rewrites that ring to R.obj (op X.left) inside the implicit arguments of the coercion, so the left-hand side has no simp normal form.

noncomputable def TauCeti.PresheafOfModules.tensorFreeYonedaOfRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (φ : (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N) : CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N

The morphism out of the tensor product with the free presheaf represented by U induced by a morphism of restrictions to the slice over U: a pure tensor of a section over V with the basis element indexed by g : V ⟶ U is sent to the value of the component at g.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PresheafOfModules.tensorFreeYonedaOfRestrict_app_tmul_freeMk {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (φ : (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N) {V : C} (m : ↑(M.obj (Opposite.op V))) (g : V ⟶ U) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (tensorFreeYonedaOfRestrict U M N φ) (Opposite.op V))) (m ⊗ₜ[↑(R.obj (Opposite.op V))] ModuleCat.freeMk g) = (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' φ (Opposite.op (CategoryTheory.Over.mk g)))) m

The morphism out of the tensor product induced by a morphism of restrictions φ sends the pure tensor of a section m over V with the basis element indexed by g : V ⟶ U to the value of the component of φ at g on m.

noncomputable def TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N) ≃ ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N)

Restricting to the slice over U and tensoring with the free presheaf represented by U are inverse: morphisms M ⊗ freeYoneda R U ⟶ N correspond to morphisms of restrictions M|_U ⟶ N|_U.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (ψ : CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N) : (tensorFreeYonedaHomEquiv U M N) ψ = restrictOfTensorFreeYoneda U M N ψ

The forward direction of the restriction--extension correspondence is TauCeti.PresheafOfModules.restrictOfTensorFreeYoneda.

@[simp]

theorem TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) (φ : (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).obj N) : (tensorFreeYonedaHomEquiv U M N).symm φ = tensorFreeYonedaOfRestrict U M N φ

The inverse direction of the restriction--extension correspondence is TauCeti.PresheafOfModules.tensorFreeYonedaOfRestrict.

theorem TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) {N' : PresheafOfModulesOfCommRing R} (ψ : CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N) (α : N ⟶ N') : (tensorFreeYonedaHomEquiv U M N') (CategoryTheory.CategoryStruct.comp ψ α) = CategoryTheory.CategoryStruct.comp ((tensorFreeYonedaHomEquiv U M N) ψ) ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).map α)

The restriction--extension correspondence is natural in the target.

theorem TauCeti.PresheafOfModules.tensorFreeYonedaHomEquiv_whiskerRight_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (U : C) (M N : PresheafOfModulesOfCommRing R) {M' : PresheafOfModulesOfCommRing R} (β : M' ⟶ M) (ψ : CategoryTheory.MonoidalCategoryStruct.tensorObj M (freeYoneda R U) ⟶ N) : (tensorFreeYonedaHomEquiv U M' N) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight β (freeYoneda R U)) ψ) = CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.pushforward₀ (CategoryTheory.Over.forget U) R).map β) ((tensorFreeYonedaHomEquiv U M N) ψ)

The restriction--extension correspondence is natural in the source.