Restricting a monoidal left action to a full subcategory

Let a monoidal category C act on the left on a category D, and let P : ObjectProperty D be stable under the action: P d implies P (c ⊙ₗ d) for every c : C. Then the action restricts to the full subcategory P.FullSubcategory, with the same action on objects and morphisms and with structure isomorphisms lifted from D. For a group G, an action of Discrete G is a categorical group action, and this restricts it to any invariant full subcategory, for instance a full subcategory of modules cut out by a condition that the action preserves. Stable properties are closed under ⊓ and isoClosure, and the essential image of a left-linear functor is stable. If the action functors on a preadditive category D are additive or R-linear, so are the restricted ones.

The comparison functors of full subcategories are then equivariant, in the sense of Mathlib's Functor.LeftLinear:

• the inclusion P.ι : P.FullSubcategory ⥤ D, with identity lineators;
• the inclusion ObjectProperty.ιOfLE h : P.FullSubcategory ⥤ Q.FullSubcategory for h : P ≤ Q, with identity lineators; it compares restricting to P directly with restricting first to Q;
• the lift P.lift F hF of a (lax, oplax or strong) left-linear functor F whose values satisfy P, with the lineators of F (which need not be identities). In particular the corestriction F.toEssImage of a left-linear functor to its essential image is left-linear, again with the lineators of F.

This follows Mathlib's construction of the monoidal structure on a full subcategory (CategoryTheory.ObjectProperty.fullMonoidalSubcategory).

Main declarations

• CategoryTheory.ObjectProperty.IsStableUnderLeftAction: the property P is stable under the left action of C;
• CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftAction: the restricted action of C on P.FullSubcategory.

class CategoryTheory.ObjectProperty.IsStableUnderLeftAction (C : Type u_1) [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) : Prop

A property P of objects of D is stable under the left action of C on D if P d implies P (c ⊙ₗ d) for all c : C and d : D.

• prop_actionObj (c : C) (d : D) (hd : P d) : P (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)

theorem CategoryTheory.ObjectProperty.prop_actionObj {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (c : C) {d : D} (hd : P d) : P (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)

instance CategoryTheory.ObjectProperty.instIsStableUnderLeftActionMin {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P Q : ObjectProperty D) [IsStableUnderLeftAction C P] [IsStableUnderLeftAction C Q] : IsStableUnderLeftAction C (P ⊓ Q)

instance CategoryTheory.ObjectProperty.instIsStableUnderLeftActionTop {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] : IsStableUnderLeftAction C ⊤

instance CategoryTheory.ObjectProperty.instIsStableUnderLeftActionIsoClosure {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] : IsStableUnderLeftAction C P.isoClosure

The closure under isomorphisms of a property stable under the action is stable.

instance CategoryTheory.ObjectProperty.instIsStableUnderLeftActionEssImageOfLeftLinear {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) [F.LeftLinear C] : IsStableUnderLeftAction C F.essImage

The essential image of a left-linear functor is stable under the action.

@[instance_reducible]

instance CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] : MonoidalCategory.MonoidalLeftActionStruct C P.FullSubcategory

The data of the left action of C on a full subcategory P.FullSubcategory of objects stable under the action, computed in D.

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct_actionHom {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {c✝ c'✝ : C} {d✝ d'✝ : P.FullSubcategory} (f : c✝ ⟶ c'✝) (g : d✝ ⟶ d'✝) : MonoidalCategory.MonoidalLeftActionStruct.actionHom f g = homMk (MonoidalCategory.MonoidalLeftActionStruct.actionHom f g.hom)

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct_actionHomLeft {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {c✝ c'✝ : C} (f : c✝ ⟶ c'✝) (X : P.FullSubcategory) : MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f X = homMk (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f X.obj)

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct_actionAssocIso {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (c c' : C) (X : P.FullSubcategory) : MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' X = P.isoMk (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' X.obj)

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct_actionHomRight {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (c : C) (x✝ x✝¹ : P.FullSubcategory) (f : x✝ ⟶ x✝¹) : MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f = homMk (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f.hom)

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct_actionObj_obj {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (c : C) (X : P.FullSubcategory) : (MonoidalCategory.MonoidalLeftActionStruct.actionObj c X).obj = MonoidalCategory.MonoidalLeftActionStruct.actionObj c X.obj

@[simp]

theorem CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftActionStruct_actionUnitIso {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (X : P.FullSubcategory) : MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X = P.isoMk (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X.obj)

@[instance_reducible]

instance CategoryTheory.ObjectProperty.fullSubcategoryMonoidalLeftAction {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] : MonoidalCategory.MonoidalLeftAction C P.FullSubcategory

A left action of C on D restricts to a left action on the full subcategory of objects satisfying a property P that is stable under the action.

instance CategoryTheory.ObjectProperty.isStableUnderLeftAction_inverseImage_ι {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (Q : ObjectProperty D) [IsStableUnderLeftAction C Q] : IsStableUnderLeftAction C (Q.inverseImage P.ι)

A stable property remains stable after restriction to another stable full subcategory.

@[instance_reducible]

instance CategoryTheory.ObjectProperty.leftLinearι {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] : P.ι.LeftLinear C

The inclusion of a full subcategory stable under the action is left-linear, with identity lineators.

@[simp]

theorem CategoryTheory.ObjectProperty.ι_μₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (c : C) (X : P.FullSubcategory) : Functor.LaxLeftLinear.μₗ P.ι c X = CategoryStruct.id (MonoidalCategory.MonoidalLeftActionStruct.actionObj c (P.ι.obj X))

@[simp]

theorem CategoryTheory.ObjectProperty.ι_δₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] (c : C) (X : P.FullSubcategory) : Functor.OplaxLeftLinear.δₗ P.ι c X = CategoryStruct.id (P.ι.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c X))

instance CategoryTheory.ObjectProperty.instAdditiveFullSubcategoryActionLeft_tauCeti {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] [Preadditive D] (c : C) [(MonoidalCategory.MonoidalLeftAction.actionLeft D c).Additive] : (MonoidalCategory.MonoidalLeftAction.actionLeft P.FullSubcategory c).Additive

If the action of c on D is additive, so is its restriction to P.FullSubcategory.

instance CategoryTheory.ObjectProperty.instLinearFullSubcategoryActionLeft_tauCeti {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] [Preadditive D] (c : C) (R : Type u_3) [Semiring R] [Linear R D] [Functor.Linear R (MonoidalCategory.MonoidalLeftAction.actionLeft D c)] : Functor.Linear R (MonoidalCategory.MonoidalLeftAction.actionLeft P.FullSubcategory c)

If the action of c on D is R-linear, so is its restriction to P.FullSubcategory.

@[instance_reducible]

instance CategoryTheory.ObjectProperty.leftLinearιOfLE {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {P : ObjectProperty D} [IsStableUnderLeftAction C P] {Q : ObjectProperty D} [IsStableUnderLeftAction C Q] (h : P ≤ Q) : (ιOfLE h).LeftLinear C

For stable properties P ≤ Q, the inclusion P.FullSubcategory ⥤ Q.FullSubcategory is left-linear with identity lineators: restricting the action to P agrees with restricting it first to Q and then to P.

@[simp]

theorem CategoryTheory.ObjectProperty.ιOfLE_μₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {P : ObjectProperty D} [IsStableUnderLeftAction C P] {Q : ObjectProperty D} [IsStableUnderLeftAction C Q] (h : P ≤ Q) (c : C) (X : P.FullSubcategory) : Functor.LaxLeftLinear.μₗ (ιOfLE h) c X = CategoryStruct.id (MonoidalCategory.MonoidalLeftActionStruct.actionObj c ((ιOfLE h).obj X))

@[simp]

theorem CategoryTheory.ObjectProperty.ιOfLE_δₗ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {P : ObjectProperty D} [IsStableUnderLeftAction C P] {Q : ObjectProperty D} [IsStableUnderLeftAction C Q] (h : P ≤ Q) (c : C) (X : P.FullSubcategory) : Functor.OplaxLeftLinear.δₗ (ιOfLE h) c X = CategoryStruct.id ((ιOfLE h).obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c X))

@[instance_reducible]

instance CategoryTheory.ObjectProperty.laxLeftLinearLift {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) (hF : ∀ (X : E), P (F.obj X)) [F.LaxLeftLinear C] : (P.lift F hF).LaxLeftLinear C

The lift through P.FullSubcategory of a lax left-linear functor is lax left-linear, with the lineators of F.

@[simp]

theorem CategoryTheory.ObjectProperty.lift_μₗ_hom {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) (hF : ∀ (X : E), P (F.obj X)) [F.LaxLeftLinear C] (c : C) (X : E) : (Functor.LaxLeftLinear.μₗ (P.lift F hF) c X).hom = Functor.LaxLeftLinear.μₗ F c X

@[instance_reducible]

instance CategoryTheory.ObjectProperty.oplaxLeftLinearLift {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) (hF : ∀ (X : E), P (F.obj X)) [F.OplaxLeftLinear C] : (P.lift F hF).OplaxLeftLinear C

The lift through P.FullSubcategory of an oplax left-linear functor is oplax left-linear, with the lineators of F.

@[simp]

theorem CategoryTheory.ObjectProperty.lift_δₗ_hom {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) (hF : ∀ (X : E), P (F.obj X)) [F.OplaxLeftLinear C] (c : C) (X : E) : (Functor.OplaxLeftLinear.δₗ (P.lift F hF) c X).hom = Functor.OplaxLeftLinear.δₗ F c X

@[instance_reducible]

instance CategoryTheory.ObjectProperty.leftLinearLift {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] (P : ObjectProperty D) [IsStableUnderLeftAction C P] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) (hF : ∀ (X : E), P (F.obj X)) [F.LeftLinear C] : (P.lift F hF).LeftLinear C

The lift through P.FullSubcategory of a left-linear functor is left-linear, with the lineators of F.

@[instance_reducible]

instance CategoryTheory.Functor.leftLinearToEssImage {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) [F.LeftLinear C] : F.toEssImage.LeftLinear C

The corestriction F.toEssImage of a left-linear functor to its essential image is left-linear, with the lineators of F.

@[simp]

theorem CategoryTheory.Functor.toEssImage_μₗ_hom {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) [F.LeftLinear C] (c : C) (X : E) : (LaxLeftLinear.μₗ F.toEssImage c X).hom = LaxLeftLinear.μₗ F c X

@[simp]

theorem CategoryTheory.Functor.toEssImage_δₗ_hom {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalCategory.MonoidalLeftAction C D] {E : Type u_3} [Category.{v_3, u_3} E] [MonoidalCategory.MonoidalLeftAction C E] (F : Functor E D) [F.LeftLinear C] (c : C) (X : E) : (OplaxLeftLinear.δₗ F.toEssImage c X).hom = OplaxLeftLinear.δₗ F c X