The algebra structure on the image tower

RS.Classical.Deligne.CountableDescent builds, inside a commutative algebra A of Ind C and above a stage i₀ of its presentation, the tower of images RS.imageRung, its colimit RS.imageSubalgebra, and the monomorphism RS.imageSubalgebraHom of that colimit into the algebra. This file makes the colimit an algebra in its own right, so that the countably presented replacement produced there is a replacement of algebras.

The multiplication. Tensoring in Ind C preserves filtered colimits (RS.Classical.Deligne.IndTensorExact), so the square of the colimit is the colimit of the squares, and the multiplication is a descent in each variable: RS.imageMul is RS.imageLeftMul descended along the right-hand variable, and RS.imageLeftMul is RS.imagePairMul descended along the left-hand one. The naturality conditions of the two descents cost nothing, because RS.imageSubalgebraHom is a monomorphism and both sides of each condition have the same composite with it.

The product of a pair of rungs. Rungs n and m are pushed up to their common upper bound, where the tower is closed under multiplication one rung at a time. Closure is an epimorphism--monomorphism lifting: the square of the stage of the presentation surjects onto the square of its image, because the tensor of Ind C is right exact in each variable (RS.Classical.Deligne.IndCoeq) and hence carries epimorphisms to epimorphisms; the next rung is a subobject of the algebra; and RS.stageMul_spec says the square commutes. Every epimorphism of an abelian category is strong, so the lifting exists.

The unit and the laws. A stage carrying the unit of the algebra (RS.UnitAtStage, satisfied by RS.unitStage and by every stage above it) puts the unit into rung zero. The laws are then free: each is an equation between maps into the colimit, and a monomorphism cancels, so each reduces to the corresponding law in A. This is RS.monObjOfMono, and it gives MonObj (RS.imageSubalgebra A i₀) and, over a symmetric C, IsCommMonObj of the same.

Subobjects closed under the operations

A monomorphism into an algebra whose source carries a multiplication and a unit lying over those of the algebra is itself an algebra: each law is an equation between maps into the source, and a monomorphism cancels.

theorem RS.one_mul_of_mono {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {S A : D} [CategoryTheory.MonObj A] (k : S ⟶ A) [CategoryTheory.Mono k] (m : CategoryTheory.MonoidalCategoryStruct.tensorObj S S ⟶ S) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ S) (hm : CategoryTheory.CategoryStruct.comp m k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom k k) CategoryTheory.MonObj.mul) (he : CategoryTheory.CategoryStruct.comp e k = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight e S) m = (CategoryTheory.MonoidalCategoryStruct.leftUnitor S).hom

The unit law of a subobject closed under the operations, left-hand version.

theorem RS.mul_one_of_mono {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {S A : D} [CategoryTheory.MonObj A] (k : S ⟶ A) [CategoryTheory.Mono k] (m : CategoryTheory.MonoidalCategoryStruct.tensorObj S S ⟶ S) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ S) (hm : CategoryTheory.CategoryStruct.comp m k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom k k) CategoryTheory.MonObj.mul) (he : CategoryTheory.CategoryStruct.comp e k = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S e) m = (CategoryTheory.MonoidalCategoryStruct.rightUnitor S).hom

The unit law of a subobject closed under the operations, right-hand version.

theorem RS.mul_assoc_of_mono {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {S A : D} [CategoryTheory.MonObj A] (k : S ⟶ A) [CategoryTheory.Mono k] (m : CategoryTheory.MonoidalCategoryStruct.tensorObj S S ⟶ S) (hm : CategoryTheory.CategoryStruct.comp m k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom k k) CategoryTheory.MonObj.mul) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight m S) m = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator S S S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S m) m)

The associativity law of a subobject closed under the operations.

theorem RS.mul_comm_of_mono {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {S A : D} [CategoryTheory.MonObj A] (k : S ⟶ A) [CategoryTheory.Mono k] (m : CategoryTheory.MonoidalCategoryStruct.tensorObj S S ⟶ S) [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (hm : CategoryTheory.CategoryStruct.comp m k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom k k) CategoryTheory.MonObj.mul) : CategoryTheory.CategoryStruct.comp (β_ S S).hom m = m

The commutativity law of a subobject closed under the operations.

@[reducible]

def RS.monObjOfMono {D : Type u} [CategoryTheory.Category.{w, u} D] [CategoryTheory.MonoidalCategory D] {S A : D} [CategoryTheory.MonObj A] (k : S ⟶ A) [CategoryTheory.Mono k] (m : CategoryTheory.MonoidalCategoryStruct.tensorObj S S ⟶ S) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ S) (hm : CategoryTheory.CategoryStruct.comp m k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom k k) CategoryTheory.MonObj.mul) (he : CategoryTheory.CategoryStruct.comp e k = CategoryTheory.MonObj.one) : CategoryTheory.MonObj S

A subobject closed under the operations is an algebra.

Equations

• RS.monObjOfMono k m e hm he = { one := e, mul := m, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

Epimorphisms and the tensor of ind-objects

The tensor product of Ind C is right exact in each variable, so it carries epimorphisms to epimorphisms; and every epimorphism of an abelian category is strong.

instance RS.epi_tensorHom_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] {X Y X' Y' : CategoryTheory.Ind C} (f : X ⟶ Y) (g : X' ⟶ Y') [CategoryTheory.Epi f] [CategoryTheory.Epi g] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)

The tensor of two epimorphisms of ind-objects is an epimorphism: both whiskerings are right exact.

instance RS.strongEpi_tensorHom_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] {X Y X' Y' : CategoryTheory.Ind C} (f : X ⟶ Y) (g : X' ⟶ Y') [CategoryTheory.Epi f] [CategoryTheory.Epi g] : CategoryTheory.StrongEpi (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)

The tensor of two epimorphisms of ind-objects is a strong epimorphism: Ind C is abelian.

The stage carrying the unit

The tower generated at a stage contains the unit of the algebra as soon as the unit factors through that stage. The chosen stage RS.unitStage does, and so does every stage above it.

class RS.UnitAtStage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i : A.presentation.I) : Prop

The unit is carried by a stage: the unit of the algebra factors through the given stage of the chosen presentation.

• exists_point : ∃ (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ indOf.obj (A.presentation.F.obj i)), CategoryTheory.CategoryStruct.comp e (presStage A i) = CategoryTheory.MonObj.one

  The unit of the algebra factors through the stage.

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

The factorisation of the unit through a stage that carries it.

instance RS.unitAtStage_unitStage {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] : UnitAtStage A (unitStage A)

The chosen unit stage carries the unit.

theorem RS.UnitAtStage.map {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {A : CategoryTheory.Ind C} [CategoryTheory.MonObj A] {i j : A.presentation.I} (α : i ⟶ j) [UnitAtStage A i] : UnitAtStage A j

Every stage above a stage carrying the unit carries it too.

The tower, its rungs, and its unit

Everything in this section is available over an abelian C: the comparison maps of the rungs, the lifting square for the rung-wise multiplication, and the unit.

@[reducible]

noncomputable def RS.imageDiagram {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 Tower (CategoryTheory.Ind C)

The image tower, read as a diagram over the ambient-universe copy of the natural numbers.

Equations

• RS.imageDiagram A i₀ = CategoryTheory.AsSmall.down.comp (RS.imageSeq A i₀)

theorem RS.imageSubalgebra_hom_ext {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) {X : CategoryTheory.Ind C} {f g : X ⟶ imageSubalgebra A i₀} (h : CategoryTheory.CategoryStruct.comp f (imageSubalgebraHom A i₀) = CategoryTheory.CategoryStruct.comp g (imageSubalgebraHom A i₀)) : f = g

Maps into the image tower are determined by their composites with the inclusion into the algebra, that inclusion being a monomorphism.

theorem RS.imageColimitι_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) (m : Tower) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (imageDiagram A i₀) m) (imageSubalgebraHom A i₀) = stageImageι A (towerIdx A i₀ m.down)

The structural maps of the colimit of the image tower, composed with the inclusion into the algebra.

theorem RS.imageDiagram_map_comp_ι {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) {m m' : Tower} (u : m ⟶ m') : CategoryTheory.CategoryStruct.comp ((imageDiagram A i₀).map u) (stageImageι A (towerIdx A i₀ m'.down)) = stageImageι A (towerIdx A i₀ m.down)

The transition maps of the image tower are compatible with the inclusions of the rungs into the algebra.

noncomputable def RS.imageRungLe {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) {n k : ℕ} (h : n ≤ k) : stageImage A (towerIdx A i₀ n) ⟶ stageImage A (towerIdx A i₀ k)

The comparison map of two rungs of the image tower.

Equations

• RS.imageRungLe A i₀ h = (RS.imageDiagram A i₀).map { down := CategoryTheory.homOfLE h }

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

noncomputable def RS.imageRungTop {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.MonoidalCategoryStruct.tensorObj (indOf.obj (towerObj A i₀ n)) (indOf.obj (towerObj A i₀ n)) ⟶ stageImage A (towerIdx A i₀ (n + 1))

The square of a rung of the generated tower, multiplied into the next rung of the image tower.

Equations

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

theorem RS.imageRungTop_comp_ι {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 (imageRungTop A i₀ n) (stageImageι A (towerIdx A i₀ (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (presStage A (towerIdx A i₀ n)) (presStage A (towerIdx A i₀ n))) CategoryTheory.MonObj.mul

theorem RS.imageRungBot_comp {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 (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageToImage A (towerIdx A i₀ n)) (stageToImage A (towerIdx A i₀ n))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageImageι A (towerIdx A i₀ n)) (stageImageι A (towerIdx A i₀ n))) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (presStage A (towerIdx A i₀ n)) (presStage A (towerIdx A i₀ n))) CategoryTheory.MonObj.mul

theorem RS.imageRungMul_sq {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.CommSq (imageRungTop A i₀ n) (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageToImage A (towerIdx A i₀ n)) (stageToImage A (towerIdx A i₀ n))) (stageImageι A (towerIdx A i₀ (n + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageImageι A (towerIdx A i₀ n)) (stageImageι A (towerIdx A i₀ n))) CategoryTheory.MonObj.mul)

The lifting square for the multiplication of a rung of the image tower with itself: the square of the stage surjects onto the square of its image, the next rung is a subobject of the algebra, and the generated tower is closed under multiplication.

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

The unit of the image tower, present as soon as the generating stage carries the unit of the algebra.

Equations

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

theorem RS.imageOne_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) [UnitAtStage A i₀] : CategoryTheory.CategoryStruct.comp (imageOne A i₀) (imageSubalgebraHom A i₀) = CategoryTheory.MonObj.one

The unit of the image tower lies over the unit of the algebra.

theorem RS.imageOne_ne_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] (i₀ : A.presentation.I) [UnitAtStage A i₀] (h : CategoryTheory.MonObj.one ≠ 0) : imageOne A i₀ ≠ 0

The unit of the image tower does not vanish when the unit of the algebra does not: it composes to the unit of the algebra.

The multiplication of the image tower

The rungs are closed under multiplication one rung at a time, by an epimorphism--monomorphism lifting; the products of pairs of rungs assemble into the multiplication of the colimit by two filtered descents.

noncomputable def RS.imageRungMul {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) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (stageImage A (towerIdx A i₀ n)) (stageImage A (towerIdx A i₀ n)) ⟶ stageImage A (towerIdx A i₀ (n + 1))

The image tower is closed under multiplication, rung by rung.

Equations

• RS.imageRungMul A i₀ n = ⋯.lift

theorem RS.imageRungMul_comp_ι {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp (imageRungMul A i₀ n) (stageImageι A (towerIdx A i₀ (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageImageι A (towerIdx A i₀ n)) (stageImageι A (towerIdx A i₀ n))) CategoryTheory.MonObj.mul

noncomputable def RS.imagePairMul {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) (n m : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (stageImage A (towerIdx A i₀ n)) (stageImage A (towerIdx A i₀ m)) ⟶ imageSubalgebra A i₀

The product of two rungs of the image tower: both are pushed up to their common upper bound, where the tower multiplies.

Equations

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

theorem RS.imagePairMul_comp_hom {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) (n m : ℕ) : CategoryTheory.CategoryStruct.comp (imagePairMul A i₀ n m) (imageSubalgebraHom A i₀) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageImageι A (towerIdx A i₀ n)) (stageImageι A (towerIdx A i₀ m))) CategoryTheory.MonObj.mul

noncomputable def RS.imageLeftMulCocone {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) (n : ℕ) : CategoryTheory.Limits.Cocone ((imageDiagram A i₀).comp (CategoryTheory.MonoidalCategory.tensorLeft (stageImage A (towerIdx A i₀ n))))

The cocone over the image tower whose leg at a rung is the product with a fixed rung.

Equations

• RS.imageLeftMulCocone A i₀ n = { pt := RS.imageSubalgebra A i₀, ι := { app := fun (m : RS.Tower) => RS.imagePairMul A i₀ n m.down, naturality := ⋯ } }

noncomputable def RS.imageLeftMul {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) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (stageImage A (towerIdx A i₀ n)) (imageSubalgebra A i₀) ⟶ imageSubalgebra A i₀

The product of a rung of the image tower with the whole tower.

Equations

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

theorem RS.imageLeftMul_fac {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) (n : ℕ) (m : Tower) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stageImage A (towerIdx A i₀ n)) (CategoryTheory.Limits.colimit.ι (imageDiagram A i₀) m)) (imageLeftMul A i₀ n) = imagePairMul A i₀ n m.down

theorem RS.imageLeftMul_comp_hom {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp (imageLeftMul A i₀ n) (imageSubalgebraHom A i₀) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (stageImageι A (towerIdx A i₀ n)) (imageSubalgebraHom A i₀)) CategoryTheory.MonObj.mul

noncomputable def RS.imageMulCocone {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) : CategoryTheory.Limits.Cocone ((imageDiagram A i₀).comp (CategoryTheory.MonoidalCategory.tensorRight (imageSubalgebra A i₀)))

The cocone over the image tower whose leg at a rung is the product of that rung with the whole tower.

Equations

• RS.imageMulCocone A i₀ = { pt := RS.imageSubalgebra A i₀, ι := { app := fun (n : RS.Tower) => RS.imageLeftMul A i₀ n.down, naturality := ⋯ } }

noncomputable def RS.imageMul {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) : CategoryTheory.MonoidalCategoryStruct.tensorObj (imageSubalgebra A i₀) (imageSubalgebra A i₀) ⟶ imageSubalgebra A i₀

The multiplication of the image tower.

Equations

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

theorem RS.imageMul_fac {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) (n : Tower) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι (imageDiagram A i₀) n) (imageSubalgebra A i₀)) (imageMul A i₀) = imageLeftMul A i₀ n.down

theorem RS.imageMul_comp_hom {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) : CategoryTheory.CategoryStruct.comp (imageMul A i₀) (imageSubalgebraHom A i₀) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (imageSubalgebraHom A i₀) (imageSubalgebraHom A i₀)) CategoryTheory.MonObj.mul

The multiplication of the image tower lies over the multiplication of the algebra.

@[instance_reducible]

noncomputable instance RS.monObjImageSubalgebra {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) [UnitAtStage A i₀] : CategoryTheory.MonObj (imageSubalgebra A i₀)

The image tower is an algebra. The laws are inherited from the algebra: each is an equation between maps into the tower, and the inclusion into the algebra is a monomorphism.

Equations

• RS.monObjImageSubalgebra A i₀ = RS.monObjOfMono (RS.imageSubalgebraHom A i₀) (RS.imageMul A i₀) (RS.imageOne A i₀) ⋯ ⋯

theorem RS.one_imageSubalgebra_ne_zero {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) [UnitAtStage A i₀] (h : CategoryTheory.MonObj.one ≠ 0) : CategoryTheory.MonObj.one ≠ 0

The unit of the image tower, read through its algebra structure, does not vanish when the unit of the algebra does not.

Commutativity

Over a symmetric C the image tower is a commutative algebra, again because the inclusion into the algebra is a monomorphism.

instance RS.isCommMonObj_imageSubalgebra {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (A : CategoryTheory.Ind C) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (i₀ : A.presentation.I) [UnitAtStage A i₀] : CategoryTheory.IsCommMonObj (imageSubalgebra A i₀)

The image tower is a commutative algebra.

Acceptance tests

The algebra structure synthesises at the chosen unit stage, and the replacement it produces is a monomorphism of commutative algebras with countably presented source and non-vanishing unit.