General pullback–tensor compatibility — decomposition skeleton (Route G) #
This is an option-free selective port of
PullbackTensorGeneral.lean
from AINTLIB commit 7ecbba9dbb7fee076a1b77a6cd516fc6de46d684. The unused
PullbackTensorMonoidal import is deliberately omitted. In particular, this file does not
import AINTLIB's option-heavy Picard or invertible-sheaf closure.
The small sheafifyValIso comparison needed at the sheaf boundary is selectively retained
from AINTLIB's Picard/InvertibleSheaf.lean at the same commit.
/develop --decompose skeleton for D-PresPB′-general (board v10.98/v10.99): the general-f
pullback–tensor gate of the GME (2.16) Picard-functoriality chain. Route G (construction-grain):
give the presheaf pushforward its lax monoidal structure, get the oplax comparison δ on the
pullback by doctrinal adjunction, show δ is an iso on free-yoneda generators (on an Opens-site
the tensor of free-yonedas is the free-yoneda of the meet — the lattice miracle — and
freeFunctorCompPullbackIso matches the pullback side), and extend along free presentations by
two single-variable five-lemma passes in the abelian target. Payoff:
functorMonoidalOfComp ⟹ (Modules.pullback f).Monoidal ⟹ Skeleton.monoidHom ⟹
Pic(f) : Pic X →* Pic Y.
All leaves are stated Nonempty-wrapped (Props, so the monoidal data carry no proof
assumptions under the v10.8 discipline; the data is built at execution time, each structure
landing only when its leaf is fully checked). Full route adjudication, verbatim anchors and
attack logs:
.mathlib-quality/decomposition-pullback-monoidal-general.md.
Taking the mate of a monoidal natural transformation between right adjoints produces a monoidal natural transformation between the corresponding left adjoints.
Monoidality of a natural transformation can be checked after precomposition with a monoidal localization functor.
[D-PresPB′-general], leaf B1a (unit component). The unit comparison of the lax
monoidal structure on presheaf-level restriction of scalars, at a section: the ring map
ψ.app U itself, as a linear map into the restricted module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
[D-PresPB′-general], leaf B1a (tensorator component). The tensorator of the lax
monoidal structure on presheaf-level restriction of scalars, at a section:
x ⊗ₜ y ↦ x ⊗ₜ y from the tensor over the downstairs ring to the (restricted) tensor over
the upstairs ring (TensorProduct.mapOfCompatibleSMul — the lax direction needs no
bijectivity: the downstairs action slides in the upstairs tensor because it factors
through ψ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
[D-PresPB′-general], leaf B1a (unit). The unit comparison as a morphism of presheaves
of modules; naturality is the naturality of ψ.
Equations
- PresheafOfModules.restrictScalarsLaxε ψ = { app := fun (U : Cᵒᵖ) => PresheafOfModules.restrictScalarsLaxεApp ψ U, naturality := ⋯ }
Instances For
[D-PresPB′-general], leaf B1a (tensorator). The tensorator as a morphism of
presheaves of modules; naturality is a tmul-chase (all components are x ⊗ₜ y ↦ x ⊗ₜ y).
Equations
- PresheafOfModules.restrictScalarsLaxμ ψ P Q = { app := fun (U : Cᵒᵖ) => PresheafOfModules.restrictScalarsLaxμApp ψ P Q U, naturality := ⋯ }
Instances For
[D-PresPB′-general], leaf B1a. Presheaf-level restriction of scalars along an
arbitrary morphism of CommRingCat-valued ring presheaves is lax monoidal (sectionwise
x ⊗ₜ y ↦ x ⊗ₜ y; no iso hypothesis).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pushforward, spelled as its definitional factorization pushforward₀ ⋙ restrictScalars (the spelling at which both factors carry their lax monoidal structures
natively — mathlib's pushforward₀OfCommRingCat.Monoidal and our
restrictScalarsLaxMonoidal). Componentwise-identity isomorphic to pushforward φ.
Equations
Instances For
The comparison of the pushforward with its factored spelling (componentwise the identity).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The comparison with the factored pushforward is the identity natural
isomorphism after unfolding the definition of pushforward.
[D-PresPB′-general], leaf B1 (lax structure on the factored pushforward).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The comparison to the factored pushforward is the identity on elements.
The transported pullback–pushforward adjunction, against the factored spelling of the
pushforward (at which the lax monoidal structure lives natively). All doctrinal structure
maps of pullbackOplaxMonoidal are homEquiv-images under this adjunction.
Equations
Instances For
Transporting the pullback--pushforward adjunction along the componentwise identity factored comparison recovers the original adjunction.
The unit of the transported adjunction agrees elementwise with the unit of the original pullback–pushforward adjunction (the comparison is componentwise the identity).
[D-PresPB′-general], leaves B1+B2 (data form). The oplax monoidal structure on the
presheaf pullback along an arbitrary morphism of CommRingCat-derived ring presheaves:
doctrinal adjunction (Adjunction.leftAdjointOplaxMonoidal) applied to the transported
adjunction. Its δ_{P,Q} : f^*ᵖ(P⊗Q) ⟶ f^*ᵖP ⊗ f^*ᵖQ is the comparison map whose
invertibility is the remaining content (leaves G1/G3).
Equations
Instances For
The unit comparison of the factored pushforward is the ring comparison φ on
elements (the pushforward₀ unit is the identity and the restrictScalars one is
φ.app itself).
The tensorator of the factored pushforward is x ⊗ₜ y ↦ x ⊗ₜ y on elements (the
pushforward₀ tensorator is the identity and the restrictScalars one is
mapOfCompatibleSMul).
After applying the factored pushforward, the doctrinal pullback tensor comparison sends the adjunction-unit image of a pure tensor to the pure tensor of the two adjunction-unit images.
At an object mapped by the site functor, the doctrinal pullback tensor comparison sends the adjunction-unit image of a pure tensor to the pure tensor of the two unit images.
After module sheafification, the doctrinal presheaf-pullback tensor comparison sends the sheafification-unit image of an adjunction-unit pure tensor to the sheafification-unit image of the pure tensor of the two unit images.
[D-PresPB′-general], leaves B1+B2 (fused milestone). The presheaf pullback along an
arbitrary ring comparison carries an oplax monoidal structure: transport the
pullback–pushforward adjunction to the factored spelling of the pushforward
(Adjunction.ofNatIsoRight along the componentwise-identity iso), where the lax structure
lives natively, and apply doctrinal adjunction (Adjunction.leftAdjointOplaxMonoidal).
Its δ_{P,Q} : f^*ᵖ(P⊗Q) ⟶ f^*ᵖP ⊗ f^*ᵖQ is the comparison map whose sheafified
invertibility is the remaining content (leaves G1/G3).
The meet equivalence of hom-types in a meet-semilattice category (all four types are subsingletons).
Equations
- One or more equations did not get rendered due to their size.
Instances For
[D-PresPB′-general], leaf G1 (meet half). On the Opens-site, the pointwise product of
two representables is represented by the meet: Hom(V,U₁) × Hom(V,U₂) ≅ Hom(V, U₁ ⊓ U₂).
Equations
- PresheafOfModules.yonedaMeetIso U₁ U₂ = CategoryTheory.NatIso.ofComponents (fun (V : X.Opensᵒᵖ) => (PresheafOfModules.meetHomEquiv U₁ U₂ (Opposite.unop V)).toIso) ⋯
Instances For
The pointwise component of the free–tensor comparison, hint-typed at the presheaf
carriers (finsuppTensorFinsupp'; both directions send generators to generators).
Equations
- PresheafOfModules.freeTensorμ T F G V = (finsuppTensorFinsupp' (↑((T.comp (CategoryTheory.forget₂ CommRingCat RingCat)).obj V)) (F.obj V) (G.obj V)).toModuleIso
Instances For
The free presheaf's restriction on generators: freeMk x ↦ freeMk (F.map f x).
Elementwise form of the tensor product of morphisms of presheaves of modules.
The free presheaf functor on morphisms, on generators:
(free R).map g sends freeMk x to freeMk (g.app x).
ModuleCat.free_hom_ext, restated at the presheaf-of-modules clothing of the free
objects (the mathlib form's (ModuleCat.free R).obj-spelling reframes goals and poisons
kabstract; the defeq crossing happens once, here, at elaboration).
The types-level pairing (x, y) ↦ freeMk x ⊗ₜ freeMk y, the adjunct of the free–tensor
comparison. Naturality is an elementwise Types-square.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The free–tensor comparison out of the free presheaf, by the universal property
(naturality supplied by freeObjDesc).
Equations
Instances For
The free–tensor comparison agrees componentwise with the pointwise
finsuppTensorFinsupp' isomorphism (both send generators to generators).
[D-PresPB′-general], leaf G1-NAT (data form). The free presheaf of modules functor
is monoidal on tensor products: free(F ⊗ G) ≅ free(F) ⊗ free(G), with hom sending the
generator freeMk (x, y) to freeMk x ⊗ₜ freeMk y (see freeTensorDesc_app /
freeTensorμ_inv_freeMk).
Equations
Instances For
[D-PresPB′-general], leaf G1-NAT (closed via the adjunction route). The pointwise
components freeTensorμ assemble: free(F) ⊗ free(G) ≅ free(F ⊗ G). The comparison is
freeTensorDesc (naturality from the universal property); each component agrees with
(freeTensorμ).inv on generators, hence is an isomorphism; isomorphy reflects along
toPresheaf.
[D-PresPB′-general], leaf G1 (the lattice miracle). On the Opens-site of a scheme, the
presheaf tensor of two free-yoneda presheaves of modules is the free-yoneda of the meet:
pointwise, Hom(V,U₁) × Hom(V,U₂) = [V ≤ U₁ ⊓ U₂] (a meet-semilattice has representable
products of representables), and the free-module functor sends products of types to tensor
products of free modules (finsuppTensorFinsupp-style). Together with mathlib's
freeFunctorCompPullbackIso this makes the oplax comparison δ an isomorphism on free-yoneda
pairs — before sheafifying.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The types-level collapse of the terminal representable: every section maps to 1.
The adjunct of the unit–free-yoneda comparison.
Equations
- PresheafOfModules.unitDescPair = { app := fun (V : X.Opensᵒᵖ) => TypeCat.ofHom fun (x : (CategoryTheory.yoneda.obj ⊤).obj V) => 1, naturality := ⋯ }
Instances For
The unit–free-yoneda comparison on the terminal open, by the universal property.
Instances For
The monoidal unit is the free-yoneda module on the terminal open: sections of the
structure presheaf are the free rank-1 module on Hom(V, ⊤) = {*}.
Instances For
[D-PresPB′-general], leaf G1 (the lattice miracle, existence form).
[D-PresPB′-general], leaf G1 (the lattice miracle). On the Opens-site of a scheme, the
presheaf tensor of two free-yoneda presheaves of modules is the free-yoneda of the meet:
pointwise, Hom(V,U₁) × Hom(V,U₂) = [V ≤ U₁ ⊓ U₂] (a meet-semilattice has representable
products of representables), and the free-module functor sends products of types to tensor
products of free modules (finsuppTensorFinsupp-style). Together with mathlib's
freeFunctorCompPullbackIso this makes the oplax comparison δ an isomorphism on free-yoneda
pairs — before sheafifying.
[D-PresPB′-general], leaf G3-EXT. A natural transformation that is an isomorphism on the objects of a diagram is an isomorphism at any colimit point of the diagram, provided both functors preserve the colimit: the component at the point is the induced comparison of colimits of isomorphic diagrams.
[D-PresPB′-general], leaf G3-TC (right half). Tensoring with a fixed presheaf of
modules preserves colimits (pointwise: evaluation jointly reflects, evaluation preserves,
and ModuleCat tensoring is a left adjoint by monoidal-closedness).
[D-PresPB′-general], leaf G3-TC (left half). Symmetric to the right half, by the braiding.
Size-u packaging of preservesColimitsOfShape_tensorRight.
Size-u packaging of preservesColimitsOfShape_tensorLeft.
[D-PresPB′-general], corepresentability workhorse. The presheaf pullback of a
free-yoneda module is the free-yoneda module of the image object: both corepresent the
functor M ↦ ((push M).obj X ≃ M.obj (F X)), by the adjunction and by mathlib's
pushforwardCompCoyonedaFreeYonedaCorepresentableBy respectively.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Characterization of pullbackFreeYonedaIso: postcomposition with a map g out of the
corepresenting free-yoneda corresponds, under the adjunction, to the generator image of
g viewed in the pushforward. This is the compute rule for the [G3-pre] δ-chase.
Evaluation form of freeYonedaEquiv: the value of a map out of a free-yoneda module is
its value on the generator freeMk (𝟙 X).
Generator evaluation of the corepresentability equivalence: the transposed morphism, evaluated on the upstairs generator, is the generator image of the original morphism.
The adjunction unit at a free-yoneda module, through the corepresentability of the
pullback: the homEquiv-transposed inverse of pullbackFreeYonedaIso. This is the compute
rule for units in the [G3-pre]/[G3-η] generator chases.
The free presheaf's restriction on generators, over an arbitrary RingCat-valued
ring presheaf.
Evaluation of a morphism out of a free-yoneda module on an arbitrary generator
freeMk h: the restriction of its generator image along h. The one compute rule for
both sides of the [G3-pre] δ-chase.
The generator image of the adjunction unit at a free-yoneda module is the generator image of the corepresentability comparison.
Full evaluation of the transported adjunction unit at a free-yoneda module on an
arbitrary generator: the restriction along h of the corepresentability comparison's
generator image.
The reusable presentation-extension core: a natural transformation out of the category of presheaves of modules over a small site that is invertible on free-yoneda modules is invertible everywhere, provided both functors preserve colimits (coproduct layer over the elements, then the cokernel-cofork layer of the canonical presentation).
The doctrinal tensor comparison in the first variable, as a natural transformation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The doctrinal tensor comparison in the second variable, as a natural transformation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
[D-PresPB′-general], leaf G3 (generic extension). If the doctrinal tensor
comparison of the presheaf pullback is invertible on free-yoneda pairs, it is invertible
on all pairs: extend along the canonical free-yoneda presentation in each variable in
turn, using that both sides are compositions of colimit-preserving functors
(pullback is a left adjoint; tensoring preserves colimits pointwise).
The comparison morphism of RingCat-valued structure presheaves induced by a scheme
morphism f : Y ⟶ X, spelled at the CommRingCat-derived clothing
X.sheaf.obj ⋙ forget₂ CommRingCat RingCat ⟶ (Opens.map f.base).op ⋙ (Y.sheaf.obj ⋙ …)
at which the presheaf-of-modules monoidal structures are found by instance search on both
sides of the pullback.
Equations
Instances For
Generator evaluation of the lattice-miracle isomorphism: the inverse sends the
generator of freeY (U₁ ⊓ U₂) to the tensor of the two restricted generators.
[D-PresPB′-general], leaf G3-η. The unit comparison
η : f^*ᵖ(𝒪_X) ⟶ 𝒪_Y of the doctrinal oplax structure on the presheaf pullback of a
scheme morphism is an isomorphism before sheafification: the presheaf unit is the
free-yoneda on the terminal open ⊤, f⁻¹(⊤) = ⊤, and maps out of a pulled-back
free-yoneda are computed by one generator (pullbackFreeYonedaIso).
[D-PresPB′-general], leaf G3-pre (δ on free-yoneda pairs). The tensor comparison
δ : f^*ᵖ(P ⊗ Q) ⟶ f^*ᵖP ⊗ f^*ᵖQ of the doctrinal oplax structure on the presheaf
pullback of a scheme morphism is an isomorphism on free-yoneda pairs, before
sheafification: both sides are the free-yoneda on f⁻¹(U₁ ⊓ U₂) = f⁻¹U₁ ⊓ f⁻¹U₂
(the lattice miracle freeYonedaTensorIso upstairs and downstairs +
pullbackFreeYonedaIso), and δ matches the canonical isomorphism on the one
generator that determines it.
[D-PresPB′-general], leaf G3 (scheme form, all pairs). The doctrinal tensor
comparison of the presheaf pullback of a scheme morphism is an isomorphism on all pairs:
the free-yoneda base case is the lattice miracle (isIso_pullback_δ_freeYoneda), extended
along the canonical presentation by isIso_pullback_δ_of_freeYoneda.
[D-PresPB′-general], leaf A (presheaf-level payoff): the presheaf pullback of a
scheme morphism is a monoidal functor — f^*ᵖ(P ⊗ Q) ≅ f^*ᵖP ⊗ f^*ᵖQ and
f^*ᵖ(𝒪_X) ≅ 𝒪_Y, before sheafification: the doctrinal oplax structure has invertible
structure maps ([G3-pre] + [G3-η] + the presentation extension).
Equations
Instances For
[D-PresPB′-general], leaf A (descent). If the presheaf-level pullback along φ₀ is
monoidal, then the sheaf-level pullback is monoidal for the localized monoidal structures:
functorMonoidalOfComp along the sheafification localization, with the lifting supplied by
mathlib's sheafificationCompPullback.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sheaf-level pullback monoidal structure exists.
Sheafifying the underlying presheaf of a sheaf of modules returns that sheaf. This small
comparison is selectively retained from AINTLIB's Picard/InvertibleSheaf.lean; none of that
file's cover-local invertibility API is needed by the Picard pullback construction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of the canonical comparison from sheafification of the underlying presheaf to a sheaf is the sheafification-adjunction unit on sections.
The canonical presentation of sheaf pullback as sheafified presheaf pullback sends the pullback-adjunction unit of a section to the sheafification-unit image of the corresponding presheaf-pullback-adjunction unit.
The comparison between pullback after sheafification and sheafification after presheaf pullback sends the unit of the first composite adjunction to the unit of the second, on elements.
[D-PresPB′-general], payoff packaging (leaves G3 + A). The pullback of sheaves of
modules along an arbitrary morphism of schemes is a monoidal functor for the (v10.97)
localized-monoidal structures: the objectwise content is the general-f sheafified
pullback–tensor comparison (nonempty_sheafify_presheafPullback_tensor, extended from the
free-yoneda generators by two single-variable presentation passes in the abelian
SheafOfModules), packaged through functorMonoidalOfComp with the Lifting instance
sheafificationCompPullback. Consumer: Skeleton.monoidHom then gives
Pic(f) : Pic X →* Pic Y — the GME (2.16) Picard functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
[PIC-P1b-MONO], leaf D-PresPB′ (general f), relocated from
PullbackTensorMonoidal and closed (respelled at the CommRingCat-derived clothing of
this file; the original ringCatSheaf-spelled statement is definitionally the same). The
presheaf pullback commutes with the presheaf tensor after sheafification — in fact
already before sheafification (PresheafOfModules.pullbackMonoidal): apply the
sheafification to the (inverse of the) tensorator of the monoidal presheaf pullback.
The Picard functor on morphisms (GME 2.2.2 (2.16), p. 108): pullback of invertible
sheaves along f : Y ⟶ X induces a group homomorphism Pic X →* Pic Y — the underlying
monoidal functor is Modules.pullback f (nonempty_pullback_monoidal), inducing a monoid
homomorphism on the skeleton of iso-classes and hence a group homomorphism on units.
Equations
Instances For
The Picard functor preserves identities.
Value form of the Picard functor: the underlying iso-class map is the skeleton map of the pullback.
The skeleton maps of pullbacks compose (pure skeleton statement — no Picard group, no choice of monoidal structures).