The unit laws for the geometric convolution #
The third ledger (KernelUnit.lean) built the unit object — diagonalKernel
with its identity transform — and its closing note named the unit's
compatibility with convolution as absent. The abstract side now has the split
(Convolution.lean): transform-level unit laws are theorems, kernel-level
ConvolutionLeftUnitData/ConvolutionRightUnitData are supplied. This file
derives the kernel level for the geometric convolution:
geometricConvUnitLeft:convKernel G (diagonalKernel δ) Q ≅ QgeometricConvUnitRight:convKernel G' P (diagonalKernel δ') ≅ P
each through a supplied section τ of the relevant triple product playing
δ × 1 (resp. 1 × δ), and the two assembly definitions discharge the
abstract structures with zero supplied fields.
What is consumed #
Existing classes at new sites: one HasFlatBaseChange square per law, the
projection formula at τ — left slot for the left law, right slot
for the right law, the same slot separation as everywhere else in this lane —
the two retraction classes of KernelUnit.lean at τ (their second
consumption site), and one factorization-free identity: nothing.
The two legacy compatibility classes mirror each other:
HasUnitPullbackRightUnitor f— twisting by anything against the pulled unit is the identity:(− ⊗ f^*𝒪) ≅ 𝟭in the argument slot.HasUnitPullbackLeftUnitor f— the pulled unit twists trivially:(f^*𝒪 ⊗ −) ≅ 𝟭.
Stable consumers no longer assume either class. Both isomorphisms are derived
from one HasMonoidalDerivedPullback, whose strong-monoidal laws relate the
unit comparison to its tensorator and whose source and target
HasCoherentDerivedTensor roots own the triangle law.
What this file does not assert #
- Nothing constructs an instance of any class, new or old.
- No claim that
diagonalKernelis unique with these properties. Compatibility of the tensor associator and unitors is inherited from the coherent roots; proving the geometric convolution itself realizes that abstract pentagon and triangle still requires a functorial geometric convolution realization.
Compatibility record asserting that the pulled-back unit is a right unit.
(− ⊗ f^*𝒪) ≅ 𝟭 — as a statement about the flipped tensor evaluated at the
pulled unit. Classically f^*𝒪 ≅ 𝒪 and 𝒪 is a two-sided unit; here it is
one field, consumed exactly once, by the left unit law's final step.
New stable consumers use the value derived from
HasMonoidalDerivedPullback; this record remains for raw migration code.
- iso : (derivedTensor T).flip.obj ((Families.SchemeBaseChange.boundedCoherentDerivedPullback f).obj HasTensorUnit.unit) ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left T))
Tensoring against the pulled unit, in the argument slot, is trivial.
Instances
Compatibility record asserting that the pulled-back unit is a left unit.
The twist-slot mirror of HasUnitPullbackRightUnitor; same classical
content, consumed by the right unit law.
- iso : (derivedTensor T).obj ((Families.SchemeBaseChange.boundedCoherentDerivedPullback f).obj HasTensorUnit.unit) ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left T))
Twisting by the pulled unit is trivial.
Instances
Forget strong monoidality to the old right-unitor-only capability.
Forget strong monoidality to the old left-unitor-only capability.
The left unit law for the geometric convolution, derived.
convKernel G (diagonalKernel δ) Q ≅ Q, in five steps: flat base change
moves Rδ_* across πXY^* onto the section τ; the projection formula at
τ pulls the twist inside; the pullback retraction τ ≫ πYW = 𝟙 computes
the pulled twist as Q; the pulled unit is a right unit; and the pushforward
retraction τ ≫ πXW = 𝟙 finishes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right unit law for the geometric convolution, derived.
convKernel G P (diagonalKernel δ) ≅ P. The mirror of
geometricConvUnitLeft, with the unit kernel arriving in the twist slot:
base change acts inside the twist, the right-slot projection formula at
τ replaces the left one, the pullback retraction computes the pulled
argument as P, and the pulled unit acts as a left unit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The geometric left unit data, assembled — with no supplied fields.
A ConvolutionLeftUnitData for the geometric convolution datum of the
self-correspondence with (p, q), with unit kernel diagonalKernel δ and
leftUnitIso the derived geometricConvUnitLeft.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The geometric right unit data, assembled — with no supplied fields.
The mirror assembly, from geometricConvUnitRight.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit layer, closed #
With this file the unit side matches the associativity side: at the transform
level both laws are theorems (Convolution.lean); at the kernel level both
are derived for the geometric convolution; and what is supplied is the
diagonal/section geometry with its named classical isomorphisms. Tensor and
pullback coherence now come from the monoidal roots. Still absent is a proof
that the geometric convKernel construction assembles the abstract
CoherentConvolutionData, as well as DualKernel.