The complement of the split factor

The evaluation followed by the coevaluation is a linear idempotent on the base change of the module; its kernel is the complement of the split unit factor, and carries the descended action.

noncomputable def RS.splitIdem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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)) : baseChange φ M ⟶ baseChange φ M

The split idempotent on the base change: evaluate, then coevaluate.

Equations

• RS.splitIdem A B φ v w d hv hw = CategoryTheory.CategoryStruct.comp (RS.splitEval A B φ v hv) (RS.splitCoeval A B φ w d hw)

theorem RS.splitIdem_idem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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 (splitIdem A B φ v w d hv hw) (splitIdem A B φ v w d hv hw) = splitIdem A B φ v w d hv hw

The split idempotent is idempotent.

theorem RS.baseChangeAct_splitIdem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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 (baseChangeAct φ M) (splitIdem A B φ v w d hv hw) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitIdem A B φ v w d hv hw)) (baseChangeAct φ M)

The split idempotent is linear over the algebra.

noncomputable def RS.splitCompl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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)) : D

The complement carrier: the kernel of the split idempotent.

Equations

• RS.splitCompl A B φ v w d hv hw = CategoryTheory.Limits.kernel (RS.splitIdem A B φ v w d hv hw)

noncomputable def RS.splitComplAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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.MonoidalCategoryStruct.tensorObj B (splitCompl A B φ v w d hv hw) ⟶ splitCompl A B φ v w d hv hw

The action of the algebra descends to the complement.

Equations

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

theorem RS.splitComplAct_ι {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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 (splitComplAct A B φ v w d hv hw) (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw))) (baseChangeAct φ M)

Defining equation of the complement action.

theorem RS.splitComplAct_ι_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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)) {Z : D} (h : baseChange φ M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (splitComplAct A B φ v w d hv hw) (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw))) (baseChangeAct φ M)) h

Defining equation of the complement action.

theorem RS.splitComplAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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.MonObj.one (splitCompl A B φ v w d hv hw)) (splitComplAct A B φ v w d hv hw) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (splitCompl A B φ v w d hv hw)).hom

The unit law of the complement action.

theorem RS.splitComplAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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.MonObj.mul (splitCompl A B φ v w d hv hw)) (splitComplAct A B φ v w d hv hw) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B (splitCompl A B φ v w d hv hw)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitComplAct A B φ v w d hv hw)) (splitComplAct A B φ v w d hv hw))

The multiplication law of the complement action.

@[implicit_reducible]

noncomputable def RS.splitComplModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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.ModObj B (splitCompl A B φ v w d hv hw)

The complement, as a module over the algebra.

Equations

• RS.splitComplModObj A B φ v w d hv hw = { smul := RS.splitComplAct A B φ v w d hv hw, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.splitComplMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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.Mod D B

The complement, bundled.

Equations

• RS.splitComplMod A B φ v w d hv hw = { X := RS.splitCompl A B φ v w d hv hw, mod := RS.splitComplModObj A B φ v w d hv hw }

noncomputable def RS.splitComplProj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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) : baseChange φ M ⟶ splitCompl A B φ v w d hv hw

The projection onto the complement: the complementary idempotent, corestricted to the kernel.

Equations

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

theorem RS.splitComplProj_ι {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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 (splitComplProj A B φ v w d hv hw p hp hδ) (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw)) = CategoryTheory.CategoryStruct.id (baseChange φ M) - splitIdem A B φ v w d hv hw

Defining equation of the projection.

theorem RS.splitComplProj_ι_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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) {Z : D} (h : baseChange φ M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (splitComplProj A B φ v w d hv hw p hp hδ) (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (baseChange φ M) - splitIdem A B φ v w d hv hw) h

Defining equation of the projection.

noncomputable def RS.splitDecomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasBinaryBiproducts 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) : baseChange φ M ≅ B ⊞ splitCompl A B φ v w d hv hw

The decomposition of the base change, carrier level: the algebra summand against the complement.

Equations

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

theorem RS.baseChangeAct_splitComplProj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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 (baseChangeAct φ M) (splitComplProj A B φ v w d hv hw p hp hδ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitComplProj A B φ v w d hv hw p hp hδ)) (splitComplAct A B φ v w d hv hw)

The projection is linear over the algebra.

theorem RS.baseChangeAct_splitComplProj_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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) {Z : D} (h : splitCompl A B φ v w d hv hw ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeAct φ M) (CategoryTheory.CategoryStruct.comp (splitComplProj A B φ v w d hv hw p hp hδ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitComplProj A B φ v w d hv hw p hp hδ)) (CategoryTheory.CategoryStruct.comp (splitComplAct A B φ v w d hv hw) h)

The projection is linear over the algebra.

theorem RS.baseChangeAct_splitDecompHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasBinaryBiproducts 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 (baseChangeAct φ M) (CategoryTheory.Limits.biprod.lift (splitEval A B φ v hv) (splitComplProj A B φ v w d hv hw p hp hδ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.biprod.lift (splitEval A B φ v hv) (splitComplProj A B φ v w d hv hw p hp hδ))) (modBiprodAct B (regularMod B) (splitComplMod A B φ v w d hv hw))

The decomposition intertwines the actions, forward direction.

theorem RS.modBiprodAct_splitDecompInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasBinaryBiproducts 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 (modBiprodAct B (regularMod B) (splitComplMod A B φ v w d hv hw)) (CategoryTheory.Limits.biprod.desc (splitCoeval A B φ w d hw) (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.biprod.desc (splitCoeval A B φ w d hw) (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw)))) (baseChangeAct φ M)

The decomposition intertwines the actions, inverse direction.

noncomputable def RS.splitDecompMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasBinaryBiproducts 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) : baseChangeMod φ M ≅ modBiprod B (regularMod B) (splitComplMod A B φ v w d hv hw)

The decomposition at the module level: the base change of the module is the regular module plus the complement, as modules over the algebra.

Equations

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

noncomputable def RS.splitComplIncl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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)) : splitComplMod A B φ v w d hv hw ⟶ baseChangeMod φ M

The kernel inclusion of the complement, as a module map.

Equations

• RS.splitComplIncl A B φ v w d hv hw = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.kernel.ι (RS.splitIdem A B φ v w d hv hw)) ⋯

noncomputable def RS.splitComplProjMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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) : baseChangeMod φ M ⟶ splitComplMod A B φ v w d hv hw

The projection onto the complement, as a module map.

Equations

• RS.splitComplProjMod A B φ v w d hv hw p hp hδ = CategoryTheory.Mod.Hom.mk' (RS.splitComplProj A B φ v w d hv hw p hp hδ) ⋯

theorem RS.splitCompl_ι_proj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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 (CategoryTheory.Limits.kernel.ι (splitIdem A B φ v w d hv hw)) (splitComplProj A B φ v w d hv hw p hp hδ) = CategoryTheory.CategoryStruct.id (splitCompl A B φ v w d hv hw)

The complement is a retract of the base change, at the carrier.

theorem RS.splitComplIncl_proj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (v : M.X ⟶ B) (w : M'.X ⟶ B) (d : ModDualityDatum A M M') [CategoryTheory.Limits.HasKernels 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 (splitComplIncl A B φ v w d hv hw) (splitComplProjMod A B φ v w d hv hw p hp hδ) = CategoryTheory.CategoryStruct.id (splitComplMod A B φ v w d hv hw)

The complement is a retract of the base change, as modules.