Module-level Schur vanishing passes to retracts #
A retract of a module inherits the vanishing of a block's action on the relative tensor powers: the module-power map of the section is a split monomorphism and intertwines the two actions.
theorem
RS.ModSchurKilled.of_split
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasCoequalizers D]
[CategoryTheory.Linear ℂ D]
(A : D)
[CategoryTheory.MonObj A]
{X Y : D}
[CategoryTheory.ModObj A X]
[CategoryTheory.ModObj A Y]
(s : X ⟶ Y)
[CategoryTheory.IsModHom A s]
(r : Y ⟶ X)
[CategoryTheory.IsModHom A r]
(hsr : CategoryTheory.CategoryStruct.comp s r = CategoryTheory.CategoryStruct.id X)
(P : SchurPackage)
{lam : YoungDiagram}
(h : ModSchurKilled A Y P lam)
:
ModSchurKilled A X P lam
Module-level Schur vanishing passes to retracts.
theorem
RS.ModSchurKilled.of_biprod_left
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.MonoidalPreadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasCoequalizers D]
[CategoryTheory.Linear ℂ D]
(A : D)
[CategoryTheory.MonObj A]
(M N : CategoryTheory.Mod D A)
(P : SchurPackage)
{lam : YoungDiagram}
(h : ModSchurKilled A (modBiprod A M N).X P lam)
:
ModSchurKilled A M.X P lam
Module-level Schur vanishing passes to the first biproduct summand.
theorem
RS.ModSchurKilled.of_modIso
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasCoequalizers D]
[CategoryTheory.Linear ℂ D]
(A : D)
[CategoryTheory.MonObj A]
{M N : CategoryTheory.Mod D A}
(e : M ≅ N)
(P : SchurPackage)
{lam : YoungDiagram}
(h : ModSchurKilled A N.X P lam)
:
ModSchurKilled A M.X P lam
Module-level Schur vanishing is invariant under isomorphism.