Library UniMath.CategoryTheory.whiskering
Whiskering
Contents :
- Precomposition with a functor for
- functors and
- natural transformations (whiskering)
- Functoriality of precomposition / postcomposition
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Lemma is_nat_trans_pre_whisker (A B C : precategory_data)
(F : functor_data A B) (G H : functor_data B C) (gamma : nat_trans G H) :
is_nat_trans
(functor_composite_data F G)
(functor_composite_data F H)
(λ a : A, gamma (F a)).
Show proof.
Definition pre_whisker {A B C : precategory_data}
(F : functor_data A B) {G H : functor_data B C} (gamma : nat_trans G H) :
nat_trans (functor_composite_data F G) (functor_composite_data F H).
Show proof.
Lemma pre_whisker_iso_is_iso {A B C : precategory_data}
(F : functor_data A B) {G H : functor_data B C} (gamma : nat_trans G H)
(X : is_nat_iso gamma)
: is_nat_iso (pre_whisker F gamma).
Show proof.
intros a.
apply X.
apply X.
Lemma pre_whisker_on_nat_z_iso {A B C : precategory_data}
(F : functor_data A B) {G H : functor_data B C} (gamma : nat_trans G H)
(X : is_nat_z_iso gamma)
: is_nat_z_iso (pre_whisker F gamma).
Show proof.
intros a.
apply X.
apply X.
Definition pre_whisker_in_funcat (A B C : category)
(F : [A, B]) {G H : [B, C]} (γ : [B, C]⟦G, H⟧) :
[A, C]⟦functor_compose F G, functor_compose F H⟧.
Show proof.
Postwhiskering
Lemma is_nat_trans_post_whisker (B C D : precategory_data)
(G H : functor_data B C) (gamma : nat_trans G H)
(K : functor C D):
is_nat_trans (functor_composite_data G K)
(functor_composite_data H K)
(λ b : B, #K (gamma b)).
Show proof.
unfold is_nat_trans.
simpl in *.
intros;
repeat rewrite <- functor_comp.
rewrite (nat_trans_ax gamma).
apply idpath.
simpl in *.
intros;
repeat rewrite <- functor_comp.
rewrite (nat_trans_ax gamma).
apply idpath.
Definition post_whisker {B C D : precategory_data}
{G H : functor_data B C} (gamma : nat_trans G H)
(K : functor C D)
: nat_trans (functor_composite_data G K) (functor_composite_data H K).
Show proof.
Lemma post_whisker_iso_is_iso {B C D : precategory}
{G H : functor_data B C} (gamma : nat_trans G H)
(K : functor C D)
(X : is_nat_iso gamma)
: is_nat_iso (post_whisker gamma K).
Show proof.
intros b.
unfold post_whisker.
simpl.
set ( gammab := make_iso (gamma b) (X b) ).
apply (functor_on_iso_is_iso C D K _ _ gammab).
unfold post_whisker.
simpl.
set ( gammab := make_iso (gamma b) (X b) ).
apply (functor_on_iso_is_iso C D K _ _ gammab).
Lemma post_whisker_z_iso_is_z_iso {B C D : precategory}
{G H : functor_data B C} (gamma : nat_trans G H)
(K : functor C D)
(X : is_nat_z_iso gamma)
: is_nat_z_iso (post_whisker gamma K).
Show proof.
Definition post_whisker_in_funcat (B C D : category)
{G H : [B, C]} (γ : [B, C]⟦G, H⟧) (K : [C, D]) :
[B, D]⟦functor_compose G K, functor_compose H K⟧.
Show proof.
Precomposition with a functor is functorial
Definition pre_composition_functor_data (A B C : category)
(H : ob [A, B]) : functor_data [B, C] [A, C].
Show proof.
Lemma pre_whisker_identity (A B : precategory_data) (C : category)
(H : functor_data A B) (G : functor_data B C)
: pre_whisker H (nat_trans_id G) =
nat_trans_id (functor_composite_data H G).
Show proof.
Lemma pre_whisker_composition (A B : precategory_data) (C : category)
(H : functor_data A B) (a b c : functor_data B C)
(f : nat_trans a b) (g : nat_trans b c)
: pre_whisker H (nat_trans_comp _ _ _ f g) =
nat_trans_comp _ _ _ (pre_whisker H f) (pre_whisker H g).
Show proof.
Lemma pre_composition_is_functor (A B C : category) (H : [A, B]) :
is_functor (pre_composition_functor_data A B C H).
Show proof.
split; simpl in *.
- unfold functor_idax .
intros.
apply pre_whisker_identity.
- unfold functor_compax .
intros.
apply pre_whisker_composition.
- unfold functor_idax .
intros.
apply pre_whisker_identity.
- unfold functor_compax .
intros.
apply pre_whisker_composition.
Definition pre_composition_functor (A B C : category) (H : [A , B]) : functor [B, C] [A, C].
Show proof.
Definition pre_comp_functor {A B C: category} :
[A, B] → [B, C] ⟶ [A, C] :=
pre_composition_functor _ _ _.
Postcomposition with a functor is functorial
Definition post_composition_functor_data (A B C : category)
(H : ob [B, C]) : functor_data [A, B] [A, C].
Show proof.
Lemma post_whisker_identity (A B : precategory) (C : category)
(H : functor B C) (G : functor_data A B)
: post_whisker (nat_trans_id G) H =
nat_trans_id (functor_composite_data G H).
Show proof.
apply nat_trans_eq.
- apply homset_property.
- intro a. unfold post_whisker. simpl.
apply functor_id.
- apply homset_property.
- intro a. unfold post_whisker. simpl.
apply functor_id.
Lemma post_whisker_composition (A B : precategory) (C : category)
(H : functor B C) (a b c : functor_data A B)
(f : nat_trans a b) (g : nat_trans b c)
: post_whisker (nat_trans_comp _ _ _ f g) H =
nat_trans_comp _ _ _ (post_whisker f H) (post_whisker g H).
Show proof.
Lemma post_composition_is_functor (A B C : category) (H : [B, C]) :
is_functor (post_composition_functor_data A B C H).
Show proof.
split; simpl in *.
- unfold functor_idax .
intros.
apply post_whisker_identity.
- unfold functor_compax .
intros.
apply post_whisker_composition.
- unfold functor_idax .
intros.
apply post_whisker_identity.
- unfold functor_compax .
intros.
apply post_whisker_composition.
Definition post_composition_functor (A B C : category) (H : [B , C]) : functor [A, B] [A, C].
Show proof.
Definition post_comp_functor {A B C : category} :
[B, C] → [A, B] ⟶ [A, C] :=
post_composition_functor _ _ _.
Lemma pre_whisker_nat_z_iso
{C D E : category} (F : functor C D)
{G1 G2 : functor D E} (α : nat_z_iso G1 G2)
: nat_z_iso (functor_composite F G1) (functor_composite F G2).
Show proof.
Lemma post_whisker_nat_z_iso
{C D E : category}
{G1 G2 : functor C D} (α : nat_z_iso G1 G2) (F : functor D E)
: nat_z_iso (functor_composite G1 F) (functor_composite G2 F).
Show proof.