Countable dimension of the Γ-algebra #
The descent to the complex numbers of Deligne's Proposition 4.5
consumes a ℂ-point of the Γ-algebra of the universal algebra, and the
countable Nullstellensatz
(RS.exists_algHom_of_countable_dimension) supplies one as soon as
the even component has at most countable dimension. This file
establishes that dimension count for the algebras built by the
tensor-product device of Deligne 2.11 over a countable index family.
The route is the compactness of the unit in the ind-completion. The
big tensor product of a family of algebras is, by construction, the
filtered colimit of the finite sub-tensor-products
(RS.bigTensor), and a morphism out of the unit into a filtered
colimit factors through a stage
(RS.exists_factor_of_unit_hom_colimit). So the even component
𝟙 ⟶ bigTensor B is the union of the images of the even components
of the stages; over a countable index family there are only countably
many stages, and a countable union of subspaces of at most countable
dimension has at most countable dimension.
The finite stages are the tensor words of the family, and they are
handled by the same one-variable colimit lemma. Call an object of
the ind-completion countably presented (RS.CountablyPresented)
when it is a countable filtered colimit of embedded objects — the
precise sense of "built from countably much data". Tensoring
preserves the colimits of the ind-completion, and the embedding is
monoidal, so a countably presented factor of a tensor word can be
absorbed one stage at a time
(RS.rank_hom_unit_tensor_presented), leaving tensor words against
an embedded object; those are finite dimensional by finite length
(RS.finiteDimensional_hom_unit). Induction along the word
(RS.rank_hom_unit_listTensor_le_aleph0) needs no product of index
categories.
Two hypotheses are carried explicitly, because the ambient linear
structure on the ind-completion is itself a hypothesis of this
development and neither follows from it: ℂ-linearity of the
embedding C ⥤ Ind C (RS.IndOfLinear), and finite length of every
object of C.
The conclusion is packaged three ways: as a dimension count for the
common extension of a countable family
(RS.exists_common_algebra_rank_le_aleph0_of_presented), as the same
count for the universal algebra of Deligne 2.11 over countable index
families (RS.exists_universal_algebra_rank_le_aleph0), and, through
the countable Nullstellensatz, as a ℂ-point of the Γ-algebra
(RS.nonempty_superPoint_gammaAlgebra).
A countable union of small subspaces is small #
Pure linear algebra: a module covered by countably many subspaces of at most countable dimension has at most countable dimension. Choose a basis of each piece; the union of the bases is a countable spanning set.
A countable union of subspaces of countable dimension has countable dimension: the union of chosen bases of the pieces is a countable spanning set.
Countable filtered colimits in the ind-completion #
The unit of the ind-completion is compact: a morphism out of it into a filtered colimit factors through a stage. So the even component of a filtered colimit is the union of the images of the even components of the stages, and over a countable diagram the previous section applies.
A countable filtered colimit of objects with countable even
component again has countable even component. Compactness of the
unit (RS.exists_factor_of_unit_hom_colimit) covers 𝟙 ⟶ colimit D
by the countably many images of the 𝟙 ⟶ D.obj i.
The big tensor product over a countable index family #
The big tensor product is the filtered colimit of its finite sub-tensor-products, indexed by the finite subsets of the index family. Over a countable family there are only countably many of those, so the even component is of at most countable dimension as soon as each finite stage is.
The big tensor product of a countable family has countable
even component, provided each finite sub-tensor-product does: the
stages are indexed by Finset J, which is countable.
The finite stages are the tensor words of the family: a bound on every word bounds every stage.
Transport along isomorphisms #
Isomorphic objects have isomorphic even components.
Countability of the even component is an isomorphism invariant.
The embedded objects #
For an embedded object the even component is the even component
downstairs, which finite length makes finite dimensional
(RS.finiteDimensional_hom_unit). The identification is ℂ-linear
only if the embedding is, which the hypothesised linear structure on
the ind-completion does not by itself provide; ℂ-linearity of the
embedding is therefore carried as an explicit hypothesis, in the
shape in which the induced structure of RS.linearOfScalarUnit
supplies it.
ℂ-linearity of the embedding C ⥤ Ind C, as a hypothesis on the
ambient linear structure of the ind-completion.
Equations
Instances For
Full faithfulness of the embedding, ℂ-linearly: for a ℂ-linear embedding the hom-modules downstairs and upstairs are the same ℂ-module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An embedded object of finite length has finite dimensional even
component, hence countable dimension: the even component is
𝟙_ C ⟶ W, which RS.finiteDimensional_hom_unit makes finite
dimensional.
Countably presented ind-objects #
An object of the ind-completion built from countably much data is a
countable filtered colimit of embedded objects. Such objects are
absorbed one at a time into a tensor word: tensoring preserves
filtered colimits of the ind-completion
(RS.tensorLeft_ind_preservesColimitsOfShape and its right-hand
version), so a tensor word against a countably
presented factor is again a countable filtered colimit, whose stages
are tensor words against an embedded factor — and the embedding is
monoidal (RS.indOfTensorIso), so those stages absorb the factor
into the base category. Iterating along the word never leaves the
one-variable colimit lemma, and no product of index categories is
needed.
An object of the ind-completion is countably presented when it is the colimit of a countable filtered diagram of embedded objects. This is the shape in which "built from countably much data" enters the dimension count of the Γ-algebra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Being countably presented is an isomorphism invariant.
Absorbing a countably presented factor. A tensor word Y
whose even component stays countable against every embedded factor
keeps that property after Y is enlarged by a countably presented
factor: the enlarged word against an embedded factor is a countable
filtered colimit of copies of the original word against an embedded
factor.
The tensor words of countably presented algebras have countable
even component. This is the finite-stage input of
RS.rank_hom_unit_bigTensor_le_aleph0, discharged.
The common extension of a countable family #
The tensor-product device of Deligne 2.11, with the dimension count carried along: a countable family of algebras whose tensor words have countable even component has a common extension with countable even component.
A countable family of nonzero algebras has a common nonzero
extension of countable even dimension: the tensor product of the
family, as in RS.exists_common_algebra, with the dimension count of
RS.rank_hom_unit_bigTensor_le_aleph0 added. The hypothesis is the
countability of the even component of every tensor word of the
family, which is the finite-stage input the colimit argument
consumes.
The common extension of a countable family of countably presented algebras has countable even component. The hypothesis is structural: each member of the family is a countable filtered colimit of embedded objects, which is what "built from countably much data" means for the algebras of Deligne 2.11.
The universal algebra over a countable family #
Deligne 2.11 with the dimension count carried along. The two
hypotheses are those of RS.exists_universal_algebra strengthened by
the requirement that the algebra chosen at each index be countably
presented; the index families are countable, so the universal algebra
— the tensor product of all the chosen algebras — has countable even
component.
The universal algebra over countable families has countable
even component: one nonzero algebra over which every object of the
family becomes a mixed sum and every chosen morphism acquires a
section, whose Γ-algebra is of at most countable dimension over ℂ.
The hypotheses are those of RS.exists_universal_algebra with the
chosen algebras required to be countably presented.
The Γ-algebra and its ℂ-point #
The even component of the Γ-algebra of a commutative monoid object is
its even component as computed above, so the dimension count is a
count of 𝟙 ⟶ R; and the countable Nullstellensatz turns it into a
ℂ-point of the Γ-algebra.
A super-commutative ℂ-algebra of at most countable dimension
has a ℂ-point. The odd-nil quotient is a nonzero commutative
ℂ-algebra of at most countable dimension, so
RS.exists_algHom_of_countable_dimension gives it a ℂ-algebra map to
ℂ, which pulls back to a point. This is the countable-dimension
replacement for the finite-type hypothesis of
RS.nonempty_superPoint.
The even component of the Γ-algebra has countable dimension whenever the even hom-module of the algebra does: the two are the same ℂ-module.
A ℂ-point of the Γ-algebra of an algebra with countable even component: the last step of the descent to the complex numbers, run over the countable-dimension Nullstellensatz. Nontriviality of the even ring is exactly the nonvanishing of the unit of the algebra.