From a countable family to a complex point of the splitting algebra #
The descent of the argument of Deligne §2.11 to the complex numbers is a chain of five steps, and this file runs it end to end for a countable family of objects and of morphisms of the small category.
This is a route to the complex numbers, not the route
RS.deligne_theorem takes: that one splits a single object and
passes to a simple quotient
(RS/Classical/Deligne/SplitEverything.lean), which reaches ℂ
without a countability restriction on the family. What the
assembly consumes from this module is RS.fibreFreeIso, the fibre
of a mixed object as a free super module.
- The splitting algebra. The tensor-product device of Deligne 2.11 produces, out of local mixedness for each object of the family and a splitting for each morphism, one nonzero commutative algebra of the ind-completion realising all of them at once.
- Countable presentation. The witnessing algebras of the input are
arbitrary;
RS.locallyMixed_countablyPresentedandRS.section_countablyPresentedreplace each of them by a countably presented one. The compactness they ask for is available because the family is indexed by objects of the small category (RS.indCompactObj_indOf). - The dimension count. Over countable index families the algebra
assembled from countably presented constituents has even component
of at most countable dimension:
RS.exists_universal_algebra_rank_le_aleph0. This is the same assembly as step 1, carrying the count, so the two steps are run together rather than one after the other; the ℂ-linearity of the embedding that the count consumes is discharged for the structures installed from a scalar unit byRS.indOfLinear_of_scalarUnit. - The point. The countable Nullstellensatz turns that count into a
ℂ-point of the Γ-algebra:
RS.nonempty_superPoint_gammaAlgebra. - The fibre. At such a point the fibre of an object of the family
is a finite-dimensional super vector space, of dimension exactly the
pair
(p | q)of the mixed sum it becomes over the algebra; this isRS.Classical.Deligne.PointBaseChangeapplied throughRS.fibreMixIso.
Contents #
RS.exists_superPoint_of_countable_family— the chain, steps 1 to 4: the splitting algebra together with a complex point of its Γ-algebra.RS.fibreFreeIso— the fibre of a mixed object, as a free super module.RS.finrank_fibre_tensor_point_evenandRS.finrank_fibre_tensor_point_odd— the two dimensions of the fibre at a point, with their finite-dimensionality.RS.exists_superVect_fibre— the fibre, packaged as anRS.SuperVectof dimension(p | q).RS.exists_superPoint_fibre_of_countable_family— the whole chain, steps 1 to 5.
The chain to a complex point #
From a countable family of objects to split to a complex point. Given a countable family of objects of the small category, each locally mixed after the embedding, and a countable family of morphisms of embedded objects, each split after base change to some nonzero commutative algebra, there is a single nonzero commutative algebra of the ind-completion over which every object of the family becomes a mixed sum and every morphism of the family acquires a section, and whose Γ-algebra has a ℂ-point.
The finite-length hypothesis is what makes the constituents of the
assembled algebra countably presented; the countability of the two
index families is what keeps the assembled algebra of countable
dimension; and the linear structures are the ones installed from the
scalar unit ψ, for which the ℂ-linearity of the embedding is
automatic.
The fibre at a complex point #
The fibre of a mixed object is a free super module. An object
that becomes the mixed sum L.mix p q after base change to the algebra
has for its fibre the free super module of rank (p | q): apply the
realization functor to the isomorphism of free modules, then
RS.fibreMixIso.
Equations
- RS.fibreFreeIso L 𝔸 e = (RS.gammaModuleFunctor L 𝔸).mapIso e ≪≫ RS.fibreMixIso L 𝔸 p q
Instances For
The even part of the fibre at a point is finite dimensional.
The odd part of the fibre at a point is finite dimensional.
The even dimension of the fibre at a point is p.
The odd dimension of the fibre at a point is q.
The fibre at a point, as a super vector space of dimension
(p | q). The packaging is RS.toSuperVect, whose components are
coordinate spaces of the two dimensions just computed.
The whole chain #
From a countable family of objects to split to a fibre functor
valued in finite-dimensional super vector spaces. The algebra and
the point of RS.exists_superPoint_of_countable_family, with the fibre
of each object of the family recorded as a super vector space of the
dimension pair its mixed sum prescribes.
Acceptance #
The intended instantiation takes for J the pairs of natural numbers,
indexing the mixed powers of a ⊗-generator. The index families are
asked to live in the same universe as the objects of the small
category, so the concrete family is ULift.{v} (ℕ × ℕ), which is
countable; there are no morphisms to split.