Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.ModPowDescent

The retract tower of a dualizable module #

Iterating the zig retract: a module that is a retract of its double-dual sandwich is a retract of every stage of the sandwich tower. Together with the merge isomorphisms this descends the vanishing of a relative power to the module itself.

source
noncomputable def RS.sandwichTower {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) :
ℕ → CategoryTheory.Mod D A

The sandwich tower: iterate tensoring with the pair M ⊗ M' on the left.

Equations
Instances For
    source
    @[simp]
    theorem RS.sandwichTower_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) :
    sandwichTower A M M' 0 = M
    source
    @[simp]
    theorem RS.sandwichTower_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (k : ℕ) :
    sandwichTower A M M' (k + 1) = modTensorMod A (modTensorMod A M M') (sandwichTower A M M' k)
    source
    theorem RS.sandwichTower_retract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (i₀ : M ⟶ modTensorMod A (modTensorMod A M M') M) (r₀ : modTensorMod A (modTensorMod A M M') M ⟶ M) (h₀ : CategoryTheory.CategoryStruct.comp i₀ r₀ = CategoryTheory.CategoryStruct.id M) (k : ℕ) :
    ∃ (i : M ⟶ sandwichTower A M M' k) (r : sandwichTower A M M' k ⟶ M), CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id M

    The retract iterates up the tower: a module that is a retract of its sandwich is a retract of every tower stage.