Countable descent for the witnessing algebras

The dimension count of RS.Classical.Deligne.GammaCountable asks each constituent algebra of the universal algebra of Deligne 2.11 to be countably presented (RS.CountablyPresented): a countable filtered colimit of embedded objects. An algebra witnessing local mixedness or a splitting is to be replaced by a countably presented one, and this file assembles the two devices such a replacement runs on: the countable tower generated inside an algebra by one stage of its presentation, and the compactness of the objects that carry the finite data to be pushed down that tower.

The tower. Every ind-object is a filtered colimit of embedded objects (Ind.presentation), the stage maps being RS.presStage, and compactness of the embedded objects factors any map out of one of them through a stage (RS.exists_presStage_factor). Starting from a stage of the presentation of an algebra, rung n + 1 of the tower is chosen above rung n and above a stage absorbing the square of rung n. The colimit RS.stageSubalgebra of the tower is then countably presented (RS.countablyPresented_stageSubalgebra), maps to the algebra (RS.stageSubalgebraHom), contains the unit (RS.exists_unit_stageSubalgebra) and is closed under multiplication one rung at a time (RS.stageRungMul_comp_hom).

The tower inside the algebra. The ind-completion of a small abelian category is abelian, so each rung may be replaced by its image in the algebra (RS.stageImage). The rung maps are then monomorphisms, and so is the map RS.imageSubalgebraHom of the resulting colimit RS.imageSubalgebra into the algebra (RS.mono_imageSubalgebraHom): a map out of an embedded object into the colimit factors through a rung, and monomorphisms of ind-objects are detected on the embedded objects (RS.mono_of_hom_indOf_injective). Countable presentation of the image tower is RS.countablyPresented_imageSubalgebra, over the hypothesis RS.IndImageEmbedded that images of embedded objects are embedded.

The compactness. The data to be pushed down is carried by mixed sums of the unit and the odd line. The unit is compact because it is embedded; the odd line is compact because its square is the unit, which makes tensoring with it an equivalence and so turns a map out of it into a point of a translate — this is RS.oddUntwist, and it gives both halves of the compactness formula, RS.exists_factor_of_sq_unit_hom_colimit and RS.factor_eq_of_sq_unit_hom_colimit. Mixed sums are finite biproducts of the two, and a finite family of stages of a filtered diagram is dominated by a single stage, whence RS.exists_factor_of_mix_hom_colimit.

Towers of embedded objects

An ℕ-shaped diagram is filtered and countable, so the colimit of a tower of embedded objects is countably presented. The index category has to live in the ambient universe, whence the AsSmall wrapper.

@[reducible, inline]

abbrev RS.Tower : Type v

The index category of a tower: the natural numbers, transported into the ambient universe.

Equations

• RS.Tower = CategoryTheory.AsSmall ℕ

instance RS.countable_tower : Countable Tower

noncomputable def RS.towerDiagram {C : Type v} [CategoryTheory.SmallCategory C] {Y : ℕ → C} (u : (n : ℕ) → Y n ⟶ Y (n + 1)) : CategoryTheory.Functor Tower C

The diagram of a tower of objects of C.

Equations

• RS.towerDiagram u = CategoryTheory.AsSmall.down.comp (CategoryTheory.Functor.ofSequence u)

theorem RS.countablyPresented_colimit_tower {C : Type v} [CategoryTheory.SmallCategory C] {Y : ℕ → C} (u : (n : ℕ) → Y n ⟶ Y (n + 1)) : CountablyPresented (CategoryTheory.Limits.colimit ((towerDiagram u).comp indOf))

The colimit of a tower of embedded objects is countably presented. This is the shape in which countable presentation is produced below: no bookkeeping beyond the tower itself.

The stages of a presentation

Mathlib's Ind.presentation exhibits every ind-object as a filtered colimit of embedded objects. The maps of the stages into the ind-object are RS.presStage, and compactness of the embedded objects (RS.exists_factor_of_hom_colimit) factors any map out of an embedded object through one of them.

@[reducible, inline]

noncomputable abbrev RS.presDiagram {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Functor A.presentation.I (CategoryTheory.Ind C)

The diagram of embedded objects presenting an ind-object.

Equations

• RS.presDiagram A = A.presentation.F.comp RS.indOf

noncomputable def RS.presStage {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : indOf.obj (A.presentation.F.obj i) ⟶ A

The structural map of a stage of the chosen presentation into the ind-object it presents.

Equations

• RS.presStage A i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (RS.presDiagram A) i) A.colimitPresentationCompYoneda.hom

theorem RS.presStage_naturality {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) {i j : A.presentation.I} (α : i ⟶ j) : CategoryTheory.CategoryStruct.comp (indOf.map (A.presentation.F.map α)) (presStage A j) = presStage A i

The structural maps are compatible with the transition maps of the presentation.

theorem RS.exists_presStage_factor {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) {Y : C} (f : indOf.obj Y ⟶ A) : ∃ (i : A.presentation.I) (g : Y ⟶ A.presentation.F.obj i), CategoryTheory.CategoryStruct.comp (indOf.map g) (presStage A i) = f

A map out of an embedded object factors through a stage of the presentation: this is compactness of the embedded objects.

theorem RS.exists_presStage_point {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ A) : ∃ (i : A.presentation.I) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj (A.presentation.F.obj i)), CategoryTheory.CategoryStruct.comp e (presStage A i) = f

A point of an ind-object factors through a stage.

The subalgebra generated by a stage

Rung n + 1 of the tower is chosen above rung n and above a stage of the presentation absorbing the square of rung n. The colimit of the tower is therefore countably presented, maps to the algebra, and is closed under multiplication one rung at a time.

noncomputable def RS.stageMulToAlg {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : indOf.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (A.presentation.F.obj i) (A.presentation.F.obj i)) ⟶ A

The square of a stage of the presentation, multiplied into the algebra.

Equations

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

noncomputable def RS.mulStage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : A.presentation.I

A stage of the presentation absorbing the square of the given stage.

Equations

• RS.mulStage A i = ⋯.choose

noncomputable def RS.mulStageMap {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : CategoryTheory.MonoidalCategoryStruct.tensorObj (A.presentation.F.obj i) (A.presentation.F.obj i) ⟶ A.presentation.F.obj (mulStage A i)

The multiplication of a stage with itself, landing in the absorbing stage.

Equations

• RS.mulStageMap A i = ⋯.choose

theorem RS.indOfTensorIso_stageMulToAlg {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : CategoryTheory.CategoryStruct.comp (indOfTensorIso (A.presentation.F.obj i) (A.presentation.F.obj i)).hom (stageMulToAlg A i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (presStage A i) (presStage A i)) CategoryTheory.MonObj.mul

The comparison of the embedding with the tensor product turns the square of a stage into the product of its two structural maps.

theorem RS.mulStageMap_spec {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : CategoryTheory.CategoryStruct.comp (indOf.map (mulStageMap A i)) (presStage A (mulStage A i)) = stageMulToAlg A i

noncomputable def RS.nextStage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : A.presentation.I

The next rung: a stage above the given one and above the stage absorbing its square.

Equations

• RS.nextStage A i = CategoryTheory.IsFiltered.max i (RS.mulStage A i)

noncomputable def RS.stageStep {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : i ⟶ nextStage A i

The transition map of the tower, at the level of the index category of the presentation.

Equations

• RS.stageStep A i = CategoryTheory.IsFiltered.leftToMax i (RS.mulStage A i)

noncomputable def RS.stageMul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : CategoryTheory.MonoidalCategoryStruct.tensorObj (A.presentation.F.obj i) (A.presentation.F.obj i) ⟶ A.presentation.F.obj (nextStage A i)

The multiplication of a stage with itself, landing in the next rung.

Equations

• RS.stageMul A i = CategoryTheory.CategoryStruct.comp (RS.mulStageMap A i) (A.presentation.F.map (CategoryTheory.IsFiltered.rightToMax i (RS.mulStage A i)))

theorem RS.stageMul_spec {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : CategoryTheory.CategoryStruct.comp (indOf.map (stageMul A i)) (presStage A (nextStage A i)) = stageMulToAlg A i

noncomputable def RS.towerIdx {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : ℕ → A.presentation.I

The stages of the generated tower.

Equations

• RS.towerIdx A i₀ 0 = i₀
• RS.towerIdx A i₀ n.succ = RS.nextStage A (RS.towerIdx A i₀ n)

@[reducible]

noncomputable def RS.towerObj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : C

The rungs of the generated tower, as objects of C.

Equations

• RS.towerObj A i₀ n = A.presentation.F.obj (RS.towerIdx A i₀ n)

noncomputable def RS.towerStep {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : towerObj A i₀ n ⟶ towerObj A i₀ (n + 1)

The transition maps of the generated tower.

Equations

• RS.towerStep A i₀ n = A.presentation.F.map (RS.stageStep A (RS.towerIdx A i₀ n))

noncomputable def RS.towerSeq {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : CategoryTheory.Functor ℕ (CategoryTheory.Ind C)

The tower as a diagram of ind-objects.

Equations

• RS.towerSeq A i₀ = (CategoryTheory.Functor.ofSequence (RS.towerStep A i₀)).comp RS.indOf

noncomputable def RS.towerNatTrans {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : towerSeq A i₀ ⟶ (CategoryTheory.Functor.const ℕ).obj A

The cocone of the tower under the algebra.

Equations

• RS.towerNatTrans A i₀ = CategoryTheory.NatTrans.ofSequence (fun (n : ℕ) => RS.presStage A (RS.towerIdx A i₀ n)) ⋯

noncomputable def RS.stageSubalgebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : CategoryTheory.Ind C

The subalgebra generated by a stage: the colimit of the tower. It is not known to be a subobject of the algebra — see the module documentation — but it is countably presented, it maps to the algebra, it contains the unit and it is closed under multiplication rung by rung.

Equations

• RS.stageSubalgebra A i₀ = CategoryTheory.Limits.colimit ((RS.towerDiagram (RS.towerStep A i₀)).comp RS.indOf)

theorem RS.countablyPresented_stageSubalgebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : CountablyPresented (stageSubalgebra A i₀)

The generated tower is countably presented.

noncomputable def RS.stageSubalgebraHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : stageSubalgebra A i₀ ⟶ A

The map of the generated tower into the algebra.

Equations

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

noncomputable def RS.stageRung {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : indOf.obj (towerObj A i₀ n) ⟶ stageSubalgebra A i₀

The rungs of the generated tower map into it.

Equations

• RS.stageRung A i₀ n = CategoryTheory.Limits.colimit.ι ((RS.towerDiagram (RS.towerStep A i₀)).comp RS.indOf) { down := n }

@[simp]

theorem RS.stageRung_comp_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : CategoryTheory.CategoryStruct.comp (stageRung A i₀ n) (stageSubalgebraHom A i₀) = presStage A (towerIdx A i₀ n)

noncomputable def RS.stageRungMul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj (towerObj A i₀ n)) (indOf.obj (towerObj A i₀ n)) ⟶ stageSubalgebra A i₀

The multiplication of a rung of the generated tower with itself, landing in the next rung.

Equations

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

theorem RS.stageRungMul_comp_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : CategoryTheory.CategoryStruct.comp (stageRungMul A i₀ n) (stageSubalgebraHom A i₀) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (presStage A (towerIdx A i₀ n)) (presStage A (towerIdx A i₀ n))) CategoryTheory.MonObj.mul

The generated tower is closed under multiplication, rung by rung: the product of a rung with itself, taken in the algebra, factors through the tower.

The unit rung

Generating the tower at a stage through which the unit of the algebra factors puts the unit into the tower.

noncomputable def RS.unitStage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] : A.presentation.I

A stage of the presentation through which the unit factors.

Equations

• RS.unitStage A = ⋯.choose

noncomputable def RS.unitStagePoint {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj (A.presentation.F.obj (unitStage A))

The unit, read at the stage that absorbs it.

Equations

• RS.unitStagePoint A = ⋯.choose

theorem RS.unitStagePoint_spec {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] : CategoryTheory.CategoryStruct.comp (unitStagePoint A) (presStage A (unitStage A)) = CategoryTheory.MonObj.one

theorem RS.exists_unit_stageSubalgebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] : ∃ (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ stageSubalgebra A (unitStage A)), CategoryTheory.CategoryStruct.comp e (stageSubalgebraHom A (unitStage A)) = CategoryTheory.MonObj.one

The tower generated at the unit stage contains the unit.

The image tower

The ind-completion of a small abelian category is abelian, so a map into an ind-object has an image, and the rungs of the generated tower can be replaced by their images in the algebra. The rung maps then become monomorphisms, and so does the map of the resulting colimit into the algebra: a map out of an embedded object into the colimit factors through a rung, and monomorphisms of ind-objects are detected on the embedded objects.

theorem RS.mono_of_hom_indOf_injective {C : Type v} [CategoryTheory.SmallCategory C] {Y Z : CategoryTheory.Ind C} (f : Y ⟶ Z) (h : ∀ (W : C) (u v : indOf.obj W ⟶ Y), CategoryTheory.CategoryStruct.comp u f = CategoryTheory.CategoryStruct.comp v f → u = v) : CategoryTheory.Mono f

Monomorphisms are detected on the embedded objects: a map of ind-objects along which maps out of embedded objects cancel is a monomorphism. Every ind-object is a filtered colimit of embedded objects, so a pair of maps into the source is determined by its restrictions to embedded objects.

noncomputable def RS.stageImage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : CategoryTheory.Ind C

The image in the ind-object of a stage of its presentation.

Equations

• RS.stageImage A i = CategoryTheory.Limits.image (RS.presStage A i)

noncomputable def RS.stageImageι {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : stageImage A i ⟶ A

The image of a stage, as a subobject of the ind-object.

Equations

• RS.stageImageι A i = CategoryTheory.Limits.image.ι (RS.presStage A i)

instance RS.mono_stageImageι {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : CategoryTheory.Mono (stageImageι A i)

noncomputable def RS.stageToImage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : indOf.obj (A.presentation.F.obj i) ⟶ stageImage A i

The stage maps through its image.

Equations

• RS.stageToImage A i = CategoryTheory.Limits.factorThruImage (RS.presStage A i)

instance RS.epi_stageToImage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : CategoryTheory.Epi (stageToImage A i)

@[simp]

theorem RS.stageToImage_comp_ι {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : CategoryTheory.CategoryStruct.comp (stageToImage A i) (stageImageι A i) = presStage A i

noncomputable def RS.stageImageMap {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) {i j : A.presentation.I} (α : i ⟶ j) : stageImage A i ⟶ stageImage A j

A transition map of the presentation includes one image into the next.

Equations

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

@[simp]

theorem RS.stageImageMap_comp_ι {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) {i j : A.presentation.I} (α : i ⟶ j) : CategoryTheory.CategoryStruct.comp (stageImageMap A α) (stageImageι A j) = stageImageι A i

noncomputable def RS.imageRung {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : CategoryTheory.Ind C

The rungs of the image tower.

Equations

• RS.imageRung A i₀ n = RS.stageImage A (RS.towerIdx A i₀ n)

noncomputable def RS.imageRungStep {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : imageRung A i₀ n ⟶ imageRung A i₀ (n + 1)

The transition maps of the image tower.

Equations

• RS.imageRungStep A i₀ n = RS.stageImageMap A (RS.stageStep A (RS.towerIdx A i₀ n))

noncomputable def RS.imageSeq {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : CategoryTheory.Functor ℕ (CategoryTheory.Ind C)

The image tower as a diagram of ind-objects.

Equations

• RS.imageSeq A i₀ = CategoryTheory.Functor.ofSequence (RS.imageRungStep A i₀)

noncomputable def RS.imageSubalgebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : CategoryTheory.Ind C

The subalgebra generated by a stage, realised inside the algebra: the colimit of the tower of images.

Equations

• RS.imageSubalgebra A i₀ = CategoryTheory.Limits.colimit (CategoryTheory.AsSmall.down.comp (RS.imageSeq A i₀))

noncomputable def RS.imageNatTrans {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : imageSeq A i₀ ⟶ (CategoryTheory.Functor.const ℕ).obj A

The cocone of the image tower under the algebra.

Equations

• RS.imageNatTrans A i₀ = CategoryTheory.NatTrans.ofSequence (fun (n : ℕ) => RS.stageImageι A (RS.towerIdx A i₀ n)) ⋯

noncomputable def RS.imageSubalgebraHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : imageSubalgebra A i₀ ⟶ A

The map of the image tower into the algebra.

Equations

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

noncomputable def RS.imageRungι {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : imageRung A i₀ n ⟶ imageSubalgebra A i₀

The rungs of the image tower map into it.

Equations

• RS.imageRungι A i₀ n = CategoryTheory.Limits.colimit.ι (CategoryTheory.AsSmall.down.comp (RS.imageSeq A i₀)) { down := n }

@[simp]

theorem RS.imageRungι_comp_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (n : ℕ) : CategoryTheory.CategoryStruct.comp (imageRungι A i₀ n) (imageSubalgebraHom A i₀) = stageImageι A (towerIdx A i₀ n)

theorem RS.mono_imageSubalgebraHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) : CategoryTheory.Mono (imageSubalgebraHom A i₀)

The image tower is a subobject of the algebra. A map out of an embedded object into the colimit factors through a rung, two such factorisations are merged at a later rung, and the rung maps into the algebra are monomorphisms.

Countable presentation of the image tower

The rungs of the image tower are images of embedded objects, and the tower is countable, so the tower is countably presented as soon as those images are again embedded. That is a condition on C alone — RS.IndImageEmbedded — and it is not a consequence of abelianness: for C the finitely presented modules over a coherent ring, the image of R ⟶ R ⧸ I is R ⧸ I, which is embedded only when I is finitely generated. It does hold as soon as the subobject orders of C satisfy the ascending chain condition, which the finite length hypothesis of RS.Classical.Deligne.GammaCountable supplies.

def RS.IndImageEmbedded (C : Type v) [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] : Prop

Embedded images: the image in the ind-completion of a map out of an embedded object is again embedded.

Equations

• RS.IndImageEmbedded C = ∀ (Y : C) (Z : CategoryTheory.Ind C) (f : RS.indOf.obj Y ⟶ Z), ∃ (W : C), Nonempty (CategoryTheory.Limits.image f ≅ RS.indOf.obj W)

theorem RS.countablyPresented_imageSubalgebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (h : IndImageEmbedded C) : CountablyPresented (imageSubalgebra A i₀)

The image tower is countably presented when the images of embedded objects are embedded: the tower is an ℕ-tower, and each rung is by hypothesis an embedded object.

Compactness of the odd line and of the mixed sums

The isomorphism witnessing local mixedness is a map out of a mixed sum of the unit and the odd line, so pushing it down to a stage needs those objects to be compact. The unit is compact because it is embedded (RS.exists_factor_of_unit_hom_colimit); the odd line is compact because its square is the unit, which makes tensoring with it an equivalence and so turns a map out of it into a point of a translate. The mixed sums are finite biproducts of the two, and a finite family of stages of a filtered diagram is dominated by a single stage.

def RS.oddUntwist {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {L : D} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) {W : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L W) : L ⟶ W

Untwisting: along a trivialisation of the square of L, a point of L ⊗ W becomes a map L ⟶ W.

Equations

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

theorem RS.oddUntwist_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {L : D} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) {W W' : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L W) (k : W ⟶ W') : oddUntwist e (CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L k)) = CategoryTheory.CategoryStruct.comp (oddUntwist e h) k

Untwisting is natural in the target.

def RS.oddZigzag {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {L : D} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) : L ≅ L

The zigzag automorphism of L attached to a trivialisation of its square: untwisting the twist of the identity.

Equations

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

theorem RS.oddUntwist_twist {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {L : D} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) {W : D} (g : L ⟶ W) : oddUntwist e (CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L g)) = CategoryTheory.CategoryStruct.comp (oddZigzag e).hom g

Untwisting undoes twisting, up to the zigzag automorphism.

theorem RS.exists_factor_of_sq_unit_hom_colimit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Ind C} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C)) {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (f : L ⟶ CategoryTheory.Limits.colimit D) : ∃ (i : I) (g : L ⟶ D.obj i), CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.colimit.ι D i) = f

An object whose square is the unit is compact: a map from it into a filtered colimit factors through a stage. Tensoring with the object preserves the colimit, and the unit is compact, so the translated point factors; untwisting brings the factorisation back.

theorem RS.oddTwist_comp {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Ind C} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C)) {Z Z' : CategoryTheory.Ind C} (x : L ⟶ Z) (y : Z ⟶ Z') : CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L (CategoryTheory.CategoryStruct.comp x y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L x)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L y)

Twisting a map out of an object with unit square into a point of a translate turns composition into whiskering.

theorem RS.factor_eq_of_sq_unit_hom_colimit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Ind C} (e : CategoryTheory.MonoidalCategoryStruct.tensorObj L L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C)) {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) {i j : I} (g₁ : L ⟶ D.obj i) (g₂ : L ⟶ D.obj j) (h : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.colimit.ι D i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.colimit.ι D j)) : ∃ (k : I) (α : i ⟶ k) (β : j ⟶ k), CategoryTheory.CategoryStruct.comp g₁ (D.map α) = CategoryTheory.CategoryStruct.comp g₂ (D.map β)

Merging of stage factorisations out of an object with unit square: two factorisations that agree after passing to a filtered colimit are merged by transition maps of the diagram. With the previous theorem this is the whole compactness formula for the odd line.

noncomputable def RS.mixFamily {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (p q : ℕ) : Fin p ⊕ Fin q → CategoryTheory.Ind C

The summands of a mixed sum.

Equations

• RS.mixFamily L p q i = Sum.elim (fun (x : Fin p) => CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C)) (fun (x : Fin q) => L.obj) i

theorem RS.exists_factor_of_mix_hom_colimit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (p q : ℕ) {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] (D : CategoryTheory.Functor I (CategoryTheory.Ind C)) (f : L.mix p q ⟶ CategoryTheory.Limits.colimit D) : ∃ (i : I) (g : L.mix p q ⟶ D.obj i), CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.colimit.ι D i) = f

The mixed sums are compact: a map from a mixed sum of the unit and the odd line into a filtered colimit factors through a stage. Each summand factors, and a finite family of stages of a filtered diagram is dominated by a single one.