Pushforward comodule

Definition

Section Pushforward_construction.

  Context `{F : Functor 𝒞 𝒟} {T S : RelativeComonad F}
           (τ : T ⇒ S) `(M : Comodule T ℰ).

  Program Definition pushforward : Comodule S ℰ ≔

Comodule.make	⦃ M	≔ M
	; mcobind	≔ λ C D ∙ λ f ↦ M ⋅mcobind (f ∘ τ(C)) ⦄.

solve_proper.

rewrite <- τ _counit. now rewrite mcobind_counit.

    now rewrite compose_assoc,
                <- τ _commutes,
                mcobind_mcobind,
                <- compose_assoc.

Section Functoriality.

  Context `{F : Functor 𝒞 𝒟} {T S : RelativeComonad F} {ℰ : Category} {M N : Comodule S ℰ}
          (τ : S ⇒ T) (α : M ⇒ N).

  Infix "⁎" ≔ pushforward (at level 0).

  Program Definition pushforward_mor : ‵ τ ⁎M ⇒ τ ⁎N ′ ≔
    Comodule.make ⦃ α ≔ α ⦄.
  Show proof.

now rewrite α_commutes.

End Functoriality.

Program Definition Pushforward
`{F : Functor 𝒞 𝒟} {T S : RelativeComonad F} (τ : T ⇒ S) {ℰ} : Functor (𝑹𝑪𝒐𝒎𝒐𝒅 T ℰ) (𝑹𝑪𝒐𝒎𝒐𝒅 S ℰ) ≔

Functor.make	⦃ F	≔ pushforward τ
	; map	≔ λ A B ∙ λ f ↦ pushforward_mor τ f ⦄.

intros f g eq_fg x. simpl. now apply eq_fg.

reflexivity.

reflexivity.

Notation "τ ⁎" ≔ (Pushforward τ) (at level 0).

Section tautological_comodule.

Context `{F : Functor 𝒞 𝒟} (T : RelativeComonad F).

Program Definition tcomod : Comodule T 𝒟 ≔

Comodule.make	⦃ M	≔ T
	; mcobind	≔ λ C D ∙ T ⋅cobind ⦄.

mcobind-counit

now rewrite cobind_counit.

mcobind-mcobind

now rewrite cobind_cobind.

End tautological_comodule.

Local Coercion tcomod : RelativeComonad >-> Comodule.
Notation "[ T ]" ≔ (tcomod T) (only parsing).

Section induced_morphism.

  Context `{F : Functor 𝒞 𝒟} {T S : RelativeComonad F}
          (τ : T ⇒ S).

  Program Definition induced_morphism : ‵ τ ⁎T ⇒ S ′ ≔
    Comodule.make ⦃ α ≔ λ C ∙ τ(C) ⦄.

α-commutes

now rewrite τ _commutes.

End induced_morphism.

Notation "⟨ τ ⟩" ≔ (induced_morphism τ) (at level 0).

Section Commutes.

  Context `{BinaryProduct 𝒞} `{BinaryProduct 𝒟} {F : Functor 𝒞 𝒟}
          {E : 𝒞} `{!CartesianStrongMonoidal F} {T S : RelativeComonadWithCut F E}
          {τ : T ⇒ S} `{M : Comodule T ℰ}.

  Program Definition Φ : ‵ τ ⁎(M [E ×─]) ⇒ (τ ⁎M )[E ×─] ′ ≔
    Comodule.make ⦃ α ≔ λ X ∙ id [M (E × X)] ⦄.
  Show proof.

    rewrite left_id, right_id.
    apply Π.cong.
    repeat rewrite compose_assoc.
    apply Π₂.cong; [ reflexivity |].
    rewrite ∘-×; apply Π₂.cong.
    rewrite compose_assoc; apply Π₂.cong; [ reflexivity |].
    apply τ _counit.
    rewrite compose_assoc. apply Π₂.cong; [ reflexivity |].
    symmetry. apply τ _cut.

End Commutes.