Set Implicit Arguments. Unset Strict Implicit. Require Export freecat1. Require Export qcat1. Module GZ_Def. Export Free_Category. Export Quotient_Functor. Definition Forward := R (f_(o_(r_ DOT))). Definition Backward := R (b_(k_(d_ DOT))). Definition forward_arrow u := Arrow.create (source u) (target u) (pair Forward u). Definition backward_arrow u := Arrow.create (target u) (source u) (pair Backward u). Lemma source_forward_arrow : forall u, source (forward_arrow u) = source u. Proof. ir. uf forward_arrow. rww Arrow.source_create. Qed. Lemma target_forward_arrow : forall u, target (forward_arrow u) = target u. Proof. ir. uf forward_arrow. rww Arrow.target_create. Qed. Lemma source_backward_arrow : forall u, source (backward_arrow u) = target u. Proof. ir. uf backward_arrow. rww Arrow.source_create. Qed. Lemma target_backward_arrow : forall u, target (backward_arrow u) = source u. Proof. ir. uf backward_arrow. rww Arrow.target_create. Qed. Definition original_arrow u := pr2 (arrow u). Lemma original_arrow_forward_arrow : forall u, original_arrow (forward_arrow u) = u. Proof. ir. uf forward_arrow. uf original_arrow. rw Arrow.arrow_create. rww pr2_pair. Qed. Lemma original_arrow_backward_arrow : forall u, original_arrow (backward_arrow u) = u. Proof. ir. uf backward_arrow. uf original_arrow. rw Arrow.arrow_create. rww pr2_pair. Qed. Definition direction u := pr1 (arrow u). Lemma direction_forward_arrow : forall u, direction (forward_arrow u) = Forward. Proof. ir. uf forward_arrow. uf direction. rw Arrow.arrow_create. rww pr1_pair. Qed. Lemma direction_backward_arrow : forall u, direction (backward_arrow u) = Backward. Proof. ir. uf backward_arrow. uf direction. rw Arrow.arrow_create. rww pr1_pair. Qed. Definition multiplicative_system a s := Category.axioms a & (forall u, inc u s -> mor a u) & (forall u v, inc u s -> inc v s -> source u = target v -> inc (comp a u v) s). Definition loc_edges a s := union2 (Image.create (morphisms a) forward_arrow) (Image.create s backward_arrow). Lemma inc_loc_edges : forall a s u, multiplicative_system a s -> inc u (loc_edges a s) = ((exists y, (mor a y & u = forward_arrow y)) \/ (exists y, (mor a y & inc y s & u = backward_arrow y))). Proof. ir. ap iff_eq; ir. ufi loc_edges H0. cp (union2_or H0). nin H1. ap or_introl. rwi Image.inc_rw H1. nin H1. ee. sh x. ee. app is_mor_mor. uh H; ee; am. sy; am. ap or_intror. rwi Image.inc_rw H1. nin H1. ee. sh x. ee. uh H; ee. ap H3. am. am. sy; am. uf loc_edges. nin H0. ap union2_first. rw Image.inc_rw. nin H0. sh x; ee. app mor_is_mor. sy; am. ap union2_second. rw Image.inc_rw. nin H0. sh x; ee. am. sy; am. Qed. Definition gz_graph a s := Graph.create (objects a) (loc_edges a s). Lemma inc_vertices_gz_graph : forall a s x, multiplicative_system a s -> inc x (vertices (gz_graph a s)) = ob a x. Proof. ir. uf gz_graph. rw vertices_create. ap iff_eq; ir. ap is_ob_ob. uh H; ee; am. am. app ob_is_ob. Qed. Lemma inc_edges_gz_graph : forall a s u, multiplicative_system a s -> inc u (edges (gz_graph a s)) = inc u (loc_edges a s). Proof. ir. uf gz_graph. rw edges_create. tv. Qed. Lemma gz_graph_axioms : forall a s, multiplicative_system a s -> Graph.axioms (gz_graph a s). Proof. ir. uhg; ee. uf gz_graph. ap Graph.create_like. ir. rwi inc_edges_gz_graph H0. rwi inc_loc_edges H0. nin H0. nin H0. ee. rw H1. uf forward_arrow. rww Arrow.create_like. nin H0. ee. rw H2. uf backward_arrow. rww Arrow.create_like. am. am. ir. rwi inc_edges_gz_graph H0. rw inc_vertices_gz_graph. rwi inc_loc_edges H0. nin H0. nin H0. ee. rw H1. rw source_forward_arrow. rww ob_source. nin H0. ee. rw H2. rw source_backward_arrow. rww ob_target. am. am. am. ir. rwi inc_edges_gz_graph H0. rw inc_vertices_gz_graph. rwi inc_loc_edges H0. nin H0. nin H0. ee. rw H1. rw target_forward_arrow. rww ob_target. nin H0. ee. rw H2. rw target_backward_arrow. rww ob_source. am. am. am. Qed. Definition gz_freecat a s := freecat (gz_graph a s). Lemma gz_freecat_axioms : forall a s, multiplicative_system a s -> Category.axioms (gz_freecat a s). Proof. ir. uf gz_freecat. app freecat_axioms. app gz_graph_axioms. Qed. Lemma ob_gz_freecat : forall a s x, multiplicative_system a s -> ob (gz_freecat a s) x = ob a x. Proof. ir. uf gz_freecat. rw ob_freecat_rw. rw inc_vertices_gz_graph. tv. am. app gz_graph_axioms. Qed. Lemma mor_gz_freecat : forall a s u, multiplicative_system a s -> mor (gz_freecat a s) u = mor_freecat (gz_graph a s) u. Proof. ir. uf gz_freecat. rw mor_freecat_rw. tv. app gz_graph_axioms. Qed. Lemma comp_gz_freecat : forall a s u v, multiplicative_system a s -> mor (gz_freecat a s) u -> mor (gz_freecat a s) v -> source u = target v -> comp (gz_freecat a s) u v = freecat_comp u v. Proof. ir. uf gz_freecat. rw comp_freecat. tv. ap gz_graph_axioms. am. am. am. am. Qed. Lemma id_gz_freecat : forall a s x, multiplicative_system a s -> ob a x -> id (gz_freecat a s) x = freecat_id x. Proof. ir. uf gz_freecat. rww id_freecat. app gz_graph_axioms. rw ob_freecat_rw. rww inc_vertices_gz_graph. app gz_graph_axioms. Qed. Definition forward_edge u := freecat_edge (forward_arrow u). Definition backward_edge u := freecat_edge (backward_arrow u). Lemma source_forward_edge : forall u, source (forward_edge u) = source u. Proof. ir. uf forward_edge. rw source_freecat_edge. rww source_forward_arrow. Qed. Lemma target_forward_edge : forall u, target (forward_edge u) = target u. Proof. ir. uf forward_edge. rw target_freecat_edge. rww target_forward_arrow. Qed. Lemma source_backward_edge : forall u, source (backward_edge u) = target u. Proof. ir. uf backward_edge. rw source_freecat_edge. rww source_backward_arrow. Qed. Lemma target_backward_edge : forall u, target (backward_edge u) = source u. Proof. ir. uf backward_edge. rw target_freecat_edge. rww target_backward_arrow. Qed. Lemma inc_forward_arrow_loc_edges : forall a s u, multiplicative_system a s ->mor a u -> inc (forward_arrow u) (loc_edges a s). Proof. ir. rw inc_loc_edges. ap or_introl. sh u. ee. am. tv. am. Qed. Lemma inc_backward_arrow_loc_edges : forall a s q, multiplicative_system a s ->inc q s -> inc (backward_arrow q) (loc_edges a s). Proof. ir. rw inc_loc_edges. ap or_intror. sh q. ee. uh H; ee; au. am. tv. am. Qed. Lemma mor_forward_edge : forall a s u, multiplicative_system a s -> mor a u -> mor (gz_freecat a s) (forward_edge u). Proof. ir. uf forward_edge. rw mor_gz_freecat. ap mor_freecat_edge. app gz_graph_axioms. rw inc_edges_gz_graph. app inc_forward_arrow_loc_edges. am. am. Qed. Lemma mor_backward_edge : forall a s q, multiplicative_system a s -> inc q s -> mor (gz_freecat a s) (backward_edge q). Proof. ir. uf backward_edge. rw mor_gz_freecat. ap mor_freecat_edge. app gz_graph_axioms. rw inc_edges_gz_graph. app inc_backward_arrow_loc_edges. am. am. Qed. Definition gz_rel a s := Z (coarse (gz_freecat a s)) (fun z => ((exists x, (ob a x & z = pair (forward_edge (id a x)) (freecat_id x))) \/ (exists q, (inc q s & z = pair (freecat_comp (forward_edge q) (backward_edge q)) (freecat_id (target q)))) \/ (exists q, (inc q s & z = pair (freecat_comp (backward_edge q) (forward_edge q)) (freecat_id (source q)))) \/ (exists u, exists v, (mor a u & mor a v & source u = target v & z = pair (freecat_comp (forward_edge u) (forward_edge v)) (forward_edge (comp a u v)))))). Lemma inc_coarse : forall a z, Category.axioms a -> inc z (coarse a) = (exists u, exists v, (mor a u & mor a v & source u = source v & target u = target v & z=pair u v)). Proof. ir. ap iff_eq; ir. ufi coarse H0. Ztac. cp (product_pr H1). ee. rwi is_pair_rw H4. sh (pr1 z). sh (pr2 z). ee. ap is_mor_mor. am. am. ap is_mor_mor. am. am. am. am. am. nin H0. nin H0. ee. rw H4. uf coarse. Ztac. ap product_inc. ap pair_is_pair. rw pr1_pair. app mor_is_mor. rw pr2_pair. app mor_is_mor. rw pr1_pair. rw pr2_pair. ee; am. Qed. Lemma inc_gz_rel : forall a s z, multiplicative_system a s -> inc z (gz_rel a s) = ((exists x, (ob a x & z = pair (forward_edge (id a x)) (freecat_id x)))\/ (exists q, (inc q s & z = pair (freecat_comp (forward_edge q) (backward_edge q)) (freecat_id (target q))))\/ (exists q, (inc q s & z = pair (freecat_comp (backward_edge q) (forward_edge q)) (freecat_id (source q))))\/ (exists u, exists v, (mor a u & mor a v & source u = target v & z = pair (freecat_comp (forward_edge u) (forward_edge v)) (forward_edge (comp a u v))))). Proof. ir. assert (lem1 : Graph.axioms (gz_graph a s)). app gz_graph_axioms. ap iff_eq; ir. ufi gz_rel H0. Ztac. uf gz_rel. Ztac. rw inc_coarse. nin H0. nin H0. ee. sh (forward_edge (id a x)). sh (freecat_id x). ee. app mor_forward_edge. app mor_id. rw mor_gz_freecat. ap mor_freecat_id. rw inc_vertices_gz_graph. am. am. am. am. rw source_forward_edge. rw source_freecat_id. rw source_id. tv. am. rw target_forward_edge. rw target_id. rww target_freecat_id. am. am. nin H0. nin H0. ee. assert (mor a x). uh H; ee. au. sh (freecat_comp (forward_edge x) (backward_edge x)). sh (freecat_id (target x)). ee. rw mor_gz_freecat. ap mor_freecat_comp. wr mor_gz_freecat. ap mor_forward_edge. am. am. am. wr mor_gz_freecat. ap mor_backward_edge. am. am. am. rw source_forward_edge. rww target_backward_edge. am. rw mor_gz_freecat. app mor_freecat_id. rw inc_vertices_gz_graph. rww ob_target. am. am. rw source_freecat_comp. rw source_backward_edge. rw source_freecat_id. tv. rw target_freecat_comp. rw target_forward_edge. rw target_freecat_id. tv. am. nin H0. nin H0. ee. assert (mor a x). uh H; ee; au. sh (freecat_comp (backward_edge x) (forward_edge x)). sh (freecat_id (source x)). ee. rw mor_gz_freecat. ap mor_freecat_comp. wr mor_gz_freecat. ap mor_backward_edge. am. am. am. wr mor_gz_freecat. ap mor_forward_edge. am. am. am. rw source_backward_edge. rww target_forward_edge. am. rw mor_gz_freecat. app mor_freecat_id. rw inc_vertices_gz_graph. rww ob_source. am. am. rw source_freecat_comp. rw source_forward_edge. rw source_freecat_id. tv. rw target_freecat_comp. rw target_backward_edge. rw target_freecat_id. tv. am. nin H0. nin H0. ee. sh (freecat_comp (forward_edge x) (forward_edge x0)). sh (forward_edge (comp a x x0)). ee. rw mor_gz_freecat. ap mor_freecat_comp. wr mor_gz_freecat. ap mor_forward_edge. am. am. am. wr mor_gz_freecat. ap mor_forward_edge. am. am. am. rw source_forward_edge. rw target_forward_edge. am. am. ap mor_forward_edge. am. rww mor_comp. rw source_freecat_comp. rw source_forward_edge. rw source_forward_edge. rww source_comp. rw target_freecat_comp. rw target_forward_edge. rw target_forward_edge. rww target_comp. am. app gz_freecat_axioms. Qed. Lemma related_gz_rel : forall a s e f, multiplicative_system a s -> related (gz_rel a s) e f = ((exists x, (ob a x & e = (forward_edge (id a x)) & f = (freecat_id x))) \/ (exists q, (inc q s & e = (freecat_comp (forward_edge q) (backward_edge q)) & f = (freecat_id (target q)))) \/ (exists q, (inc q s & e = (freecat_comp (backward_edge q) (forward_edge q)) & f = (freecat_id (source q)))) \/ (exists u, exists v, (mor a u & mor a v & source u = target v & e = (freecat_comp (forward_edge u) (forward_edge v)) & f = (forward_edge (comp a u v))))). Proof. ir. ap iff_eq; ir. uh H0. rwi inc_gz_rel H0. nin H0; [ap or_introl | ap or_intror]. nin H0. sh x; ee. am. transitivity (pr1 (pair e f)). rww pr1_pair. rw H1. rww pr1_pair. transitivity (pr2 (pair e f)). rww pr2_pair. rw H1. rww pr2_pair. nin H0; [ap or_introl | ap or_intror]. nin H0. ee. sh x; ee. am. transitivity (pr1 (pair e f)). rww pr1_pair. rw H1. rww pr1_pair. transitivity (pr2 (pair e f)). rww pr2_pair. rw H1. rww pr2_pair. nin H0; [ap or_introl | ap or_intror]. nin H0. sh x; ee. am. transitivity (pr1 (pair e f)). rww pr1_pair. rw H1. rww pr1_pair. transitivity (pr2 (pair e f)). rww pr2_pair. rw H1. rww pr2_pair. nin H0. nin H0. sh x. sh x0. ee. am. am. am. transitivity (pr1 (pair e f)). rww pr1_pair. rw H3. rww pr1_pair. transitivity (pr2 (pair e f)). rww pr2_pair. rw H3. rww pr2_pair. am. uhg. rw inc_gz_rel. nin H0; [ap or_introl | ap or_intror]. nin H0. ee. sh x. ee. am. rw H1; rww H2. nin H0; [ap or_introl | ap or_intror]. nin H0. ee. sh x. ee. am. rw H1; rww H2. nin H0; [ap or_introl | ap or_intror]. nin H0. ee. sh x. ee. am. rw H1; rww H2. nin H0. nin H0. sh x. sh x0. ee. am. am. am. rw H3; rww H4. am. Qed. Lemma sub_gz_rel_coarse : forall a s, sub (gz_rel a s) (coarse (gz_freecat a s)). Proof. ir. uf gz_rel. ap Z_sub. Qed. Lemma cat_rel_gz_rel : forall a s, multiplicative_system a s -> cat_rel (gz_freecat a s) (gz_rel a s). Proof. ir. ap cat_rel_subset. sh (coarse (gz_freecat a s)). ee. ap cat_rel_coarse. app gz_freecat_axioms. ap sub_gz_rel_coarse. Qed. Definition gz_cer a s := cer (gz_freecat a s) (gz_rel a s). Lemma cat_equiv_rel_gz_cer : forall a s, multiplicative_system a s -> cat_equiv_rel (gz_freecat a s) (gz_cer a s). Proof. ir. uf gz_cer. ap cat_equiv_rel_cer. ap cat_rel_gz_rel. am. Qed. Lemma related_gz_cer_first_mor : forall a s e f, multiplicative_system a s -> related (gz_cer a s) e f -> mor (gz_freecat a s) e. Proof. ir. cp (cat_equiv_rel_gz_cer H). uh H1; ee. uh H1. ee. apply H6 with f. am. Qed. Lemma related_gz_cer_second_mor : forall a s e f, multiplicative_system a s -> related (gz_cer a s) e f -> mor (gz_freecat a s) f. Proof. ir. cp (cat_equiv_rel_gz_cer H). uh H1; ee. uh H1. ee. apply H7 with e. am. Qed. Lemma related_gz_cer_same_source : forall a s e f, multiplicative_system a s -> related (gz_cer a s) e f -> source e = source f. Proof. ir. cp (cat_equiv_rel_gz_cer H). uh H1; ee. uh H1. ee. au. Qed. Lemma related_gz_cer_same_target : forall a s e f, multiplicative_system a s -> related (gz_cer a s) e f -> target e = target f. Proof. ir. cp (cat_equiv_rel_gz_cer H). uh H1; ee. uh H1. ee. au. Qed. Lemma related_cer : forall a r u v, cat_rel a r -> related r u v -> related (cer a r) u v. Proof. ir. cp (cer_contains H). uhg. ap H1. am. Qed. Lemma related_gz_cer_forward_edge_id : forall a s x, multiplicative_system a s -> ob a x -> related (gz_cer a s) (forward_edge (id a x)) (freecat_id x). Proof. ir. uf gz_cer. ap related_cer. app cat_rel_gz_rel. rw related_gz_rel. ap or_introl. sh x. ee. am. tv. tv. am. Qed. Lemma related_gz_cer_comp_forward_backward : forall a s q, multiplicative_system a s -> inc q s -> related (gz_cer a s) (freecat_comp (forward_edge q) (backward_edge q)) (freecat_id (target q)). Proof. ir. uf gz_cer. ap related_cer. app cat_rel_gz_rel. rw related_gz_rel. ap or_intror. ap or_introl. sh q. ee. am. tv. tv. am. Qed. Lemma related_gz_cer_comp_backward_forward : forall a s q, multiplicative_system a s -> inc q s -> related (gz_cer a s) (freecat_comp (backward_edge q) (forward_edge q)) (freecat_id (source q)). Proof. ir. uf gz_cer. ap related_cer. app cat_rel_gz_rel. rw related_gz_rel. ap or_intror; ap or_intror; ap or_introl. sh q; ee; try am; try tv. am. Qed. Lemma related_gz_cer_comp_forward : forall a s u v, multiplicative_system a s -> mor a u -> mor a v -> source u = target v -> related (gz_cer a s) (freecat_comp (forward_edge u) (forward_edge v)) (forward_edge (comp a u v)). Proof. ir. uf gz_cer. ap related_cer. app cat_rel_gz_rel. rw related_gz_rel. ap or_intror; ap or_intror; ap or_intror. sh u. sh v. ee; try am; try tv. am. Qed. Lemma compatible_gz_cer_criterion : forall a s f, multiplicative_system a s -> Functor.axioms f -> source f = gz_freecat a s -> (forall x, ob a x -> fmor f (forward_edge (id a x)) = id (target f) (fob f x)) -> (forall q, inc q s -> are_inverse (target f) (fmor f (forward_edge q)) (fmor f (backward_edge q))) -> (forall u v, mor a u -> mor a v -> source u = target v -> comp (target f) (fmor f (forward_edge u)) (fmor f (forward_edge v)) = fmor f (forward_edge (comp a u v))) -> compatible (gz_cer a s) f. Proof. ir. uf gz_cer. ap compatible_cer. rw compatible_rw. ee. am. rw H1. app cat_rel_gz_rel. ir. rwi related_gz_rel H5. nin H5. nin H5. ee. rw H6. assert (y = id (freecat (gz_graph a s)) x0). rw id_freecat. am. app gz_graph_axioms. change (ob (gz_freecat a s) x0). rww ob_gz_freecat. rw H2. rw H8. rw fmor_id. tv. am. am. change (ob (gz_freecat a s) x0). rww ob_gz_freecat. am. nin H5. nin H5. ee. rw H6. assert (y = id (freecat (gz_graph a s)) (target x0)). rw id_freecat. am. app gz_graph_axioms. change (ob (gz_freecat a s) (target x0)). rww ob_gz_freecat. rww ob_target. uh H; ee; au. rw H8. rw fmor_id. assert (freecat_comp (forward_edge x0) (backward_edge x0) = comp (source f) (forward_edge x0) (backward_edge x0)). rw H1. rw comp_gz_freecat. reflexivity. am. ap mor_forward_edge. am. uh H; ee; au. ap mor_backward_edge. am. am. rw source_forward_edge. rww target_backward_edge. rw H9. rw fmor_comp. cp (H3 _ H5). uh H10. ee. rw H14. rw source_fmor. rw source_backward_edge. reflexivity. am. rw H1. ap mor_backward_edge. am. am. am. tv. rw H1. ap mor_forward_edge. am. uh H; ee; au. rw H1. app mor_backward_edge. rw source_forward_edge. rww target_backward_edge. am. am. change (ob (gz_freecat a s) (target x0)). rw ob_gz_freecat. rw ob_target. tv. uh H; ee; au. am. nin H5. nin H5. ee. rw H6. assert (y = id (freecat (gz_graph a s)) (source x0)). rw id_freecat. am. app gz_graph_axioms. change (ob (gz_freecat a s) (source x0)). rww ob_gz_freecat. rww ob_source. uh H; ee; au. rw H8. rw fmor_id. assert (freecat_comp (backward_edge x0) (forward_edge x0) = comp (source f) (backward_edge x0) (forward_edge x0)). rw H1. rw comp_gz_freecat. reflexivity. am. ap mor_backward_edge. am. am. ap mor_forward_edge. am. uh H; ee; au. rw source_backward_edge. rww target_forward_edge. rw H9. rw fmor_comp. cp (H3 _ H5). uh H10. ee. rw H15. rw source_fmor. rw source_forward_edge. reflexivity. am. rw H1. ap mor_forward_edge. am. uh H; ee; au. am. tv. rw H1. ap mor_backward_edge. am. am. rw H1. app mor_forward_edge. uh H; ee; au. rw source_backward_edge. rww target_forward_edge. am. am. change (ob (gz_freecat a s) (source x0)). rw ob_gz_freecat. rw ob_source. tv. uh H; ee; au. am. nin H5. nin H5. ee. rw H8. rw H9. assert (freecat_comp (forward_edge x0) (forward_edge x1) = comp (source f) (forward_edge x0) (forward_edge x1)). rw H1. rw comp_gz_freecat. reflexivity. am. app mor_forward_edge. app mor_forward_edge. rw source_forward_edge. rw target_forward_edge. am. rw H10. wr comp_fmor. ap H4. am. am. am. am. rw H1. app mor_forward_edge. rw H1. app mor_forward_edge. rw source_forward_edge. rw target_forward_edge. am. am. sy; am. Qed. Definition gz_loc a s := quotient_cat (gz_freecat a s) (gz_cer a s). Lemma gz_loc_axioms : forall a s, multiplicative_system a s -> Category.axioms (gz_loc a s). Proof. ir. uf gz_loc. ap quotient_cat_axioms. ap cat_equiv_rel_gz_cer. am. Qed. Definition gz_qprojection a s := qprojection (gz_freecat a s) (gz_cer a s). Lemma source_gz_qprojection : forall a s, multiplicative_system a s -> source (gz_qprojection a s) = gz_freecat a s. Proof. ir. uf gz_qprojection. rw source_qprojection. tv. Qed. Lemma target_gz_qprojection : forall a s, multiplicative_system a s -> target (gz_qprojection a s) = gz_loc a s. Proof. ir. uf gz_qprojection. rw target_qprojection. tv. Qed. Lemma gz_qprojection_axioms : forall a s, multiplicative_system a s -> Functor.axioms (gz_qprojection a s). Proof. ir. uf gz_qprojection. ap qprojection_axioms. app cat_equiv_rel_gz_cer. Qed. Definition gz_proj a s := qfunctor a (gz_freecat a s) (gz_cer a s) (fun x => x) forward_edge. Lemma source_gz_proj : forall a s, multiplicative_system a s -> source (gz_proj a s) = a. Proof. ir. uf gz_proj. rw source_qfunctor. tv. Qed. Lemma target_gz_proj : forall a s, multiplicative_system a s -> target (gz_proj a s) = gz_loc a s. Proof. ir. uf gz_proj. rw target_qfunctor. tv. Qed. Definition gz_forward a s u := arrow_class (gz_cer a s) (forward_edge u). Definition gz_backward a s u := arrow_class (gz_cer a s) (backward_edge u). Lemma source_gz_forward : forall a s u, multiplicative_system a s -> mor a u -> source (gz_forward a s u) = source u. Proof. ir. uf gz_forward. rw source_arrow_class. rw source_forward_edge. tv. Qed. Lemma target_gz_forward : forall a s u, multiplicative_system a s -> mor a u -> target (gz_forward a s u) = target u. Proof. ir. uf gz_forward. rw target_arrow_class. rw target_forward_edge. tv. Qed. Lemma source_gz_backward : forall a s q, multiplicative_system a s -> inc q s -> source (gz_backward a s q) = target q. Proof. ir. uf gz_backward. rw source_arrow_class. rw source_backward_edge. tv. Qed. Lemma target_gz_backward : forall a s q, multiplicative_system a s -> inc q s -> target (gz_backward a s q) = source q. Proof. ir. uf gz_backward. rw target_arrow_class. rw target_backward_edge. tv. Qed. Lemma mor_gz_forward : forall a s u, multiplicative_system a s -> mor a u -> mor (gz_loc a s) (gz_forward a s u). Proof. ir. uf gz_forward. uf gz_loc. ap mor_quotient_cat_arrow_class. app cat_equiv_rel_gz_cer. app mor_forward_edge. Qed. Lemma mor_gz_backward : forall a s q, multiplicative_system a s -> inc q s -> mor (gz_loc a s) (gz_backward a s q). Proof. ir. uf gz_backward. uf gz_loc. ap mor_quotient_cat_arrow_class. app cat_equiv_rel_gz_cer. app mor_backward_edge. Qed. Lemma qfunctor_property_forward_edge : forall a s, multiplicative_system a s -> qfunctor_property a (gz_freecat a s) (gz_cer a s) (fun x => x) forward_edge. Proof. ir. uhg; ee. uh H; ee; am. app cat_equiv_rel_gz_cer. ir. rww ob_gz_freecat. ir. app mor_forward_edge. ir. rww source_forward_edge. ir. rww target_forward_edge. ir. rw id_gz_freecat. ap related_gz_cer_forward_edge_id. am. am. am. am. ir. rw comp_gz_freecat. ap symmetric_ap. cp (cat_equiv_rel_gz_cer H). uh H3. ee. uh H4. ee. am. ap related_gz_cer_comp_forward. am. am. am. am. am. app mor_forward_edge. app mor_forward_edge. rw source_forward_edge. rww target_forward_edge. Qed. Lemma gz_proj_axioms : forall a s, multiplicative_system a s -> Functor.axioms (gz_proj a s). Proof. ir. uf gz_proj. ap qfunctor_axioms. ap qfunctor_property_forward_edge. am. Qed. Lemma fob_gz_proj : forall a s x, multiplicative_system a s -> ob a x -> fob (gz_proj a s) x = x. Proof. ir. uf gz_proj. rw fob_qfunctor. tv. app qfunctor_property_forward_edge. am. Qed. Lemma fmor_gz_proj : forall a s u, multiplicative_system a s -> mor a u -> fmor (gz_proj a s) u = gz_forward a s u. Proof. ir. uf gz_proj. rw fmor_qfunctor. tv. am. Qed. Lemma gz_forward_id : forall a s x, multiplicative_system a s -> ob a x -> gz_forward a s (id a x) = id (gz_loc a s) x. Proof. ir. wr fmor_gz_proj. rw fmor_id. rw target_gz_proj. rw fob_gz_proj. tv. am. am. am. ap gz_proj_axioms. am. rww source_gz_proj. am. am. app mor_id. Qed. Lemma comp_gz_forward : forall a s u v, multiplicative_system a s -> mor a u -> mor a v -> source u = target v -> comp (gz_loc a s) (gz_forward a s u) (gz_forward a s v) = gz_forward a s (comp a u v). Proof. ir. wrr fmor_gz_proj. wrr fmor_gz_proj. assert (gz_loc a s = target (gz_proj a s)). rww target_gz_proj. rw H3. rw comp_fmor. rw source_gz_proj. rww fmor_gz_proj. rww mor_comp. am. app gz_proj_axioms. rw source_gz_proj. am. am. rww source_gz_proj. am. Qed. Lemma are_inverse_gz_forward_backward : forall a s q, multiplicative_system a s -> inc q s -> are_inverse (gz_loc a s) (gz_forward a s q) (gz_backward a s q). Proof. ir. assert (mor a q). uh H; ee; au. uhg; ee. app mor_gz_forward. app mor_gz_backward. rww source_gz_forward. rww target_gz_backward. rww source_gz_backward. rww target_gz_forward. rww source_gz_backward. assert (mor (gz_freecat a s) (forward_edge q)). app mor_forward_edge. assert (mor (gz_freecat a s) (backward_edge q)). app mor_backward_edge. assert (source (forward_edge q) = target (backward_edge q)). rww source_forward_edge. rww target_backward_edge. assert (cat_equiv_rel (gz_freecat a s) (gz_cer a s)). app cat_equiv_rel_gz_cer. uf gz_loc. uf gz_forward. uf gz_backward. rw comp_quotient_cat. rw quot_comp_arrow_class. rw id_quotient_cat. uf quot_id. rewrite <- related_arrow_class_eq with (a:=gz_freecat a s). rw comp_gz_freecat. rw id_gz_freecat. ap related_gz_cer_comp_forward_backward. am. am. am. rww ob_target. am. am. am. am. am. rw mor_comp. tv. am. am. am. tv. am. rww ob_gz_freecat. rww ob_target. am. am. am. am. am. ap is_quotient_arrow_arrow_class. am. am. ap is_quotient_arrow_arrow_class. am. am. rw source_arrow_class. rw target_arrow_class. am. rww source_gz_forward. assert (mor (gz_freecat a s) (forward_edge q)). app mor_forward_edge. assert (mor (gz_freecat a s) (backward_edge q)). app mor_backward_edge. assert (source (backward_edge q) = target (forward_edge q)). rww target_forward_edge. rww source_backward_edge. assert (cat_equiv_rel (gz_freecat a s) (gz_cer a s)). app cat_equiv_rel_gz_cer. uf gz_loc. uf gz_forward. uf gz_backward. rw comp_quotient_cat. rw quot_comp_arrow_class. rw id_quotient_cat. uf quot_id. rewrite <- related_arrow_class_eq with (a:=gz_freecat a s). rw comp_gz_freecat. rw id_gz_freecat. ap related_gz_cer_comp_backward_forward. am. am. am. rww ob_source. am. am. am. am. am. rw mor_comp. tv. am. am. am. tv. am. rww ob_gz_freecat. rww ob_source. am. am. am. am. am. ap is_quotient_arrow_arrow_class. am. am. ap is_quotient_arrow_arrow_class. am. am. rw source_arrow_class. rw target_arrow_class. am. Qed. Lemma invertible_gz_loc_gz_forward : forall a s q, multiplicative_system a s -> inc q s -> invertible (gz_loc a s) (gz_forward a s q). Proof. ir. uhg. sh (gz_backward a s q). ap are_inverse_gz_forward_backward. am. am. Qed. End GZ_Def. Module GZ_Thm. Export Ob_Iso_Functor. Export GZ_Def. (** The first step in showing the universal property of [gz_proj] and Theorem 1.2, is to apply the general results of [Ob_Iso_Functor] to show that [pull_functor (gz_proj a s) b] is an isomorphism onto a full subcategory. We have to show that [add_inverses (gz_loc a s) (mor_image (gz_proj a s))] generates [gz_loc a s], basically because of the induction statement [mor_freecat_induction] saying that [gz_freecat (gz_graph a s)] is generated by the edges of the graph. **) Lemma inc_gz_forward_mor_image : forall a s u, multiplicative_system a s -> mor a u -> inc (gz_forward a s u) (mor_image (gz_proj a s)). Proof. ir. rw inc_mor_image. sh u. ee. rw source_gz_proj. am. am. rw fmor_gz_proj. tv. am. am. app gz_proj_axioms. Qed. Lemma inc_gz_backward_add_inverses : forall a s q, multiplicative_system a s -> inc q s -> inc (gz_backward a s q) (add_inverses (gz_loc a s) (mor_image (gz_proj a s))). Proof. ir. rw inc_add_inverses. ee. ap mor_gz_backward. am. am. ap or_intror. ee. uhg. sh (gz_forward a s q). ap are_inverse_symm. ap are_inverse_gz_forward_backward. am. am. assert (inverse (gz_loc a s) (gz_backward a s q) = gz_forward a s q). ap inverse_eq. ap are_inverse_symm. app are_inverse_gz_forward_backward. rw H1. app inc_gz_forward_mor_image. uh H; ee; au. app gz_loc_axioms. uhg; ir. rwi inc_mor_image H1. nin H1. ee. ap mor_is_mor. wr H2. assert (gz_loc a s = target (gz_proj a s)). rw target_gz_proj. tv. am. rw H3. app mor_fmor. app gz_proj_axioms. app gz_proj_axioms. Qed. Lemma gz_loc_induction : forall a s (P:E->Prop), multiplicative_system a s -> (forall u, mor a u -> P (gz_forward a s u)) -> (forall q, inc q s -> P (gz_backward a s q)) -> (forall x, ob a x -> P (id (gz_loc a s) x)) -> (forall u v, mor (gz_loc a s) u -> mor (gz_loc a s) v -> source u = target v -> P u -> P v -> P (comp (gz_loc a s) u v)) -> (forall y, mor (gz_loc a s) y -> P y). Proof. ir. assert (lem1 : cat_equiv_rel (gz_freecat a s) (gz_cer a s)). app cat_equiv_rel_gz_cer. set (Q:= fun z => P (arrow_class (gz_cer a s) z)). ufi gz_loc H4. rwi mor_quotient_cat H4. uh H4; ee. nin H5. ee. rw H6. change (Q x). apply mor_freecat_induction with (g:=gz_graph a s) (P:=Q). app gz_graph_axioms. ir. rwi inc_vertices_gz_graph H7. assert (P (id (gz_loc a s) x0)). ap H2. am. ufi gz_loc H8. rwi id_quotient_cat H8. uf Q. ufi quot_id H8. rwi id_gz_freecat H8. am. am. am. am. rww ob_gz_freecat. am. ir. rwi inc_edges_gz_graph H7. rwi inc_loc_edges H7. assert (Q (freecat_edge u)). nin H7. nin H7. ee. uf Q. rw H11. exact (H0 _ H7). nin H7. ee. rw H12. exact (H1 _ H11). uf chain_tack. assert (P (comp (gz_loc a s) (arrow_class (gz_cer a s) (freecat_edge u)) (arrow_class (gz_cer a s) v))). ap H3. uf gz_loc. ap mor_quotient_cat_arrow_class. am. uf gz_freecat. rw mor_freecat_rw. ap mor_freecat_edge. app gz_graph_axioms. rw inc_edges_gz_graph. rw inc_loc_edges. am. am. am. app gz_graph_axioms. uf gz_loc. ap mor_quotient_cat_arrow_class. am. rw mor_gz_freecat. am. am. rw source_arrow_class. rw source_freecat_edge. rw target_arrow_class. am. nin H7. nin H7; ee. rw H12. exact (H0 _ H7). nin H7; ee. rw H13. exact (H1 _ H12). exact H10. uf Q. ufi gz_loc H12. rwi comp_quotient_cat H12. rwi quot_comp_arrow_class H12. rwi comp_gz_freecat H12. am. am. rw mor_gz_freecat. ap mor_freecat_edge. app gz_graph_axioms. rw inc_edges_gz_graph. rw inc_loc_edges. am. am. am. am. rww mor_gz_freecat. rww source_freecat_edge. am. rw mor_gz_freecat. ap mor_freecat_edge. app gz_graph_axioms. rw inc_edges_gz_graph. rw inc_loc_edges. am. am. am. am. rww mor_gz_freecat. rww source_freecat_edge. am. ap is_quotient_arrow_arrow_class. am. rw mor_gz_freecat. ap mor_freecat_edge. app gz_graph_axioms. rw inc_edges_gz_graph. rw inc_loc_edges. am. am. am. am. ap is_quotient_arrow_arrow_class. am. rww mor_gz_freecat. rw source_arrow_class. rw source_freecat_edge. rw target_arrow_class. am. am. am. rwi mor_gz_freecat H5. am. am. am. Qed. Lemma subcategory_all_criterion : forall a b, is_subcategory a b -> (forall u, mor b u -> mor a u) -> a = b. Proof. ir. ap is_subcategory_extensionality. am. uhg; dj. uh H; ee; am. uh H; ee; am. uh H; ee; sy; am. ir. assert (x = source (id b x)). rww source_id. rw H5. rw ob_source. tv. ap H0. app mor_id. ap H0; am. sy. ap is_subcategory_same_comp. am. app H5. app H5. am. sy. ap is_subcategory_same_id. am. au. Qed. Lemma gz_loc_subcategory_all_criterion : forall a s b, multiplicative_system a s -> is_subcategory b (gz_loc a s) -> (forall u, mor a u -> mor b (gz_forward a s u)) -> (forall q, inc q s -> mor b (gz_backward a s q)) -> b = gz_loc a s. Proof. ir. assert (forall x, ob a x -> ob b x). ir. assert (mor b (gz_forward a s (id a x))). ap H1. app mor_id. assert (x = source (gz_forward a s (id a x))). rw source_gz_forward. rw source_id. tv. am. am. app mor_id. rw H5. rw ob_source. tv. ap H1. app mor_id. ap subcategory_all_criterion. am. ir. apply gz_loc_induction with (a:=a)(s:=s)(P:=mor b). am. ir. ap H1. am. ir. ap H2. am. ir. assert (ob b x). app H3. assert (id b x = id (gz_loc a s) x). app is_subcategory_same_id. assert (mor b (gz_forward a s (id a x))). ap H1. app mor_id. wr H7. app mor_id. ir. assert (comp b u0 v = comp (gz_loc a s) u0 v). ap is_subcategory_same_comp. am. am. am. am. wr H10. rww mor_comp. am. Qed. Lemma add_inverses_mor_image_gz_proj_generates_gz_loc : forall a s, multiplicative_system a s -> generates (gz_loc a s) (add_inverses (gz_loc a s) (mor_image (gz_proj a s))). Proof. ir. uhg; ee. app gz_loc_axioms. uhg; ir. rwi inc_add_inverses H0. ee. app mor_is_mor. app gz_loc_axioms. uhg; ir. rwi inc_mor_image H1. nin H1. ee. ap mor_is_mor. wr H2. assert (gz_loc a s = target (gz_proj a s)). rww target_gz_proj. rw H3. app mor_fmor. app gz_proj_axioms. app gz_proj_axioms. ir. ap gz_loc_subcategory_all_criterion. am. am. ir. uh H1. ap is_mor_mor. uh H0; ee; am. uhg. ap H1. rw inc_add_inverses. ee. ap mor_gz_forward. am. am. ap or_introl. app inc_gz_forward_mor_image. app gz_loc_axioms. uhg; ir. ap mor_is_mor. rwi inc_mor_image H3. nin H3. ee. wr H4. rw fmor_gz_proj. app mor_gz_forward. rwi source_gz_proj H3. am. am. am. rwi source_gz_proj H3. am. am. app gz_proj_axioms. ir. ap is_mor_mor. uh H0; ee; am. uhg. uh H1. ap H1. app inc_gz_backward_add_inverses. Qed. Lemma ob_gz_loc : forall a s x, multiplicative_system a s -> ob (gz_loc a s) x = ob a x. Proof. ir. uf gz_loc. rw ob_quotient_cat. rw ob_gz_freecat. tv. am. app cat_equiv_rel_gz_cer. Qed. Lemma ob_iso_gz_proj : forall a s, multiplicative_system a s -> ob_iso (gz_proj a s). Proof. ir. uhg; ee. uhg; ee. app gz_proj_axioms. ir. rwi source_gz_proj H0. rwi source_gz_proj H1. rwi fob_gz_proj H2. rwi fob_gz_proj H2. am. am. am. am. am. am. am. uhg; ee. app gz_proj_axioms. ir. rwi target_gz_proj H0. rwi ob_gz_loc H0. uhg; ee. ap gz_proj_axioms. am. sh x. ee. rww source_gz_proj. rww fob_gz_proj. am. am. Qed. (** The following corollary says that the functor of pullback (or composition) along the projection [gz_proj a s] induces an isomorphism of [functor_catgory (gz_loc a s) b] to a subcategory of [functor_category a b]. This is modulo the disclaimer at the end of [qcat.v] because the property [iso_to_full_subcategory] really says that the functor is fully faithful and an isomorphism on objects; we still have to show that this implies that it induces an isomorphism to a full subcategory. **) Lemma iso_to_subcategory_pull_gz_proj : forall a s b, multiplicative_system a s -> Category.axioms b -> iso_to_full_subcategory (pull_morphism b (gz_proj a s)). Proof. ir. ap iso_to_full_subcategory_pull_morphism_criterion. am. app ob_iso_gz_proj. rw target_gz_proj. app add_inverses_mor_image_gz_proj_generates_gz_loc. am. Qed. (** As a corollary we obtain the uniqueness part of the universal property of [gz_proj]. **) Lemma gz_proj_epimorphic : forall a s f g, multiplicative_system a s -> Functor.axioms f -> Functor.axioms g -> source f = gz_loc a s -> source g = gz_loc a s -> fcompose f (gz_proj a s) = fcompose g (gz_proj a s) -> f = g. Proof. ir. assert (Category.axioms (target f)). uh H0; ee; am. assert (target f = target g). transitivity (target (fcompose f (gz_proj a s))). rww target_fcompose. rw H4. rww target_fcompose. cp (iso_to_subcategory_pull_gz_proj H H5). uh H7; ee. uh H9; ee. ap H10. rw source_pull_morphism. rw target_gz_proj. rw ob_functor_cat. uhg; ee. am. am. tv. app gz_loc_axioms. uh H0; ee; am. am. rw source_pull_morphism. rw target_gz_proj. rw ob_functor_cat. uhg; ee. am. am. sy; am. app gz_loc_axioms. am. am. rw fob_pull_morphism. rw fob_pull_morphism. am. app gz_proj_axioms. am. rw target_gz_proj. rw ob_functor_cat. uhg; ee. am. am. sy; am. app gz_loc_axioms. am. am. app gz_proj_axioms. am. rw target_gz_proj. rw ob_functor_cat. uhg; ee. am. am. tv. app gz_loc_axioms. am. am. Qed. (** We now show the essential part of GZ's Theorem 1.2, which is the versal part of the universal property of [gz_proj], which we mainly express by constructing the functor [gz_dotted]. **) Definition loc_compatible a s f := multiplicative_system a s & Functor.axioms f & source f = a & (forall q, inc q s -> invertible (target f) (fmor f q)). Definition fr_dotted a s f := free_functor (gz_graph a s) (target f) (fun x => fob f x) (fun u => Y (direction u = Forward) (fmor f (original_arrow u)) (inverse (target f) (fmor f (original_arrow u)))). Lemma backward_neq_forward : Backward <> Forward. Proof. uhg; ir. ufi Backward H. ufi Forward H. cp (R_inj H). discriminate H0. Qed. Lemma Y_etc_forward_arrow : forall f u, Y (direction (forward_arrow u) = Forward) (fmor f (original_arrow (forward_arrow u))) (inverse (target f) (fmor f (original_arrow (forward_arrow u)))) = fmor f u. Proof. ir. rw Y_if_rw. rw original_arrow_forward_arrow. tv. rww direction_forward_arrow. Qed. Lemma Y_etc_backward_arrow : forall f q, Y (direction (backward_arrow q) = Forward) (fmor f (original_arrow (backward_arrow q))) (inverse (target f) (fmor f (original_arrow (backward_arrow q)))) = inverse (target f) (fmor f q). Proof. ir. rw Y_if_not_rw. rw original_arrow_backward_arrow. tv. rw direction_backward_arrow. ap backward_neq_forward. Qed. Lemma fr_dotted_property : forall a s f, loc_compatible a s f -> free_functor_property (gz_graph a s) (target f) (fun x => fob f x) (fun u => Y (direction u = Forward) (fmor f (original_arrow u)) (inverse (target f) (fmor f (original_arrow u)))). Proof. ir. uh H; uhg; ee. app gz_graph_axioms. uh H0; ee; am. ir. rwi inc_vertices_gz_graph H3. ap ob_fob. am. rww H1. am. ir. rwi inc_edges_gz_graph H3. rwi inc_loc_edges H3. nin H3. nin H3. ee. rw H4. rw Y_etc_forward_arrow. wri H1 H3. app mor_fmor. nin H3. ee. rw H5. rw Y_etc_backward_arrow. ap mor_inverse. ap H2. am. am. am. ir. rwi inc_edges_gz_graph H3. rwi inc_loc_edges H3. nin H3. nin H3. ee. rw H4. rw Y_etc_forward_arrow. rw source_forward_arrow. rww source_fmor. rw H1. am. nin H3. ee. rw H5. rw Y_etc_backward_arrow. assert (invertible (target f) (fmor f x)). au. rw source_inverse. rw source_backward_arrow. rw target_fmor. tv. am. rww H1. am. am. am. ir. rwi inc_edges_gz_graph H3. rwi inc_loc_edges H3. nin H3. nin H3. ee. rw H4. rw Y_etc_forward_arrow. rw target_forward_arrow. rww target_fmor. rw H1. am. nin H3. ee. rw H5. rw Y_etc_backward_arrow. assert (invertible (target f) (fmor f x)). au. rw target_inverse. rw target_backward_arrow. rw source_fmor. tv. am. rww H1. am. am. am. Qed. Lemma source_fr_dotted : forall a s f, source (fr_dotted a s f) = gz_freecat a s. Proof. ir. uf fr_dotted. rw source_free_functor. tv. Qed. Lemma target_fr_dotted : forall a s f, target (fr_dotted a s f) = target f. Proof. ir. uf fr_dotted. rw target_free_functor. tv. Qed. Lemma fob_fr_dotted : forall a s f x, loc_compatible a s f -> ob a x -> fob (fr_dotted a s f) x = fob f x. Proof. ir. uf fr_dotted. rw fob_free_functor. tv. ap fr_dotted_property. am. rw inc_vertices_gz_graph. am. uh H; ee; am. Qed. Lemma fmor_fr_dotted_forward_edge : forall a s f u, loc_compatible a s f -> mor a u -> fmor (fr_dotted a s f) (forward_edge u) = fmor f u. Proof. ir. uf fr_dotted. uf forward_edge. rw fmor_ff_freecat_edge. rw Y_etc_forward_arrow. tv. ap fr_dotted_property. am. rw inc_edges_gz_graph. ap inc_forward_arrow_loc_edges. uh H; ee; am. am. uh H; ee; am. Qed. Lemma fmor_fr_dotted_backward_edge : forall a s f q, loc_compatible a s f -> inc q s -> fmor (fr_dotted a s f) (backward_edge q) = inverse (target f) (fmor f q). Proof. ir. uf fr_dotted. uf backward_edge. rw fmor_ff_freecat_edge. rw Y_etc_backward_arrow. tv. ap fr_dotted_property. am. rw inc_edges_gz_graph. ap inc_backward_arrow_loc_edges. uh H; ee; am. am. uh H; ee; am. Qed. Lemma fr_dotted_axioms : forall a s f, loc_compatible a s f -> Functor.axioms (fr_dotted a s f). Proof. ir. uf fr_dotted. ap free_functor_axioms. ap fr_dotted_property. am. Qed. Lemma compatible_gz_cer_fr_dotted : forall a s f, loc_compatible a s f -> compatible (gz_cer a s) (fr_dotted a s f). Proof. ir. ap compatible_gz_cer_criterion. uh H; ee; am. ap fr_dotted_axioms. am. rw source_fr_dotted. tv. ir. rw fmor_fr_dotted_forward_edge. rw target_fr_dotted. rw fob_fr_dotted. rw fmor_id. tv. uh H; ee; am. uh H; ee; am. am. am. am. am. app mor_id. ir. cp H. uh H1; ee. cp (H4 _ H0). assert (mor a q). uh H1; ee; au. rww fmor_fr_dotted_forward_edge. rww fmor_fr_dotted_backward_edge. rww target_fr_dotted. ap invertible_inverse. am. ir. rww fmor_fr_dotted_forward_edge. rww fmor_fr_dotted_forward_edge. rww fmor_fr_dotted_forward_edge. rw target_fr_dotted. rw fmor_comp. tv. uh H; ee; am. uh H; ee; am. am. am. am. rww mor_comp. Qed. Definition gz_dotted a s f := qdotted (gz_cer a s) (fr_dotted a s f). Lemma source_gz_dotted : forall a s f, source (gz_dotted a s f) = gz_loc a s. Proof. ir. uf gz_dotted. rw source_qdotted. rw source_fr_dotted. tv. Qed. Lemma target_gz_dotted : forall a s f, target (gz_dotted a s f) = target f. Proof. ir. uf gz_dotted. rw target_qdotted. rw target_fr_dotted. tv. Qed. Lemma fob_gz_dotted : forall a s f x, loc_compatible a s f -> ob a x -> fob (gz_dotted a s f) x = fob f x. Proof. ir. uf gz_dotted. rw fob_qdotted. rw fob_fr_dotted. tv. am. am. rw source_fr_dotted. ap cat_equiv_rel_gz_cer. uh H; ee; am. app compatible_gz_cer_fr_dotted. rw source_fr_dotted. rw ob_gz_freecat. am. uh H; ee; am. Qed. Lemma fmor_gz_dotted_gz_forward : forall a s f u, loc_compatible a s f -> mor a u -> fmor (gz_dotted a s f) (gz_forward a s u) = fmor f u. Proof. ir. cp H. uh H1; ee. uf gz_dotted. uf gz_forward. rw fmor_qdotted_arrow_class. rw fmor_fr_dotted_forward_edge. tv. am. am. rw source_fr_dotted. ap cat_equiv_rel_gz_cer. am. app compatible_gz_cer_fr_dotted. rw source_fr_dotted. rw mor_gz_freecat. uf forward_edge. ap mor_freecat_edge. ap gz_graph_axioms. am. rw inc_edges_gz_graph. rw inc_loc_edges. ap or_introl. sh u. ee. am. tv. am. am. am. Qed. Lemma fmor_gz_dotted_gz_backward : forall a s f q, loc_compatible a s f -> inc q s -> fmor (gz_dotted a s f) (gz_backward a s q) = inverse (target f) (fmor f q). Proof. ir. cp H. uh H1; ee. assert (mor a q). uh H1; ee; au. uf gz_dotted. uf gz_backward. rw fmor_qdotted_arrow_class. rw fmor_fr_dotted_backward_edge. tv. am. am. rw source_fr_dotted. ap cat_equiv_rel_gz_cer. am. app compatible_gz_cer_fr_dotted. rw source_fr_dotted. rw mor_gz_freecat. uf backward_edge. ap mor_freecat_edge. ap gz_graph_axioms. am. rw inc_edges_gz_graph. rw inc_loc_edges. ap or_intror. sh q. ee. am. am. tv. am. am. am. Qed. Lemma gz_dotted_axioms : forall a s f, loc_compatible a s f -> Functor.axioms (gz_dotted a s f). Proof. ir. uf gz_dotted. ap qdotted_axioms. rw source_fr_dotted. ap cat_equiv_rel_gz_cer. uh H; ee; am. ap compatible_gz_cer_fr_dotted. am. Qed. (** By the following, we have successfully constructed the dotted functor filling in our diagram. This shows the versality property of localizatin. **) Lemma fcompose_gz_dotted_gz_proj : forall a s f, loc_compatible a s f -> fcompose (gz_dotted a s f) (gz_proj a s) = f. Proof. ir. cp H . uh H0; ee. ap Functor.axioms_extensionality. ap fcompose_axioms. ap gz_dotted_axioms. am. ap gz_proj_axioms. am. rw source_gz_dotted. rw target_gz_proj. tv. am. am. rw source_fcompose. rw source_gz_proj. sy; am. am. rw target_fcompose. rw target_gz_dotted. tv. ir. rwi source_fcompose H4. rwi source_gz_proj H4. rw fmor_fcompose. (** An interesting point is that the following step which is somehow essential, takes a long time to be read by the computer. **) rw fmor_gz_proj. rw fmor_gz_dotted_gz_forward. tv. am. am. am. am. app gz_dotted_axioms. app gz_proj_axioms. rw source_gz_dotted. rw target_gz_proj. tv. am. rw source_gz_proj. am. am. am. Qed. (** We also have to show that our sufficient condition in versality is also necessary, in order to get a characterization of the functors which factor through gz_proj. **) Lemma loc_compatible_fcompose : forall a s g, multiplicative_system a s -> Functor.axioms g -> source g = gz_loc a s -> loc_compatible a s (fcompose g (gz_proj a s)). Proof. ir. uhg; ee. am. ap fcompose_axioms. am. app gz_proj_axioms. rww target_gz_proj. rww source_fcompose. rww source_gz_proj. ir. rw target_fcompose. rw fmor_fcompose. ap invertible_fmor. am. rw H1. rw fmor_gz_proj. ap invertible_gz_loc_gz_forward. am. am. am. uh H; ee; au. tv. am. app gz_proj_axioms. rww target_gz_proj. rw source_gz_proj. uh H; ee; au. am. Qed. Definition ob_image f := Z (objects (target f)) (fun x => (exists y, (ob (source f) y & fob f y = x))). (** The following statement characterizes the essential image of [pull_functor (gz_proj a s) b]. **) Lemma ob_image_pull_gz_proj : forall a s b f, multiplicative_system a s -> Category.axioms b -> inc f (ob_image (pull_morphism b (gz_proj a s))) = (Functor.axioms f & source f = a & target f = b & (forall q, inc q s -> invertible b (fmor f q))). Proof. ir. cp H. uh H1; ee. ap iff_eq; ir. assert (ob (functor_cat a b) f). ufi ob_image H4. Ztac. rwi target_pull_morphism H5. rwi source_gz_proj H5. assert (ob (functor_cat a b) f). ap is_ob_ob. ap functor_cat_axioms. uh H; ee; am. am. am. am. am. assert (exists g, (ob (functor_cat (gz_loc a s) b) g & f = fcompose g (gz_proj a s))). ufi ob_image H4. Ztac. nin H7. ee. rwi source_pull_morphism H7. rwi target_gz_proj H7. rwi fob_pull_morphism H8. sh x. ee. am. sy; am. app gz_proj_axioms. am. rw target_gz_proj. am. am. am. rwi ob_functor_cat H5. uh H5; ee. am. am. am. ir. nin H6. ee. assert (loc_compatible a s f). rw H10. ap loc_compatible_fcompose. am. rwi ob_functor_cat H6. uh H6; ee; am. app gz_loc_axioms. am. rwi ob_functor_cat H6. uh H6; ee; am. app gz_loc_axioms. am. uh H11. ee. wr H8. ap H14. am. am. am. assert (loc_compatible a s f). uhg; ee. am. am. am. rw H6. am. ee. uf ob_image. ap Z_inc. rw target_pull_morphism. ap ob_is_ob. rw source_gz_proj. rw ob_functor_cat. uhg; ee. am. am. am. am. am. am. sh (gz_dotted a s f). ee. rw source_pull_morphism. rw target_gz_proj. rw ob_functor_cat. uhg; ee. app gz_dotted_axioms. rww source_gz_dotted. rww target_gz_dotted. app gz_loc_axioms. am. am. rw fob_pull_morphism. rw fcompose_gz_dotted_gz_proj. tv. am. app gz_proj_axioms. am. rw target_gz_proj. rw ob_functor_cat. uhg; ee. app gz_dotted_axioms. rww source_gz_dotted. rww target_gz_dotted. app gz_loc_axioms. am. am. Qed. End GZ_Thm. (*** preliminary version, Tuesday Nov. 16th 2004---Carlos Simpson ***)