Compact generation and semiorthogonality

Compactness propagates Hom-vanishing from the summands of a coproduct to the coproduct itself. This file combines that fact with the universal property of ObjectProperty.coprodClosure to extend semiorthogonality through coproducts and extensions on both sides.

The indexing universe is kept explicit. This is the closure step needed for the perfect-to-quasicoherent passage in Proposition 3.15 of arXiv:1902.08184.

The last section lifts that step from a pair of properties to a whole semiorthogonal sequence: closing every component of a sequence of compact objects under coproducts and extensions leaves it semiorthogonal, and the closure's components are triangulated, replete, and coproduct-closed for free. Those three are exactly the hypotheses the base-change layer otherwise has to assume about its source sequence.

theorem CategoryTheory.ObjectProperty.triangEnvelope_le_rightOrthogonal_triangEnvelope {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P Q : ObjectProperty C) [Q.IsStableUnderShift ℤ] (h : Q ≤ P.rightOrthogonal) : Q.triangEnvelope ≤ P.triangEnvelope.rightOrthogonal

Semiorthogonality of two shift-stable generating properties extends to their triangulated envelopes.

theorem CategoryTheory.ObjectProperty.shiftClosure_triangEnvelope_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.Nonempty] [IsTriangulated C] : (P.shiftClosure ℤ).triangEnvelope = P.triangEnvelope

Adding all shifts before taking the triangulated envelope does not change the result.

theorem CategoryTheory.IsCompactObject.singletonRightOrthogonalIsClosedUnderColimitsOfShape {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : IsCompactObject K) (ι : Type w) : (ObjectProperty.singleton K).rightOrthogonal.IsClosedUnderColimitsOfShape (Discrete ι)

The right orthogonal to one compact object is closed under coproducts in the compactness universe.

theorem CategoryTheory.IsCompactObject.leftOrthogonal_coprodClosure {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {K : C} (hK : IsCompactObject K) {P : ObjectProperty C} (h : P.leftOrthogonal K) : P.coprodClosure.leftOrthogonal K

A compact object left-orthogonal to the generators remains left-orthogonal to their coproduct-and-extension closure.

theorem CategoryTheory.ObjectProperty.coprodClosure_le_leftOrthogonal_coprodClosure {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (hcompact : P ≤ compactObjects) (horth : P ≤ Q.leftOrthogonal) : P.coprodClosure ≤ Q.coprodClosure.leftOrthogonal

If every generator in P is compact and P is left-orthogonal to Q, then the two coproduct-and-extension closures remain left-orthogonal.

theorem CategoryTheory.ObjectProperty.coprodClosure_le_rightOrthogonal_coprodClosure {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (hcompact : P ≤ compactObjects) (horth : Q ≤ P.rightOrthogonal) : Q.coprodClosure ≤ P.coprodClosure.rightOrthogonal

Right-orthogonal form of coprodClosure_le_leftOrthogonal_coprodClosure, matching the orientation of SemiorthogonalSequence.semiorthogonal.

def CategoryTheory.Triangulated.SemiorthogonalSequence.coprodClosure {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type u₁} [Preorder ι] (S : SemiorthogonalSequence C ι) (hcompact : ∀ (i : ι), S.component i ≤ ObjectProperty.compactObjects) : SemiorthogonalSequence C ι

Close every component of a semiorthogonal sequence under coproducts and extensions.

Semiorthogonality survives because compactness carries Hom-vanishing across a coproduct. Only the earlier component's compactness is used at each pair; the hypothesis is stated uniformly because that is how a compact-generator sequence arrives.

Equations

• S.coprodClosure hcompact = { component := fun (i : ι) => (S.component i).coprodClosure, semiorthogonal := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.coprodClosure_component {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type u₁} [Preorder ι] (S : SemiorthogonalSequence C ι) (hcompact : ∀ (i : ι), S.component i ≤ ObjectProperty.compactObjects) (i : ι) : (S.coprodClosure hcompact).component i = (S.component i).coprodClosure

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.le_coprodClosure_component {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type u₁} [Preorder ι] (S : SemiorthogonalSequence C ι) (hcompact : ∀ (i : ι), S.component i ≤ ObjectProperty.compactObjects) (i : ι) : S.component i ≤ (S.coprodClosure hcompact).component i

Every component sits inside its own closure. This is Definition 3.3 compatibility for the identity functor, stated without the vocabulary so that this file keeps its narrow import.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.coprodClosure_hasTriangulatedComponents {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type u₁} [Preorder ι] (S : SemiorthogonalSequence C ι) (hcompact : ∀ (i : ι), S.component i ≤ ObjectProperty.compactObjects) (hS : S.HasTriangulatedComponents) : (S.coprodClosure hcompact).HasTriangulatedComponents

Closure preserves triangulatedness of the components.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.coprodClosure_isClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type u₁} [Preorder ι] (S : SemiorthogonalSequence C ι) (hcompact : ∀ (i : ι), S.component i ≤ ObjectProperty.compactObjects) (i : ι) : ((S.coprodClosure hcompact).component i).IsClosedUnderIsomorphisms

The closed components are closed under isomorphisms, with no hypothesis on the sequence.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.coprodClosure_isClosedUnderColimitsOfShape {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type u₁} [Preorder ι] (S : SemiorthogonalSequence C ι) (hcompact : ∀ (i : ι), S.component i ≤ ObjectProperty.compactObjects) (i : ι) (κ : Type w) : ((S.coprodClosure hcompact).component i).IsClosedUnderColimitsOfShape (Discrete κ)

The closed components are closed under coproducts in the closure universe, with no hypothesis on the sequence.