1 (*******************************************************************************)
2 (* Chapter 7.2: Representable Structure *)
3 (*******************************************************************************)
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 ProductCategories_ch1_6_1.
11 Require Import OppositeCategories_ch1_6_2.
12 Require Import Enrichment_ch2_8.
13 Require Import Subcategories_ch7_1.
14 Require Import NaturalTransformations_ch7_4.
15 Require Import NaturalIsomorphisms_ch7_5.
16 Require Import MonoidalCategories_ch7_8.
17 Require Import Coherence_ch7_8.
19 (* FIXME: an object is a Generator if its covariant representable functor is faithful *)
21 Section RepresentableStructure.
22 Context `(ec:ECategory(mn:=mn)(V:=V)).
24 Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
25 Definition hom_covariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
27 Lemma hom_covariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
28 : hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
29 set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
31 repeat setoid_rewrite associativity.
32 apply comp_respects; try reflexivity.
33 set (@ecomp_is_functorial) as qq.
34 repeat setoid_rewrite associativity in qq.
38 Lemma hom_contravariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
39 : hom_contravariant (f >>> g) ~~ (hom_contravariant g) >>> (hom_contravariant (a:=x) f).
40 set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
41 unfold hom_contravariant.
42 repeat setoid_rewrite associativity.
43 etransitivity; [ idtac | symmetry; apply associativity ].
44 apply comp_respects; try reflexivity.
45 set (@ecomp_is_functorial _ _ _ _ _ _ _ _ _ _ _ _ _ x f g) as qq.
46 setoid_rewrite juggle2 in qq.
50 Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d)
51 : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f.
54 unfold hom_contravariant.
57 Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b)
58 : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)).
59 destruct a as [a1 a2].
60 destruct b as [b1 b2].
61 case f as [f1 f2]; intros.
62 exact ( hom_contravariant (a:=a2) f1 >>> hom_covariant (a:=b1) f2 ).
65 Definition YonedaBiFunctor : Functor (ec⁽ºᑭ⁾ ×× ec) V (fun a => (fst_obj _ _ a)~~>(snd_obj _ _ a)).
66 refine {| fmor := fun a b f => YonedaBiFunctor_fmor a b f |}.
67 abstract (intros; destruct a; destruct b; destruct f;
70 repeat (apply comp_respects; try reflexivity); simpl;
71 [ apply (@fmor_respects _ _ _ _ _ _ (fun x => (bin_obj x _))); auto
72 | apply (fmor_respects ((o1 ~~> o0) ⋊-)); auto ]).
74 destruct a; unfold YonedaBiFunctor_fmor;
76 unfold hom_contravariant;
78 [ apply comp_respects; setoid_rewrite associativity; simpl;
79 [ etransitivity; [ apply comp_respects; [ reflexivity | apply eleft_identity ] | apply iso_comp2 ]
80 | etransitivity; [ apply comp_respects; [ reflexivity | apply eright_identity ] | apply iso_comp2 ]
82 | apply left_identity ]
84 abstract (destruct a; destruct b; destruct c;
86 destruct g; unfold YonedaBiFunctor_fmor;
87 setoid_rewrite juggle3;
88 setoid_rewrite hom_swap;
89 setoid_rewrite <- juggle3;
90 setoid_rewrite <- hom_contravariant_distributes;
91 setoid_rewrite <- hom_covariant_distributes;
97 Definition RepresentableFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
98 Definition RepresentableFunctor (X:ec) : Functor ec V (fun a => X~~>a) :=
99 func_llecnac(C:=ec⁽ºᑭ⁾)(D:=ec) X >>>> YonedaBiFunctor.
101 Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (RepresentableFunctor a \ f).
103 setoid_rewrite <- associativity.
104 unfold hom_contravariant.
105 repeat setoid_rewrite <- associativity.
106 setoid_rewrite juggle1.
107 setoid_rewrite eleft_identity.
108 repeat setoid_rewrite <- associativity.
109 setoid_rewrite juggle1.
110 setoid_rewrite iso_comp1.
111 setoid_rewrite right_identity.
112 unfold hom_covariant.
113 repeat setoid_rewrite <- associativity.
114 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (eid a)) as qq.
116 apply iso_shift_right' in qq.
117 apply symmetry in qq.
118 setoid_rewrite <- associativity in qq.
119 apply iso_shift_left' in qq.
120 apply symmetry in qq.
122 setoid_rewrite associativity.
123 setoid_rewrite juggle3.
124 setoid_rewrite (centralmor_first(CentralMorphism:=eid_central(ECategory:=ec) a)).
125 repeat setoid_rewrite associativity.
126 setoid_rewrite eleft_identity.
127 set (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn) f) as qqq.
129 setoid_rewrite <- qqq.
130 setoid_rewrite <- associativity.
131 set (coincide pmon_triangle) as qqqq.
133 setoid_rewrite iso_comp1.
134 setoid_rewrite left_identity.
135 set (@eqv_equivalence) as qmt.
140 End RepresentableStructure.
141 Opaque RepresentableFunctor.
143 Structure MonoidalEnrichment :=
144 { me_enr : Enrichment
145 ; me_fobj : prod_obj me_enr me_enr -> me_enr
146 ; me_f : Functor (me_enr ×× me_enr) me_enr me_fobj
148 ; me_mon : MonoidalCat me_enr me_fobj me_f me_i
149 ; me_mf : MonoidalFunctor me_mon (enr_v_mon me_enr) (RepresentableFunctor me_enr me_i)
151 Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
152 Coercion me_enr : MonoidalEnrichment >-> Enrichment.
154 (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
155 Structure MonicMonoidalEnrichment :=
156 { ffme_enr : MonoidalEnrichment
157 ; ffme_mf_full : FullFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
158 ; ffme_mf_faithful : FaithfulFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
159 ; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
161 Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
162 Transparent RepresentableFunctor.