Pullback of pure tensor sections

This is an option-free selective port of the generic tensor-section kernel from projects/ModularCurves/ModularCurves/EllipticCurve/PoleSheaf.lean and the canonical pullback evaluator from projects/ModularCurves/ModularCurves/EllipticCurve/PullbackTensorSection.lean at AINTLIB commit 7ecbba9dbb7fee076a1b77a6cd516fc6de46d684.

Only the generic, option-free cone needed to evaluate the pullback cotensorator is retained. The sheafification comparison and its coherence lemmas stay private, and its target is written directly as a sheafification rather than reintroducing AINTLIB's broader Scheme.Modules.tensorObj API. The public surface consists of tensorSection, its functoriality theorem tensorSection_map, and the named downstream consumer pullback_δ_unit_tensorSection.

@[instance_reducible]

noncomputable def pullbackTensorSectionMonoidalCategory (X : AlgebraicGeometry.Scheme) : CategoryTheory.MonoidalCategory X.Modules

Equations

• pullbackTensorSectionMonoidalCategory X = AlgebraicGeometry.Scheme.Modules.monoidalCategory X

@[instance_reducible]

noncomputable def pullbackTensorSectionSheafModulesMonoidalCategory (X : AlgebraicGeometry.Scheme) : CategoryTheory.MonoidalCategory (SheafOfModules X.ringCatSheaf)

Equations

• pullbackTensorSectionSheafModulesMonoidalCategory X = id (AlgebraicGeometry.Scheme.Modules.monoidalCategory X)

noncomputable def ModularCurves.tensorSection {X : AlgebraicGeometry.Scheme} (M N : X.Modules) (U : X.Opens) (x : ↑(M.presheaf.obj (Opposite.op U))) (y : ↑(N.presheaf.obj (Opposite.op U))) : ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj M N).presheaf.obj (Opposite.op U))

The pure tensor of two sections over the same open, regarded as a section of the localized tensor product of sheaves of modules.

Equations

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

theorem ModularCurves.tensorSection_map {X : AlgebraicGeometry.Scheme} {M M' N N' : X.Modules} (f : M ⟶ M') (g : N ⟶ N') (U : X.Opens) (x : ↑(M.presheaf.obj (Opposite.op U))) (y : ↑(N.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.tensorHom f g).val.app (Opposite.op U))) (tensorSection M N U x y) = tensorSection M' N' U ((CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op U))) x) ((CategoryTheory.ConcreteCategory.hom (g.val.app (Opposite.op U))) y)

Forming a pure tensor section commutes with morphisms in both module factors.

theorem ModularCurves.pullback_δ_unit_tensorSection {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (M N : X.Modules) (U : X.Opens) (x : ↑(M.presheaf.obj (Opposite.op U))) (y : ↑(N.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.Scheme.Modules.pullback f) M N).val.app (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))) ((CategoryTheory.ConcreteCategory.hom (((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).val.app (Opposite.op U))) (tensorSection M N U x y)) = tensorSection ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M) ((AlgebraicGeometry.Scheme.Modules.pullback f).obj N) ((TopologicalSpace.Opens.map f.base).obj U) ((CategoryTheory.ConcreteCategory.hom (((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).unit.app M).val.app (Opposite.op U))) x) ((CategoryTheory.ConcreteCategory.hom (((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).unit.app N).val.app (Opposite.op U))) y)

The canonical pullback cotensorator sends the pullback-unit image of a pure tensor section to the pure tensor of the two pullback-unit sections.