Adjointness of the split idempotents

The split idempotent on the base change and its dual counterpart are adjoint for the base-changed pairing: moving either across the pairing gives the other. The two coevaluation identities turn each side into a tensor of the two evaluations, and the whisker exchange identifies them.

Passing to the complementary idempotents gives the adjointness in the form the dévissage step consumes.

theorem RS.splitIdem_adj {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) (hw : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitIdemDual A B φ v w d hv hw) (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (splitIdem A B φ v w d hv hw)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)

The split idempotents are adjoint for the base-changed pairing.

theorem RS.splitComplIdem_adj {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) (hw : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id (baseChange φ M') - splitIdemDual A B φ v w d hv hw) (baseChangeMod φ M).X) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M').X (CategoryTheory.CategoryStruct.id (baseChange φ M) - splitIdem A B φ v w d hv hw)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M') (baseChangeMod φ M)) (baseChangeDatum A B φ d).pair)

The complementary split idempotents are adjoint for the base-changed pairing, at the carrier.

theorem RS.splitComplMap_adj {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.Limits.HasKernels 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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] {M M' : CategoryTheory.Mod D A} (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) (hv : CategoryTheory.CategoryStruct.comp (actLeft A M.X) v = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A v) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) (hw : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ B) CategoryTheory.MonObj.mul)) (p : modTensor A M M' ⟶ B) (hp : CategoryTheory.CategoryStruct.comp (modTensorπ A M M') p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom v w) CategoryTheory.MonObj.mul) (hδ : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp d.copair p) = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (modTensorMap B (CategoryTheory.CategoryStruct.comp (splitComplProjModDual A B φ v w d hv hw p hp hδ) (splitComplInclDual A B φ v w d hv hw)) (CategoryTheory.CategoryStruct.id (baseChangeMod φ M))) (baseChangeDatum A B φ d).pair = CategoryTheory.CategoryStruct.comp (modTensorMap B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M')) (CategoryTheory.CategoryStruct.comp (splitComplProjMod A B φ v w d hv hw p hp hδ) (splitComplIncl A B φ v w d hv hw))) (baseChangeDatum A B φ d).pair

Adjointness of the split idempotents, in the module form the dévissage step consumes.