Brown approximation towers for compact generators

This file proves the constructive part of Theorem A.13 of arXiv:2607.28411v1. For a universe-zero small property G of compact objects, the Brown tower starts with the coproduct of all maps from generators to the target. At each successor stage it attaches a coproduct of shifted generators which kills the kernel on Hom. Compactness identifies Hom into the mapping telescope with the sequential direct limit, producing the universal approximation map required by the aisle constructor.

The universe hypotheses are explicit. ObjectProperty.Small.{0} G says that the generators form a set, LocallySmall.{0} C makes the Hom sets available as universe-zero indices, and HasCoproducts.{0} C supplies exactly the coproducts used by the construction.

structure CategoryTheory.Triangulated.TStructure.GeneratorApproximationMap {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (G : ObjectProperty C) (A : C) : Type (max u v)

A universal approximation map tested only on the chosen generators.

For U = Coprod(G), generator-level Hom control is enough: completing the map to a triangle first proves that its cone is right orthogonal to G, and coproduct/extension closure then upgrades that orthogonality to all of Coprod(G).

• left : C

  The approximating object.

• left_mem : G.coprodClosure self.left

  The approximating object lies in Coprod(G).

• hom : self.left ⟶ A

  The universal approximation morphism.

• hom_surjective (Z : C) (hZ : G Z) : Function.Surjective fun (f : Z ⟶ self.left) => CategoryStruct.comp f self.hom

  Hom into the target is surjective on generators.

• shift_hom_injective (Z : C) (hZ : G Z) : Function.Injective fun (f : Z ⟶ (shiftFunctor C 1).obj self.left) => CategoryStruct.comp f ((shiftFunctor C 1).map self.hom)

  Shifted Hom into the target is injective on generators.

theorem CategoryTheory.Triangulated.TStructure.GeneratorApproximationMap.exists_triangle {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} {A : C} (a : GeneratorApproximationMap G A) : ∃ (Y : C) (_ : G.coprodClosure.rightOrthogonal Y) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj a.left), Pretriangulated.Triangle.mk a.hom g h ∈ Pretriangulated.distinguishedTriangles

The cone of a generator approximation is right orthogonal to the whole coproduct-and-extension closure of the generators.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation.ofGeneratorApproximationMaps {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} (hG : G ≤ G.shift 1) (happrox : ∀ (A : C), Nonempty (GeneratorApproximationMap G A)) : CompactGeneratorApproximation G

Generator-level universal maps are enough to construct the compactly generated approximation triangles of Theorem A.13.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.GeneratorIndex {C : Type u} [Category.{v, u} C] (G : ObjectProperty C) [ObjectProperty.Small.{0, v, u} G] : Type

A universe-zero indexing type for the chosen generators.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.GeneratorIndex G = Shrink.{0, ?u.1} (Subtype G)

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.generator {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] (i : GeneratorIndex G) : C

The generator represented by a small generator index.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.generator i = ↑((equivShrink (Subtype G)).symm i)

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.generator_mem {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] (i : GeneratorIndex G) : G (generator i)

Every small generator index represents an object satisfying G.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.EvaluationIndex {C : Type u} [Category.{v, u} C] [LocallySmall.{0, v, u} C] (G : ObjectProperty C) [ObjectProperty.Small.{0, v, u} G] (A : C) : Type

The universe-zero index of all maps from generators to A.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.evaluationSource {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] (A : C) (i : EvaluationIndex G A) : C

The generator underlying an evaluation summand.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.evaluationSource A i = CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.generator i.fst

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.evaluationMap {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] (A : C) (i : EvaluationIndex G A) : evaluationSource A i ⟶ A

The map to A represented by an evaluation summand.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.evaluationMap A i = (equivShrink (CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.generator i.fst ⟶ A)).symm i.snd

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialObject {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : C

The initial Brown approximation: the coproduct of every map from a generator to the target.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialObject A = ∐ CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.evaluationSource A

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialHom {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : initialObject A ⟶ A

The evaluation morphism from the initial Brown approximation.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialHom A = CategoryTheory.Limits.Sigma.desc (CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.evaluationMap A)

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialObject_mem {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : G.coprodClosure (initialObject A)

The initial Brown object belongs to Coprod(G).

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialHom_surjective {C : Type u} [Category.{v, u} C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A Z : C) (hZ : G Z) : Function.Surjective fun (f : Z ⟶ initialObject A) => CategoryStruct.comp f (initialHom A)

Every map from a generator to A factors through the initial evaluation morphism.

structure CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.Stage {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (G : ObjectProperty C) (A : C) : Type (max u v)

One stage of the Brown approximation tower.

• obj : C

  The stage object.

• mem : G.coprodClosure self.obj

  Every stage is built from coproducts and extensions of generators.

• hom : self.obj ⟶ A

  The stage approximation map.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialStage {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : Stage G A

The initial Brown stage.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.KernelIndex {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] {A : C} (s : Stage G A) : Type

The universe-zero index of the shifted-generator maps in the kernel of a stage approximation.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelSource {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] {A : C} (s : Stage G A) (i : KernelIndex s) : C

The shifted generator underlying a kernel summand.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelMap {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] {A : C} (s : Stage G A) (i : KernelIndex s) : kernelSource s i ⟶ s.obj

The kernel morphism represented by a kernel summand.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : C

The coproduct of all shifted-generator kernel maps.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelObject s = ∐ CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelSource s

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelHom {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : kernelObject s ⟶ s.obj

The universal kernel map into a Brown stage.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelHom s = CategoryTheory.Limits.Sigma.desc (CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelMap s)

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelHom_comp_stageHom {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : CategoryStruct.comp (kernelHom s) s.hom = 0

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelHom_comp_stageHom_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (kernelHom s) (CategoryStruct.comp s.hom h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.kernelObject_shift_mem {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : G.coprodClosure ((shiftFunctor C 1).obj (kernelObject s))

Shifting the kernel coproduct forward by one puts it in Coprod(G): its summands become the original generators.

structure CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.StepData {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : Type (max u v)

The successor data attached to a Brown stage.

• next : Stage G A

  The successor stage.

• transition : s.obj ⟶ self.next.obj

  The transition to the successor stage.

• connecting : self.next.obj ⟶ (shiftFunctor C 1).obj (kernelObject s)

  The third morphism in the attachment triangle.

• distinguished : Pretriangulated.Triangle.mk (kernelHom s) self.transition self.connecting ∈ Pretriangulated.distinguishedTriangles

  The attachment is a distinguished triangle.

• transition_hom : CategoryStruct.comp self.transition self.next.hom = s.hom

  The successor map extends the current approximation map.

• kills (Z : C) (hZ : G Z) (f : (shiftFunctor C (-1)).obj Z ⟶ s.obj) (hf : CategoryStruct.comp f s.hom = 0) : CategoryStruct.comp f self.transition = 0

  Every shifted-generator kernel map is killed at the successor.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.stepData_nonempty {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : Nonempty (StepData s)

The successor attachment data exist for every Brown stage.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.step {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] {A : C} (s : Stage G A) : StepData s

Attach all shifted-generator kernel maps to produce the next Brown stage.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.step s = Classical.choice ⋯

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tower {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : ℕ → Stage G A

The recursively constructed Brown stages.

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tower A 0 = CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.initialStage A

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.towerTransition {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) (n : ℕ) : (tower A n).obj ⟶ (tower A (n + 1)).obj

The transition morphisms in the Brown tower.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.towerTransition_comp_hom {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) (n : ℕ) : CategoryStruct.comp (towerTransition A n) (tower A (n + 1)).hom = (tower A n).hom

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.towerTransition_comp_hom_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) (n : ℕ) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (towerTransition A n) (CategoryStruct.comp (tower A (n + 1)).hom h) = CategoryStruct.comp (tower A n).hom h

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.towerTransition_kills {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A Z : C) (hZ : G Z) (n : ℕ) (f : (shiftFunctor C (-1)).obj Z ⟶ (tower A n).obj) (hf : CategoryStruct.comp f (tower A n).hom = 0) : CategoryStruct.comp f (towerTransition A n) = 0

At stage n + 1, the tower kills every shifted-generator map in the kernel of the stage-n approximation.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.towerObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) (n : ℕ) : C

The sequence of objects underlying the Brown tower.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.towerObject A n = (CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tower A n).obj

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.telescope {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : MappingTelescope.Data (towerObject A) (towerTransition A)

The chosen mapping telescope of the Brown tower.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.limitHom {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) : (telescope A).obj ⟶ A

The universal morphism from the Brown telescope to the target.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.limitHom A = Classical.choose ⋯

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.inclusion_comp_limitHom {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) (n : ℕ) : CategoryStruct.comp ((telescope A).inclusion n) (limitHom A) = (tower A n).hom

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.inclusion_comp_limitHom_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A : C) (n : ℕ) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp ((telescope A).inclusion n) (CategoryStruct.comp (limitHom A) h) = CategoryStruct.comp (tower A n).hom h

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.telescope_mem {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (A : C) : G.coprodClosure (telescope A).obj

The Brown telescope belongs to Coprod(G).

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.limitHom_surjective {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (A Z : C) (hZ : G Z) : Function.Surjective fun (f : Z ⟶ (telescope A).obj) => CategoryStruct.comp f (limitHom A)

The Brown telescope map is surjective on Hom from every generator.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.limitHom_shift_injective {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hcompact : G ≤ ObjectProperty.compactObjects) (A Z : C) (hZ : G Z) : Function.Injective fun (f : Z ⟶ (shiftFunctor C 1).obj (telescope A).obj) => CategoryStruct.comp f ((shiftFunctor C 1).map (limitHom A))

The Brown telescope map is injective on shifted Hom from every generator.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.generatorApproximationMap {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (hcompact : G ≤ ObjectProperty.compactObjects) (A : C) : GeneratorApproximationMap G A

The universal generator approximation produced by the Brown tower.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.compactGeneratorApproximation {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (hcompact : G ≤ ObjectProperty.compactObjects) : CompactGeneratorApproximation G

The constructive Brown-representability output required by Theorem A.13.

noncomputable def CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tStructure {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (hcompact : G ≤ ObjectProperty.compactObjects) : TStructure C

The compactly generated t-structure constructed from the Brown tower.

Equations

• CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tStructure hG hcompact = ⋯.tStructure

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tStructure_isCompactlyGeneratedBy {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (hcompact : G ≤ ObjectProperty.compactObjects) : (tStructure hG hcompact).IsCompactlyGeneratedBy G

The Brown t-structure is compactly generated by G.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tStructure_le_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (hcompact : G ≤ ObjectProperty.compactObjects) : (tStructure hG hcompact).le 0 = G.coprodClosure

Formula (A.2), nonpositive half: the Brown aisle is Coprod(G).

@[simp]

theorem CategoryTheory.Triangulated.TStructure.CompactGeneratorBrown.tStructure_ge_one {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G : ObjectProperty C} [ObjectProperty.Small.{0, v, u} G] [LocallySmall.{0, v, u} C] [Limits.HasCoproducts C] (hG : G ≤ G.shift 1) (hcompact : G ≤ ObjectProperty.compactObjects) : (tStructure hG hcompact).ge 1 = G.coprodClosure.rightOrthogonal

Formula (A.2), degree-one half: the Brown coaisle is the right orthogonal of Coprod(G).