Set Implicit Arguments. Unset Strict Implicit. Require Export gzfractions1. Require Export gzdef1. Module GZ_Localization. Export GZ_Thm. Export Left_Fraction_Category. (** We start by some general considerations about the notion of localization. Before getting started we give some lemmas to recall the definitions of [localizing_system] and [multiplicative_system]. This is just for the reader who wishes to look at the present file first before looking at the main constructions in [freecat.v], [qcat.v], [gzdef.v] and [gzfractions.v]. **) Lemma localizing_system_recall : forall a s, localizing_system a s = (Category.axioms a & (forall u, inc u s -> mor a u)). Proof. ir. tv. Qed. Lemma multiplicative_system_recall : forall a s, multiplicative_system a s = (localizing_system a s & (forall y z, inc y s -> inc z s -> source y = target z -> inc (comp a y z) s)). Proof. ir. tv. Qed. Definition localizes a s f := localizing_system a s & Functor.axioms f & source f = a & (forall y, inc y s -> invertible (target f) (fmor f y)). Definition completes_triangle f g h := Functor.axioms f & Functor.axioms g & Functor.axioms h & source f = source g & source h = target f & target h = target g & fcompose h f = g. Definition dotted_choice f g := choose (completes_triangle f g). Lemma completes_triangle_dotted_choice : forall f g, completes_triangle f g (dotted_choice f g) = (exists h, (completes_triangle f g h)). Proof. ir. ap iff_eq; ir. sh (dotted_choice f g). am. exact (choose_pr H). Qed. Definition is_localization a s f := localizes a s f & (forall g, (localizes a s g -> completes_triangle f g (dotted_choice f g))) & (forall g h, completes_triangle f g h -> h = dotted_choice f g). Lemma dotted_choice_axioms : forall f g, (exists a, exists s, (is_localization a s f & localizes a s g)) -> Functor.axioms (dotted_choice f g). Proof. ir. nin H. nin H. ee. cp H0; uh H; ee. cp (H2 _ H1). uh H4. ee; am. Qed. Lemma source_dotted_choice : forall f g, (exists a, exists s, (is_localization a s f & localizes a s g)) -> source (dotted_choice f g) = target f. Proof. ir. nin H. nin H. ee. cp H0; uh H; ee. cp (H2 _ H1). uh H4. ee; am. Qed. Lemma target_dotted_choice : forall f g, (exists a, exists s, (is_localization a s f & localizes a s g)) -> target (dotted_choice f g) = target g. Proof. ir. nin H. nin H. ee. cp H0; uh H; ee. cp (H2 _ H1). uh H4. ee; am. Qed. Lemma fcompose_dotted_choice : forall f g, (exists a, exists s, (is_localization a s f & localizes a s g)) -> fcompose (dotted_choice f g) f = g. Proof. ir. nin H. nin H. ee. cp H0; uh H; ee. cp (H2 _ H1). uh H4. ee; am. Qed. Lemma localizes_fcompose : forall a s f g, localizes a s f -> Functor.axioms g -> source g = target f -> localizes a s (fcompose g f). Proof. ir. uh H; ee. uhg; ee. am. app fcompose_axioms. rww source_fcompose. ir. rw fmor_fcompose. ap invertible_fmor. am. rw H1. ap H4. am. rww target_fcompose. am. am. am. rw H3. ap inc_ms_mor. sh s; ee; am. Qed. Lemma eq_dotted_choice : forall f g h, completes_triangle f g h -> (exists a, exists s, (is_localization a s f)) -> h = dotted_choice f g. Proof. ir. nin H0. nin H0. cp H0. uh H1; ee. ap H3. am. Qed. Lemma fcompose_dotted_choice_dotted_choice : forall f g h, (exists a, exists s, (is_localization a s f & is_localization a s g & localizes a s h)) -> fcompose (dotted_choice g h) (dotted_choice f g) = dotted_choice f h. Proof. ir. nin H. nin H. ee. ap eq_dotted_choice. cp H0. uh H2; ee. uhg; ee. uh H; ee. uh H; ee; am. uh H1; ee; am. ap fcompose_axioms. app dotted_choice_axioms. sh x; sh x0; ee; try am. app dotted_choice_axioms. sh x; sh x0; ee; try am. rw source_dotted_choice. rw target_dotted_choice. tv. sh x; sh x0; ee; try am. sh x; sh x0; ee; try am. uh H; ee. uh H; ee. rw H8. uh H1; ee. rww H11. rw source_fcompose. rw source_dotted_choice. tv. sh x; sh x0; ee; try am. rw target_fcompose. rww target_dotted_choice. sh x; sh x0; ee; try am. rw fcompose_assoc. rw fcompose_dotted_choice. rw fcompose_dotted_choice. tv. sh x; sh x0; ee; try am. sh x; sh x0; ee; try am. app dotted_choice_axioms. sh x; sh x0; ee; try am. app dotted_choice_axioms. sh x; sh x0; ee; try am. uh H; ee. uh H; ee; am. rw source_dotted_choice. rw target_dotted_choice. tv. sh x; sh x0; ee; try am. sh x; sh x0; ee; try am. rw source_dotted_choice. tv. sh x; sh x0; ee; try am. sh x; sh x0; ee; try am. Qed. Lemma dotted_choice_refl : forall f, (exists a, exists s, (is_localization a s f)) -> dotted_choice f f = fidentity (target f). Proof. ir. sy. ap eq_dotted_choice. nin H. nin H. cp H. uh H0; ee. uh H0; ee. uhg; ee. am. am. rww fidentity_axioms. rww category_axioms_target. tv. rww source_fidentity. rww target_fidentity. rw left_fidentity. tv. am. tv. am. Qed. (** Our main corollary is that two different localizations are isomorphic. **) Lemma are_finverse_dotted_choice : forall f g, (exists a, exists s, (is_localization a s f & is_localization a s g)) -> are_finverse (dotted_choice f g) (dotted_choice g f). Proof. ir. nin H. nin H. ee. cp H; cp H0. uh H1; uh H2. ee. uhg; ee. ap dotted_choice_axioms. sh x; sh x0; ee; am. ap dotted_choice_axioms. sh x; sh x0; ee; am. rw source_dotted_choice. rw target_dotted_choice. tv. sh x; sh x0; ee; am. sh x; sh x0; ee; am. rw source_dotted_choice. rw target_dotted_choice. tv. sh x; sh x0; ee; am. sh x; sh x0; ee; am. rw fcompose_dotted_choice_dotted_choice. rw source_dotted_choice. rw dotted_choice_refl. tv. sh x; sh x0; ee; am. sh x; sh x0; ee; am. sh x; sh x0; ee; try am. rw fcompose_dotted_choice_dotted_choice. rw source_dotted_choice. rw dotted_choice_refl. tv. sh x; sh x0; ee; am. sh x; sh x0; ee; am. sh x; sh x0; ee; try am. Qed. Lemma has_finverse_dotted_choice : forall f g, (exists a, exists s, (is_localization a s f & is_localization a s g)) -> has_finverse (dotted_choice f g). Proof. ir. uhg; ee. sh (dotted_choice g f). app are_finverse_dotted_choice. Qed. Lemma finverse_dotted_choice : forall f g, (exists a, exists s, (is_localization a s f & is_localization a s g)) -> finverse (dotted_choice f g) = dotted_choice g f. Proof. ir. apply finverse_unique with (f:= (dotted_choice f g)). ap finverse_pr. app has_finverse_dotted_choice. app are_finverse_dotted_choice. Qed. (** Now we point out that our two constructions, one general and one under the hypothesis [has_left_fractions a s], are localizations in the above sense. This allows us to deduce that they are isomorphic. **) Lemma is_localization_gz_proj : forall a s, localizing_system a s -> is_localization a s (gz_proj a s). Proof. ir. uhg; dj. uhg; ee. am. app gz_proj_axioms. rww source_gz_proj. ir. (** The following is a bit silly for two reasons: one, [localizes] was already defined before as [loc_compatible]; two, the lemma saying [loc_compatible a s (gz_proj a s)] wasn't done, only a more general lemma [loc_compatible_fcompose] was done so to get the special case we need to plug in the [fidentity]. **) assert (loc_compatible a s (gz_proj a s)). assert (gz_proj a s = fcompose (fidentity (gz_loc a s)) (gz_proj a s)). sy. rw left_fidentity. tv. app gz_proj_axioms. rww target_gz_proj. rw H1. ap loc_compatible_fcompose. am. rww fidentity_axioms. app gz_loc_axioms. rww source_fidentity. uh H1; ee. au. ir. rw completes_triangle_dotted_choice. sh (gz_dotted a s g). uhg; ee. app gz_proj_axioms. uh H1; ee; am. app gz_dotted_axioms. rww source_gz_proj. uh H1; ee; sy; am. rww source_gz_dotted. rww target_gz_proj. rww target_gz_dotted. rww fcompose_gz_dotted_gz_proj. ir. assert (localizes a s g). uh H2; ee. wr H8. ap localizes_fcompose. am. am. am. cp (H1 g H3). apply gz_proj_epimorphic with (a:=a) (s:=s). am. uh H2; ee. am. uh H4; ee; am. uh H2; ee. rw H8. rww target_gz_proj. uh H4; ee. rw H8. rww target_gz_proj. uh H2; ee. rw H10. uh H4; ee. sy; am. Qed. Lemma is_localization_lf_proj : forall a s, has_left_fractions a s -> is_localization a s (lf_proj a s). Proof. ir. uhg; dj. uhg; ee. uh H; ee; uh H; ee; am. app lf_proj_axioms. rww source_lf_proj. ir. rw target_lf_proj. ap invertible_fmor_lf_proj. am. am. rw completes_triangle_dotted_choice. (** Again it turns out that we basically had another copy of [localizes] called [lf_dotted_situation], the only difference being that the latter includes [has_left_fractions]. This type of duplication is probably inevitable (psychologically speaking) and it is probably best not to worry too much about it. **) assert (lf_dotted_situation a s g). uhg; ee. am. uh H1; ee; am. uh H1; ee; am. uh H1; ee; am. sh (lf_dotted a s g). uhg; ee. app lf_proj_axioms. uh H1; ee; am. app lf_dotted_axioms. rww source_lf_proj. uh H1; ee; sy; am. rww source_lf_dotted. rww target_lf_proj. rww target_lf_dotted. rww fcompose_lf_dotted_lf_proj. assert (localizes a s g). uh H2; ee. wr H8. app localizes_fcompose. cp (H1 g H3). apply lf_dotted_like_unique with (a:=a) (s:=s). am. uh H2; ee; am. uh H4; ee; am. uh H2; ee. rw H8. rww target_lf_proj. uh H4; ee. rw H8. rww target_lf_proj. uh H2; uh H4; ee. rww H10. Qed. Lemma are_finverse_dotted_choice_gz_proj_lf_proj : forall a s, has_left_fractions a s -> are_finverse (dotted_choice (gz_proj a s) (lf_proj a s)) (dotted_choice (lf_proj a s) (gz_proj a s)). Proof. ir. ap are_finverse_dotted_choice. sh a. sh s. ee. ap is_localization_gz_proj. uh H; ee; uh H; ee; am. ap is_localization_lf_proj. am. Qed. (** Now we investigate how localization fits with the opposite category construction, in order to obtain the right fraction construction directly from the left one. ***) Definition oppms s := Image.create s flip. Lemma inc_oppms : forall s y, inc y (oppms s) = inc (flip y) s. Proof. ir. ap iff_eq; ir. ufi oppms H. rwi Image.inc_rw H. nin H. ee. wr H0. rww flip_flip. uf oppms. rw Image.inc_rw. sh (flip y). ee. am. rww flip_flip. Qed. Lemma oppms_oppms : forall s, oppms (oppms s) = s. Proof. ir. ap extensionality; uhg; ir. rwi inc_oppms H. rwi inc_oppms H. rwi flip_flip H. am. rw inc_oppms. rw inc_oppms. rww flip_flip. Qed. Lemma localizing_system_oppms : forall a s, localizing_system (opp a) (oppms s) = localizing_system a s. Proof. assert (forall a s, localizing_system (opp a) (oppms s) -> localizing_system a s). ir. uh H; ee. uhg; ee. rwi axioms_opp H. am. ir. assert (u = flip (flip u)). rww flip_flip. rw H2. wr mor_opp. ap H0. rw inc_oppms. rww flip_flip. ir. ap iff_eq; ir. ap H. am. ap H. rw opp_opp. rw oppms_oppms. am. Qed. Lemma multiplicative_system_oppms : forall a s, multiplicative_system (opp a) (oppms s) = multiplicative_system a s. Proof. assert (forall a s, multiplicative_system (opp a) (oppms s) -> multiplicative_system a s). ir. uh H; ee. uhg; dj. rwi localizing_system_oppms H. am. ir. assert (mor a y). ap inc_ms_mor. sh s; ee; am. assert (mor a z). ap inc_ms_mor. sh s; ee; am. assert (comp a y z = flip (comp (opp a) (flip z) (flip y))). rw comp_opp. rww flip_flip. rww flip_flip. rww flip_flip. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip. rw target_flip. sy; am. alike. alike. rw H7. wr inc_oppms. ap H0. rw inc_oppms. rww flip_flip. rw inc_oppms. rww flip_flip. rw source_flip; try alike. rww target_flip; try alike. sy; am. ir. ap iff_eq; ir. ap H. am. ap H. rw opp_opp. rw oppms_oppms. am. Qed. Lemma are_inverse_opp : forall a u v, are_inverse (opp a) (flip u) (flip v) = are_inverse a u v. Proof. assert (forall a u v, are_inverse a u v -> are_inverse (opp a) (flip u) (flip v)). ir. uh H; ee. uhg; ee. rww mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip; try alike. sy; am. rw source_flip; try alike. rw target_flip; try alike. sy; am. rw comp_opp. rw flip_flip. rw flip_flip. rw H4. rw id_opp. rw source_flip; try alike. rww H1. rw ob_opp. rw source_flip; try alike. rww ob_target. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip; try alike. sy; am. rw comp_opp. rw flip_flip. rw flip_flip. rw H3. rw id_opp. rw source_flip; try alike. rww H2. rw ob_opp. rw source_flip; try alike. rww ob_target. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip; try alike. sy; am. ir. ap iff_eq; ir. assert (a = opp (opp a)). rww opp_opp. assert (u = flip (flip u)). rww flip_flip. assert (v = flip (flip v)). rww flip_flip. rw H1; rw H2; rw H3. ap H. am. au. Qed. Lemma invertible_opp : forall a u, invertible (opp a) (flip u) = invertible a u. Proof. assert (forall a u, invertible a u -> invertible (opp a) (flip u)). ir. uhg; ee. uh H; ee. nin H. sh (flip x). rww are_inverse_opp. ir. ap iff_eq; ir. assert (a = opp (opp a)). rww opp_opp. assert (u = flip (flip u)). rww flip_flip. rw H1; rw H2. ap H. am. au. Qed. Lemma localizes_oppms_oppf : forall a s f, localizes (opp a) (oppms s) (oppf f) = localizes a s f. Proof. assert (forall a s f, localizes a s f -> localizes (opp a) (oppms s) (oppf f)). ir. uhg; ee. rw localizing_system_oppms. uh H; ee; am. app oppf_axioms. uh H; ee; am. rw source_oppf. ap uneq. uh H; ee; am. uh H; ee; am. ir. rw target_oppf. rw fmor_oppf. rw invertible_opp. uh H; ee. ap H3. wrr inc_oppms. uh H; ee; am. rww source_oppf. rw mor_opp. rwi inc_oppms H0. uh H; ee. rw H2. ap inc_ms_mor. sh s; ee; am. uh H; ee; am. uh H; ee; am. ir. ap iff_eq; ir. assert (a = opp (opp a)). rww opp_opp. assert (s = oppms (oppms s)). rww oppms_oppms. assert (f = oppf (oppf f)). rww oppf_oppf. rw H1; rw H2; rw H3. ap H. am. au. Qed. Lemma completes_triangle_oppf : forall f g h, completes_triangle (oppf f) (oppf g) (oppf h) = completes_triangle f g h. Proof. assert (forall f g h, completes_triangle f g h-> completes_triangle (oppf f) (oppf g) (oppf h)). ir. uh H; ee. uhg; ee. app oppf_axioms. app oppf_axioms. app oppf_axioms. rww source_oppf. rw source_oppf. rww H2. am. rw source_oppf. rw target_oppf. rww H3. am. am. rw target_oppf. rw target_oppf. rww H4. am. am. rw fcompose_oppf. rww H5. am. am. am. ir. ap iff_eq; ir. assert (f = oppf (oppf f)). rww oppf_oppf. assert (g = oppf (oppf g)). rww oppf_oppf. assert (h = oppf (oppf h)). rww oppf_oppf. rw H1; rw H2; rw H3. app H. au. Qed. Lemma is_localization_oppms_oppf : forall a s f, is_localization (opp a) (oppms s) (oppf f) = is_localization a s f. Proof. assert (forall a s f, is_localization a s f -> is_localization (opp a) (oppms s) (oppf f) ). ir. uhg; dj. rw localizes_oppms_oppf. uh H; ee; am. ir. assert (g = oppf (oppf g)). rww oppf_oppf. rwi H2 H1. rwi localizes_oppms_oppf H1. rw completes_triangle_dotted_choice. sh (oppf (dotted_choice f (oppf g))). wr completes_triangle_oppf. rw oppf_oppf. rw oppf_oppf. uh H; ee. ap H3. am. ir. wri completes_triangle_oppf H2. rwi oppf_oppf H2. uh H; ee. cp (H4 _ _ H2). assert (completes_triangle f (oppf g) (oppf (dotted_choice (oppf f) g))). wr completes_triangle_oppf. rw oppf_oppf. rw oppf_oppf. ap H1. wri completes_triangle_oppf H2. rwi oppf_oppf H2. rwi oppf_oppf H2. uh H2; ee. wr H11. ap localizes_fcompose. am. am. am. cp (H4 _ _ H6). assert (h = oppf (oppf h)). rww oppf_oppf. rw H8. rw H5. wr H7. rw oppf_oppf. tv. ir. ap iff_eq; ir. assert (a = opp (opp a)). rww opp_opp. assert (s = oppms (oppms s)). rww oppms_oppms. assert (f = oppf (oppf f)). rww oppf_oppf. rw H1; rw H2; rw H3. ap H. am. app H. Qed. (** We thus obtain a rapid treatment of right fractions. First recall the definition of left fractions, rewritten slightly. **) Lemma has_left_fractions_rw : forall a s, has_left_fractions a s = ( multiplicative_system a s & (forall x, ob a x -> inc (id a x) s) & (forall r g, inc r s -> mor a g -> source r = source g -> exists p, exists q, (mor a p & inc q s & target p = target q & source p = target r & source q = target g & comp a q g = comp a p r)) & (forall v r t, inc v s -> mor a r -> mor a t -> source r = target v -> source t = target v -> comp a r v = comp a t v -> exists w, (inc w s & source w = target r & source w = target t & comp a w r = comp a w t))). Proof. ir. ap iff_eq; ir. uh H; ee; try am. ir. cp (H1 r g H3 H4 H5). nin H6. ee. sh (lf_forward x). sh (lf_backward x). ee; try am. ap mor_lf_forward. sh s; am. ap inc_lf_backward. sh a; am. rw target_lf_forward. rw target_lf_backward. tv. sh a; sh s; am. rw source_lf_forward. am. uh H6; ee; am. rw source_lf_backward. am. uh H6; ee; am. uhg; ee; try am. ir. cp (H1 r g H3 H4 H5). nin H6. nin H6; ee. sh (lf_symbol x x0). ee; try am. ap is_lf_symbol_lf_symbol. uhg; ee. uh H; ee; am. am. am. am. rw source_lf_symbol. am. rww target_lf_symbol. rw lf_backward_lf_symbol. rww lf_forward_lf_symbol. Qed. Definition has_right_fractions a s := multiplicative_system a s & (forall x, ob a x -> inc (id a x) s) & (forall r g, inc r s -> mor a g -> target r = target g -> exists p, exists q, (mor a q & inc p s & source p = source q & target p = source g & target q = source r & comp a g p = comp a r q)) & (forall v r t, inc v s -> mor a r -> mor a t -> source v = target r -> source v = target t -> comp a v r = comp a v t -> exists w, (inc w s & source r = target w & source t = target w & comp a r w = comp a t w)). Lemma has_right_fractions_rw : forall a s, has_right_fractions a s = has_left_fractions (opp a) (oppms s). Proof. ir. ap iff_eq; ir. rw has_left_fractions_rw. uh H; ee. rw multiplicative_system_oppms. am. ir. rw inc_oppms. rw id_opp. rw flip_flip. ap H0. rwi ob_opp H3. am. am. ir. assert (mor (opp a) r). ap inc_ms_mor. sh (oppms s). ee. wr localizing_system_oppms. rw oppms_oppms. rw opp_opp. uh H; ee; am. am. cp H4. rwi inc_oppms H3. rwi mor_opp H4. assert (target (flip r) = target (flip g)). rw target_flip. rw target_flip. am. alike. alike. cp (H1 (flip r) (flip g) H3 H4 H8). nin H9. nin H9. ee. assert (mor a x). ap inc_ms_mor. sh s; ee; try am. uh H; ee; am. sh (flip x0). sh (flip x). ee. rw mor_opp. rww flip_flip. rw inc_oppms. rww flip_flip. rw target_flip; try alike. rw target_flip; try alike. sy; am. rw source_flip; try alike. rwi source_flip H13; try alike. am. rw source_flip; try alike. rwi source_flip H12; try alike. am. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. ap uneq. am. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H13; try alike. am. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H12; try alike. am. ir. cp H4. cp H5. cp H6. cp H7. assert (mor (opp a) v). rw mor_opp. ap inc_ms_mor. sh s; ee. uh H; ee; am. wrr inc_oppms. rwi inc_oppms H3. rwi mor_opp H4. rwi mor_opp H5. assert (target v = source (flip v)). rww source_flip; try alike. wri target_flip H6; try alike. wri target_flip H7. rwi H14 H6. rwi H14 H7. assert (comp a (flip v) (flip r) = comp a (flip v) (flip t)). transitivity (flip (flip (comp a (flip v) (flip r)))). rww flip_flip. rwi comp_opp H8. rw H8. rw comp_opp. rww flip_flip. am. am. am. am. am. am. assert (source (flip v) = target (flip r)). sy; am. assert (source (flip v) = target (flip t)). sy; am. cp (H2 (flip v) (flip r) (flip t) H3 H4 H5 H16 H17 H15). nin H18. ee. assert (mor a x). ap inc_ms_mor. sh s. ee. uh H; ee; am. am. sh (flip x). ee. rw inc_oppms. rww flip_flip. rw source_flip; try alike. wr H19. rww source_flip; try alike. rw source_flip; try alike. wr H20. rww source_flip; try alike. rw comp_opp. rw flip_flip. rw comp_opp. rw flip_flip. rww H21. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. wr H20. rww source_flip; try alike. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. wr H19. rww source_flip; try alike. alike. (** Now we have to do essentially the same thing in the other direction. **) cp H. rwi has_left_fractions_rw H0. ee. uhg; ee. wr multiplicative_system_oppms. am. ir. wri ob_opp H4. cp (H1 x H4). rwi id_opp H5. rwi inc_oppms H5. rwi flip_flip H5. am. am. ir. assert (mor a r). ap inc_ms_mor. sh s; ee. wr localizing_system_oppms. uh H0; ee; am. am. assert (inc (flip r) (oppms s)). rw inc_oppms. rww flip_flip. assert (mor (opp a) (flip g)). rw mor_opp. rww flip_flip. assert (source (flip r) = source (flip g)). rw source_flip; try alike. rw source_flip; try alike. am. cp (H2 _ _ H8 H9 H10). nin H11. nin H11. ee. assert (mor (opp a) x0). ap inc_ms_mor. sh (oppms s); ee. uh H0; ee; am. am. sh (flip x0). sh (flip x). ee. wrr mor_opp. wrr inc_oppms. rw source_flip; try alike. rw source_flip; try alike. sy; am. rw target_flip; try alike. rwi target_flip H15; try alike. am. rw target_flip; try alike. rwi target_flip H14; try alike. am. rwi comp_opp H16. rwi flip_flip H16. rwi comp_opp H16. rwi flip_flip H16. transitivity (flip (flip (comp a g (flip x0)))). rww flip_flip. rw H16. rww flip_flip. am. rw mor_opp. rww flip_flip. am. am. rw mor_opp. rww flip_flip. am. ir. assert (mor a v). ap inc_ms_mor. sh s. ee. wr localizing_system_oppms. uh H0; ee; am. am. assert (inc (flip v) (oppms s)). rw inc_oppms. rww flip_flip. assert (mor (opp a) (flip r)). rw mor_opp. rww flip_flip. assert (mor (opp a) (flip t)). rw mor_opp. rww flip_flip. assert (source (flip r) = target (flip v)). rw source_flip; try alike. rw target_flip; try alike. sy; am. assert (source (flip t) = target (flip v)). rw source_flip; try alike. rw target_flip; try alike. sy; am. assert (comp (opp a) (flip r) (flip v) = comp (opp a) (flip t) (flip v)). rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw flip_flip. rww H9. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip; try alike. sy; am. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip; try alike. sy; am. cp (H3 _ _ _ H11 H12 H13 H14 H15 H16). nin H17. ee. assert (mor (opp a) x). ap inc_ms_mor. sh (oppms s). ee. uh H0; ee; am. am. cp H18; cp H19. rwi target_flip H22; try alike. rwi target_flip H23; try alike. sh (flip x). ee. wr inc_oppms. am. rw target_flip; try alike. sy; am. rw target_flip; try alike. sy; am. rwi comp_opp H20. rwi flip_flip H20. rwi comp_opp H20. rwi flip_flip H20. transitivity (flip (flip (comp a r (flip x)))). rw flip_flip. reflexivity. rw H20. rw flip_flip. reflexivity. am. rw mor_opp. rww flip_flip. am. am. rw mor_opp. rww flip_flip. am. Qed. Definition right_frac_cat a s := opp (left_frac_cat (opp a) (oppms s)). Definition rf_proj a s := oppf (lf_proj (opp a) (oppms s)). Lemma right_frac_cat_axioms : forall a s, has_right_fractions a s -> Category.axioms (right_frac_cat a s). Proof. ir. uf right_frac_cat. ap opp_axioms. ap left_frac_cat_axioms. rwi has_right_fractions_rw H. am. Qed. Lemma rf_proj_axioms : forall a s, has_right_fractions a s -> Functor.axioms (rf_proj a s). Proof. ir. rwi has_right_fractions_rw H. uf rf_proj. ap oppf_axioms. ap lf_proj_axioms. am. Qed. Lemma source_rf_proj : forall a s, has_right_fractions a s -> source (rf_proj a s) = a. Proof. ir. rwi has_right_fractions_rw H. uf rf_proj. rw source_oppf. rw source_lf_proj. rww opp_opp. app lf_proj_axioms. Qed. Lemma target_rf_proj : forall a s, has_right_fractions a s -> target (rf_proj a s) = right_frac_cat a s. Proof. ir. rwi has_right_fractions_rw H. uf rf_proj. rw target_oppf. rw target_lf_proj. tv. app lf_proj_axioms. Qed. Lemma is_localization_rf_proj : forall a s, has_right_fractions a s -> is_localization a s (rf_proj a s). Proof. ir. rwi has_right_fractions_rw H. uf rf_proj. wr is_localization_oppms_oppf. rw oppf_oppf. ap is_localization_lf_proj. am. Qed. (** We finish with the consequences of the left (or right) fraction conditions on the description of arrows in the original [gz_localization]. In order to attain a self-contained statement we avoid the notation [lf_symbol] etc. from [gzfractions.v]. **) Definition lf_vee a s p q := localizing_system a s & mor a p & inc q s & target p = target q. Definition lf_vee_image f p q := comp (target f) (inverse (target f) (fmor f q)) (fmor f p). (** The following is basically a restatement of the definition [lf_equiv] from [gzfractions.v]. **) Definition lf_vee_equivalent a s p q r t := lf_vee a s p q & lf_vee a s r t & source p = source r & source q = source t & (exists y, exists z, (mor a y & mor a z & source y = target p & source z = target r & target y = target z & comp a y p = comp a z r & comp a y q = comp a z t & inc (comp a y q) s)). Definition left_fraction_description a s f := localizes a s f & ob_iso f & (forall y, mor (target f) y -> exists p, exists q, (lf_vee a s p q & y = lf_vee_image f p q)) & (forall p q r t, lf_vee a s p q -> lf_vee a s r t -> (lf_vee_image f p q = lf_vee_image f r t) -> lf_vee_equivalent a s p q r t). (** Dualize for the description of right fractions. **) Definition rf_wedge a s p q := localizing_system a s & mor a p & inc q s & source p = source q. Definition rf_wedge_image f p q := comp (target f) (fmor f p) (inverse (target f) (fmor f q)). Definition rf_wedge_equivalent a s p q r t := rf_wedge a s p q & rf_wedge a s r t & target p = target r & target q = target t & (exists y, exists z, (mor a y & mor a z & target y = source p & target z = source r & source y = source z & comp a p y = comp a r z & comp a q y = comp a t z & inc (comp a q y) s)). Definition right_fraction_description a s f := localizes a s f & ob_iso f & (forall y, mor (target f) y -> exists p, exists q, (rf_wedge a s p q & y = rf_wedge_image f p q)) & (forall p q r t, rf_wedge a s p q -> rf_wedge a s r t -> (rf_wedge_image f p q = rf_wedge_image f r t) -> rf_wedge_equivalent a s p q r t). (** Now we get to the results concerning these descriptions. The basic idea is that we can prove the [left_fraction_description] for the construction of localization by left fractions. Then we want to prove that this description is valid for any other localization since they are all isomorphic. In particular it is valid for the standard one. If one looks at the standard construction this is a theorem which looks hard to prove directly. Dualizing we get the same result for right fractions. **) Lemma lf_vee_image_lf_proj : forall a s p q, has_left_fractions a s -> lf_vee a s p q -> lf_vee_image (lf_proj a s) p q = lf_class a s (lf_symbol p q). Proof. ir. assert (is_lf_symbol a s (lf_symbol p q)). ap is_lf_symbol_lf_symbol. uh H0; uhg; ee. uh H; ee. uh H; ee; am. am. am. am. cp (comp_etc_lf_symbol H H1). wr H2. uf lf_vee_image. rw target_lf_proj. rw inverse_fmor_lf_proj. rw lf_backward_lf_symbol. rw lf_forward_lf_symbol. rw fmor_lf_proj. tv. am. uh H0; ee; am. am. uh H0; ee; am. Qed. Lemma left_fraction_description_lf_proj : forall a s, has_left_fractions a s -> left_fraction_description a s (lf_proj a s). Proof. ir. cp (is_localization_lf_proj H). uhg; ee. uh H0; ee; am. uhg. ee. uhg. ee. app lf_proj_axioms. ir. rwi source_lf_proj H1. rwi source_lf_proj H2. rwi fob_lf_proj H3. rwi fob_lf_proj H3. am. am. am. am. am. uhg. ee. app lf_proj_axioms. ir. rwi target_lf_proj H1. rwi ob_left_frac_cat H1. uhg. ee. app lf_proj_axioms. sh x. ee. rww source_lf_proj. rww fob_lf_proj. am. ir. rwi target_lf_proj H1. cp (lfc_mor_expression H H1). nin H2. nin H2. ee. sh x. sh x0. ee. uhg. ee. uh H; ee. uh H; ee; am. am. am. am. uf lf_vee_image. rw target_lf_proj. rw inverse_fmor_lf_proj. rw fmor_lf_proj. am. am. am. am. am. assert (localizing_system a s). uh H; ee; uh H; ee; am. ir. rwi lf_vee_image_lf_proj H4. rwi lf_vee_image_lf_proj H4. assert (lem1 : source p = source r). transitivity (source (lf_class a s (lf_symbol p q))). rw source_lf_class. rww source_lf_symbol. rw H4. rw source_lf_class. rww source_lf_symbol. assert (lem2 : source q = source t). transitivity (target (lf_class a s (lf_symbol p q))). rw target_lf_class. rww target_lf_symbol. rw H4. rw target_lf_class. rww target_lf_symbol. rwi eq_lf_class H4. uh H4; ee. nin H4. ee. uh H4; uh H5. ee. nin H10; nin H15; ee. cp H2; cp H3. uh H20; uh H21; ee. uhg. ee. uhg; ee. am. am. am. am. am. am. am. sh x1. sh x0. ee. am. am. rw H18. uf lf_vertex. rw lf_backward_lf_symbol. sy; am. rw H16. uf lf_vertex. rw lf_backward_lf_symbol. sy; am. transitivity (lf_vertex x). wr H19. rw lf_vertex_lf_extend. tv. am. ap is_lf_symbol_lf_symbol. uhg. ee; try am. am. am. wr H17. rw lf_vertex_lf_extend. tv. am. ap is_lf_symbol_lf_symbol. uhg. ee; try am. am. am. transitivity (lf_forward x). wr H19. rw lf_forward_lf_extend. rw lf_forward_lf_symbol. tv. wr H17. rw lf_forward_lf_extend. rww lf_forward_lf_symbol. transitivity (lf_backward x). wr H19. rw lf_backward_lf_extend. rw lf_backward_lf_symbol. tv. wr H17. rw lf_backward_lf_extend. rw lf_backward_lf_symbol. tv. assert (comp a x1 q = lf_backward x). wr H19. rw lf_backward_lf_extend. rw lf_backward_lf_symbol. tv. rw H28. ap inc_lf_backward. sh a; am. am. ap is_lf_symbol_lf_symbol. uhg. ee; try am. uh H2; ee; am. uh H2; ee; am. uh H2; ee; am. ap is_lf_symbol_lf_symbol. uhg. ee; try am. uh H3; ee; am. uh H3; ee; am. uh H3; ee; am. am. am. am. am. Qed. Lemma mor_lf_vee_image : forall f p q, (exists a, exists s, (lf_vee a s p q & localizes a s f)) -> mor (target f) (lf_vee_image f p q). Proof. ir. nin H. nin H. ee. uf lf_vee_image. rww mor_comp. app mor_inverse. uh H0; ee. ap H3. uh H; ee; am. app mor_fmor. uh H0; ee; am. uh H0; ee. rw H2. uh H; ee; am. rw source_inverse. uh H0; ee. rww target_fmor. rww target_fmor. uh H; ee. rww H6. rw H2. uh H; ee; am. rw H2. ap inc_ms_mor. uh H; sh x0; ee; am. uh H0; ee. ap H3. uh H; ee; am. Qed. Lemma lf_vee_image_fcompose : forall f g p q, Functor.axioms f -> Functor.axioms g -> source f = target g -> mor (source g) p -> mor (source g) q -> invertible (source f) (fmor g q) -> target p = target q -> lf_vee_image (fcompose f g) p q = fmor f (lf_vee_image g p q). Proof. ir. assert (mor (source f) (fmor g p)). rw H1. app mor_fmor. assert (invertible (source f) (fmor g q)). rw H1. wrr H1. assert (mor (source f) (fmor g q)). rw H1. app mor_fmor. uf lf_vee_image. rw target_fcompose. rww fmor_fcompose. rww fmor_comp. rww fmor_inverse. rww fmor_fcompose. app mor_inverse. wrr H1. wrr H1. rww source_inverse. rww target_fmor. rww target_fmor. rww H5. wrr H1. Qed. Lemma left_fraction_description_invariant : forall a s f g, left_fraction_description a s f -> has_finverse g -> source g = target f -> left_fraction_description a s (fcompose g f). Proof. ir. uh H0; nin H0. uh H0; ee. assert (Functor.axioms f). uh H; ee. uh H; ee. am. uhg; ee. ap localizes_fcompose. uh H; ee; am. am. am. uhg; ee. uhg; ee. app fcompose_axioms. ir. rwi source_fcompose H8. rwi source_fcompose H9. assert (ob_inj f). uh H; ee. uh H11; ee; am. uh H11; ee. ap H12. am. am. transitivity (fob x (fob (fcompose g f) x0)). transitivity (fob (fidentity (source g)) (fob f x0)). rw fob_fidentity. tv. rw H1. app ob_fob. wr H6. rw fob_fcompose. rw fob_fcompose. tv. am. am. am. am. am. am. am. rw H1. app ob_fob. rw H10. rw fob_fcompose. transitivity (fob (fidentity (source g)) (fob f y)). wr H6. rw fob_fcompose. tv. am. am. am. rw H1. app ob_fob. rw fob_fidentity. tv. rw H1. app ob_fob. am. am. am. am. assert (ob_surj f). uh H; ee. uh H8; ee; am. uh H8; ee. uhg; ee. ap fcompose_axioms. am. am. am. ir. rwi target_fcompose H10. assert (ob (source x) x0). rww H4. uhg. ee. app fcompose_axioms. assert (ob (target f) (fob x x0)). wr H1. rw H3. app ob_fob. cp (H9 _ H12). uh H13. ee. nin H14. ee. sh x1. ee. rww source_fcompose. rw fob_fcompose. rw H15. wr fob_fcompose. rw H5. rww fob_fidentity. am. am. am. am. am. am. am. am. ir. rwi target_fcompose H8. assert (mor (target f) (fmor x y)). wr H1. rw H3. app mor_fmor. rww H4. uh H; ee. cp (H11 _ H9). nin H13. nin H13. ee. sh x0. sh x1. ee. am. rww lf_vee_image_fcompose. wr H14. wr fmor_fcompose. rw H5. rww fmor_fidentity. rww H4. am. am. am. rww H4. uh H; ee. rw H16. uh H13; ee; am. uf lf_vee_image. uh H; ee. rw H16. ap inc_ms_mor. sh s. ee. am. uh H13; ee; am. rw H1. uh H; ee. ap H17. uh H13; ee; am. uh H13; ee; am. assert (lem1 : source f = a). uh H; ee. uh H; ee. uh H; ee; am. ir. uh H; ee. ap H13. am. am. transitivity (fmor x (fmor g (lf_vee_image f p q))). wrr fmor_fcompose. rw H6. rww fmor_fidentity. rw H1. ap mor_lf_vee_image. sh a; sh s. ee. am. am. rw H1. ap mor_lf_vee_image. sh a; sh s; ee; am. rwi lf_vee_image_fcompose H10. rwi lf_vee_image_fcompose H10. rw H10. wr fmor_fcompose. rw H6. rww fmor_fidentity. rw H1. ap mor_lf_vee_image. sh a; sh s; ee; am. am. am. am. rw H1. ap mor_lf_vee_image. sh a; sh s; ee; am. am. am. am. rw lem1. uh H9; ee; am. rw lem1. ap inc_ms_mor. sh s; ee. uh H; ee; am. uh H9; ee; am. rw H1. uh H; ee. ap H16. uh H9; ee; am. uh H9; ee; am. am. am. am. rw lem1. uh H8; ee; am. rw lem1. ap inc_ms_mor. sh s; ee. uh H; ee; am. uh H8; ee; am. rw H1. uh H; ee. ap H16. uh H8; ee; am. uh H8; ee; am. Qed. Lemma left_fraction_description_for_loc : forall a s f, has_left_fractions a s -> is_localization a s f -> left_fraction_description a s f. Proof. ir. assert (f = fcompose (dotted_choice (lf_proj a s) f) (lf_proj a s)). sy. ap fcompose_dotted_choice. sh a. sh s. ee. ap is_localization_lf_proj. am. uh H0; ee; am. rw H1. ap left_fraction_description_invariant. app left_fraction_description_lf_proj. uhg. sh (dotted_choice f (lf_proj a s)). ap are_finverse_dotted_choice. sh a; sh s. ee. app is_localization_lf_proj. am. rw source_dotted_choice. tv. sh a; sh s; ee. app is_localization_lf_proj. uh H0; ee; am. Qed. Lemma left_fraction_description_gz_proj : forall a s, has_left_fractions a s -> left_fraction_description a s (gz_proj a s). Proof. ir. ap left_fraction_description_for_loc. am. ap is_localization_gz_proj. uh H; ee. uh H; ee; am. Qed. Lemma inverse_opp : forall a u, invertible a (flip u) -> inverse (opp a) u = flip (inverse a (flip u)). Proof. ir. uh H; ee. nin H. assert (are_inverse (opp a) (flip x) u). uh H; ee. assert (source x = source u). rwi target_flip H2. am. wri mor_opp H. alike. assert (target x = target u). rwi source_flip H1. sy; am. wri mor_opp H. alike. uhg; dj. rw mor_opp. rww flip_flip. rww mor_opp. rw source_flip; try alike. rwi source_flip H1; try alike. sy; am. rw target_flip; try alike. rwi target_flip H2; try alike. sy; am. rw comp_opp. rw flip_flip. rw H3. rw id_opp. rww H5. rww ob_source. am. am. rw source_flip. am. alike. rw comp_opp. rw flip_flip. rw H4. rw id_opp. rw H9. rw H1. rww H6. rww ob_source. am. am. am. ap inverse_eq. ap are_inverse_symm. assert (inverse a (flip u) = x). ap inverse_eq. am. rw H1. am. Qed. Lemma right_fraction_description_rw : forall a s f, right_fraction_description a s f = left_fraction_description (opp a) (oppms s) (oppf f). Proof. assert (prop1 : forall a s f, left_fraction_description a s f -> right_fraction_description (opp a) (oppms s) (oppf f)). ir. assert (Functor.axioms f). uh H; ee. uh H; ee. am. uh H; ee. uhg; ee. rw localizes_oppms_oppf. am. uhg; ee. uhg; ee. ap oppf_axioms. am. ir. rwi source_oppf H4. rwi source_oppf H5. rwi ob_opp H4. rwi ob_opp H5. rwi fob_oppf H6. rwi fob_oppf H6. uh H1; ee. uh H1; ee. app H8. am. rw source_oppf. rww ob_opp. am. am. rww source_oppf. rww ob_opp. am. am. uh H1; ee. uh H4; ee. uhg; ee. app oppf_axioms. ir. rwi target_oppf H6. rwi ob_opp H6. cp (H5 _ H6). uh H7; ee. nin H8. ee. uhg; ee. app oppf_axioms. sh x0. ee. rww source_oppf. rww ob_opp. rww fob_oppf. rww source_oppf. rww ob_opp. am. ir. rwi target_oppf H4. rwi mor_opp H4. cp (H2 _ H4). nin H5. nin H5. ee. sh (flip x). sh (flip x0). ee. uhg; ee. rw localizing_system_oppms. uh H; ee; am. rw mor_opp. rw flip_flip. uh H5; ee; am. rw inc_oppms. rw flip_flip. uh H5; ee; am. assert (mor a x). uh H5; ee ;am. assert (mor a x0). ap inc_ms_mor. sh s. ee. uh H; ee; am. uh H5; ee; am. rw source_flip; try alike. rw source_flip; try alike. uh H5; ee. am. transitivity (flip (flip y)). rww flip_flip. rw H6. uf lf_vee_image. uf rf_wedge_image. rw target_oppf. rw fmor_oppf. rw fmor_oppf. rw comp_opp. rw flip_flip. rw flip_flip. rw flip_flip. rw inverse_opp. rw flip_flip. rw flip_flip. reflexivity. rw flip_flip. uh H; ee. ap H9. uh H5; ee; am. rw flip_flip. rw mor_opp. rw flip_flip. ap mor_fmor. am. uh H; ee. rw H8. uh H5; ee; am. rw flip_flip. rw inverse_opp. rw flip_flip. rw mor_opp. rw flip_flip. ap mor_inverse. uh H; ee. ap H9. uh H5; ee; am. rw flip_flip. uh H; ee. ap H9. uh H5; ee; am. rw flip_flip. rw flip_flip. rw inverse_opp. rw flip_flip. rw target_flip. rw source_inverse. rw source_flip. rw target_fmor. rw target_fmor. ap uneq. uh H5; ee; am. am. uh H; ee. rw H8. ap inc_ms_mor. sh s; ee. am. uh H5; ee; am. am. uh H; ee. rw H8. uh H5; ee; am. assert (mor (target f) (fmor f x)). ap mor_fmor. am. uh H; ee. rw H8. uh H5; ee; am. alike. uh H; ee. ap H9. uh H5; ee; am. assert (mor (target f) (inverse (target f) (fmor f x0))). ap mor_inverse. uh H; ee. ap H9. uh H5; ee; am. alike. rw flip_flip. uh H; ee. ap H9. uh H5; ee; am. am. rw source_oppf. rw mor_opp. rw flip_flip. uh H; ee. rw H8. ap inc_ms_mor. sh s; ee. am. uh H5; ee; am. am. am. rw source_oppf. rw mor_opp. rw flip_flip. uh H; ee. rw H8. uh H5; ee; am. am. am. am. ir. uh H4; uh H5; ee. cp H. uh H; ee. assert (mor a (flip p)). wrr mor_opp. assert (inc (flip q) s). wrr inc_oppms. assert (mor a (flip q)). ap inc_ms_mor. sh s; ee; am. assert (mor (opp a) q). ap inc_ms_mor. sh (oppms s); ee; am. assert (target (flip p) = target (flip q)). rw target_flip; try alike. rw target_flip; try alike. am. assert (mor a (flip r)). wrr mor_opp. assert (inc (flip t) s). wrr inc_oppms. assert (mor a (flip t)). ap inc_ms_mor. sh s; ee; am. assert (mor (opp a) t). ap inc_ms_mor. sh (oppms s); ee; am. assert (target (flip r) = target (flip t)). rw target_flip; try alike. rw target_flip; try alike. am. assert (lf_vee a s (flip p) (flip q)). uhg; ee; try am. assert (lf_vee a s (flip r) (flip t)). uhg; ee; try am. assert (invertible (target f) (fmor f (flip q))). uh H; ee. ap H16. am. assert (sfa : source f = a). uh H; ee; am. assert (rf_wedge_image (oppf f) p q = flip (lf_vee_image f (flip p) (flip q))). uf rf_wedge_image. uf lf_vee_image. rw target_oppf. rw comp_opp. rw fmor_oppf. rw fmor_oppf. rw flip_flip. rw inverse_opp. rw flip_flip. rw flip_flip. tv. rw flip_flip. am. am. rw source_oppf. rw sfa. am. am. am. rw source_oppf. rw sfa. am. am. rw mor_opp. rw fmor_oppf. rw flip_flip. ap mor_fmor. am. rw sfa. am. am. rw source_oppf. rw sfa. am. am. rw inverse_opp. rw mor_opp. rw flip_flip. rw fmor_oppf. rw flip_flip. ap mor_inverse. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw flip_flip. am. am. rw source_oppf. rww sfa. am. rw target_inverse. rw fmor_oppf. rw fmor_oppf. rw source_flip. rw source_flip. rw target_fmor. rw target_fmor. rww H21. am. rww sfa. am. rww sfa. assert (mor (target f) (fmor f (flip q))). ap mor_fmor. am. rww sfa. alike. assert (mor (target f) (fmor f (flip p))). ap mor_fmor. am. rww sfa. alike. am. rw source_oppf. rww sfa. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw invertible_opp. am. am. rw source_oppf. rww sfa. am. am. assert (invertible (target f) (fmor f (flip t))). uh H; ee. ap H16. am. assert (rf_wedge_image (oppf f) r t = flip (lf_vee_image f (flip r) (flip t))). uf rf_wedge_image. uf lf_vee_image. rw target_oppf. rw comp_opp. rw fmor_oppf. rw fmor_oppf. rw flip_flip. rw inverse_opp. rw flip_flip. rw flip_flip. reflexivity. rw flip_flip. am. am. rw source_oppf. rw sfa. am. am. am. rw source_oppf. rw sfa. am. am. rw mor_opp. rw fmor_oppf. rw flip_flip. ap mor_fmor. am. rw sfa. am. am. rw source_oppf. rw sfa. am. am. rw inverse_opp. rw mor_opp. rw flip_flip. rw fmor_oppf. rw flip_flip. ap mor_inverse. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw flip_flip. am. am. rw source_oppf. rww sfa. am. rw target_inverse. rw fmor_oppf. rw fmor_oppf. rw source_flip. rw source_flip. rw target_fmor. rw target_fmor. rww H26. am. rww sfa. am. rww sfa. assert (mor (target f) (fmor f (flip t))). ap mor_fmor. am. rww sfa. alike. assert (mor (target f) (fmor f (flip r))). ap mor_fmor. am. rww sfa. alike. am. rw source_oppf. rww sfa. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw invertible_opp. am. am. rw source_oppf. rww sfa. am. am. assert (lf_vee_equivalent a s (flip p) (flip q) (flip r) (flip t)). ap H3. am. am. transitivity (flip (flip (lf_vee_image f (flip p) (flip q)))). rww flip_flip. wr H30. rw H6. rw H32. rww flip_flip. uh H33; ee. nin H37. nin H37. ee. cp H35; cp H36. rwi source_flip H45. rwi source_flip H45. rwi source_flip H46. rwi source_flip H46. uhg; ee. uhg; ee; am. uhg; ee; am. am. am. sh (flip x). sh (flip x0). ee. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw target_flip. rwi target_flip H39. am. alike. alike. rw target_flip; try alike. rwi target_flip H40; try alike. am. rw source_flip; try alike. rw source_flip; try alike. am. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw H42. reflexivity. am. rw mor_opp. rww flip_flip. rw target_flip; try alike. rwi target_flip H40; try alike. sy; am. am. rw mor_opp. rww flip_flip. rw target_flip; try alike. rwi target_flip H39; try alike. sy; am. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw H43. reflexivity. am. rw mor_opp. rww flip_flip. rw target_flip; try alike. rwi target_flip H40; try alike. rw H40. sy; am. am. rw mor_opp. rww flip_flip. rw target_flip; try alike. rwi target_flip H39; try alike. rw H39. sy; am. rw inc_oppms. rw comp_opp. rw flip_flip. rw flip_flip. am. am. rw mor_opp. rww flip_flip. rw target_flip; try alike. rwi target_flip H39; try alike. rw H39. sy; am. alike. alike. alike. alike. assert (prop2 : forall a s f, right_fraction_description a s f -> left_fraction_description (opp a) (oppms s) (oppf f)). (** We try just to recopy the proof of the previous assertion and change as little as possible **) ir. assert (Functor.axioms f). uh H; ee. uh H; ee. am. uh H; ee. uhg; ee. rw localizes_oppms_oppf. am. uhg; ee. uhg; ee. ap oppf_axioms. am. ir. rwi source_oppf H4. rwi source_oppf H5. rwi ob_opp H4. rwi ob_opp H5. rwi fob_oppf H6. rwi fob_oppf H6. uh H1; ee. uh H1; ee. app H8. am. rw source_oppf. rww ob_opp. am. am. rww source_oppf. rww ob_opp. am. am. uh H1; ee. uh H4; ee. uhg; ee. app oppf_axioms. ir. rwi target_oppf H6. rwi ob_opp H6. cp (H5 _ H6). uh H7; ee. nin H8. ee. uhg; ee. app oppf_axioms. sh x0. ee. rww source_oppf. rww ob_opp. rww fob_oppf. rww source_oppf. rww ob_opp. am. ir. rwi target_oppf H4. rwi mor_opp H4. cp (H2 _ H4). nin H5. nin H5. ee. sh (flip x). sh (flip x0). ee. uhg; ee. rw localizing_system_oppms. uh H; ee; am. rw mor_opp. rw flip_flip. uh H5; ee; am. rw inc_oppms. rw flip_flip. uh H5; ee; am. assert (mor a x). uh H5; ee ;am. assert (mor a x0). ap inc_ms_mor. sh s. ee. uh H; ee; am. uh H5; ee; am. rw target_flip; try alike. rw target_flip; try alike. uh H5; ee. am. transitivity (flip (flip y)). rww flip_flip. rw H6. uf lf_vee_image. uf rf_wedge_image. rw target_oppf. rw fmor_oppf. rw fmor_oppf. rw comp_opp. rw flip_flip. rw flip_flip. rw flip_flip. rw inverse_opp. rw flip_flip. rw flip_flip. reflexivity. rw flip_flip. uh H; ee. ap H9. uh H5; ee; am. rw flip_flip. rw inverse_opp. rw flip_flip. rw mor_opp. rw flip_flip. ap mor_inverse. uh H; ee. ap H9. uh H5; ee; am. rw flip_flip. uh H; ee. ap H9. uh H5; ee; am. rw flip_flip. rw mor_opp. rw flip_flip. ap mor_fmor. am. uh H; ee. rw H8. uh H5; ee; am. rw flip_flip. rw flip_flip. rw inverse_opp. rw flip_flip. rw source_flip. rw target_inverse. rw target_flip. rw source_fmor. rw source_fmor. ap uneq. uh H5; ee; sy; am. am. uh H; ee. rw H8. uh H5; ee. am. am. uh H; ee. rw H8. ap inc_ms_mor. sh s; ee. am. uh H5; ee; am. assert (mor (target f) (fmor f x)). ap mor_fmor. am. uh H; ee. rw H8. uh H5; ee; am. alike. uh H; ee. ap H9. uh H5; ee; am. assert (mor (target f) (inverse (target f) (fmor f x0))). ap mor_inverse. uh H; ee. ap H9. uh H5; ee; am. alike. rw flip_flip. uh H; ee. ap H9. uh H5; ee; am. am. rw source_oppf. rw mor_opp. rw flip_flip. uh H; ee. rw H8. uh H5; ee; am. am. am. rw source_oppf. rw mor_opp. rw flip_flip. uh H; ee. rw H8. ap inc_ms_mor. sh s; ee. am. uh H5; ee; am. am. am. am. ir. uh H4; uh H5; ee. cp H. uh H; ee. assert (mor a (flip p)). wrr mor_opp. assert (inc (flip q) s). wrr inc_oppms. assert (mor a (flip q)). ap inc_ms_mor. sh s; ee; am. assert (mor (opp a) q). ap inc_ms_mor. sh (oppms s); ee; am. assert (source (flip p) = source (flip q)). rw source_flip; try alike. rw source_flip; try alike. am. assert (mor a (flip r)). wrr mor_opp. assert (inc (flip t) s). wrr inc_oppms. assert (mor a (flip t)). ap inc_ms_mor. sh s; ee; am. assert (mor (opp a) t). ap inc_ms_mor. sh (oppms s); ee; am. assert (source (flip r) = source (flip t)). rw source_flip; try alike. rw source_flip; try alike. am. assert (rf_wedge a s (flip p) (flip q)). uhg; ee; try am. assert (rf_wedge a s (flip r) (flip t)). uhg; ee; try am. assert (invertible (target f) (fmor f (flip q))). uh H; ee. ap H16. am. assert (sfa : source f = a). uh H; ee; am. assert (lf_vee_image (oppf f) p q = flip (rf_wedge_image f (flip p) (flip q))). uf rf_wedge_image. uf lf_vee_image. rw target_oppf. rw comp_opp. rw fmor_oppf. rw fmor_oppf. rw flip_flip. rw inverse_opp. rw flip_flip. rw flip_flip. tv. rw flip_flip. am. am. rw source_oppf. rw sfa. am. am. am. rw source_oppf. rw sfa. am. am. rw inverse_opp. rw mor_opp. rw flip_flip. rw fmor_oppf. rw flip_flip. ap mor_inverse. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw flip_flip. am. am. rw source_oppf. rww sfa. am. rw mor_opp. rw fmor_oppf. rw flip_flip. ap mor_fmor. am. rw sfa. am. am. rw source_oppf. rw sfa. am. am. rw source_inverse. rw fmor_oppf. rw fmor_oppf. rw target_flip. rw target_flip. rw source_fmor. rw source_fmor. rww H21. am. rww sfa. am. rww sfa. assert (mor (target f) (fmor f (flip p))). ap mor_fmor. am. rww sfa. alike. assert (mor (target f) (fmor f (flip q))). ap mor_fmor. am. rww sfa. alike. am. rw source_oppf. rww sfa. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw invertible_opp. am. am. rw source_oppf. rww sfa. am. am. assert (invertible (target f) (fmor f (flip t))). uh H; ee. ap H16. am. assert (lf_vee_image (oppf f) r t = flip (rf_wedge_image f (flip r) (flip t))). uf rf_wedge_image. uf lf_vee_image. rw target_oppf. rw comp_opp. rw fmor_oppf. rw fmor_oppf. rw flip_flip. rw inverse_opp. rw flip_flip. rw flip_flip. reflexivity. rw flip_flip. am. am. rw source_oppf. rw sfa. am. am. am. rw source_oppf. rw sfa. am. am. rw inverse_opp. rw mor_opp. rw flip_flip. rw fmor_oppf. rw flip_flip. ap mor_inverse. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw flip_flip. am. am. rw source_oppf. rww sfa. am. rw mor_opp. rw fmor_oppf. rw flip_flip. ap mor_fmor. am. rw sfa. am. am. rw source_oppf. rw sfa. am. am. rw source_inverse. rw fmor_oppf. rw fmor_oppf. rw target_flip. rw target_flip. rw source_fmor. rw source_fmor. rww H26. am. rww sfa. am. rww sfa. assert (mor (target f) (fmor f (flip r))). ap mor_fmor. am. rww sfa. alike. assert (mor (target f) (fmor f (flip t))). ap mor_fmor. am. rww sfa. alike. am. rw source_oppf. rww sfa. am. am. rw source_oppf. rww sfa. am. rw fmor_oppf. rw invertible_opp. am. am. rw source_oppf. rww sfa. am. am. assert (rf_wedge_equivalent a s (flip p) (flip q) (flip r) (flip t)). ap H3. am. am. transitivity (flip (flip (rf_wedge_image f (flip p) (flip q)))). rww flip_flip. wr H30. rw H6. rw H32. rww flip_flip. uh H33; ee. nin H37. nin H37. ee. cp H35; cp H36. rwi target_flip H45. rwi target_flip H45. rwi target_flip H46. rwi target_flip H46. uhg; ee. uhg; ee; am. uhg; ee; am. am. am. sh (flip x). sh (flip x0). ee. rw mor_opp. rww flip_flip. rw mor_opp. rww flip_flip. rw source_flip. rwi source_flip H39. am. alike. alike. rw source_flip; try alike. rwi source_flip H40; try alike. am. rw target_flip; try alike. rw target_flip; try alike. am. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw H42. reflexivity. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H40; try alike. am. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H39; try alike. am. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw H43. reflexivity. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H40; try alike. rw H40. am. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H39; try alike. rw H39. am. rw inc_oppms. rw comp_opp. rw flip_flip. rw flip_flip. am. rw mor_opp. rww flip_flip. am. rw source_flip; try alike. rwi source_flip H39; try alike. rw H39. am. alike. alike. alike. alike. (*** Whew! Now we can easily finish the proof using [prop1] and [prop2]. ***) ir. ap iff_eq; ir. ap prop2. am. assert (a = opp (opp a)). rww opp_opp. assert (s = oppms (oppms s)). rww oppms_oppms. assert (f = oppf (oppf f)). rww oppf_oppf. rw H0; rw H1; rw H2. ap prop1. am. Qed. Lemma right_fraction_description_for_loc : forall a s f, has_right_fractions a s -> is_localization a s f -> right_fraction_description a s f. Proof. ir. rw right_fraction_description_rw. ap left_fraction_description_for_loc. wr has_right_fractions_rw. am. rw is_localization_oppms_oppf. am. Qed. Lemma right_fraction_description_gz_proj : forall a s, has_right_fractions a s -> right_fraction_description a s (gz_proj a s). Proof. ir. ap right_fraction_description_for_loc. am. ap is_localization_gz_proj. uh H; ee. uh H; ee; am. Qed. (** Given the explicit construction of [gz_loc a s] and the functor [gz_proj a s] via the quotient of a free category by a list of relations, the theorems [left_fraction_description_gz_proj] and [right_fraction_description_gz_proj] are nontrivial theorems with a nice proof as indicated in Gabriel-Zisman which we have now checked formally. ***) End GZ_Localization.