Factor extraction on the dual module

The mirror of the splitting extraction: over the same splitting data, the unit of the splitting algebra is a direct factor of the base change of the dual module. The dual insertion extends B-linearly to an evaluation on the base change of the dual; the copairing, with the primal factor pushed into the algebra, supplies a coevaluation; the section identity again makes the pair a retract, and the kernel of the induced linear idempotent is the complement. No braiding is needed anywhere: the copairing already presents the primal factor on the left.

noncomputable def RS.splitCoevalCoreDual {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (v : M.X ⟶ B) (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)) : modTensor A M M' ⟶ baseChange φ M'

The dual coevaluation core: push the primal factor into the algebra — the module tensor product lands in the base change of the dual module. No swap is needed: the primal factor is already on the left.

Equations

• RS.splitCoevalCoreDual A B φ v hv = RS.modTensorMap A (RS.insHom A B φ v hv) (CategoryTheory.CategoryStruct.id M')

theorem RS.modTensorπ_splitCoevalCoreDual {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (v : M.X ⟶ B) (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)) : CategoryTheory.CategoryStruct.comp (modTensorπ A M M') (splitCoevalCoreDual A B φ v hv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight v M'.X) (modTensorπ A (restrictRegular φ) M')

Defining equation of the dual coevaluation core.

theorem RS.modTensorπ_splitCoevalCoreDual_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (v : M.X ⟶ B) (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)) {Z : D} (h : baseChange φ M' ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A M M') (CategoryTheory.CategoryStruct.comp (splitCoevalCoreDual A B φ v hv) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight v M'.X) (modTensorπ A (restrictRegular φ) M')) h

Defining equation of the dual coevaluation core.

theorem RS.splitCoevalCoreDual_splitEval {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (v : M.X ⟶ B) (w : M'.X ⟶ B) (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) : CategoryTheory.CategoryStruct.comp (splitCoevalCoreDual A B φ v hv) (splitEval A B φ w hw) = p

Evaluating the dual coevaluation core multiplies the two insertions: the core composite is any descended pair product. Unlike the primal statement, no braiding step is needed.

noncomputable def RS.splitCoevalDual {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) (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)) : B ⟶ baseChange φ M'

The dual coevaluation: the copair element with its primal factor pushed into the algebra, multiplied against the algebra.

Equations

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

theorem RS.mul_splitCoevalDual {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) (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)) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (splitCoevalDual A B φ v d hv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitCoevalDual A B φ v d hv)) (baseChangeAct φ M')

The dual coevaluation is linear over the algebra.

theorem RS.mul_splitCoevalDual_assoc {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) (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)) {Z : D} (h : baseChange φ M' ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp (splitCoevalDual A B φ v d hv) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitCoevalDual A B φ v d hv)) (CategoryTheory.CategoryStruct.comp (baseChangeAct φ M') h)

The dual coevaluation is linear over the algebra.

theorem RS.splitCoevalDual_splitEval {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 (splitCoevalDual A B φ v d hv) (splitEval A B φ w hw) = CategoryTheory.CategoryStruct.id B

The dual retract identity: over splitting data, the dual coevaluation followed by the dual evaluation is the identity — the algebra is a direct factor of the base change of the dual module.

noncomputable def RS.splitCoevalDualMod {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) (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)) : regularMod B ⟶ baseChangeMod φ M'

The dual coevaluation, as a module morphism from the regular module.

Equations

• RS.splitCoevalDualMod A B φ v d hv = CategoryTheory.Mod.Hom.mk' (RS.splitCoevalDual A B φ v d hv) ⋯

noncomputable def RS.splitIdemDual {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 dual split idempotent on the base change of the dual module: evaluate, then coevaluate.

Equations

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

theorem RS.splitIdemDual_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 (splitIdemDual A B φ v w d hv hw) (splitIdemDual A B φ v w d hv hw) = splitIdemDual A B φ v w d hv hw

The dual split idempotent is idempotent.

theorem RS.baseChangeAct_splitIdemDual {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') (splitIdemDual A B φ v w d hv hw) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitIdemDual A B φ v w d hv hw)) (baseChangeAct φ M')

The dual split idempotent is linear over the algebra.

noncomputable def RS.splitComplDual {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 dual complement carrier: the kernel of the dual split idempotent.

Equations

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

noncomputable def RS.splitComplActDual {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 (splitComplDual A B φ v w d hv hw) ⟶ splitComplDual A B φ v w d hv hw

The action of the algebra descends to the dual complement.

Equations

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

theorem RS.splitComplActDual_ι {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 (splitComplActDual A B φ v w d hv hw) (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw))) (baseChangeAct φ M')

Defining equation of the dual complement action.

theorem RS.splitComplActDual_ι_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 (splitComplActDual A B φ v w d hv hw) (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw))) (baseChangeAct φ M')) h

Defining equation of the dual complement action.

theorem RS.splitComplActDual_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 (splitComplDual A B φ v w d hv hw)) (splitComplActDual A B φ v w d hv hw) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (splitComplDual A B φ v w d hv hw)).hom

The unit law of the dual complement action.

theorem RS.splitComplActDual_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 (splitComplDual A B φ v w d hv hw)) (splitComplActDual A B φ v w d hv hw) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B (splitComplDual A B φ v w d hv hw)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitComplActDual A B φ v w d hv hw)) (splitComplActDual A B φ v w d hv hw))

The multiplication law of the dual complement action.

@[implicit_reducible]

noncomputable def RS.splitComplModObjDual {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 (splitComplDual A B φ v w d hv hw)

The dual complement, as a module over the algebra.

Equations

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

noncomputable def RS.splitComplModDual {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 dual complement, bundled.

Equations

• RS.splitComplModDual A B φ v w d hv hw = { X := RS.splitComplDual A B φ v w d hv hw, mod := RS.splitComplModObjDual A B φ v w d hv hw }

noncomputable def RS.splitComplProjDual {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' ⟶ splitComplDual A B φ v w d hv hw

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

Equations

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

theorem RS.splitComplProjDual_ι {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 (splitComplProjDual A B φ v w d hv hw p hp hδ) (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw)) = CategoryTheory.CategoryStruct.id (baseChange φ M') - splitIdemDual A B φ v w d hv hw

Defining equation of the dual projection.

theorem RS.splitComplProjDual_ι_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 (splitComplProjDual A B φ v w d hv hw p hp hδ) (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (baseChange φ M') - splitIdemDual A B φ v w d hv hw) h

Defining equation of the dual projection.

noncomputable def RS.splitDecompDual {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 ⊞ splitComplDual A B φ v w d hv hw

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

Equations

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

theorem RS.baseChangeAct_splitComplProjDual {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') (splitComplProjDual A B φ v w d hv hw p hp hδ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitComplProjDual A B φ v w d hv hw p hp hδ)) (splitComplActDual A B φ v w d hv hw)

The dual projection is linear over the algebra.

theorem RS.baseChangeAct_splitComplProjDual_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 : splitComplDual A B φ v w d hv hw ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeAct φ M') (CategoryTheory.CategoryStruct.comp (splitComplProjDual A B φ v w d hv hw p hp hδ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitComplProjDual A B φ v w d hv hw p hp hδ)) (CategoryTheory.CategoryStruct.comp (splitComplActDual A B φ v w d hv hw) h)

The dual projection is linear over the algebra.

theorem RS.baseChangeAct_splitDecompDualHom {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 φ w hw) (splitComplProjDual A B φ v w d hv hw p hp hδ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.biprod.lift (splitEval A B φ w hw) (splitComplProjDual A B φ v w d hv hw p hp hδ))) (modBiprodAct B (regularMod B) (splitComplModDual A B φ v w d hv hw))

The dual decomposition intertwines the actions, forward direction.

theorem RS.modBiprodAct_splitDecompDualInv {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) (splitComplModDual A B φ v w d hv hw)) (CategoryTheory.Limits.biprod.desc (splitCoevalDual A B φ v d hv) (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.biprod.desc (splitCoevalDual A B φ v d hv) (CategoryTheory.Limits.kernel.ι (splitIdemDual A B φ v w d hv hw)))) (baseChangeAct φ M')

The dual decomposition intertwines the actions, inverse direction.

noncomputable def RS.splitComplInclDual {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)) : splitComplModDual A B φ v w d hv hw ⟶ baseChangeMod φ M'

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

Equations

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

noncomputable def RS.splitComplProjModDual {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' ⟶ splitComplModDual A B φ v w d hv hw

The projection onto the dual complement, as a module map.

Equations

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

theorem RS.splitComplDual_ι_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.ι (splitIdemDual A B φ v w d hv hw)) (splitComplProjDual A B φ v w d hv hw p hp hδ) = CategoryTheory.CategoryStruct.id (splitComplDual A B φ v w d hv hw)

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

theorem RS.splitComplInclDual_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 (splitComplInclDual A B φ v w d hv hw) (splitComplProjModDual A B φ v w d hv hw p hp hδ) = CategoryTheory.CategoryStruct.id (splitComplModDual A B φ v w d hv hw)

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