Associativity of the geometric convolution: the quadruple product #
#542 split associativity of convolution into a free transform-level theorem
and a supplied kernel-level layer (ConvolutionAssocData), and recorded that
the geometric route to the latter runs through the quadruple product. This
file is that route: geometricConvolutionAssoc derives the kernel-level
isomorphism
(P ∗ Q) ∗ R ≅ P ∗ (Q ∗ R)
for convKernel, by comparing both bracketings with a common
quadKernel = Rρ₁₄_*(ρ₁₂^*P ⊗ ρ₂₃^*Q ⊗ ρ₃₄^*R) on a supplied quadruple
product, and geometricConvolutionAssocData assembles a genuine
ConvolutionAssocData for the geometric convolution data with zero
supplied fields.
What is consumed #
Almost everything is an existing class at new instance sites — the same
seven-input vocabulary as geometricCompIso, evaluated at objects rather
than whiskered as functors: two HasFlatBaseChange squares, one
HasProjectionFormula and one HasProjectionFormulaRight (again at
different morphisms, which is again why they are separate classes), two
HasMonoidalDerivedPullback roots, and HasCoherentDerivedTensor. The
tensorator and associator used here therefore belong to structures that also
state their associativity, unitality, pentagon, and triangle laws.
Two classes are new, because no existing shape covers a one-step route:
HasPullbackFactorization π p r—p^* ⋙ π^* ≅ r^*for a triangleπ ≫ p = r. Not an instance ofHasCommonPullbackRoute: that compares two two-step routes, and degenerating one leg to an identity would drag in a pullback-along-identity input plus unitor transport for every use. (Conversely a common route is two factorizations glued; the route classes are left as they are because #540 already consumes them in that form.)HasPushforwardFactorization π q r— the pushforward companion.
Each factorization carries its triangle identity as a comm guard, not
consumed by the derivation, in the pattern of the route classes.
What this file does not assert #
- Nothing constructs an instance of any class here, new or old, and no
scheme is shown to admit one.
QuadrupleProductGeometrycarries the quadruple object and its projections as data and does not assert that anything is a product; the guards state the intended instantiation. - This file does not assemble the geometric construction into abstract
CoherentConvolutionData; that requires functoriality ofconvKernelon kernel morphisms and comparison of the geometric associator/unitors with the coherent root. The tensor and pullback inputs themselves are coherent.
Derived pullback along a factorization, supplied.
For a commuting triangle π ≫ p = r, the two-step pullback agrees with the
one-step pullback. The equation is a guard: the derivation consumes iso
alone, and comm is what makes it the right isomorphism to ask for.
Deliberately not expressed through HasCommonPullbackRoute: that class
compares two two-step routes, and using it with an identity leg would demand
a pullback-along-identity input plus unitor transport at every use site.
The triangle commutes. A guard, not consumed.
- iso : (Families.SchemeBaseChange.boundedCoherentDerivedPullback p).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback π) ≅ Families.SchemeBaseChange.boundedCoherentDerivedPullback r
The two-step pullback is the one-step pullback.
Instances
Derived pushforward along a factorization, supplied.
The pushforward companion of HasPullbackFactorization; guard as there.
The triangle commutes. A guard, not consumed.
The two-step pushforward is the one-step pushforward.
Instances
The quadruple product and its projections, supplied.
quad plays X₁ ×_S X₂ ×_S X₃ ×_S X₄; the ρs play its projections onto
the four pairwise products the associativity statement mentions, and the
σs its projections onto the four triple products carried by the given
TripleProductGeometrys.
Carried as data, like TripleProductGeometry, and for the same reason:
nothing here consumes an assertion that any object is a product. The
commuting triangles relating σs, the triples' projections, and the ρs
live as guards on the factorization-class instances a caller supplies.
- quad : Families.SchemeBaseChange S
The quadruple product
X₁ ×_S X₂ ×_S X₃ ×_S X₄. Projection to
X₁ ×_S X₂.Projection to
X₂ ×_S X₃.Projection to
X₃ ×_S X₄.Projection to
X₁ ×_S X₄, along whichquadKernelis pushed.Projection to
X₁ ×_S X₂ ×_S X₃.Projection to
X₂ ×_S X₃ ×_S X₄.Projection to
X₁ ×_S X₃ ×_S X₄.Projection to
X₁ ×_S X₂ ×_S X₄.
Instances For
The quadruple kernel Rρ₁₄_*(ρ₃₄^*R ⊗ (ρ₂₃^*Q ⊗ ρ₁₂^*P)), the common
value both bracketings of the convolution are compared with. Slot convention
as in convKernel: the outer kernel occupies the first bifunctor slot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left bracketing meets the quadruple kernel. Five steps: flat base
change across the (πXW, πXY) square, the projection formula at σ₁₃₄, and
three factorizations, with the pullback of the inner convolution computed by
HasMonoidalDerivedPullback at σ₁₂₃. Every step is an isomorphism between
objects of Dᵇ(Coh Z₁₄), obtained by evaluating a class isomorphism at an
object and transporting with mapIso — no whiskering.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right bracketing meets the quadruple kernel. Six steps this time:
the extra one is the associator from HasCoherentDerivedTensor — the convolved kernel sits in the
twist slot on this side, so after base change, the right-slot projection
formula at σ₁₂₄, and the factorizations, the tensors arrive bracketed the
other way and associativity of the derived tensor is what reconciles them.
This is the consumption site #542 promised that class.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Associativity of the geometric convolution, derived.
(P ∗ Q) ∗ R ≅ P ∗ (Q ∗ R) for convKernel, through the quadruple kernel.
The two comparisons consume disjoint instance packs except for the shared
factorizations onto the ρs; nothing constructs any of the inputs, so this
moves the trust boundary of kernel-level associativity from "the isomorphism
exists" to the named classical isomorphisms on the quadruple product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The geometric convolution associativity data, assembled — with no supplied fields.
A ConvolutionAssocData for the four geometric convolution data, with
assocIso the derived geometricConvolutionAssoc. Together with #542's
convolutionTransformAssoc this closes the associativity layer: the
transform level was free, the kernel level is now derived, and what is
supplied is the quadruple-product geometry with its named classical
isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Where the associativity layer now stands #
At the transform level associativity is a theorem for any convolution data
(#542). At the kernel level it is now derived for the geometric convolution
from the quadruple-product inputs above. What remains supplied is exactly
those inputs. The abstract CoherentConvolutionData root states the pentagon
and triangle; this geometric file has not yet promoted convKernel to that
functorial root, so it deliberately exports only the derived three-kernel
comparison.