Closing the countable descent

RS.Classical.Deligne.CountableDescent builds, inside a commutative algebra A of Ind C and above a stage of its presentation, the countable tower RS.imageSubalgebra and the monomorphism RS.imageSubalgebraHom of that tower into the algebra; RS.Classical.Deligne.ImageSubalgebra makes the tower an algebra in its own right. This file uses that replacement to push the two witnessing statements of Deligne 2.9 and 2.10 down to countably presented algebras: RS.locallyMixed_countablyPresented and RS.section_countablyPresented.

The data. An algebra witnessing local mixedness carries an isomorphism of free modules, and one witnessing a splitting carries a section. Neither is a datum of the ambient category, so the free--forgetful adjunction (RS.freeModHomEquiv) is used first to transpose them: an isomorphism freeMod A X ≅ freeMod A (L.mix p q) becomes a pair of morphisms X ⟶ A ⊗ L.mix p q and L.mix p q ⟶ A ⊗ X subject to two unit identities (RS.roundTrip_of_freeModIso), and a section becomes a single morphism W ⟶ A ⊗ V subject to one (RS.sectionDatum_of_section). Both transpositions are reversible (RS.freeModIsoOfRoundTrip, RS.exists_section_of_datum), so the whole descent takes place in the ambient category.

The descent. The algebra is the filtered colimit of the stages of its presentation (RS.presIsColimit), tensoring preserves filtered colimits, and the objects carrying the data are compact (RS.IndCompactObj, satisfied by the embedded objects and by the mixed sums). So each datum factors through a stage (RS.exists_presStage_whiskerRight_factor), finitely many data are brought to a common stage above the one carrying the unit, and there they enter the tower generated at that stage (RS.exists_imageSubalgebra_pair, RS.exists_imageSubalgebra_single).

The identities. What is left is to know that the identities descend with the data. The inclusion of the tower into the algebra is a monomorphism and stays one after tensoring, the tensor product of Ind C being exact in each variable (RS.mono_imageSubalgebraHom_whiskerRight); the inclusion carries the unit and the multiplication of the tower to those of the algebra; so each identity may be verified after composing with the inclusion, where it is the identity already known (RS.roundTrip_descend, RS.sectionDatum_descend). Countable presentation of the tower is RS.countablyPresented_imageSubalgebra, over the embedded-image hypothesis discharged from finite length by RS.indImageEmbedded_of_lengthLE.

Compact objects of the ind-completion

def RS.IndCompactObj {C : Type v} [CategoryTheory.SmallCategory C] (Y : CategoryTheory.Ind C) : Prop

Compactness of an ind-object, phrased as in RS.Classical.Deligne.IndCompact: a morphism from the object into a filtered colimit factors through a stage of the diagram.

Equations

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

theorem RS.indCompactObj_indOf {C : Type v} [CategoryTheory.SmallCategory C] (Z : C) : IndCompactObj (indOf.obj Z)

The embedded objects are compact.

theorem RS.IndCompactObj.factor_of_isColimit {C : Type v} [CategoryTheory.SmallCategory C] {Y : CategoryTheory.Ind C} (hY : IndCompactObj Y) {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] {K : CategoryTheory.Functor I (CategoryTheory.Ind C)} (c : CategoryTheory.Limits.Cocone K) (hc : CategoryTheory.Limits.IsColimit c) (f : Y ⟶ c.pt) : ∃ (i : I) (g : Y ⟶ K.obj i), CategoryTheory.CategoryStruct.comp g (c.ι.app i) = f

Compactness against an arbitrary colimit cocone: the factorisation of the definition does not depend on the chosen colimit.

The presentation as a colimit cocone

noncomputable def RS.presCocone {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.Cocone (presDiagram A)

The cocone of the chosen presentation of an ind-object, with the ind-object itself as its point.

Equations

• RS.presCocone A = { pt := A, ι := { app := fun (i : A.presentation.I) => RS.presStage A i, naturality := ⋯ } }

@[simp]

theorem RS.presCocone_pt {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) : (presCocone A).pt = A

@[simp]

theorem RS.presCocone_ι_app {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) (i : A.presentation.I) : (presCocone A).ι.app i = presStage A i

noncomputable def RS.presIsColimit {C : Type v} [CategoryTheory.SmallCategory C] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.IsColimit (presCocone A)

The presentation cocone is a colimit cocone.

Equations

• RS.presIsColimit A = (CategoryTheory.Limits.colimit.isColimit (RS.presDiagram A)).ofIsoColimit (CategoryTheory.Limits.Cocone.ext A.colimitPresentationCompYoneda ⋯)

Descending the finite data to a stage

theorem RS.exists_presStage_whiskerRight_factor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) {Y M : CategoryTheory.Ind C} (hY : IndCompactObj Y) (f : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A M) : ∃ (i : A.presentation.I) (g : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj (A.presentation.F.obj i)) M), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (presStage A i) M) = f

A map from a compact object into a base change factors through a stage of the presentation: tensoring preserves filtered colimits, so the base change of the presentation cocone is again a colimit cocone.

Descending the round-trip identities along a subalgebra

theorem RS.whiskerLeft_freeAct_comp_whiskerRight {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : B ⟶ A) (hmul : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom φ φ) CategoryTheory.MonObj.mul) {X M : D} (v : M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X))) (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp v (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)))

The product of the subalgebra, read in the algebra: the left-hand free action of the subalgebra, followed by the inclusion, is the left-hand free action of the algebra applied to the transported datum.

theorem RS.roundTrip_descend {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : B ⟶ A) (hone : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one φ = CategoryTheory.MonObj.one) (hmul : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom φ φ) CategoryTheory.MonObj.mul) {X M : D} (u : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B M) (v : M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B X) [CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X)] (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ M)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp v (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)) : CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)

Descent of a round trip to a subalgebra: the identity that holds in the algebra for the transported data already holds in the subalgebra, because the inclusion is a monomorphism and stays one after tensoring.

theorem RS.sectionDatum_descend {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : B ⟶ A) (hone : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one φ = CategoryTheory.MonObj.one) {V W : D} (g : V ⟶ W) (t : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B V) [CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ W)] (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ V)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W)) : CategoryTheory.CategoryStruct.comp t (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W)

Descent of a splitting datum to a subalgebra. Only the unit is involved: the datum is a single map, not a round trip.

Rebuilding the module data from the descended maps

theorem RS.freeModHomEquiv_symm_comp {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {X M : D} (N : CategoryTheory.Mod D R) (u : X ⟶ (freeMod R M).X) (k : freeMod R M ⟶ N) : (freeModHomEquiv R X N) (CategoryTheory.CategoryStruct.comp ((freeModHomEquiv R X (freeMod R M)).symm u) k) = CategoryTheory.CategoryStruct.comp u k.hom

Restricting a composite out of a free module along the unit is postcomposition of the restriction of the first factor.

theorem RS.freeModHomEquiv_id {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (X : D) : (freeModHomEquiv R X (freeMod R X)) (CategoryTheory.CategoryStruct.id (freeMod R X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)

Restricting the identity of a free module along the unit is the unit itself.

noncomputable def RS.freeModIsoOfRoundTrip {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {X M : D} (u : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R M) (v : M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R X) (h₁ : CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)) (h₂ : CategoryTheory.CategoryStruct.comp v (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R u) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R M).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one M)) : freeMod R X ≅ freeMod R M

An isomorphism of free modules from a round trip: a pair of maps in the ambient category satisfying the two unit identities extends to an isomorphism of free modules, by the free--forgetful adjunction.

Equations

• RS.freeModIsoOfRoundTrip R u v h₁ h₂ = { hom := (RS.freeModHomEquiv R X (RS.freeMod R M)).symm u, inv := (RS.freeModHomEquiv R M (RS.freeMod R X)).symm v, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.freeModHomEquiv_comp {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {X : D} {N P : CategoryTheory.Mod D R} (f : freeMod R X ⟶ N) (k : N ⟶ P) : (freeModHomEquiv R X P) (CategoryTheory.CategoryStruct.comp f k) = CategoryTheory.CategoryStruct.comp ((freeModHomEquiv R X N) f) k.hom

Restriction along the unit turns composition in the category of modules into composition in the ambient category.

theorem RS.freeModHom_eq_whiskerLeft {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {M : D} (N : CategoryTheory.Mod D R) (f : freeMod R M ⟶ N) : f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R ((freeModHomEquiv R M N) f)) (actLeft R N.X)

A module map out of a free module is the extension of its restriction along the unit.

theorem RS.roundTrip_of_freeModIso {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {X M : D} (Φ : freeMod R X ≅ freeMod R M) : CategoryTheory.CategoryStruct.comp ((freeModHomEquiv R X (freeMod R M)) Φ.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R ((freeModHomEquiv R M (freeMod R X)) Φ.inv)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)

The round trip attached to an isomorphism of free modules: the transposes of the two directions satisfy the unit identity.

theorem RS.sectionDatum_of_section {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {V W : D} (g : V ⟶ W) (s : freeMod R W ⟶ freeMod R V) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R g) = CategoryTheory.CategoryStruct.id (freeMod R W)) : CategoryTheory.CategoryStruct.comp ((freeModHomEquiv R W (freeMod R V)) s) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W)

The datum attached to a splitting: the transpose of a section of the free module on a morphism satisfies the unit identity.

theorem RS.exists_section_of_datum {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {V W : D} (g : V ⟶ W) (t : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (h : CategoryTheory.CategoryStruct.comp t (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W)) : ∃ (s : freeMod R W ⟶ freeMod R V), CategoryTheory.CategoryStruct.comp s (freeModMap R g) = CategoryTheory.CategoryStruct.id (freeMod R W)

A splitting from its datum: a map satisfying the unit identity extends to a section of the free module on a morphism.

Entering the image subalgebra

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

The generating stage, mapped into rung zero of the image tower and on into the subalgebra it generates.

Equations

• RS.stageIntoImageSubalgebra A i₀ = CategoryTheory.CategoryStruct.comp (RS.stageToImage A i₀) (RS.imageRungι A i₀ 0)

theorem RS.stageIntoImageSubalgebra_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) : CategoryTheory.CategoryStruct.comp (stageIntoImageSubalgebra A i₀) (imageSubalgebraHom A i₀) = presStage A i₀

theorem RS.exists_imageSubalgebra_factor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) {Y M : CategoryTheory.Ind C} {i : A.presentation.I} (α : i ⟶ i₀) (g : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (indOf.obj (A.presentation.F.obj i)) M) (f : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A M) (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (presStage A i) M) = f) : ∃ (g' : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (imageSubalgebra A i₀) M), CategoryTheory.CategoryStruct.comp g' (CategoryTheory.MonoidalCategoryStruct.whiskerRight (imageSubalgebraHom A i₀) M) = f

A stage factorisation enters the image subalgebra: a datum factoring through a stage below the generating one factors through the subalgebra generated there.

theorem RS.exists_imageSubalgebra_pair {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] {Y Y' M M' : CategoryTheory.Ind C} (hY : IndCompactObj Y) (hY' : IndCompactObj Y') (f : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A M) (f' : Y' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A M') : ∃ (j : A.presentation.I) (_ : UnitAtStage A j) (g : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (imageSubalgebra A j) M) (g' : Y' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (imageSubalgebra A j) M'), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (imageSubalgebraHom A j) M) = f ∧ CategoryTheory.CategoryStruct.comp g' (CategoryTheory.MonoidalCategoryStruct.whiskerRight (imageSubalgebraHom A j) M') = f'

Two data descend to a common image subalgebra, generated at a stage that also carries the unit of the algebra.

theorem RS.exists_imageSubalgebra_single {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] {Y M : CategoryTheory.Ind C} (hY : IndCompactObj Y) (f : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A M) : ∃ (j : A.presentation.I) (_ : UnitAtStage A j) (g : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (imageSubalgebra A j) M), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (imageSubalgebraHom A j) M) = f

A single datum descends to an image subalgebra, generated at a stage that also carries the unit of the algebra.

The two theorems

theorem RS.mono_imageSubalgebraHom_whiskerRight {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) (M : CategoryTheory.Ind C) : CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerRight (imageSubalgebraHom A i₀) M)

The inclusion of the image subalgebra stays a monomorphism after tensoring: the tensor product of Ind C is exact in each variable.

theorem RS.indCompactObj_mix {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] (L : OddLine (CategoryTheory.Ind C)) (p q : ℕ) : IndCompactObj (L.mix p q)

The mixed sums are compact.

theorem RS.locallyMixed_countablyPresented {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (L : OddLine (CategoryTheory.Ind C)) (X : CategoryTheory.Ind C) (hX : IndCompactObj X) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) (h : L.LocallyMixed X) : ∃ (p : ℕ) (q : ℕ) (A : CategoryTheory.Ind C) (x : CategoryTheory.MonObj A) (_ : CategoryTheory.IsCommMonObj A), CategoryTheory.MonObj.one ≠ 0 ∧ CountablyPresented A ∧ Nonempty (freeMod A X ≅ freeMod A (L.mix p q))

The countably presented form of local mixedness: an object of Ind C that becomes a mixed sum of the unit and the odd line over some algebra with non-vanishing unit already becomes one over a countably presented such algebra, provided the object is compact and the objects of C have finite length.

theorem RS.section_countablyPresented {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] {V W : CategoryTheory.Ind C} (g : V ⟶ W) (_hV : IndCompactObj V) (hW : IndCompactObj W) (hlen : ∀ (Z : C), ∃ (N : ℕ), LengthLE Z N) (h : ∃ (A : CategoryTheory.Ind C) (x : CategoryTheory.MonObj A) (_ : CategoryTheory.IsCommMonObj A), CategoryTheory.MonObj.one ≠ 0 ∧ ∃ (s : freeMod A W ⟶ freeMod A V), CategoryTheory.CategoryStruct.comp s (freeModMap A g) = CategoryTheory.CategoryStruct.id (freeMod A W)) : ∃ (A : CategoryTheory.Ind C) (x : CategoryTheory.MonObj A) (_ : CategoryTheory.IsCommMonObj A), CategoryTheory.MonObj.one ≠ 0 ∧ CountablyPresented A ∧ ∃ (s : freeMod A W ⟶ freeMod A V), CategoryTheory.CategoryStruct.comp s (freeModMap A g) = CategoryTheory.CategoryStruct.id (freeMod A W)

The countably presented form of the local splitting: a morphism of Ind C whose free module acquires a section over some algebra with non-vanishing unit already acquires one over a countably presented such algebra, provided the two objects are compact and the objects of C have finite length.

Acceptance tests

The compactness hypothesis of the two theorems is satisfied by the embedded objects, which is the shape in which the theorems are consumed.