src/SectionRetract_ch2_4.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6 Require Import ProductCategories_ch1_6_1.
   7 Require Import NaturalIsomorphisms_ch7_5.
   8
   9 (******************************************************************************)
  10 (* Chapter 2.4: Sections and Retractions                                      *)
  11 (******************************************************************************)
  12
  13 (* FIXME: do sections as well *)
  14
  15 Class RetractsInto `{C:Category} (A B:C) :=
  16 { retract_embed   : A~~{C}~~>B
  17 ; retract_project : B~~{C}~~>A
  18 ; retract_pf      : retract_embed >>> retract_project ~~ id _
  19 }.
  20 Notation "A ⊆ B" := (@RetractsInto _ _ _ A B) (at level 100).
  21 Implicit Arguments retract_embed   [ Ob Hom C A B ].
  22 Implicit Arguments retract_project [ Ob Hom C A B ].
  23
  24 (* Remark 2.14 *)
  25 Instance FunctorsPreserveRetracts `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj){a b:C}(r:a ⊆ b) : ((Fobj a) ⊆ (Fobj b)) :=
  26 { retract_embed   := F \ (retract_embed r)
  27 ; retract_project := F \ (retract_project r)
  28 }.
  29   setoid_rewrite (fmor_preserves_comp F).
  30   setoid_rewrite retract_pf.
  31   apply fmor_preserves_id.
  32   Defined.
  33
  34 Instance iso_retract `{CX:Category}(a b:CX)(i:a ≅ b) : (a ⊆ b) :=
  35 { retract_embed   := iso_forward i
  36 ; retract_project := iso_backward i
  37 }.
  38   apply (iso_comp1 i).
  39   Defined.
  40
  41 Instance retract_comp `{CX:Category}(a b c:CX)(r1:a ⊆ b)(r2:b ⊆ c) : (a ⊆ c) :=
  42 { retract_embed   := (retract_embed r1) >>> (retract_embed r2)
  43 ; retract_project := (retract_project r2) >>> (retract_project r1)
  44 }.
  45   setoid_rewrite juggle3.
  46   setoid_rewrite retract_pf.
  47   setoid_rewrite right_identity.
  48   apply retract_pf.
  49   Defined.
  50
  51 Instance retract_prod `{C:Category}`{D:Category}{a b:C}{d e:D}(r1:a ⊆ b)(r2:d ⊆ e)
  52   : @RetractsInto _ _ (C ×× D) (pair_obj a d) (pair_obj b e) :=
  53 { retract_embed   := pair_mor (pair_obj a d) (pair_obj b e) (retract_embed   r1) (retract_embed   r2)
  54 ; retract_project := pair_mor (pair_obj b e) (pair_obj a d) (retract_project r1) (retract_project r2)
  55 }.
  56   simpl; split; apply retract_pf.
  57   Defined.
  58
  59 Structure RetractionOfCategories `{C:Category} `{D:Category} :=
  60 { retraction_section_fobj       : C -> D
  61 ; retraction_section            : Functor C D retraction_section_fobj
  62 ; retraction_retraction_fobj    : D -> C
  63 ; retraction_retraction         : Functor D C retraction_retraction_fobj
  64 ; retraction_composes           : retraction_section >>>> retraction_retraction ≃ functor_id _
  65 }.
  66 Implicit Arguments RetractionOfCategories [ [Ob] [Hom] [Ob0] [Hom0] ].
  67 Coercion retraction_section : RetractionOfCategories >-> Functor.