Factor extraction from splitting data

The dévissage engine of the trichotomy: from splitting data over a duality datum, the unit of the splitting algebra is a direct factor of the base change of the module. The insertion extends B-linearly to an evaluation on the base change; the copairing against the dual insertion supplies a coevaluation; the section identity of the data makes the pair a retract.

theorem RS.splitEvalCond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] {M : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj 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 (modTensorLegM A (restrictRegular φ) M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B v) CategoryTheory.MonObj.mul) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (restrictRegular φ) M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B v) CategoryTheory.MonObj.mul)

The descent condition of the evaluation: an insertion that is linear over the base through φ coequalizes the two legs of the base-change tensor.

noncomputable def RS.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 : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj 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)) : baseChange φ M ⟶ B

The evaluation of the insertion on the base change: the B-linear extension of a base-linear insertion.

Equations

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

theorem RS.modTensorπ_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 : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj 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 (restrictRegular φ) M) (splitEval A B φ v hv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B v) CategoryTheory.MonObj.mul

Defining equation of the evaluation.

theorem RS.modTensorπ_splitEval_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 : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj 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 : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (modTensorπ A (restrictRegular φ) M) (splitEval A B φ v hv)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B v) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)

Defining equation of the evaluation.

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

A base-linear insertion, bundled as a module morphism into the restricted regular module.

Equations

• RS.insHom A B φ w hw = CategoryTheory.Mod.Hom.mk' w hw

@[simp]

theorem RS.insHom_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {M' : CategoryTheory.Mod D A} (B : D) [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (w : M'.X ⟶ B) (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)) : (insHom A B φ w hw).hom = w

noncomputable def RS.splitCoevalCore {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 φ] (w : M'.X ⟶ B) (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)) : modTensor A M M' ⟶ baseChange φ M

The coevaluation core: swap the pair and push the dual factor into the algebra — the module tensor product lands in the base change.

Equations

• RS.splitCoevalCore A B φ w hw = CategoryTheory.CategoryStruct.comp (RS.modTensorSwap A M M') (RS.modTensorMap A (RS.insHom A B φ w hw) (CategoryTheory.CategoryStruct.id M))

theorem RS.modTensorπ_splitCoevalCore {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 φ] (w : M'.X ⟶ B) (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 (modTensorπ A M M') (splitCoevalCore A B φ w hw) = CategoryTheory.CategoryStruct.comp (β_ M.X M'.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w M.X) (modTensorπ A (restrictRegular φ) M))

Defining equation of the coevaluation core.

theorem RS.modTensorπ_splitCoevalCore_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 φ] (w : M'.X ⟶ B) (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 (modTensorπ A M M') (CategoryTheory.CategoryStruct.comp (splitCoevalCore A B φ w hw) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (β_ M.X M'.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w M.X) (modTensorπ A (restrictRegular φ) M))) h

Defining equation of the coevaluation core.

theorem RS.splitCoevalCore_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 (splitCoevalCore A B φ w hw) (splitEval A B φ v hv) = p

Evaluating the coevaluation core multiplies the two insertions: the core composite is any descended pair product.

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

The evaluation is linear over the algebra.

theorem RS.baseChangeAct_splitEval_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 : 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) (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 : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeAct φ M) (CategoryTheory.CategoryStruct.comp (splitEval A B φ v hv) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitEval A B φ v hv)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)

The evaluation is linear over the algebra.

noncomputable def RS.splitCoeval {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)] (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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)) : B ⟶ baseChange φ M

The coevaluation: the copair element with its dual 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_splitCoeval {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)] (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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.MonObj.mul (splitCoeval A B φ w d hw) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitCoeval A B φ w d hw)) (baseChangeAct φ M)

The coevaluation is linear over the algebra.

theorem RS.mul_splitCoeval_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)] (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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.MonObj.mul (CategoryTheory.CategoryStruct.comp (splitCoeval A B φ w d hw) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (splitCoeval A B φ w d hw)) (CategoryTheory.CategoryStruct.comp (baseChangeAct φ M) h)

The coevaluation is linear over the algebra.

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

The retract identity (the dévissage step of the trichotomy): over splitting data, the coevaluation followed by the evaluation is the identity — the algebra is a direct factor of the base change of the module.

noncomputable def RS.splitEvalMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {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) (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)) : baseChangeMod φ M ⟶ regularMod B

The evaluation, as a module morphism onto the regular module.

Equations

• RS.splitEvalMod A B φ v hv = CategoryTheory.Mod.Hom.mk' (RS.splitEval A B φ v hv) ⋯

noncomputable def RS.splitCoevalMod {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)] (w : M'.X ⟶ B) (d : ModDualityDatum A M M') (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)) : regularMod B ⟶ baseChangeMod φ M

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

Equations

• RS.splitCoevalMod A B φ w d hw = CategoryTheory.Mod.Hom.mk' (RS.splitCoeval A B φ w d hw) ⋯