Library UniMath.CategoryTheory.Monoidal.Actions

Generalisation of the concept of actions, over monoidal categories.

Originally introduced under the name C-categories (for C a monoidal category) by Bodo Pareigis (1977).

This notion is found in G. Janelidze and G.M. Kelly: A Note on Actions of a Monoidal Category, Theory and Applications of Categories, Vol. 9, 2001, No. 4, pp 61-91, who remark that one triangle equation of Pareigis is redundant.

The presentation is close to the definitions in the paper "Second-Order and Dependently-Sorted Abstract Syntax" by Marcelo Fiore (2008). The order of the arguments of the action functor has been chosen differently from Janelidze & Kelly, but as in Pareigis.

Author of nearly all of the proof lines: Ralph Matthes 2021

the original definition by Pareigis has a second triangle equation that is redundant in the context of action_triangle_eq and action_pentagon_eq (see Janelidze and Kelly 2001 for this claim)

Definition action_second_triangle_eq (ϱ : action_right_unitor) (χ : action_convertor) :=
  ∏ (a : A ), ∏ (v : Mon_V ), ϱ (a ⊙ v) = (χ ((a , v ), I )) · (id a ) #⊙ (ρ' v ).

Definition action_pentagon_eq (χ : action_convertor) := ∏ (a : A ), ∏ (u v w : Mon_V ),
  (χ ((a ⊙ u , v ), w )) · (χ ((a , u ), v ⊗ w )) =
  (χ ((a , u ), v )) #⊙ (id w ) · (χ ((a , u ⊗ v ), w )) · (id a ) #⊙ (α' ((u , v ), w )).

End Actions_Natural_Transformations.

Definition action : UU := ∑ (odot : A ⊠ Mon_V ⟶ A ), ∑ (ϱ : action_right_unitor odot ), ∑ (χ : action_convertor odot ), (action_triangle_eq odot ϱ χ ) × (action_pentagon_eq odot χ ).

Section Projections.

  Context (actn : action).

  Definition act_odot : A ⊠ Mon_V ⟶ A := pr1 actn.
  Definition act_ϱ : action_right_unitor act_odot := pr1 (pr2 actn).
  Definition act_χ : action_convertor act_odot := pr1 (pr2 (pr2 actn)).
  Definition act_triangle : action_triangle_eq act_odot act_ϱ act_χ := pr1 (pr2 (pr2 (pr2 actn))).
  Definition act_pentagon : action_pentagon_eq act_odot act_χ := pr2 (pr2 (pr2 (pr2 actn))).

End Projections.

Section Alternative_Definition.

we are following the introductory pages of Janelidze and Kelly, A note on actions of a monoidal category, Theory and Applications of Categories, Vol. 9, No. 4, 2001, pp. 61–91.

  Let Mon_EndA : monoidal_cat := monoidal_cat_of_endofunctors A.

  Context (FF: strong_monoidal_functor Mon_V Mon_EndA).

  Let ϵ : functor_identity A ⟹ (FF I: functor A A )
    := lax_monoidal_functor_ϵ FF.
  Let ϵ_inv : (FF I: functor A A ) ⟹ functor_identity A := strong_monoidal_functor_ϵ_inv FF.
  Let μ := lax_monoidal_functor_μ FF.
  Let ϵ_is_z_iso := strong_monoidal_functor_ϵ_is_z_iso FF.
  Let μ_is_nat_z_iso := strong_monoidal_functor_μ_is_nat_z_iso FF.
  Let FFunital := lax_monoidal_functor_unital FF.
  Let FFassoc := lax_monoidal_functor_assoc FF.

  Local Definition odot : functor (category_binproduct A Mon_V) A := uncurry_functor _ _ _ FF.

  Local Definition aux ρ : nat_z_iso (odot_I_functor odot) (FF I: functor A A).
  Proof.
    use make_nat_z_iso.
    - use tpair.
      + intro F. apply identity.
      + cbn. intros F F' α.
        unfold functor_fix_snd_arg_data. cbn.
        rewrite id_left, id_right.
        assert (H := functor_id FF I).
        apply (maponpaths (fun f ⇒ pr1 f F')) in H.
        etrans.
        { apply maponpaths. exact H. }
        apply id_right.
    - intro F.
      use make_is_z_isomorphism.
      + apply identity.
      + split; apply id_left.
  Defined.

  Local Definition ϱ : action_right_unitor odot.
  Proof.
    eapply nat_z_iso_comp.
    - exact aux ρ.
    - use make_nat_z_iso.
      + exact ϵ_inv.
      + use nat_trafo_pointwise_z_iso_if_z_iso; [apply A |].
        apply is_z_isomorphism_inv.
  Defined.

  Local Definition aux χ _dom : nat_z_iso (odot_x_odot_y_functor odot) (functor_composite (precategory_binproduct_unassoc A Mon_V Mon_V) (uncurry_functor _ _ _ (monoidal_functor_map_dom Mon_V Mon_EndA FF))).
  Proof.
    use make_nat_z_iso.
    - use make_nat_trans.
      + intro auv.
        apply identity.
      + intros auv auv' fgg'.
        rewrite id_left, id_right.
        cbn.
        rewrite functor_comp.
        rewrite <- assoc.
        apply idpath.
    - intro auv.
      use make_is_z_isomorphism.
      + apply identity.
      + split; apply id_left.
  Defined.

  Local Definition aux χ _codom : nat_z_iso (functor_composite (precategory_binproduct_unassoc A Mon_V Mon_V)
            (uncurry_functor _ _ _ (monoidal_functor_map_codom Mon_V Mon_EndA FF))) (odot_x_otimes_y_functor odot).
  Proof.
    use make_nat_z_iso.
    - use make_nat_trans.
      + intro auv.
        apply identity.
      + intros auv auv' fgg'.
        rewrite id_left, id_right.
        apply idpath.
    - intro auv.
      use make_is_z_isomorphism.
      + apply identity.
      + split; apply id_left.
  Defined.

  Local Definition χ : action_convertor odot.
  Proof.
    refine (nat_z_iso_comp aux χ _dom _).
    refine (nat_z_iso_comp _ aux χ _codom).
    use make_nat_z_iso.
    - exact (pre_whisker (precategory_binproduct_unassoc _ _ _) (uncurry_nattrans _ _ _ μ)).
    - intro auv. induction auv as [[a u] v].
      unfold pre_whisker. cbn.
      exact (nat_trafo_pointwise_z_iso_if_z_iso A _ (μ_is_nat_z_iso (u,,v)) a).
  Defined.

  Lemma action_triangle_eq_from_alt: action_triangle_eq odot ϱ χ.
  Proof.
    intros a v.
    cbn.
    unfold functor_fix_fst_arg_ob.
    rewrite id_left.
    rewrite functor_id.
    do 2 rewrite id_left.
    rewrite id_right.
    assert (Hunital1 := pr1 (FFunital v)).
    apply (maponpaths pr1) in Hunital1.
    apply toforallpaths in Hunital1.
    assert (Hunital1inst := Hunital1 a).
    cbn in Hunital1inst.
    rewrite id_right in Hunital1inst.
    unfold MonoidalFunctors.λ_C in Hunital1inst.
    apply pathsinv0.
    transparent assert (aux: (is_z_isomorphism (# (FF v: functor A A ) (ϵ_inv a )))).
    { apply functor_on_is_z_isomorphism.
      transparent assert (aux1: (is_nat_z_iso ϵ_inv)).
      { use nat_trafo_pointwise_z_iso_if_z_iso; [apply A |].
        apply is_z_iso_inv_from_z_iso. }
      apply aux1.
    }
    apply (z_iso_inv_to_left(C:=A) _ _ _ (# (FF v: functor A A ) (ϵ_inv a ),,aux)).
    unfold inv_from_z_iso.
    cbn.
    rewrite assoc.
    apply pathsinv0.
    etrans.
    2: { exact Hunital1inst. }
    assert (aux2 := functor_id FF v).
    apply (maponpaths pr1) in aux2.
    apply toforallpaths in aux2.
    exact (aux2 a).
  Qed.

  Lemma action_pentagon_eq_from_alt: action_pentagon_eq odot χ.
  Proof.
    intros a x y z.
    cbn.
    rewrite functor_id.
    do 5 rewrite id_left.
    do 4 rewrite id_right.
    assert (aux := functor_id FF z).
    apply (maponpaths pr1) in aux.
    apply toforallpaths in aux.
    rewrite aux.
    cbn.
    rewrite id_right.
    assert (Hassoc := FFassoc x y z).
    apply (maponpaths pr1) in Hassoc.
    apply toforallpaths in Hassoc.
    assert (Hassocinst := Hassoc a).
    clear Hassoc.
    cbn in Hassocinst.
    rewrite id_right, id_left in Hassocinst.
    do 2 rewrite functor_id in Hassocinst.
    rewrite id_left in Hassocinst.
    apply pathsinv0.
    exact Hassocinst.
  Qed.

  Definition action_from_alt: action.
  Proof.
    ∃ odot. ∃ ϱ. ∃ χ. exact (action_triangle_eq_from_alt ,, action_pentagon_eq_from_alt).
  Defined.

one might also consider the other direction: that an action gives rise to a strong monoidal functor from Mon_V to Mon_EndA, showing that the "concrete" action definition adhered to in the further development is also complete w.r.t. that "generic" definition

End Alternative_Definition.

End Actions_Definition.

Definition tensorial_action : action Mon_V.
Proof.
  ∃ tensor.
  ∃ ρ'.
  ∃ α'.
  exact (monoidal_cat_eq Mon_V).
Defined.

Section Strong_Monoidal_Functor_Action.

Context {Mon_A : monoidal_cat}.

Local Definition I_A : Mon_A := monoidal_cat_unit Mon_A.
Local Definition tensor_A : Mon_A ⊠ Mon_A ⟶ Mon_A := monoidal_cat_tensor Mon_A.
Notation "X ⊗_A Y" := (tensor_A (X , Y)) (at level 31).
Notation "f #⊗_A g" := (#tensor_A (f #, g )) (at level 31).
Local Definition α_A : associator tensor_A := monoidal_cat_associator Mon_A.
Local Definition λ_A : left_unitor tensor_A I_A := monoidal_cat_left_unitor Mon_A.
Local Definition ρ _A : right_unitor tensor_A I_A := monoidal_cat_right_unitor Mon_A.
Local Definition triangle_eq_A : triangle_eq tensor_A I_A λ_A ρ _A α_A := pr1 (monoidal_cat_eq Mon_A).
Local Definition pentagon_eq_A : pentagon_eq tensor_A α_A := pr2 (monoidal_cat_eq Mon_A).

Context (U : strong_monoidal_functor Mon_V Mon_A).

Definition otimes_U_functor : Mon_A ⊠ Mon_V ⟶ Mon_A := functor_composite (pair_functor (functor_identity _) U) tensor_A.

Lemma otimes_U_functor_ok: functor_on_objects otimes_U_functor =
  λ av , ob1 av ⊗_A U (ob2 av).
Proof.
  apply idpath.
Qed.

Definition U_action_ρ _nat_trans : odot_I_functor Mon_A otimes_U_functor ⟹ functor_identity Mon_A.
  refine (nat_trans_comp _ _ _ _ ρ _A).
  unfold odot_I_functor.
  set (aux := nat_trans_from_functor_fix_snd_morphism_arg _ _ _ tensor_A _ _ (strong_monoidal_functor_ϵ_inv U)).
  use tpair.
  - intro a.
    apply (aux a).
  - cbn; red.
    intros a a' f.
    cbn.
    rewrite functor_id.
    exact (pr2 aux a a' f).
Defined.

Lemma U_action_ρ _nat_trans_ok: nat_trans_data_from_nat_trans U_action_ρ _nat_trans = λ x , id x #⊗_A (strong_monoidal_functor_ϵ_inv U ) · ρ _A x.
Proof.
  apply idpath.
Qed.

Definition U_action_ρ _is_nat_z_iso : is_nat_z_iso U_action_ρ _nat_trans.
Proof.
  intro.
  cbn.
  use is_z_iso_comp_of_is_z_isos.
  - use is_z_iso_tensor_z_iso.
    + exact (identity_is_z_iso _ ).
    + apply (is_z_iso_inv_from_z_iso _ _ (make_z_iso _ _ (strong_monoidal_functor_ϵ_is_z_iso U))).
  - exact (pr2 ρ _A c).
Defined.

Definition U_action_ρ : action_right_unitor Mon_A otimes_U_functor := make_nat_z_iso _ _ U_action_ρ _nat_trans U_action_ρ _is_nat_z_iso.

Definition U_action_χ _nat_trans : odot_x_odot_y_functor Mon_A otimes_U_functor ⟹ odot_x_otimes_y_functor Mon_A otimes_U_functor.
Proof.
  apply (nat_trans_comp _ _ _ (pre_whisker (pair_functor (pair_functor (functor_identity _) U) U) α_A)).
  exact (pre_whisker (precategory_binproduct_unassoc _ _ _) (post_whisker_fst_param (lax_monoidal_functor_μ U) tensor_A)).
Defined.

Lemma U_action_χ _nat_trans_ok: nat_trans_data_from_nat_trans U_action_χ _nat_trans =
  λ x , let k := ob1 (ob1 x) in
       let k' := ob2 (ob1 x) in
       let k'' := ob2 x in
       α_A ((k , U k'), U k'') · id k #⊗_A (lax_monoidal_functor_μ U (k', k'')).
Proof.
  apply idpath.
Qed.

Lemma U_action_χ _is_nat_z_iso : is_nat_z_iso U_action_χ _nat_trans.
Proof.
  intro x.
  pose (k := ob1 (ob1 x)); pose (k' := ob2 (ob1 x)); pose (k'' := ob2 x).
  use is_z_iso_comp_of_is_z_isos.
  - exact (pr2 α_A ((k, U k'), U k'')).
  - use is_z_iso_tensor_z_iso.
    + use identity_is_z_iso.
    + exact (strong_monoidal_functor_μ_is_nat_z_iso U (k', k'')).
Defined.

Definition U_action_χ : action_convertor Mon_A otimes_U_functor :=
  make_nat_z_iso _ _ U_action_χ _nat_trans U_action_χ _is_nat_z_iso.

Lemma U_action_tlaw : action_triangle_eq Mon_A otimes_U_functor U_action_ρ U_action_χ.
Proof.
  red.
  intros a x.
  cbn.
  unfold nat_trans_from_functor_fix_snd_morphism_arg_data.
  unfold nat_trans_data_post_whisker_fst_param.
  cbn.
  unfold make_dirprod.
  rewrite functor_id.
  apply pathsinv0.
  etrans.
  { rewrite assoc'. apply maponpaths. apply pathsinv0. apply functor_comp. }
  unfold compose at 2. simpl. unfold make_dirprod. rewrite id_left.
  rewrite <- (id_left (id U x)).
  apply pathsinv0.
  intermediate_path (# tensor_A ((# tensor_A (id a #, strong_monoidal_functor_ϵ_inv U )) #, id U x ) · # tensor_A (ρ _A a #, id U x )).
  { rewrite <- functor_comp.
    apply idpath. }
  pose (f := # tensor_A (# tensor_A (id a #, lax_monoidal_functor_ϵ U ) #, id U x )).
  apply (pre_comp_with_z_iso_is_inj'(f:=f)).
  { use is_z_iso_tensor_z_iso.
    - use is_z_iso_tensor_z_iso.
      + exact (identity_is_z_iso _).
      + exact (strong_monoidal_functor_ϵ_is_z_iso U).
    - exact (identity_is_z_iso _ ).
  }
  rewrite assoc.
  intermediate_path (# tensor_A (ρ _A a #, id U x )).
  { apply pathsinv0. etrans.
    - apply (!(id_left _)).
    - apply cancel_postcomposition.
      unfold f.
      rewrite <- functor_comp.
      apply pathsinv0. apply functor_id_id.
      apply pathsdirprod; simpl.
      + etrans.
        × apply pathsinv0. apply functor_comp.
        × apply functor_id_id.
          apply pathsdirprod; simpl.
          -- apply id_left.
          -- apply pathsinv0. apply z_iso_inv_on_left.
             rewrite id_left. apply idpath.
      + apply id_left.
  }

  rewrite assoc.
  apply pathsinv0. etrans.
  { apply cancel_postcomposition.
    apply (nat_trans_ax α_A ((a, I_A ), U x) ((a, U I ), U x) ((id a ,, lax_monoidal_functor_ϵ U ) ,, id U x)). }
  simpl.
  etrans.
  { rewrite assoc'. apply maponpaths. apply pathsinv0.
    apply functor_comp. }
  unfold compose at 2. simpl. unfold make_dirprod. rewrite id_left.
  rewrite assoc.
  etrans.
  - apply maponpaths.
    eapply (maponpaths (fun u: Mon_A ⟦I_A ⊗_A (U x), U x⟧ ⇒ # tensor_A (id a #, u ))).
    apply pathsinv0.
    apply (lax_monoidal_functor_unital U x).
  - fold λ_A.
    apply pathsinv0.
    apply triangle_eq_A.
Qed.

Lemma U_action_plaw : action_pentagon_eq Mon_A otimes_U_functor U_action_χ.
Proof.
  red.
  intros a x y z.
  cbn.
  unfold nat_trans_data_post_whisker_fst_param.
  unfold ob1, ob2.
  cbn.
  rewrite functor_id.
  apply pathsinv0. etrans.
  { repeat rewrite assoc'.
    apply maponpaths.
    apply maponpaths.
    apply pathsinv0.
    apply functor_comp.
  }
  unfold compose at 4. cbn. unfold make_dirprod.
  rewrite id_left.
  etrans.
  { rewrite assoc.
    apply cancel_postcomposition.
    apply cancel_postcomposition.
    rewrite <- (id_left (id U z)).
    intermediate_path (# tensor_A ((α_A ((a , U x ), U y ) #, id U z ) · (# tensor_A (id a #, lax_monoidal_functor_μ U (x , y )) #, id U z ))).
    - apply idpath.
    - apply functor_comp.
  }
  etrans.
  { apply cancel_postcomposition.
    rewrite assoc'.
    apply maponpaths.
    apply (nat_trans_ax α_A ((a, U x ⊗_A U y), U z) ((a, U (x ⊗ y)), U z) ((id a ,, lax_monoidal_functor_μ U (x, y)) ,, id U z)).
  }
  etrans.
  { unfold assoc_right. cbn.
    rewrite assoc'.
    apply maponpaths.
    rewrite assoc'.
    apply maponpaths.
    apply pathsinv0.
    apply functor_comp.
  }
  unfold compose at 3. cbn. unfold make_dirprod.
  rewrite id_left.
  etrans.
  { do 2 apply maponpaths.
    rewrite assoc.
    eapply (maponpaths (fun u: Mon_A ⟦(U x ⊗_A U y) ⊗_A U z, U (x ⊗ (y ⊗ z))⟧ ⇒ id a #⊗_A u)).
    apply (lax_monoidal_functor_assoc U).
  }
  fold α_A. fold tensor_A. fold tensor.
  etrans.
  { rewrite assoc. apply maponpaths.
    rewrite assoc'.
    rewrite <- (id_left (id a)).
    intermediate_path (# tensor_A ((id a #, α_A ((U x , U y ), U z )) · (id a #, # tensor_A (id U x #, lax_monoidal_functor_μ U (y , z )) · lax_monoidal_functor_μ U (x , y ⊗ z )))).
    2: { apply functor_comp. }
    apply idpath.
  }
  etrans.
  { do 2 apply maponpaths.
    rewrite <- (id_left (id a)).
    intermediate_path (# tensor_A ((id a #, # tensor_A (id U x #, lax_monoidal_functor_μ U (y , z ))) · (id a #, lax_monoidal_functor_μ U (x , y ⊗ z )))).
    2: { apply functor_comp. }
    apply idpath.
  }
  repeat rewrite assoc.
  apply cancel_postcomposition.
  etrans.
  { apply cancel_postcomposition.
    apply pathsinv0.
    apply pentagon_eq_A.
  }

  repeat rewrite assoc'.
  apply maponpaths.
  etrans.
  { apply pathsinv0.
    apply (nat_trans_ax α_A ((a, U x), U y ⊗_A U z) ((a, U x), U (y ⊗ z)) ((id a ,, id U x) ,, lax_monoidal_functor_μ U (y, z))).
  }
  cbn. unfold make_dirprod.
  apply cancel_postcomposition.
  change (# tensor_A (# tensor_A (id (a , U x )) #, lax_monoidal_functor_μ U (y , z )) = # tensor_A (id (a ⊗_A U x ) #, lax_monoidal_functor_μ U (y , z ))).
  rewrite functor_id.
  apply idpath.
Qed.

Definition U_action : action Mon_A.
  ∃ otimes_U_functor.
  ∃ U_action_ρ.
  ∃ U_action_χ.
  split.
  - exact U_action_tlaw.
  - exact U_action_plaw.
Defined.

End Strong_Monoidal_Functor_Action.

End A.

Arguments act_odot {_ _} _.
Arguments act_ϱ {_ _} _.
Arguments act_χ {_ _} _.
Arguments act_triangle {_ _} _.
Arguments act_pentagon {_ _} _.