src/RepresentableStructure_ch7_2.v

   1 (*******************************************************************************)
   2 (* Chapter 7.2: Representable Structure                                        *)
   3 (*******************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import Categories_ch1_3.
   8 Require Import Functors_ch1_4.
   9 Require Import Isomorphisms_ch1_5.
  10 Require Import EpicMonic_ch2_1.
  11 Require Import ProductCategories_ch1_6_1.
  12 Require Import OppositeCategories_ch1_6_2.
  13 Require Import Enrichment_ch2_8.
  14 Require Import Subcategories_ch7_1.
  15 Require Import NaturalTransformations_ch7_4.
  16 Require Import NaturalIsomorphisms_ch7_5.
  17 Require Import MonoidalCategories_ch7_8.
  18 Require Import Coherence_ch7_8.
  19
  20 Section RepresentableStructure.
  21   Context `(ec:ECategory(mn:=mn)(V:=V)).
  22
  23   Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
  24   Definition hom_covariant     {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
  25
  26   Lemma hom_covariant_distributes     {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
  27      : hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
  28      set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
  29      unfold hom_covariant.
  30      repeat setoid_rewrite associativity.
  31      apply comp_respects; try reflexivity.
  32      set (@ecomp_is_functorial) as qq.
  33      repeat setoid_rewrite associativity in qq.
  34      apply qq.
  35      Qed.
  36
  37   (*
  38   Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d)
  39      : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f.
  40      etransitivity.
  41      unfold hom_covariant.
  42      unfold hom_contravariant.
  43      Defined.
  44
  45   Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b)
  46         : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)).
  47     destruct a as [a1 a2].
  48     destruct b as [b1 b2].
  49     case f as [f1 f2]; intros.
  50     exact ( hom_contravariant (a:=a2) f1 >>> hom_covariant (a:=b1) f2 ).
  51     Defined.
  52
  53   Definition YonedaBiFunctor : Functor (ec⁽ºᑭ⁾ ×× ec) V (fun a => (fst_obj _ _ a)~~>(snd_obj _ _ a)).
  54     refine {| fmor := fun a b f => YonedaBiFunctor_fmor a b f |}.
  55     abstract (intros; destruct a; destruct b; destruct f;
  56               destruct f';
  57               destruct H;
  58               repeat (apply comp_respects; try reflexivity); simpl;
  59               [ apply (@fmor_respects _ _ _ _ _ _ (fun x => (bin_obj x _))); auto
  60               | apply (fmor_respects ((o1 ~~> o0) ⋊-)); auto ]).
  61     abstract (
  62       destruct a; unfold YonedaBiFunctor_fmor;
  63       unfold hom_covariant;
  64       unfold hom_contravariant;
  65       etransitivity; simpl;
  66       [ apply comp_respects; setoid_rewrite associativity; simpl;
  67         [ etransitivity; [ apply comp_respects; [ reflexivity | apply eleft_identity ] | apply iso_comp2 ]
  68         | etransitivity; [ apply comp_respects; [ reflexivity | apply eright_identity ] | apply iso_comp2 ]
  69         ]
  70       | apply left_identity ]
  71       ).
  72     abstract (destruct a; destruct b; destruct c;
  73               destruct f;
  74               destruct g; unfold YonedaBiFunctor_fmor;
  75               setoid_rewrite juggle3;
  76               setoid_rewrite hom_swap;
  77               setoid_rewrite <- juggle3;
  78               setoid_rewrite <- hom_contravariant_distributes;
  79               setoid_rewrite <- hom_covariant_distributes;
  80               simpl;
  81               apply comp_respects;
  82               reflexivity).
  83     Defined.
  84
  85   Definition HomFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
  86   *)
  87
  88   Definition HomFunctor   (X:ec) : Functor ec     V (ehom X).
  89     refine {| fmor := @hom_covariant X |}.
  90     intros.
  91       unfold hom_covariant.
  92       apply comp_respects; try reflexivity.
  93       apply comp_respects; try reflexivity.
  94       apply fmor_respects; auto.
  95     intros.
  96       unfold hom_covariant.
  97       apply (epic _ (iso_epic ((pmon_cancelr mn) (X ~~> a)))).
  98       setoid_rewrite <- associativity.
  99       setoid_rewrite <- associativity.
 100       setoid_rewrite iso_comp1.
 101       setoid_rewrite left_identity.
 102       setoid_rewrite right_identity.
 103       apply (@eright_identity).
 104     intros.
 105       symmetry.
 106       apply hom_covariant_distributes.
 107       Defined.
 108
 109   Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).
 110     simpl.
 111     setoid_rewrite <- associativity.
 112     unfold hom_contravariant.
 113     repeat setoid_rewrite <- associativity.
 114     setoid_rewrite juggle1.
 115     setoid_rewrite eleft_identity.
 116     repeat setoid_rewrite <- associativity.
 117     setoid_rewrite juggle1.
 118     setoid_rewrite iso_comp1.
 119     setoid_rewrite right_identity.
 120     unfold hom_covariant.
 121     repeat setoid_rewrite <- associativity.
 122     set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (eid a)) as qq.
 123     simpl in qq.
 124     apply iso_shift_right' in qq.
 125     apply symmetry in qq.
 126     setoid_rewrite <- associativity in qq.
 127     apply iso_shift_left' in qq.
 128     apply symmetry in qq.
 129     setoid_rewrite qq.
 130     setoid_rewrite associativity.
 131     setoid_rewrite juggle3.
 132     setoid_rewrite (centralmor_first(CentralMorphism:=eid_central(ECategory:=ec) a)).
 133     repeat setoid_rewrite associativity.
 134     setoid_rewrite eleft_identity.
 135     set (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn) f) as qqq.
 136     simpl in qqq.
 137     setoid_rewrite <- qqq.
 138     setoid_rewrite <- associativity.
 139     set (coincide pmon_triangle) as qqqq.
 140     setoid_rewrite qqqq.
 141     setoid_rewrite iso_comp1.
 142     setoid_rewrite left_identity.
 143     set (@eqv_equivalence) as qmt.
 144     apply qmt.
 145     Qed.
 146
 147
 148 End RepresentableStructure.
 149 Opaque HomFunctor.
 150
 151 Structure MonoidalEnrichment {e:Enrichment} :=
 152 { me_enr         :=e
 153 ; me_fobj        : prod_obj e e -> e
 154 ; me_f           : Functor (e ×× e) e me_fobj
 155 ; me_i           : e
 156 ; me_mon         : MonoidalCat e me_fobj me_f me_i
 157 ; me_mf          : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i)
 158 }.
 159 Implicit Arguments MonoidalEnrichment [ ].
 160 Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
 161 Coercion me_enr : MonoidalEnrichment >-> Enrichment.
 162
 163 (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
 164 Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
 165 { ffme_enr             := me
 166 ; ffme_mf_full         : FullFunctor         (HomFunctor e (me_i me))
 167 ; ffme_mf_faithful     : FaithfulFunctor     (HomFunctor e (me_i me))
 168 ; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me))
 169 }.
 170 Implicit Arguments MonicMonoidalEnrichment [ ].
 171 Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
 172 Transparent HomFunctor.
 173
 174 Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
 175 { smme_se       : SurjectiveEnrichment e
 176 ; smme_monoidal : MonoidalEnrichment e
 177 ; smme_me       : MonicMonoidalEnrichment _ smme_monoidal
 178 }.
 179 Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
 180 Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
 181
 182 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
 183 Structure SMME :=
 184 { smme_e   : Enrichment
 185 ; smme_see : SurjectiveEnrichment smme_e
 186 ; smme_mon : MonoidalEnrichment smme_e
 187 ; smme_mee : MonicMonoidalEnrichment _ smme_mon
 188 }.
 189 Coercion smme_e   : SMME >-> Enrichment.
 190 Coercion smme_see : SMME >-> SurjectiveEnrichment.
 191 Coercion smme_mon : SMME >-> MonoidalEnrichment.
 192 Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.