The zigzag laws of a base-changed duality datum #
The statement that base change preserves the zigzag laws, named so that the dévissage steps can refer to it directly.
def
RS.BaseChangeZigzagStatement
{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]
[∀ (Z : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorLeft Z)]
[∀ (Z : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorRight Z)]
:
Base change preserves the zigzag laws: the statement of record for the dévissage steps.
Equations
- One or more equations did not get rendered due to their size.