Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.CompactlyGenerated.Coaisle

Coaisles of compactly generated t-structures #

The aisle of a compactly generated t-structure is the coproduct-and-extension closure of its generators, so the degree-one coaisle is the right orthogonal of that closure. A coproduct of objects of the coaisle is again right orthogonal to every generator, because a map from a compact generator into a coproduct is a finite sum of maps into the summands (IsCompactObject.exists_finite_sum), and right orthogonality to a fixed object passes from the generators to their closure by ObjectProperty.coprodClosure_le: being left orthogonal to a fixed object is closed under isomorphisms, colimits, and extensions, which are exactly that lemma's three hypotheses. Only the generator case is specific to this file.

Main results #

References #

source
theorem CategoryTheory.Triangulated.TStructure.IsCompactlyGeneratedBy.isGE_one_coproduct {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {G : ObjectProperty C} (h : t.IsCompactlyGeneratedBy G) {ι : Type} (X : ι → C) [Limits.HasCoproduct X] (hX : ∀ (i : ι), t.IsGE (X i) 1) :
t.IsGE (∐ X) 1

The degree-one coaisle of a compactly generated t-structure is closed under coproducts.

Degree one and not a general n because IsCompactlyGeneratedBy fixes the aisle at degree zero (le_zero_eq), so t.isGE_iff_orthogonal 0 1 is the pair that matches it; it is also the degree the recognition formula (A.8) uses, through Slicing.IndExtensions.isGE_one_iff_ltProp. The index universe is Type 0 because IsCompactObject.exists_finite_sum is, and that lemma is pinned there by the DirectSum bridge in its proof; generalizing this one means generalizing that one first.