Projective flags of periodic complexes #
A cyclic cochain complex K has a projective flag when it admits a finite filtration
0 = F₀ ⊆ F₁ ⊆ ⋯ ⊆ Fₘ = K by subcomplexes, split in every degree, whose subquotients have
projective terms and zero differential. Choosing the degreewise splittings writes each term as
Kⁱ = P₁ⁱ ⊕ ⋯ ⊕ Pₘⁱ with a strictly triangular differential. We record the filtration one
step at a time: a complex with a projective flag is either zero, or a degreewise split extension
of a complex with a projective quotient carrying zero differential by a complex that already has
a projective flag (HasProjectiveFlag).
Projective flags are the periodic analogue of the free flags of Avramov, Buchweitz and Iyengar.
Every complex with a projective flag is homotopically projective
(HasProjectiveFlag.isHomotopicallyProjective): the layers with zero differential are
homotopically projective, and homotopically projective complexes are closed under degreewise split
extensions. Its terms are projective (HasProjectiveFlag.projective_X), but projectivity of the
terms does not suffice: the dual-number differential module of
TauCeti.Algebra.Homology.Periodic.Examples has a free term but no projective flag. Mapping
cones of maps from complexes with projective terms and zero differential into complexes with a
projective flag again have a projective flag (HasProjectiveFlag.homotopyCofiber).
No positive-period assumption is needed. At period zero, when ZMod 0 is integer indexing, the
filtration describes bounded-length iterated extensions of complexes of projectives with zero
differential.
Main definitions #
TauCeti.PeriodicComplex.HasProjectiveFlag: the complex has a finite projective flag.
Main results #
TauCeti.PeriodicComplex.HasProjectiveFlag.isHomotopicallyProjective: a complex with a projective flag is homotopically projective.TauCeti.PeriodicComplex.HasProjectiveFlag.projective_X: its terms are projective.TauCeti.PeriodicComplex.HasProjectiveFlag.homotopyCofiber: mapping cones of maps from projective complexes with zero differential preserve projective flags.
References #
- Luchezar L. Avramov, Ragnar-Olaf Buchweitz and Srikanth Iyengar, Class and rank of differential modules, Inventiones Mathematicae 169 (2007), 1–35, Section 2.
- T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.
A cyclic cochain complex has a projective flag when it is obtained from zero by finitely
many extensions, each split in every degree, by complexes with projective terms and zero
differential. The successive extensions form a finite filtration 0 = F₀ ⊆ ⋯ ⊆ Fₘ = K by
subcomplexes, split in every degree, whose subquotients have projective terms and zero
differential.
- of_isZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{n : ℕ}
[CategoryTheory.Preadditive C]
{K : CochainComplex C (ZMod n)}
(hK : CategoryTheory.Limits.IsZero K)
: HasProjectiveFlag K
A zero complex has the empty projective flag.
- extension
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{n : ℕ}
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex (CochainComplex C (ZMod n)))
(hS : ∀ (i : ZMod n), Nonempty (S.map (HomologicalComplex.eval C (ComplexShape.up (ZMod n)) i)).Splitting)
(h₁ : HasProjectiveFlag S.X₁)
[∀ (i : ZMod n), CategoryTheory.Projective (S.X₃.X i)]
(hd : ∀ (i j : ZMod n), S.X₃.d i j = 0)
: HasProjectiveFlag S.X₂
Extending a complex with a projective flag, degreewise split, by a complex with projective terms and zero differential gives a complex with a projective flag.
Instances For
Having a projective flag is invariant under isomorphism of complexes.
A complex with projective terms and zero differential has a projective flag of length one.
The mapping cone of a map from a complex with projective terms and zero differential to a complex with a projective flag has a projective flag.
The terms of a complex with a projective flag are projective.
A complex with a projective flag is homotopically projective: every map from it to an acyclic complex is null-homotopic.