Deligne's growth and generation hypotheses in the doubling #
RS/Classical/Deligne/Doubling.lean builds the ℤ/2-graded
doubling Doubled A, the faithful summing functor
total : Doubled A ⥤ A, X ↦ X.even ⊞ X.odd along which the
monoidal structure is induced, and the even embedding
evenEmbed : A ⥤ Doubled A. This module transports two of
Deligne's hypotheses across that construction: moderate growth of
the lengths of tensor powers, and finite ⊗-generation.
Growth travels along the summing functor. It is monoidal, so its
comparison isomorphisms assemble by induction into
total.obj (Y ^ ⊗ N) ≅ (total.obj Y) ^ ⊗ N; and it reflects the
subobject order — the graded components of a monomorphism are
monomorphisms, a biproduct of monomorphisms is a monomorphism, and
a factorisation of the summed subobjects splits back into its
matrix entries. So a strictly increasing chain of subobjects
upstairs gives one of the same length downstairs, and the constants
that bound the growth of total.obj Y in A bound the growth of
Y in the doubling verbatim.
Generation travels along the diagonal embedding dbl,
M ↦ (M, M), which is additive and preserves monomorphisms and
epimorphisms. A super-object Y is a retract of
dbl (Y.even ⊞ Y.odd), so a subquotient presentation of
Y.even ⊞ Y.odd downstairs presents both graded components at
once. The generator taken upstairs is
gen X = (X ⊞ Xᘁ ⊞ 𝟙_ A, 𝟙_ A): the ambient generator, its dual
and the unit in even degree, the unit in odd degree. Its pure
tensor powers already contain the diagonal double of every mixed
power of X as a retract — read the word X, …, X, (𝟙, 𝟙), Xᘁ, …, Xᘁ off the letters of gen X, the diagonal letter
spreading an even word over both degrees. No dual is ever formed
in the doubling: the presentations produced here use mixed powers
with no dual factors at all.
The even component of a monomorphism of super-objects is a monomorphism: a morphism killed by it is the even component of a morphism killed by it.
The odd component of a monomorphism of super-objects is a monomorphism.
A morphism of super-objects with monomorphic components is a monomorphism: morphisms are compared componentwise.
A morphism of super-objects with epimorphic components is an epimorphism.
A biproduct of two monomorphisms is a monomorphism: a morphism killed by it is killed in each matrix entry.
The summing functor preserves monomorphisms: on components a monomorphism of super-objects is a pair of monomorphisms, and the biproduct of two monomorphisms is one.
The diagonal matrix entries of a factorisation of one biproduct of morphisms through another factor the two given morphisms.
A factorisation of the summed subobjects splits back into its diagonal matrix entries, which assemble into a factorisation of the subobjects themselves.
The summing functor reflects the subobject order.
Length in the doubling is length of the total object: a
strictly increasing chain of subobjects of Z maps to a strictly
increasing chain of subobjects of total.obj Z.
The summing functor carries the graded tensor powers of Y to
the ambient tensor powers of total.obj Y: the comparison
isomorphisms of the monoidal functor total, assembled by
induction on the exponent.
Equations
- One or more equations did not get rendered due to their size.
- Y.totalTensorPowIso 0 = RS.Doubled.epsIso.symm
Instances For
Y is a retract of Z: a section split by a retraction.
A retract is in particular a subquotient, and — unlike the
subquotient relation — the property is visibly stable under tensor
products, tensor powers and biproducts.
Equations
- RS.IsRetractOf Y Z = ∃ (s : Y ⟶ Z) (r : Z ⟶ Y), CategoryTheory.CategoryStruct.comp s r = CategoryTheory.CategoryStruct.id Y
Instances For
An isomorphism is a retraction.
Every object is a retract of itself.
Retractions compose.
A subquotient sandwiched between two retractions is a subquotient: a split monomorphism extends the inclusion and a split epimorphism extends the quotient map.
Retractions multiply.
Retractions raise to tensor powers.
Retractions assemble over a finite biproduct.
The diagonal embedding M ↦ (M, M): the ambient object placed
in both degrees at once.
Equations
- RS.Doubled.dbl = { obj := fun (M : A) => { even := M, odd := M }, map := fun {X Y : A} (f : X ⟶ Y) => RS.Doubled.homMk f f, map_id := ⋯, map_comp := ⋯ }
Instances For
The diagonal embedding is additive.
The diagonal embedding preserves subquotients: its components are the given morphisms, so monomorphisms and epimorphisms are preserved.
A retraction of super-objects from a pair of component retractions.
Every super-object is a retract of the diagonal double of the sum of its two components.
Tensoring an even object on the left multiplies both graded components: the mixed blocks vanish.
Equations
Instances For
Tensoring an even object on the right multiplies both graded components.
Equations
Instances For
Tensor powers of an even object are even.
Equations
- One or more equations did not get rendered due to their size.
- RS.Doubled.evenTensorPowIso Z 0 = CategoryTheory.Iso.refl (RS.tensorPow (RS.Doubled A) (RS.Doubled.evenEmbed.obj Z) 0)
Instances For
The generator of the doubling attached to a generator X of
A: the ambient generator, its dual and the unit in even degree,
the unit in odd degree. The odd component is what makes the odd
half of a super-object reachable; the dual and the unit in the even
component are what let the words of a mixed power be read off
without ever forming a dual in the doubling. It is reducible, so
that the component computations below see its two blocks.
Equations
- RS.Doubled.gen X = { even := X ⊞ Xᘁ ⊞ CategoryTheory.MonoidalCategoryStruct.tensorUnit A, odd := CategoryTheory.MonoidalCategoryStruct.tensorUnit A }
Instances For
The even copy of X is a retract of the generator.
The even copy of the dual of X is a retract of the
generator.
The diagonal double of the unit is a retract of the generator.
The word in the generator that reads off a mixed power: a
even copies of X, then the diagonal double of the unit, then b
even copies of the dual of X.
Equations
- One or more equations did not get rendered due to their size.
- RS.Doubled.genWord X a N.succ = CategoryTheory.MonoidalCategoryStruct.tensorObj (RS.Doubled.genWord X a N) (RS.Doubled.evenEmbed.obj Xᘁ)
Instances For
The word is the diagonal double of the mixed power: the diagonal factor spreads the even word over both degrees, and the remaining brackets are reassociated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The word is a retract of a tensor power of the generator: letter by letter.
The diagonal double of a mixed power of X is a retract of a
pure power of the generator — a mixed power of the generator with
no dual factors.
Moderate length growth passes to the doubling. The
constants bounding the growth of total.obj Y in A bound the
growth of Y in the doubling verbatim.
Tensor generation passes to the doubling. A super-object
is a retract of the diagonal double of the sum of its components,
that sum is a subquotient of a biproduct of mixed powers of X,
and the diagonal double of a mixed power of X is a retract of a
pure power of Doubled.gen X.