(** * Theory of Sets EII-6 Equivalence relations Copyright INRIA (2009) Apics Team (Jose Grimm). Part of this code comes from Carlos Simpson *) Require Export set2. Require Export set3. (* $Id: set4.v,v 1.69 2010/07/19 15:35:47 grimm Exp $ *) Set Implicit Arguments. (** ** EII-6-1 Definition of an equivalence relation *) Module Relation. Definition substrate r := union2 (domain r) (range r ). Lemma inc_pr1_substrate : forall r y, inc y r -> inc (P y) (substrate r). Proof. ir. uf substrate. ap union2_first. uf domain. aw. ex_tac. Qed. Lemma inc_pr2_substrate : forall r y, inc y r -> inc (Q y) (substrate r). Proof. ir. uf substrate. ap union2_second. uf range. aw. ex_tac. Qed. Lemma inc_arg1_substrate: forall r x y, related r x y -> inc x (substrate r). Proof. ir. assert (P (J x y) = x). aw. wr H0. app inc_pr1_substrate. Qed. Lemma inc_arg2_substrate: forall r x y, related r x y -> inc y (substrate r). Proof. ir. assert (Q (J x y) = y). aw. wr H0. app inc_pr2_substrate. Qed. Ltac substr_tac := match goal with | H:inc ?x ?r |- inc (P ?x) (substrate ?r) => ap (inc_pr1_substrate H) | H:inc ?x ?r |- inc (Q ?x) (substrate ?r) => ap (inc_pr2_substrate H) | H:related ?r ?x _ |- inc ?x (substrate ?r) => ap (inc_arg1_substrate H) | H:related ?r _ ?y |- inc ?y (substrate ?r) => ap (inc_arg2_substrate H) | H:inc(J ?x _ ) ?r|- inc ?x (substrate ?r) => ap (inc_arg1_substrate H) | H: inc (J _ ?y) ?r |- inc ?y (substrate ?r) => ap (inc_arg2_substrate H) end. Lemma substrate_smallest : forall r s, (forall y, inc y r -> inc (P y) s) -> (forall y, inc y r -> inc (Q y) s) -> sub (substrate r) s. Proof. ir. red. uf substrate. uf domain. uf range. ir. nin (union2_or H1); awi H2;nin H2;nin H2; wr H3; [app H | app H0]. Qed. Lemma inc_substrate_rw : forall r x, is_graph r -> inc x (substrate r) = ((exists y, inc (J x y) r) \/ (exists y, inc (J y x) r)). Proof. ir. uf substrate. rw inc_union2_rw. app iff_eq. ir. awi H0; am. aw. Qed. (** Reflexivity properties for a relation *) Definition reflexive_r (r:EEP) x := forall y, inc y x = r y y. Definition symmetric_r (r:EEP) := forall x y, r x y -> r y x. Definition transitive_r (r:EEP) := forall x y z, r x y -> r y z -> r x z . Definition equivalence_r (r:EEP) := symmetric_r r & transitive_r r. Definition equivalence_re (r:EEP) x := equivalence_r r & reflexive_r r x. (** Same definitions for a graph *) Definition is_reflexive r := is_graph r & (forall y, inc y (substrate r) ->related r y y). Definition is_symmetric r := is_graph r & (forall x y, related r x y -> related r y x). Definition is_transitive r := is_graph r & (forall x y z, related r x y -> related r y z -> related r x z). Definition is_equivalence r := is_reflexive r & is_transitive r & is_symmetric r. (** Basic properties *) Lemma equivalence_is_graph : forall r, is_equivalence r -> is_graph r. Proof. ir. nin H; nin H; am. Qed. Hint Resolve equivalence_is_graph : fprops. Lemma reflexive_inc_substrate : forall r x, is_reflexive r -> inc x (substrate r) = inc (J x x) r. Proof. uf is_reflexive. ir. nin H. ap iff_eq; ir. ap (H0 _ H1). rww inc_substrate_rw. left; ex_tac; trivial. Qed. Lemma reflexive_ap : forall r x, is_reflexive r -> inc x (substrate r) -> related r x x. Proof. ir. red. wrr reflexive_inc_substrate. Qed. Lemma reflexive_ap2 : forall r x y, is_reflexive r -> related r x y -> related r x x. Proof. ir. app reflexive_ap. substr_tac. Qed. Lemma symmetric_ap : forall r x y, is_symmetric r -> related r x y -> related r y x. Proof. uf is_symmetric. intros r x y [H1 H2] H3. apply (H2 _ _ H3). Qed. Lemma transitive_ap : forall r x z, is_transitive r -> (exists y, related r x y & related r y z) -> related r x z. Proof. uf is_transitive. intros r x z [H1 H2] [y [H3 H4]]. ap (H2 _ _ _ H3 H4). Qed. Lemma symmetric_transitive_reflexive : forall r, is_symmetric r -> is_transitive r -> is_reflexive r. Proof. ir. red. assert (is_graph r). nin H; am. split. am. ir. rwii inc_substrate_rw H2. nin H2; nin H2; app transitive_ap; uf related; ex_tac; app symmetric_ap. Qed. Lemma equivalence_relation_pr1 : forall r, is_graph r -> (forall x y, related r x y -> related r y x) -> (forall x y z, related r x y -> related r y z -> related r x z) -> is_equivalence r. Proof. intros. assert (is_symmetric r). red. auto. assert (is_transitive r). red. auto. red. eee. app symmetric_transitive_reflexive. Qed. Lemma symmetric_transitive_equivalence : forall r, is_symmetric r -> is_transitive r -> is_equivalence r. Proof. ir. red. eee. app symmetric_transitive_reflexive. Qed. Lemma reflexivity_e : forall r u, is_equivalence r -> inc u (substrate r) -> related r u u. Proof. ir. nin H. app reflexive_ap. Qed. Lemma symmetricity_e : forall r u v, is_equivalence r -> related r u v -> related r v u. Proof. ir. destruct H as [_ [_ Hc ]]. app symmetric_ap. Qed. Lemma transitivity_e : forall r u v w, is_equivalence r -> related r u v -> related r v w -> related r u w. Proof. ir. destruct H as [_ [Hc _]]. app transitive_ap. exists v. split; am. Qed. Ltac equiv_tac:= match goal with | H: is_equivalence ?r, H1: inc ?u (substrate ?r) |- related ?r ?u ?u => ap (reflexivity_e H H1) | H: is_equivalence ?r |- inc (J ?u ?u) ?r => app reflexivity_e | H:is_equivalence ?r, H1:related ?r ?u ?v |- related ?r ?v ?u => app (symmetricity_e H H1) | H:is_equivalence ?r, H1: inc (J ?u ?v) ?r |- inc (J ?v ?u) ?r => app (symmetricity_e H H1) | H:is_equivalence ?r, H1:related ?r ?u ?v, H2: related ?r ?v ?w |- related ?r ?u ?w => app (transitivity_e H H1 H2) | H:is_equivalence ?r, H1:related ?r ?v ?u, H2: related ?r ?v ?w |- related ?r ?u ?w => app (transitivity_e H (symmetricity_e H H1) H2) | H: is_equivalence ?r, H1: inc (J ?u ?v) ?r, H2: inc (J ?v ?w) ?r |- inc (J ?u ?w) ?r => app (transitivity_e H H1 H2) end. Lemma domain_is_substrate: forall g, is_equivalence g -> domain g = substrate g. Proof. ir. uf substrate. set_extens. inter2tac. nin (union2_or H0). am. awi H1. nin H1. aw. exists x0. equiv_tac. fprops. fprops. Qed. Lemma substrate_sub : forall r s, sub r s -> sub (substrate r) (substrate s). Proof. ir; uf substrate; uf range; uf domain; uf sub; ir. nin (union2_or H0) ; [ ap union2_first| ap union2_second]; awi H1; aw; destruct H1 as [z [H2 H3]]; cp (H _ H2);ex_tac. Qed. Lemma inc_substrate : forall r x, is_equivalence r -> inc x (substrate r) = (exists y, related r x y). Proof. ir. app iff_eq. ir. exists x. equiv_tac. ir. nin H0. substr_tac. Qed. (** Comparison of the two sets of definitions *) Lemma reflexive_reflexive: forall r, is_reflexive r -> reflexive_r (related r) (substrate r). Proof. ir. uf reflexive_r. red in H. ee. ir. app iff_eq. app H0. ir. substr_tac. Qed. Lemma symmetric_symmetric: forall r, is_symmetric r -> symmetric_r (related r). Proof. ir. nin H. am. Qed. Lemma transitive_transitive: forall r, is_transitive r -> transitive_r (related r). Proof. ir. nin H. am. Qed. Lemma equivalence_equivalence: forall r, is_equivalence r -> equivalence_re (related r)(substrate r). Proof. ir. red in H. ee. red. split. red. split. app symmetric_symmetric. app transitive_transitive. app reflexive_reflexive. Qed. (** We say that [g] is the graph of [r] if [related g] is the same function as [r]. We define the graph of [r] on [x] as the set of pairs of [x] related by [r] *) Definition is_graph_of g (r:EEP):= forall u v, r u v = related g u v. Definition graph_on (r:EEP) x:= Zo(product x x)(fun w => r (P w)(Q w)). Lemma graph_on_graph: forall r x, is_graph(graph_on r x). Proof. ir. uf graph_on. red. ir. Ztac. awi H0. ee. am. Qed. Lemma graph_on_rw0: forall r x a b, inc (J a b) (graph_on r x) = (inc a x & inc b x & r a b). Proof. ir. uf graph_on. app iff_eq. ir. Ztac. awi H0. awi H1. intuition. ir. ee. Ztac. fprops. aw. Qed. Lemma graph_on_rw1: forall r x a b, related (graph_on r x) a b = (inc a x & inc b x & r a b). Proof. ir. uf related. ap graph_on_rw0. Qed. Lemma graph_on_substrate: forall r x, sub (substrate (graph_on r x)) x. Proof. ir. red. ir. rwi inc_substrate_rw H. nin H; nin H; rwi graph_on_rw0 H; intuition. app (graph_on_graph (r:=r)(x:=x)). Qed. Lemma equivalence_has_graph0: forall r x, equivalence_re r x -> is_graph_of (graph_on r x) r. Proof. ir. red. ir. rw graph_on_rw1. app iff_eq. ir. nin H. nin H. assert (r v u). app H. assert (r u u). apply (H2 _ _ _ H0 H3). assert (r v v). apply (H2 _ _ _ H3 H0). ee. rww H1. rww H1. am. ir. ee. am. Qed. Lemma graph_on_rw2: forall r x u v, equivalence_re r x -> related (graph_on r x) u v = r u v. Proof. ir. sy. app (equivalence_has_graph0 H). Qed. Lemma equivalence_has_graph:forall r x, equivalence_re r x -> exists g, is_graph_of g r. Proof. ir. exists (graph_on r x). app equivalence_has_graph0. Qed. Lemma equivalence_if_has_graph:forall r g, is_graph g -> is_graph_of g r -> equivalence_r r -> equivalence_re r (domain g). Proof. uf is_graph_of. uf related. ir. red. split. am. red. ir. aw. app iff_eq. ir. nin H2. wri H0 H2. red in H1. ee. assert (r x y). app H1. app (H3 _ _ _ H2 H4). ir. exists y. wrr H0. Qed. Lemma equivalence_if_has_graph2:forall r g, is_graph g -> is_graph_of g r -> equivalence_r r -> is_equivalence g. Proof. ir. red in H0. ap equivalence_relation_pr1. am. ir. wri H0 H2; wr H0. red in H1; ee. app H1. ir. wri H0 H3;wri H0 H2; wr H0. red in H1; ee. app (H4 _ _ _ H2 H3). Qed. Lemma equivalence_has_graph2: forall r x, equivalence_re r x -> exists g, is_equivalence g & (forall u v, r u v = related g u v). Proof. ir. exists (graph_on r x). ee. assert (is_graph (graph_on r x)). app graph_on_graph. assert (is_graph_of (graph_on r x) r). app equivalence_has_graph0. red in H. ee. app (equivalence_if_has_graph2 H0 H1 H). ir. rww graph_on_rw2. Qed. (** Finest relation on a set: an element is only related to itself The correspondence is the identity, the graph is the diagonal *) Definition restricted_eq x := fun u => fun v => inc u x & u = v. Lemma diagonal_equivalence1: forall x, equivalence_re (restricted_eq x) x. Proof. ir. uf restricted_eq. split. split. red. ir. intuition. ue. red. ir. eee. red. ir. ap iff_eq; ir;eee. Qed. Lemma diagonal_equivalence2: forall x, is_graph_of (identity_g x) (restricted_eq x). Proof. ir. red. ir. uf related. aw. Qed. Lemma diagonal_equivalence: forall x, is_equivalence (identity_g x). Proof. ir. assert (is_graph (identity_g x)). fprops. pose (diagonal_equivalence2 x). cp (diagonal_equivalence1 x). red in H0. ee. ap (equivalence_if_has_graph2 H i H0). Qed. Lemma diagonal_substrate: forall x, substrate(identity_g x) = x. Proof. ir. wr domain_is_substrate. app identity_domain. app diagonal_equivalence. Qed. (** The coarsest relation on a set: everything is related *) Definition coarse u := product u u. Lemma coarse_substrate : forall u, substrate (coarse u) = u. Proof. ir. uf coarse. uf substrate. nin (emptyset_dichot u). assert (product u u = emptyset). rw H. srw. rw H0. srw. rw H. app union2idem. rww product_domain. rww product_range. app union2idem. Qed. Lemma coarse_related : forall u x y, related (coarse u) x y = (inc x u & inc y u). Proof. uf coarse. uf related. ir. ap iff_eq. ir. awi H; intuition. ir. ee. fprops. Qed. Lemma coarse_graph: forall x, is_graph (coarse x). Proof. ir. uf coarse. app product_is_graph. Qed. Lemma coarse_equivalence : forall u, is_equivalence (coarse u). Proof. ir. assert (lemA : is_graph (coarse u)). app coarse_graph. red. ee. red. split. am. ir. rwi coarse_substrate H. rw coarse_related. auto. red. split. am. intros x y z. do 3 rw coarse_related. ir. intuition. split. trivial. intros x y. do 2 rw coarse_related. ir. intuition. Qed. Lemma inter2_is_graph1: forall x y, is_graph x -> is_graph (intersection2 x y). Proof. red. ir. app H. inter2tac. Qed. Lemma inter2_is_graph2: forall x y, is_graph y -> is_graph (intersection2 x y). Proof. red. ir. app H. inter2tac. Qed. Lemma union2_is_graph: forall x y, is_graph x -> is_graph y -> is_graph (union2 x y). Proof. red. ir. nin (union2_or H1). app H. app H0. Qed. Lemma sub_graph_coarse_substrate: forall r, is_graph r -> sub r (coarse (substrate r)). Proof. ir. red. ir. uf coarse. assert (is_pair x). app H. app product_inc. substr_tac. substr_tac. Qed. (** Example of an equivalence without graph: equipotency *) Lemma equipotent_equivalence: equivalence_r equipotent. Proof. red. ee. red. app equipotent_symmetric. red. app equipotent_transitive. Qed. (** Example 5 page E II.114 *) Lemma equivalence_relation_bourbaki_ex5: forall a e, sub a e -> is_equivalence ( Zo(product e e)(fun y=> (inc (P y)(complement e a) & (P y = Q y)) \/ (inc (P y) a & inc(Q y) a))). Proof. ir. set (f := fun x y:Set => (inc x (complement e a) & x = y) \/ (inc x a & inc y a)). set (g := (Zo (product e e) (fun z => f (P z) (Q z)))). change (is_equivalence g). assert (Ha: forall x y, inc x e -> inc y e -> (related g x y) = f x y). ir. uf related. uf g. app iff_eq; ir; Ztac. awi H4. am. fprops. aw. assert (Hb: forall x, inc x e -> related g x x). ir. rww Ha. uf f. nin (inc_or_not x a). right. int. left. split. srw. au. tv. assert (Hc: substrate g = e). app extensionality. uf g. app substrate_smallest; ir; Ztac; cp (product_pr H1); eee. red. ir. set (Hb _ H0). substr_tac. assert (Hd:is_graph g). red. uf g. ir. Ztac. awi H1. eee. assert(He:forall x y, related g x y -> (inc x e & inc y e)). uf related. uf g. ir. Ztac. awi H1. eee. red. ee;red; ee; tv. rww Hc. ir. set (He _ _ H0). set (He _ _ H1). ee. rwii Ha H0. rwii Ha H1. rww Ha. nin H0. nin H0. ue. right. nin H1. nin H1. ue. eee. ir. nin (He _ _ H0). rww Ha; rwi Ha H0. nin H0. left. nin H0. wrr H3. eee. right. eee. am. am. Qed. (** Intersection of equivalence relations is an equivalence *) Lemma inter_rel_graph : forall z, nonempty z -> (forall r, inc r z -> is_graph r) -> is_graph (intersection z). Proof. intros z H H1 y H2. nin H. apply (H1 y0 H). apply intersection_forall with z. am. am. Qed. Lemma inter_rel_rw : forall z x y, nonempty z -> related (intersection z) x y = (forall r, inc r z -> related r x y). Proof. uf related. ir. ap iff_eq; ir. apply intersection_forall with z. am. am. app intersection_inc. Qed. Lemma inter_rel_reflexive : forall z, nonempty z -> (forall r, inc r z -> is_reflexive r) -> is_reflexive (intersection z). Proof. ir. red. split. app inter_rel_graph. ir. nin (H0 _ H1); am. ir. rww inter_rel_rw. ir. nin (H0 _ H2). ap H4. assert (sub (intersection z) r). app intersection_sub. app (substrate_sub H5). Qed. Lemma inter_rel_substrate : forall z e, nonempty z -> (forall r, inc r z -> is_reflexive r) -> (forall r, inc r z -> substrate r = e) -> substrate (intersection z) = e. Proof. ir. cp (inter_rel_reflexive H H0). set_extens. red in H2. ee. cp (H4 _ H3). red in H5. nin H. set (intersection_forall H5 H). wr (H1 _ H). app (inc_arg1_substrate i). assert (related (intersection z) x x). rww inter_rel_rw. ir. wri (H1 _ H4) H3. nin (H0 _ H4). app H6. substr_tac. Qed. Lemma inter_rel_transitive : forall X, nonempty X -> (forall r, inc r X -> is_transitive r) -> is_transitive (intersection X). Proof. ir; red; ir; split. app inter_rel_graph. ir. nin (H0 _ H1); am. intros x y z. do 3 rww inter_rel_rw. ir. nin (H0 _ H3). apply (H5 _ y _ (H1 _ H3) (H2 _ H3)). Qed. Lemma inter_rel_symmetric : forall z, nonempty z -> (forall r, inc r z -> is_symmetric r) -> is_symmetric (intersection z). Proof. ir. red. split. app inter_rel_graph. ir. nin (H0 _ H1); am. intros x y. do 2 rww inter_rel_rw. ir. nin (H0 _ H2). apply (H4 _ _ (H1 _ H2)). Qed. Lemma inter_rel_equivalence : forall z, nonempty z -> (forall r, inc r z -> is_equivalence r) -> is_equivalence (intersection z). Proof. ir. app symmetric_transitive_equivalence. app inter_rel_symmetric. ir. destruct (H0 _ H1) as [H3 [H4 H5]]. am. app inter_rel_transitive. ir. destruct (H0 _ H1) as [H3 [H4 H5]]. am. Qed. (** The set of all relations or all equivalences of a set *) Definition all_relations x := powerset (product x x). Lemma inc_all_relations : forall r x, inc r (all_relations x) = (is_graph r & sub (substrate r) x). Proof. ir. uf all_relations. rw powerset_inc_rw. apply iff_eq. ir. assert (is_graph r). red. intros. cp (H y H0). awi H1;eee. ee. am. red. ir. rwi inc_substrate_rw H1. nin H1; nin H1; cp (H _ H1); awi H2;eee. am. ir. ee. red; ir. aw. split; [app H | split; app H0; substr_tac]. Qed. Definition all_equivalence_relations x := Zo (all_relations x) (fun r => (is_equivalence r) & (substrate r = x)). Lemma inc_all_equivalence_relations : forall r x, inc r (all_equivalence_relations x) = (is_equivalence r & (substrate r = x)). Proof. uf all_equivalence_relations; ir; ap iff_eq; ir; Ztac. tv. rw inc_all_relations. ee. fprops. ue. Qed. Lemma inc_coarse_all_equivalence_relations : forall u, inc (coarse u) (all_equivalence_relations u). Proof. intros. rewrite inc_all_equivalence_relations. split. apply coarse_equivalence. rww coarse_substrate. Qed. (** We show that an equivalence is a self-inverse projector *) Lemma selfinverse_graph_symmetric: forall r, is_symmetric r = (r= inverse_graph r). Proof. ir. uf is_symmetric. uf related. ap iff_eq. ir. nin H. set_extens. cp (H _ H1); cp (pair_recov H2). wr H3. aw. app H0. ue. cp (inverse_graph_is_graph H1). cp (pair_recov H2). wri H3 H1. awi H1. cp (H0 _ _ H1). ue. ir. split. rw H. fprops. ir. rw H. aw. Qed. Lemma idempotent_graph_transitive: forall r, is_graph r-> (is_transitive r = sub (compose_graph r r) r). Proof. ir. ap iff_eq. ir. red. ir. awi H1. ee. nin H2. ee. red in H0. ee. ufi related H4. assert (J (P x) (Q x) = x). aw. wr H5. app (H4 _ _ _ H2 H3). ir. red in H0. red. ee. am. uf related. ir. app H0. aw. split. fprops. ex_tac. Qed. Theorem equivalence_pr: forall r, (is_equivalence r = ((compose_graph r r) = r & r= inverse_graph r)). Proof. ir. app iff_eq. ir. split. assert (is_graph r). fprops. app extensionality. wr idempotent_graph_transitive. red in H; eee. am. red. ir. assert (is_pair x). app H0. aw. ee. am. assert (J (P x) (Q x)= x). aw. exists (P x). rw H3. ee. equiv_tac. substr_tac. am. wr selfinverse_graph_symmetric. red in H; ee. am. ir. ee. assert (is_graph r). rw H0. fprops. app symmetric_transitive_equivalence. rww selfinverse_graph_symmetric. rw idempotent_graph_transitive. ue. am. Qed. (** ** EII-6-2 Equivalence classes; quotient set *) (** Equivalence associated to a function [f] by [f x = f y] *) Definition eq_rel_associated f := fun x => fun y => (inc x (source f) & (inc y (source f)) & (W x f = W y f)). Definition equivalence_associated f := compose_graph (inverse_graph (graph f)) (graph f). Lemma ea_equivalence: forall f, is_function f -> equivalence_re(eq_rel_associated f)(source f). Proof. ir. uf eq_rel_associated. red. split. red. split. red. ir. intuition. red. ir. intuition. ue. red. ir. ap iff_eq; intuition. Qed. Lemma graph_of_ea: forall f, is_function f -> is_graph_of (equivalence_associated f) (eq_rel_associated f). Proof. ir. red. ir. assert (is_graph (graph f)). fprops. assert(is_graph (inverse_graph (graph f))). fprops. uf equivalence_associated. app iff_eq. ir. red. red in H2. ee. aw. ee. fprops. exists (W u f). ee. graph_tac. aw. rw H4. graph_tac. ir. red in H2. awi H2. nin H2. nin H3. nin H3. awi H4. red. ee. app (related_inc_source H H3). app (related_inc_source H H4). rw (W_pr H H3). rw (W_pr H H4). tv. Qed. Lemma graph_ea_equivalence: forall f, is_function f-> is_equivalence (equivalence_associated f). Proof. ir. pose (graph_of_ea H). assert(is_graph (equivalence_associated f)). uf equivalence_associated. fprops. app (equivalence_if_has_graph2 H0 i). nin (ea_equivalence H). am. Qed. Lemma graph_ea_substrate: forall f, is_function f-> substrate (equivalence_associated f) = source f. Proof. ir. cp (graph_ea_equivalence H). cp (graph_of_ea H). red in H1. ufi eq_rel_associated H1. set_extens. rwi inc_substrate H2. nin H2. wri H1 H2. ee. am. am. rw inc_substrate. exists x. wr H1. au. am. Qed. Lemma ea_related:forall f x y, is_function f -> related (equivalence_associated f) x y = (inc x (source f) & inc y (source f) & W x f = W y f). Proof. ir. cp (graph_of_ea H). red in H0. ufi eq_rel_associated H0. sy. app H0. Qed. (** The class of [x] is the set of elements related to [x] *) Definition class (r x:Set) := fun_image (Zo r (fun z => P z = x)) Q. Lemma inc_class : forall r x y, is_equivalence r -> inc y (class r x) = related r x y. Proof. ir. uf class. aw. ap iff_eq; ir. nin H0. nin H0. Ztac. assert (J x y = x0). wr H1; wr H3. aw. assert (is_graph r). fprops. app H4. red. ue. exists (J x y). ee. Ztac. aw. aw. Qed. Hint Rewrite inc_class : bw. Lemma class_is_cut: forall r x, is_equivalence r -> class r x = im_singleton r x. Proof. ir. set_extens. aw. bwi H0. am. am. awi H0. bw. Qed. Lemma sub_class_substrate: forall r x, is_equivalence r -> sub (class r x) (substrate r). Proof. ir. red. ir. bwi H0. substr_tac. am. Qed. Lemma nonempty_class_symmetric : forall r x, is_equivalence r -> nonempty (class r x) = inc x (substrate r). Proof. ir. app iff_eq. ir. nin H0. bwi H0. substr_tac. am. ir. exists x. bw. equiv_tac. Qed. Lemma related_class_eq1: forall r u v, is_equivalence r -> related r u v -> class r u = class r v. Proof. ir. assert (is_graph r). fprops. set_extens; bwi H2; bw. equiv_tac. equiv_tac. Qed. Lemma related_class_eq : forall r u v, is_equivalence r -> related r u u -> related r u v = (class r u = class r v). Proof. ir. ee. ap iff_eq; ir. app related_class_eq1. assert (inc u (class r u)). bw. rwi H1 H2. bwi H2. equiv_tac. am. Qed. (** Definition of the quotient of an equivalence *) Definition is_class r x := is_equivalence r & inc (rep x) (substrate r) & x = class r (rep x). Definition quotient r := fun_image (substrate r) (class r). Lemma inc_rep_itself:forall r x, is_equivalence r -> inc x (quotient r) -> inc (rep x) x. Proof. ir. ap nonempty_rep. ufi quotient H0. awi H0. nin H0. nin H0. wr H1. rww nonempty_class_symmetric. Qed. Lemma non_empty_in_quotient: forall r x, is_equivalence r -> inc x (quotient r) -> nonempty x. Proof. ir. exists (rep x). app (inc_rep_itself H H0). Qed. Lemma is_class_class : forall r x, is_equivalence r -> inc x (substrate r) -> is_class r (class r x). Proof. ir. red. assert (inc (class r x) (quotient r)). uf quotient. aw. ex_tac. cp (inc_rep_itself H H1). bwi H2. ee. am. substr_tac. app related_class_eq1. fprops. Qed. Lemma inc_itself_class : forall r x, is_equivalence r ->inc x (substrate r) -> inc x (class r x). Proof. ir. bw. equiv_tac. Qed. Lemma inc_quotient : forall r x, is_equivalence r -> inc x (quotient r) = is_class r x. Proof. ir. ap iff_eq. ir. cp (inc_rep_itself H H0). ufi quotient H0. awi H0. nin H0. nin H0. wr H2. app is_class_class. ir. uf quotient. red in H0. ee. aw. ex_tac. au. Qed. Lemma class_rep : forall r x, is_equivalence r -> inc x (quotient r) -> class r (rep x) = x. Proof. ir. rewrite (inc_quotient x H) in H0. destruct H0 as [_ [_ H3]]. sy. am. Qed. Lemma in_class_related : forall r y z, is_equivalence r -> related r y z = (exists x, is_class r x & inc y x & inc z x). Proof. ir. ap iff_eq; ir. assert (inc y (substrate r)). substr_tac. exists (class r y). ee. app is_class_class. bw. equiv_tac. bw. destruct H0 as [x [[ _ [Hb Hc]] [Hd He]]]. rwi Hc Hd; rwi Hc He; bwi Hd; bwi He. equiv_tac. am. am. am. Qed. Lemma related_rep_in_class:forall r x y, is_equivalence r -> inc x (quotient r) -> inc y x -> related r (rep x) y. Proof. ir. rww in_class_related. exists x. ee. wrr inc_quotient. app (inc_rep_itself H H0). am. Qed. Lemma is_class_rw : forall r x, is_equivalence r -> is_class r x = (nonempty x & sub x (substrate r) & (forall y z, inc y x -> (inc z x = related r y z)) ). Proof. ir. apply iff_eq; intros. assert (W:=H0). red in H0. nin H0. nin H1. split. rw H2. exists (rep x). bw. equiv_tac. split. red. ir. rwi H2 H3. app (sub_class_substrate (x:=rep x) H). ir. ap iff_eq; ir. rw (in_class_related y z H). exists x; intuition. rw H2. bw. rwi H2 H3. bwi H3. equiv_tac. am. nin H0. nin H1. cp (nonempty_rep H0). red. split. am. split. app H1. set_extens. bw. wrr H2. bwi H4. rww (H2 (rep x)). am. Qed. Lemma class_dichot : forall r x y, is_class r x -> is_class r y -> (x = y \/ disjoint x y). Proof. ir. nin (emptyset_dichot (intersection2 x y)). right; am. left. nin H1. nin (intersection2_both H1). nin H. ee. rw H5. nin H0. ee. rw H7. app related_class_eq1. rwi H5 H2. rwi H7 H3. bwi H2. bwi H3. assert (related r y0 (rep y)). equiv_tac. equiv_tac. fprops. fprops. Qed. Lemma inc_class_quotient : forall r x, is_equivalence r -> inc x (substrate r) -> inc (class r x) (quotient r). Proof. ir. rww inc_quotient. app is_class_class. Qed. Lemma inc_in_quotient_substrate : forall r x y, is_equivalence r -> inc x y -> inc y (quotient r) -> inc x (substrate r). Proof. ir. rwii inc_quotient H1. rwii is_class_rw H1. ee. app H2. Qed. Hint Resolve inc_class_quotient: gprops. Lemma union_quotient : forall r, is_equivalence r -> union (quotient r) = substrate r. Proof. ir. set_extens. nin (union_exists H0). nin H1. app (inc_in_quotient_substrate H H1 H2). apply union_inc with (class r x). bw. equiv_tac. gprops. Qed. Lemma inc_rep_substrate : forall r x, is_equivalence r -> inc x (quotient r) -> inc (rep x) (substrate r). Proof. ir. rwi (inc_quotient x H) H0. destruct H0 as [_ [H2 _]]. am. Qed. Hint Resolve inc_rep_substrate: fprops. Lemma related_rep_class : forall r x, is_equivalence r -> inc x (substrate r) -> related r x (rep (class r x)). Proof. ir. cut (related r (rep (class r x)) x). ir. equiv_tac. app related_rep_in_class. rww inc_quotient. app is_class_class. app inc_itself_class. Qed. Lemma related_rep_rep : forall r u v, is_equivalence r -> inc u (quotient r) -> inc v (quotient r) -> related r (rep u) (rep v) = (u = v). Proof. ir. app iff_eq. ir. wr (class_rep H H0). wr (class_rep H H1). app related_class_eq1. ir. wr H2. assert (inc (rep u) (substrate r)). fprops. equiv_tac. Qed. Lemma related_rw : forall r u v, is_equivalence r -> related r u v = (inc u (substrate r) & inc v (substrate r) & class r u = class r v). Proof. ir. ap iff_eq; ir. split. substr_tac. ee. substr_tac. app related_class_eq1. ee. rww related_class_eq. equiv_tac. Qed. Lemma is_class_pr: forall r x y, is_equivalence r -> inc x y -> inc y (quotient r) -> y = class r x. Proof. ir. assert (class r (rep y) = y). app class_rep. wr H2. app related_class_eq1. app (related_rep_in_class H H1 H0). Qed. (** Canonical projection on the quotient *) Definition canon_proj (r:Set) := BL(fun x=> class r x) (substrate r) (quotient r). Lemma canon_proj_function: forall r, is_equivalence r -> is_function (canon_proj r). Proof. ir. uf canon_proj. ap bl_function. red. ir. gprops. Qed. Lemma canon_proj_source: forall r, source (canon_proj r) = substrate r. Proof. ir. uf canon_proj. aw. Qed. Lemma canon_proj_target: forall r, target (canon_proj r) = quotient r. Proof. ir. uf canon_proj. aw. Qed. Hint Rewrite canon_proj_source canon_proj_target: aw. Hint Resolve canon_proj_function: fprops. Lemma canon_proj_W:forall r x, is_equivalence r -> inc x (substrate r) -> W x (canon_proj r) = class r x. Proof. ir. uf canon_proj. aw. red. tv. ir. gprops. Qed. Hint Rewrite canon_proj_W : aw. Lemma canon_proj_inc:forall r x, is_equivalence r-> inc x (substrate r) -> inc (W x (canon_proj r)) (quotient r). Proof. ir. aw. gprops. Qed. Lemma related_graph_canon_proj: forall r x y, is_equivalence r -> inc x (substrate r) -> inc y (quotient r) -> inc (J x y) (graph (canon_proj r)) = inc x y. Proof. ir. uf related. assert (is_function (canon_proj r)). fprops. app iff_eq. ir. cp (W_pr H2 H3). awi H4. wr H4. bw. equiv_tac. am. am. ir. assert (y = W x (canon_proj r)). aw. cp (class_rep H H1). wr H4. wri H4 H3. bwi H3. app related_class_eq1. am. rw H4. graph_tac. aw. Qed. Lemma canon_proj_show_surjective:forall r x, is_equivalence r-> inc x (quotient r) -> W (rep x)(canon_proj r) = x. Proof. ir. assert (inc (rep x) (substrate r)). fprops. aw. app class_rep. Qed. Lemma canon_proj_surjective:forall r, is_equivalence r-> surjective (canon_proj r). Proof. ir. app surjective_pr6. fprops. ir. awi H0. ir. exists (rep y). ee. aw. fprops. aw. app class_rep. fprops. Qed. Lemma sub_im_canon_proj_quotient: forall r a x, is_equivalence r -> sub a (substrate r) -> inc x (image_by_fun (canon_proj r) a) -> inc x (quotient r). Proof. ir. assert (is_function (canon_proj r)). fprops. awi H1. nin H1; ee. wr H3. aw. gprops. app H0. am. aw. Qed. (** Criterion 55 *) Lemma related_e_rw: forall r u v, is_equivalence r -> (related r u v = (inc u (source (canon_proj r)) & inc v (source (canon_proj r)) & W u (canon_proj r) = W v (canon_proj r))). Proof. ir. rw related_rw. app iff_eq; ir. nin H0; nin H1. aw. eee. nin H0; nin H1. awii H0. awii H1. awii H2. eee. am. Qed. (** The diagonal is the graph of equality *) Lemma diagonal_class: forall x u, inc u x -> class (identity_g x) u = singleton u. Proof. ir. assert (is_equivalence (identity_g x)). app diagonal_equivalence. set_extens. bwi H1. ufi related H1. awi H1. ee. ue. am. bw. uf related. aw. ee. am. db_tac. Qed. Lemma canon_proj_diagonal_bijective: forall x, bijective (canon_proj (identity_g x)). Proof. ir. assert(is_equivalence (identity_g x)). app diagonal_equivalence. assert (is_function (canon_proj (identity_g x))). fprops. red. split. ir. red. ee. am. ir. awi H1; awi H2. awii H3. rwi diagonal_substrate H1. rwi diagonal_substrate H2. do 2 rwii diagonal_class H3. app singleton_inj. app canon_proj_surjective. Qed. (** Relation associated to [P] in a product *) Definition first_proj_eqr (x y:Set) := eq_rel_associated(first_proj (product x y)). Definition first_proj_eq (x y :Set) := equivalence_associated (first_proj (product x y)). Lemma first_proj_eq_pr: forall x y a b, first_proj_eqr x y a b = (inc a (product x y) & inc b (product x y) & P a = P b). Proof. ir. uf first_proj_eqr. assert (is_graph (product x y)). app product_is_graph. uf eq_rel_associated. assert (source (first_proj (product x y)) = product x y). uf first_proj. aw. rw H0. ap iff_eq; ir; eee; try (do 2 rwii first_proj_W H3). do 2 rww first_proj_W. Qed. Lemma first_proj_graph: forall x y, is_graph_of(first_proj_eq x y)(first_proj_eqr x y). Proof. ir. uf first_proj_eq; uf first_proj_eqr. app graph_of_ea. app first_proj_function. Qed. Lemma first_proj_equivalence: forall x y, is_equivalence (first_proj_eq x y). Proof. ir. uf first_proj_eq. app graph_ea_equivalence. app first_proj_function. Qed. Lemma first_proj_eq_related: forall x y a b, related (first_proj_eq x y) a b = (inc a (product x y) & inc b (product x y) & P a = P b). Proof. ir. cp (first_proj_graph x y). red in H. wr H. rww first_proj_eq_pr. Qed. Lemma first_proj_substrate: forall x y, substrate(first_proj_eq x y) = product x y. Proof. ir. uf first_proj_eq. set (f:=(first_proj (product x y))). assert(is_function f). uf f. app first_proj_function. rww graph_ea_substrate. uf f. uf first_proj. aw. Qed. Lemma first_proj_class:forall x y z, nonempty y -> is_class (first_proj_eq x y) z = exists u, inc u x & z = product (singleton u) y. Proof. ir. set (r:=first_proj_eq x y). assert (is_equivalence r). uf r; app first_proj_equivalence. cp (first_proj_substrate x y). fold r in H1. app iff_eq. ir. rwi is_class_rw H2. ee. rwi H1 H3. nin H2. exists (P y0). ee. cp (H3 _ H2). awi H5. ee. am. assert(forall z0, inc z0 z = (inc y0 (product x y) & inc z0 (product x y) & P y0 = P z0)). ir. rw (H4 y0 z0 H2). uf r. rww first_proj_eq_related. set_extens. aw. cp (H3 _ H6). awi H7. eee. rwi H5 H6. ee. intuition. rw H5. awi H6; ee. ap (H3 _ H2). cp (H3 _ H2). awi H9. aw. ee. am. ue. am. ue. am. ir. nin H2. ee. rw is_class_rw. ee. nin H. exists (J x0 y0). rw H3. aw. eee. rw H1. rw H3. app product_monotone_left. app sub_singleton. ir. rwi H3 H4. awi H4. ee. uf r. rw first_proj_eq_related. rw H3. aw. rw H5. ap iff_eq; ir; eee. am. Qed. Lemma first_proj_equiv_proj: forall x y, nonempty y-> bijective (BL (fun u => product (singleton u) y) x (quotient (first_proj_eq x y))). Proof. ir. set (f:=fun u => product (singleton u) y). set (g:= (BL f x (quotient (first_proj_eq x y)))). assert (is_equivalence (first_proj_eq x y)). app first_proj_equivalence. assert(transf_axioms f x (quotient (first_proj_eq x y))). red. ir. rw inc_quotient. rw first_proj_class. ex_tac. am. am. uf g. app bl_bijective. ir. ufi f H4. app singleton_inj. wr (product_domain (singleton u) H). rw H4. rww product_domain. ir. rwi inc_quotient H2. rwi first_proj_class H2. nin H2. ee. exists x0. au. am. am. Qed. (** Partition of a set and induced equivalence *) Definition in_same_coset f x y:= exists i, inc i (source f) & inc x (W i f) & inc y (W i f). Definition partition_relation f x := graph_on (in_same_coset f) x. Lemma isc_reflexive: forall f x, is_function f -> partition_fam (graph f) x -> reflexive_r (in_same_coset f) x. Proof. ir. red. ir. red in H. ee. app iff_eq. ir. nin (partition_inc_exists H0 H3). ee. red. exists x0. rw H2. au. ir. nin H3. ee. red in H0. ee. wr H7. apply unionb_inc with x0. ue. am. Qed. Lemma isc_symmetric: forall f, symmetric_r (in_same_coset f). Proof. ir. red. uf in_same_coset. ir. nin H. ee. ex_tac. au. Qed. Lemma isc_transitive: forall f x, is_function f -> partition_fam (graph f) x -> transitive_r (in_same_coset f). Proof. ir. red. uf in_same_coset. ir. nin H1; nin H2. ee. exists x1. eee. red in H. ee. rwi H8 H1; rwi H8 H2. rww (partition_inc_unique H0 H1 H6 H2 H3). Qed. Lemma isc_equivalence: forall f x, is_function f -> partition_fam (graph f) x -> equivalence_re (in_same_coset f) x. Proof. ir. red. ee. red. ee. app isc_symmetric. app (isc_transitive H H0). app isc_reflexive. Qed. Lemma partition_rel_graph: forall f x, is_function f -> partition_fam (graph f) x -> is_graph_of (partition_relation f x) (in_same_coset f). Proof. ir. uf partition_relation. app equivalence_has_graph0. app isc_equivalence. Qed. Lemma partition_relation_pr: forall f x a b, is_function f -> partition_fam (graph f) x -> related (partition_relation f x) a b = in_same_coset f a b. Proof. ir. cp (partition_rel_graph H H0). sy. app H1. Qed. Lemma partition_is_equivalence: forall f x, is_function f -> partition_fam (graph f) x -> is_equivalence (partition_relation f x). Proof. ir. assert (is_graph (partition_relation f x)). uf partition_relation. app graph_on_graph. cp (partition_rel_graph H H0). cp (isc_equivalence H H0). red in H3; ee. ap (equivalence_if_has_graph2 H1 H2 H3). Qed. Lemma partition_relation_substrate: forall f x, is_function f -> partition_fam (graph f) x -> substrate (partition_relation f x)= x. Proof. ir. app extensionality. uf partition_relation. app graph_on_substrate. red. ir. cp (partition_is_equivalence H H0). rwi (isc_reflexive H H0) H1. wri (partition_relation_pr x0 x0 H H0) H1. substr_tac. Qed. Lemma partition_class_inc: forall f x a b, is_function f -> partition_fam (graph f) x -> inc a (class (partition_relation f x) b) = (exists i, inc i (source f) & inc b (W i f) & inc a (W i f)). Proof. ir. change (inc a (class (partition_relation f x) b) = in_same_coset f b a). wr (partition_relation_pr b a H H0). bw. ap (partition_is_equivalence H H0). Qed. Lemma partition_relation_class: forall f x a, is_function f -> partition_fam (graph f) x -> is_class (partition_relation f x) a -> exists u, inc u (source f) & a = W u f. Proof. ir. red in H1. ee. assert (related (partition_relation f x) (rep a) (rep a)). equiv_tac. rwi (partition_relation_pr (rep a) (rep a) H H0) H4. nin H4. ee. ex_tac. set_extens. rwi H3 H7. rwi partition_class_inc H7. nin H7. red in H;ee. rwi H11 H7. rwi H11 H4. rww (partition_inc_unique H0 H4 H6 H7 H8). am. am. rw H3. rww partition_class_inc. ex_tac. au. Qed. Lemma partition_relation_class2: forall f x u, is_function f -> partition_fam (graph f) x -> inc u (source f) -> nonempty (W u f) -> is_class (partition_relation f x) (W u f) . Proof. ir. cp (partition_is_equivalence H H0). assert (inc (rep (W u f)) (W u f)). app nonempty_rep. red. ee. am. rww partition_relation_substrate. assert (sub (W u f) x). red in H0. ee. wr H6. red. ir. apply unionb_inc with u. red in H; ee. wrr H9. am. app H5. set_extens. rww partition_class_inc. ex_tac. au. rwii partition_class_inc H5. nin H5. ee. red in H. ee. rwi H9 H5. rwi H9 H1. rww (partition_inc_unique H0 H1 H4 H5 H6). Qed. Lemma partition_fun_bijective: forall f x, is_function f -> partition_fam (graph f) x -> (forall u, inc u (source f) -> nonempty (W u f)) -> bijective (BL (fun u => W u f) (source f) (quotient (partition_relation f x))). Proof. ir. app bl_bijective. red. ir. rw inc_quotient. app partition_relation_class2. app H1. app partition_is_equivalence. ir. nin (H1 _ H2). assert (inc y (W v f)). wrr H4. red in H. ee. rwi H8 H2; rwi H8 H3. app (partition_inc_unique H0 H2 H5 H3 H6). ir. rwi inc_quotient H2. nin (partition_relation_class H H0 H2). ee. ex_tac. au. app partition_is_equivalence. Qed. Lemma sub_quotient_powerset: forall r, is_equivalence r -> sub (quotient r) (powerset (substrate r)). Proof. ir. red. ir. rwii inc_quotient H0. rwii is_class_rw H0. ee. app powerset_inc. Qed. Lemma partition_from_equivalence: forall r, is_equivalence r -> partition(quotient r)(substrate r). Proof. ir. red. ee. app union_quotient. ir. app (non_empty_in_quotient H H0). intros a b. do 2 rww inc_quotient. ir. app (class_dichot H0 H1). Qed. (** A system of representatives for the partition f of x as a set f or a function g *) Definition representative_system s f x := is_function f & partition_fam (graph f) x & sub s x & (forall i, inc i (source f) -> is_singleton (intersection2 (W i f) s)). Definition representative_system_function g f x := injective g & (representative_system (range (graph g)) f x). Lemma rep_sys_function_pr: forall g f x i, representative_system_function g f x -> inc i (source f) -> exists_unique (fun a=> inc a (source g) & inc (W a g) (W i f)). Proof. ir. nin H. red in H1. ee. nin (H4 _ H0). nin H. red. split. cp (singleton_inc x0). wri H5 H7. nin (intersection2_both H7). rwi range_inc_rw H9. nin H9. ee. ex_tac. wr H10. am. am. ir. ee. app H6. assert (forall a, inc a (source g) -> inc (W a g) (W i f) -> W a g = x0). ir. app singleton_eq. wr H5. inter2tac. app inc_W_range_graph. rww H11. rww H11. Qed. Lemma rep_sys_function_pr2: forall g f x, injective g -> is_function f -> partition_fam (graph f) x -> sub (target g) x -> (forall i, inc i (source f) -> exists_unique (fun a=> inc a (source g) & inc (W a g) (W i f))) -> representative_system_function g f x. Proof. ir. red. ee. am. nin H. red. eee. apply sub_trans with (target g). red in H; ee. fprops. am. ir. nin (H3 _ H5). ee. nin H6. exists (W x0 g). set_extens. nin (intersection2_both H8). awi H10. nin H10. cp (W_pr H H10). wr H11. assert (x2 = x0). app H7. ee. graph_tac. ue. rw H12. fprops. fprops. ee. awi H8. rw H8. inter2tac. app inc_W_range_graph. Qed. Lemma section_canon_proj_pr: forall g f x y r, r = partition_relation f x -> is_function f -> partition_fam (graph f) x -> is_right_inverse g (canon_proj r) -> inc y x -> related r y (W (class r y) g). Proof. ir. assert(is_equivalence r). rw H. app partition_is_equivalence. assert(substrate r = x). rw H; rww partition_relation_substrate. wri H5 H3. assert (inc (class r y) (quotient r)). gprops. assert(source g = target (canon_proj r)). app source_right_inverse. awi H7. red in H2. ee. rww related_class_eq. sy. wrr canon_proj_W. wr compose_W. rw H8. srw. aw. am. ue. ue. red in H2. ee. awi H10. wr H5. rw H10. app inc_W_target. ue. ue. wr H. equiv_tac. Qed. Lemma section_is_representative_system_function: forall g f x, is_function f -> partition_fam (graph f) x -> is_right_inverse g (canon_proj (partition_relation f x)) -> (forall u, inc u (source f) -> nonempty (W u f)) -> representative_system_function g f x. Proof. ir. assert (injective g). assert (is_function (canon_proj (partition_relation f x))). assert (is_equivalence (partition_relation f x)). app partition_is_equivalence. fprops. ap (right_inverse_injective H1). app rep_sys_function_pr2. red in H1; ee. red in H1; ee. wr H6. aw. rw partition_relation_substrate. app sub_refl. am. am. ir. set (r:=(partition_relation f x)) in *. assert (Hc: source f = domain (graph f)). red in H. ee. am. assert (Ha:is_equivalence r). uf r. app partition_is_equivalence. assert (substrate r = x). uf r. rww partition_relation_substrate. cp (source_right_inverse H1). simpl in H6. rw H6. red. ee. pose (z:= (rep (W i f))). assert (inc z (W i f)). uf z. app nonempty_rep. app H2. assert (inc z x). red in H0; ee. wr H9. apply unionb_inc with i. ue. am. exists (class r z). ee. aw. wri H5 H8. gprops. cp (section_canon_proj_pr (refl_equal r) H H0 H1 H8). ufi r H9. rwii partition_relation_pr H9. red in H9. nin H9. ee. fold r in H11. rwi Hc H4; rwi Hc H9. rww (partition_inc_unique H0 H4 H7 H9 H10). ir. ee. assert (forall u, inc u (quotient r) -> inc (W u g) (W i f) -> W i f = u). ir. cp H11. rwii inc_quotient H11. red in H11; ee. rw H15. app is_class_pr. rwi H5 H14. cp (section_canon_proj_pr (refl_equal r) H H0 H1 H14). ufi r H16. rwii partition_relation_pr H16. fold r in H16. red in H16; nin H16. ee. cp H16. wri H15 H18. rwi Hc H4; rwi Hc H16. rww (partition_inc_unique H0 H4 H12 H16 H18). rww inc_quotient. uf r. app partition_relation_class2. app H2. awi H7. ufi canon_proj H8. awi H8. wr (H11 _ H7 H10). wr (H11 _ H8 H9). tv. Qed. (** ** EII-6-3 Relations compatible with an equivalence relation *) (** A relation is compoatible if the set of objectcts satisfying the relation is a union of classes *) Definition compatible_with_equiv_p (p:EP)(r:Set) := forall x x', p x -> related r x x' -> p x'. Lemma trivial_equiv: forall p x, compatible_with_equiv_p p (identity_g x). Proof. red. ir. ufi related H0; awi H0. ee. ue. Qed. (** A compatible relation induces a relation on the quotient *) Definition relation_on_quotient p r := fun t => inc t (quotient r) & exists x, inc x t & p x. Lemma rel_on_quo_pr: forall p r t, is_equivalence r -> compatible_with_equiv_p p r -> relation_on_quotient p r t = (inc t (quotient r) & forall x, inc x t -> p x). Proof. ir. ap iff_eq. ir. red in H1. ee. am. nin H2. ee. ir. rwii inc_quotient H1. red in H1. ee. rwi H6 H2. bwi H2. rwi H6 H4. bwi H4. assert (related r x x0). equiv_tac. red in H0. app (H0 _ _ H3 H7). am. am. ir. ee. red. ee. am. pose (non_empty_in_quotient H H1). exists (rep t). assert (inc (rep t) t). app nonempty_rep. eee. Qed. Lemma rel_on_quo_pr2: forall p r y, is_equivalence r -> compatible_with_equiv_p p r -> (inc y (substrate r) & relation_on_quotient p r (W y (canon_proj r))) = (inc y (substrate r) & p y). Proof. ir. ap iff_eq. ir. ee. am. awii H2. red in H2. ee. nin H3. ee. red in H0; ee. bwi H3. app (H0 x y H4). equiv_tac. am. ir. ee. am. red. ee. aw. gprops. aw. exists y. bw. ee. equiv_tac. am. Qed. (** ** EII-6-4 saturated subsets *) (** A set is satured if it is a union of classes*) Definition saturated (r x:Set) := compatible_with_equiv_p (fun y=> inc y x) r. Lemma saturated_pr: forall r x, is_equivalence r -> sub x (substrate r) -> (saturated r x) = (forall y, inc y x -> sub (class r y) x). Proof. ir. app iff_eq. ir. red. ir. bwi H3. app (H1 _ _ H2 H3). am. intros H1 u v H2 H3. app (H1 _ H2). bw. Qed. Lemma saturated_pr2: forall r x, is_equivalence r -> sub x (substrate r) -> (saturated r x) = exists y, (forall z, inc z y -> is_class r z) & x = union y. Proof. ir. app iff_eq. ir. exists (Zo (powerset x)(fun z => exists a, inc a x & z = class r a)). split. ir. Ztac. nin H4. ee. rw H5. app is_class_class. app H0. set_extens. assert (inc x0 (class r x0)). bw. cp (H0 _ H2). equiv_tac. eapply union_inc. eexact H3. Ztac. rw powerset_inc_rw. rwi saturated_pr H1. app H1. am. am. ex_tac. nin (union_exists H2). ee. Ztac. nin H6. ee. rwi H7 H3. rwi saturated_pr H1. ap (H1 _ H6). am. am. am. ir. nin H1. ee. rww saturated_pr. ir. rwi H2 H3. nin (union_exists H3). ee. cp (H1 _ H5). red. ir. bwi H7. red in H6. ee. rwi H9 H4. bwi H4. assert (related r (rep x1) x2). equiv_tac. rw H2. ap (union_sub H5). rw H9. bw. am. am. Qed. (** If f is the canonical projection this defines that smallest saturated set that contains x*) Definition inverse_direct_value f x := image_by_fun (inverse_fun f) (image_by_fun f x). Lemma class_is_inv_direct_value: forall r x, is_equivalence r -> inc x (substrate r) -> class r x = inverse_direct_value (canon_proj r) (singleton x). Proof. ir. uf inverse_direct_value. uf image_by_fun. simpl. assert (is_function (canon_proj r)). fprops. set_extens. aw. exists (class r x). ee. aw. exists x. ee. fprops. change (inc (J x (class r x)) (graph (canon_proj r))). rww related_graph_canon_proj. bw. equiv_tac. gprops. uf inverse_fun. aw. cp (sub_class_substrate H H2). assert (class r x = W x0 (canon_proj r)). rww canon_proj_W. app related_class_eq1. bwi H2. am. am. rw H4. graph_tac. aw. awi H2. nin H2. awi H2. nin H2. nin H2. ee. rwi (singleton_eq H2) H4. ufi inverse_fun H3. awi H3. cp (W_pr H1 H4). awii H5. rw H5. cp (W_pr H1 H3). assert (inc x0 (source (canon_proj r))). ap (inc_pr1graph_source H1 H3). simpl in H7. awii H6. wr H6. bw. awi H7. equiv_tac. awi H7. am. Qed. Lemma saturated_pr3: forall r x, is_equivalence r -> sub x (substrate r) -> saturated r x = (x= inverse_direct_value (canon_proj r) x). Proof. ir. set (p:=canon_proj r). assert (Ha: is_function p). uf p. fprops. app iff_eq. ir. app extensionality. uf inverse_direct_value. app inverse_direct_image. uf p. aw. red. ir. assert (forall u v, inc u (inverse_direct_value p v) = inc u (image_by_graph (inverse_graph (graph p)) (image_by_graph (graph p) v))). uf inverse_direct_value. uf image_by_fun. uf inverse_fun. aw. assert (exists a, inc a x & inc x0 (inverse_direct_value p (singleton a))). rwi H3 H2. awi H2. nin H2. ee. awi H2. nin H2. ee. ex_tac. rw H3. aw. ex_tac. aw. ex_tac. fprops. nin H4. ee. ufi p H5. wri (class_is_inv_direct_value H (H0 _ H4)) H5. rwi saturated_pr H1. app (H1 _ H4). am. am. ir. rww saturated_pr. ir. rw H1. uf inverse_direct_value. assert (inc (W y p) (image_by_fun p x)). aw. ex_tac. uf p. aw. cp (class_is_inv_direct_value H (H0 _ H2)). ufi inverse_direct_value H4. fold p in H4. rw H4. assert (inc y (source (canon_proj r))). aw. app H0. rw (image_singleton Ha H5). uf image_by_fun. app image_by_increasing. simpl. uf inverse_fun. aw. app inverse_graph_is_graph. app sub_singleton. Qed. Lemma saturated_pr4: forall r x, is_equivalence r -> sub x (substrate r) -> saturated r x = (exists b, sub b (quotient r) & x = image_by_fun (inverse_fun (canon_proj r)) b). Proof. ir. assert (HH:quotient r = target (canon_proj r)). aw. ap iff_eq. ir. rwii saturated_pr3 H1. ufi inverse_direct_value H1. exists (image_by_fun (canon_proj r) x). split. apply sub_trans with (range (graph (canon_proj r))). uf image_by_fun. app sub_image_by_graph. rw HH. fprops. assert (is_function (canon_proj r)). fprops. fct_tac. tv. ir. nin H1. ee. pose (canon_proj_surjective H). rwi HH H1. cp (direct_inv_im_surjective s H1). wri H2 H3. cp (f_equal (image_by_fun (inverse_fun (canon_proj r))) H3). wri H2 H4. rww saturated_pr3. sy. am. Qed. (** Links between saturation and union, intersection, complement *) Lemma saturated_union: forall r x, is_equivalence r -> (forall y, inc y x -> sub y (substrate r)) -> (forall y, inc y x -> saturated r y) -> (sub (union x) (substrate r) & saturated r (union x)). Proof. ir. assert (sub (union x) (substrate r)). red. ir. nin (union_exists H2). ee. app (H0 _ H4). ee. am. rww saturated_pr. ir. nin (union_exists H3). ee. pose (H1 _ H5). rwii saturated_pr s. pose (s _ H4). apply sub_trans with x0. am. app union_sub. app H0. Qed. Lemma saturated_intersection : forall r x, is_equivalence r -> nonempty x -> (forall y, inc y x -> sub y (substrate r)) -> (forall y, inc y x -> saturated r y) -> (sub (intersection x) (substrate r) & saturated r (intersection x)). Proof. ir. assert (sub (intersection x) (substrate r)). nin H0. apply sub_trans with y. app (intersection_sub H0). app H1. ee. am. rww saturated_pr. ir. red. ir. app intersection_inc. ir. pose (H2 _ H6). rwi saturated_pr s. app (s _ (intersection_forall H4 H6)). am. app H1. Qed. Lemma saturated_complement : forall r a, is_equivalence r -> sub a (substrate r) -> saturated r a -> saturated r (complement (substrate r) a). Proof. intros r a H0 H1. do 2 rww saturated_pr4. ir. nin H. ee. exists (complement (quotient r) x). ee. app sub_complement. assert (is_function (canon_proj r)). fprops. cp (inv_image_complement x H3). ufi inv_image_by_fun H4. uf image_by_fun. simpl in H4. ufi image_by_fun H2. ufi inv_image_by_graph H4. uf inverse_fun. aw. awi H4. set (t := inverse_graph (graph (canon_proj r))) in *. assert (HH:target (canon_proj r) = quotient r). uf canon_proj. aw. awi H4. rw H4. ufi inverse_fun H2. awi H2. ue. app sub_complement. Qed. Definition saturation_of (r x:Set):= inverse_direct_value (canon_proj r) x. Lemma saturation_of_pr: forall r x, is_equivalence r -> sub x (substrate r) -> saturation_of r x = union (Zo (quotient r)(fun z=> exists i, inc i x & z = class r i)). Proof. ir. assert (is_function (canon_proj r)). fprops. uf saturation_of. uf inverse_direct_value. set_extens. ufi image_by_fun H2. awi H2. nin H2. ee. awi H2. nin H2. ee. ufi inverse_fun H3. awi H3. assert (inc x0 (source (canon_proj r))). graph_tac. assert (inc x1 (target (canon_proj r))). graph_tac. awi H5; awi H6. apply union_inc with x1. wrr (related_graph_canon_proj H (x:=x0)(y:=x1)). Ztac. ex_tac. assert (inc x2 (source (canon_proj r))). graph_tac. awi H7. assert (W x2 (canon_proj r) = x1). app W_pr. wr H8. app canon_proj_W. nin (union_exists H2). ee. Ztac. nin H6. ee. uf image_by_fun. aw. exists x1. ee. cp (H0 _ H6). aw. exists x2. ee. am. rww related_graph_canon_proj. rw H7. bw. equiv_tac. simpl. aw. uf inverse_fun. aw. rww related_graph_canon_proj. app (inc_in_quotient_substrate H H3 H5). Qed. Lemma saturation_of_smallest: forall r x, is_equivalence r -> sub x (substrate r) -> (saturated r (saturation_of r x) & sub x (saturation_of r x) & (forall y, sub y (substrate r) -> saturated r y -> sub x y -> sub (saturation_of r x) y)). Proof. ir. assert (is_function (canon_proj r)). fprops. ee. set (a:= (saturation_of r x)). rww saturated_pr4. ufi saturation_of a. assert (Hw:quotient r = target (canon_proj r)). aw. rw Hw. exists (image_by_fun (canon_proj r) x). ee. uf image_by_fun. apply sub_trans with (range (graph (canon_proj r))). app sub_image_by_graph. red in H1. ee. fprops. tv. uf a. unfold saturation_of. uf inverse_direct_value. uf image_by_fun. uf inverse_fun. aw. red. ir. awi H2. nin H2. ee. awi H3. cp (inc_pr1graph_source H1 H3). awi H4. am. uf saturation_of. uf inverse_direct_value. red. ir. uf image_by_fun. aw. cp (H0 _ H2). assert(inc (J x0 (class r x0)) (graph (canon_proj r))). rww related_graph_canon_proj. bw. equiv_tac. gprops. exists (class r x0). ee. aw. ex_tac. simpl. uf inverse_fun. aw. ir. uf saturation_of. aw. rwi saturated_pr3 H3. rw H3. uf inverse_direct_value. uf image_by_fun; app image_by_increasing. uf inverse_fun. aw. fprops. app image_by_increasing. fprops. am. am. Qed. Definition union_image x f:= union (Zo x (fun z=> exists i, inc i (source f) & z = W i f)). Lemma saturation_of_union: forall r f g, is_equivalence r -> is_function f -> is_function g -> (forall i, inc i (source f) -> sub (W i f) (substrate r)) -> source f = source g -> (forall i, inc i (source f) -> saturation_of r (W i f) = W i g) -> saturation_of r (union_image (powerset(substrate r)) f) = union_image (powerset(substrate r)) g. Proof. ir. assert (is_function (canon_proj r)). fprops. uf saturation_of. uf inverse_direct_value. uf union_image. ufi saturation_of H4. ufi inverse_direct_value H4. uf image_by_fun. ufi image_by_fun H4. simpl. simpl in H4. set_extens. awi H6. nin H6. ee. awi H6. nin H6. ee. nin (union_exists H6). ee. Ztac. nin H12. ee. assert (inc (W x3 g) (Zo (powerset (substrate r)) (fun z => exists i, inc i (source g) & z = W i g))). clear H10. Ztac. wr (H4 x3). app powerset_inc. red. ir. awi H10. nin H10. ee. ufi inverse_fun H14. awi H14. cp (inc_pr1graph_source H5 H14). awii H15. ue. ue. rwi H3 H12. ex_tac. assert (inc x (W x3 g)). wr (H4 x3). aw. exists x0. ee. aw. exists x1. ee. wr H13. am. am. am. am. union_tac. nin (union_exists H6). ee. Ztac. nin H10; ee. clear H8. wri H3 H10. rwi H11 H7. wri (H4 _ H10) H7. awi H7. nin H7. ee. awi H7. nin H7. ee. aw. exists x2. ee. aw. ex_tac. apply union_inc with (W x1 f). am. Ztac. app powerset_inc. app H2. ex_tac. am. Qed. (** ** EII-6-5 Mappings compatible with equivalence relations *) (** The canonical projection is surjective, thus has a section *) Definition section_canon_proj (r:Set) := BL rep (quotient r) (substrate r). Lemma section_canon_proj_axioms:forall r, is_equivalence r -> transf_axioms rep (quotient r) (substrate r). Proof. ir. red. ir. fprops. Qed. Lemma section_canon_proj_W: forall r x, is_equivalence r -> inc x (quotient r) -> W x (section_canon_proj r) = (rep x). Proof. ir. uf section_canon_proj. aw. app section_canon_proj_axioms. Qed. Lemma section_canon_proj_function: forall r, is_equivalence r -> is_function (section_canon_proj r). Proof. ir. uf section_canon_proj. app bl_function. app section_canon_proj_axioms. Qed. Lemma right_inv_canon_proj: forall r, is_equivalence r -> is_right_inverse (section_canon_proj r) (canon_proj r). Proof. ir. assert (Ha:source (section_canon_proj r) = quotient r). uf section_canon_proj. aw. assert (is_function (section_canon_proj r)). app section_canon_proj_function. assert (is_function (canon_proj r)). fprops. assert (composable (canon_proj r) (section_canon_proj r)). red. eee. uf section_canon_proj. aw. red. ee. am. app function_exten. fct_tac. app identity_function. aw. aw. aw. rw Ha. ir. ufi section_canon_proj H3; awi H3. aw. rww section_canon_proj_W. rww identity_W. app class_rep. rww section_canon_proj_W. fprops. ue. Qed. (** A mapping is compatible with an equivalence if it is constant on classes; it is compatible with two equivalences is the image of a class is a subset of a class *) Definition compatible_with_equiv f r := is_function f & source f = substrate r & forall x x', related r x x' -> W x f = W x' f. Definition compatible_with_equivs f r r' := is_function f & target f = substrate r' & compatible_with_equiv (compose (canon_proj r') f) r. (* This is the definition of Bourbaki *) Lemma compatible_with_equiv_pr: forall f r, is_function f -> source f = substrate r -> compatible_with_equiv f r = (forall y, compatible_with_equiv_p (fun x => y = W x f) r). Proof. uf compatible_with_equiv. uf compatible_with_equiv_p. ir. app iff_eq. ir. ee. rw H2. app H5. ir. eee. ir. app (H1 (W x f) x x'). Qed. Lemma compatible_constant_on_classes: forall f r x y, is_equivalence r -> compatible_with_equiv f r -> inc y (class r x) -> W x f = W y f. Proof. ir. red in H0; ee. app H3. bwi H1. am. am. Qed. Lemma compatible_constant_on_classes2: forall f r x, is_equivalence r -> compatible_with_equiv f r -> is_constant_function(restriction f (class r x)). Proof. ir. assert (Ha: sub (class r x) (substrate r)). app sub_class_substrate. red. red in H0. nin H0. nin H1. wri H1 Ha. ee. app restriction_function. assert (source (restriction f (class r x)) = class r x). uf restriction. aw. rw H3. ir. do 2 rww restriction_W. app H2. bwi H4. bwi H5. equiv_tac. am. am. Qed. Lemma compatible_with_proj: forall f r x y, is_equivalence r -> compatible_with_equiv f r -> inc x (substrate r) -> inc y (substrate r) -> W x (canon_proj r) = W y (canon_proj r) -> W x f = W y f. Proof. ir. awii H3. apply compatible_constant_on_classes with r. am. am. rw H3. bw. equiv_tac. Qed. Lemma compatible_with_pr:forall r r' f x y, is_equivalence r -> is_equivalence r' -> compatible_with_equivs f r r' -> related r x y -> related r' (W x f) (W y f). Proof. ir. red in H1. ee. red in H4. ee. cp (H6 _ _ H2). assert (composable (canon_proj r') f). red. ee. fprops. am. aw. sy. am. rwi related_rw H2. ee. wri H5 H2. wri H5 H9. awi H2. awi H9. assert (inc (W y f) (substrate r')). wr H3. fprops. assert (inc (W x f) (substrate r')). wr H3. fprops. awii H7. wr inc_class. rw H7. bw. equiv_tac. am. am. Qed. Lemma compatible_with_pr2:forall r r' f, is_equivalence r -> is_equivalence r' -> is_function f -> target f = substrate r'-> source f = substrate r-> (forall x y, related r x y -> related r' (W x f) (W y f)) -> compatible_with_equivs f r r'. Proof. ir. red. eee. assert (composable (canon_proj r') f). red. ee. fprops. am. sy. aw. red. ee. fct_tac. aw. ir. cp (H4 _ _ H6). rwii related_rw H6. ee. wri H3 H6; wri H3 H8. aw. app related_class_eq1. wr H2. fprops. wr H2. fprops. Qed. Lemma compatible_with_proj3 :forall r r' f x y, is_equivalence r -> is_equivalence r' -> compatible_with_equivs f r r'-> inc x (substrate r) -> inc y (substrate r) -> W x (canon_proj r) = W y (canon_proj r) -> class r' (W x f) = class r' (W y f). Proof. ir. awii H4. app related_class_eq1. wri related_class_eq H4. app (compatible_with_pr H H0 H1 H4). am. equiv_tac. Qed. (** A compatible mapping induces a mapping on the quotient *) Definition fun_on_quotient r f := compose f (section_canon_proj r). Lemma exists_fun_on_quotient: forall f r, is_equivalence r -> is_function f -> source f = substrate r -> compatible_with_equiv f r = (exists h, composable h (canon_proj r) & compose h (canon_proj r) = f). Proof. ir. rw exists_left_composable. aw. app iff_eq. ir. ap (compatible_with_proj H H2 H3 H4 H5). ir. red. eee. ir. rwi related_rw H3. ee. app H2. aw. am. am. app canon_proj_surjective. aw. Qed. Lemma exists_unique_fun_on_quotient: forall f r h, is_equivalence r -> compatible_with_equiv f r -> composable h (canon_proj r) -> compose h (canon_proj r) = f -> h = fun_on_quotient r f. Proof. ir. assert (surjective (canon_proj r)). app canon_proj_surjective. pose (right_inv_canon_proj H). assert (is_function f). red in H0; eee. assert (source f = source (canon_proj r)). red in H0; ee. aw. assert (surjective (canon_proj r)). app canon_proj_surjective. app (exists_left_composable_aux H4 H3 H5 i H1 H2). Qed. Lemma compose_foq_proj :forall f r, is_equivalence r -> compatible_with_equiv f r -> compose (fun_on_quotient r f) (canon_proj r) = f. Proof. ir. assert (Ha:= H0). set (g:= canon_proj r). red in H0; ee. assert (surjective g). uf g. app canon_proj_surjective. assert (source f = source g). uf g. aw. assert (forall x y, inc x (source g) -> inc y (source g) -> W x g = W y g -> W x f = W y f). wr H4. rw H1. fold g; ir. ap (compatible_with_proj H Ha H5 H6). fold g. am. app (left_composable_value H0 H3 H4 H5 (right_inv_canon_proj H) (refl_equal ( fun_on_quotient r f))). Qed. (** A mappoing compatible with two relations induces a mapping on the two quotients *) Definition fun_on_rep f:EE := fun x=> f(rep x). Definition fun_on_reps r' f := fun x=> W (f(rep x)) (canon_proj r'). Definition function_on_quotient r f b := BL(fun_on_rep f)(quotient r)(b). Definition function_on_quotients r r' f := BL(fun_on_reps r' f)(quotient r)(quotient r'). Definition fun_on_quotients r r' f := compose (compose (canon_proj r') f) (section_canon_proj r). Lemma foq_axioms: forall r f b, is_equivalence r -> transf_axioms f (substrate r) b -> transf_axioms (fun_on_rep f) (quotient r) b. Proof. uf transf_axioms. ir. uf fun_on_rep. app H0. fprops. Qed. Lemma foqs_axioms: forall r r' f, is_equivalence r -> is_equivalence r' -> transf_axioms f (substrate r)(substrate r') -> transf_axioms (fun_on_reps r' f) (quotient r) (quotient r'). Proof. uf transf_axioms. ir. uf fun_on_reps. assert (inc (rep c) (substrate r)). fprops. aw. gprops. app H1. Qed. Lemma foqc_axioms: forall r f, is_equivalence r -> is_function f -> source f = substrate r -> composable f (section_canon_proj r). Proof. ir. red. ee. am. app section_canon_proj_function. uf section_canon_proj. aw. Qed. Lemma foqcs_axioms:forall r r' f, is_equivalence r -> is_equivalence r' -> is_function f -> source f = substrate r -> target f = substrate r' -> composable (compose (canon_proj r') f) (section_canon_proj r). Proof. ir. red. ee. assert (is_function (canon_proj r')). fprops. fct_tac. sy; aw. app section_canon_proj_function. uf section_canon_proj. aw. Qed. Lemma foq_function:forall r f b, is_equivalence r -> transf_axioms f (substrate r) b -> is_function (function_on_quotient r f b). Proof. ir. uf function_on_quotient. app bl_function. app foq_axioms. Qed. Lemma foqs_function: forall r r' f, is_equivalence r -> is_equivalence r' -> transf_axioms f (substrate r)(substrate r') -> is_function (function_on_quotients r r' f). Proof. ir. uf function_on_quotients. app bl_function. app foqs_axioms. Qed. Lemma foqc_function:forall r f, is_equivalence r -> is_function f -> source f = substrate r -> is_function (fun_on_quotient r f). Proof. ir. uf fun_on_quotient. fct_tac. app section_canon_proj_function. uf section_canon_proj. aw. Qed. Lemma foqcs_function:forall r r' f, is_equivalence r -> is_equivalence r' -> is_function f -> source f = substrate r -> target f = substrate r' -> is_function (fun_on_quotients r r' f). Proof. ir. uf fun_on_quotients. app compose_function. app foqcs_axioms. Qed. Lemma foq_W:forall r f b x, is_equivalence r -> transf_axioms f (substrate r) b -> inc x (quotient r) -> W x (function_on_quotient r f b) = f (rep x). Proof. ir. uf function_on_quotient. aw. app foq_axioms. Qed. Lemma foqc_W:forall r f x, is_equivalence r -> is_function f -> source f = substrate r -> inc x (quotient r) -> W x (fun_on_quotient r f) = W (rep x) f. Proof. ir. uf fun_on_quotient. aw. rw section_canon_proj_W. tv. am. am. app foqc_axioms. uf section_canon_proj. aw. Qed. Lemma foqs_W: forall r r' f x, is_equivalence r -> is_equivalence r' -> transf_axioms f (substrate r)(substrate r') -> inc x (quotient r) -> W x (function_on_quotients r r' f) = class r' (f (rep x)). Proof. ir. uf function_on_quotients. aw. uf fun_on_reps. aw. red in H1. app H1. fprops. app foqs_axioms. Qed. Lemma foqcs_W:forall r r' f x, is_equivalence r -> is_equivalence r' -> is_function f -> source f = substrate r -> target f = substrate r' -> inc x (quotient r) -> W x (fun_on_quotients r r' f) = class r' (W (rep x) f). Proof. ir. uf fun_on_quotients. assert (is_function (section_canon_proj r)). app section_canon_proj_function. assert (composable (canon_proj r') f). red. eee. aw. assert (inc (W x (section_canon_proj r)) (target (section_canon_proj r))). app inc_W_target. uf section_canon_proj. aw. rw compose_W. rww section_canon_proj_W. uf section_canon_proj. aw. wr H3. app inc_W_target. ue. ue. red. ee. fct_tac. am. uf section_canon_proj. aw. uf section_canon_proj. aw. Qed. Lemma fun_on_quotient_pr: forall r f x, W x f = fun_on_rep (fun w => W x f) (W x (canon_proj r)). Proof. ir. tv. Qed. Lemma fun_on_quotient_pr2: forall r r' f x, W (W x f) (canon_proj r') = fun_on_reps r' (fun w => W x f) (W x (canon_proj r)). Proof. ir. tv. Qed. Lemma composable_fun_proj: forall r f b, is_equivalence r -> transf_axioms f (substrate r) b -> composable (function_on_quotient r f b) (canon_proj r). Proof. ir. red. eee. app foq_function. uf function_on_quotient. aw. Qed. Lemma composable_fun_projs: forall r r' f, is_equivalence r -> is_equivalence r' -> transf_axioms f (substrate r) (substrate r') -> composable (function_on_quotients r r' f) (canon_proj r). Proof. ir. red. eee. app foqs_function. uf function_on_quotients. aw. Qed. Lemma composable_fun_projc: forall r f, is_equivalence r -> compatible_with_equiv f r -> composable (fun_on_quotient r f) (canon_proj r). Proof. ir. red. red in H0. eee. app foqc_function. uf fun_on_quotient. aw. uf section_canon_proj. aw. Qed. Lemma composable_fun_projcs: forall r r' f, is_equivalence r -> is_equivalence r' -> compatible_with_equivs f r r'-> composable (fun_on_quotients r r' f) (canon_proj r). Proof. ir. red in H1; ee. red in H3. ee. red. eee. app foqcs_function. awi H4. am. uf fun_on_quotients. aw. uf section_canon_proj. aw. Qed. Lemma fun_on_quotient_pr3: forall r f x, is_equivalence r -> inc x (substrate r) -> compatible_with_equiv f r -> W x f = W (W x (canon_proj r)) (fun_on_quotient r f). Proof. ir. wr compose_W. rww compose_foq_proj. app composable_fun_projc. aw. Qed. (** Figure 3 (French version only) *) Lemma fun_on_quotient_pr4: forall r r' f, is_equivalence r -> is_equivalence r' -> compatible_with_equivs f r r'-> compose (canon_proj r') f = compose (fun_on_quotients r r' f)(canon_proj r). Proof. ir. uf fun_on_quotients. red in H1. ee. sy. ap (compose_foq_proj H H3). Qed. Lemma fun_on_quotient_pr5: forall r r' f x, is_equivalence r -> is_equivalence r' -> compatible_with_equivs f r r'-> inc x (substrate r) -> W (W x f) (canon_proj r') = W (W x (canon_proj r)) (fun_on_quotients r r' f). Proof. ir. cp H1. nin H1. nin H4. nin H5. nin H6. awi H6. wr compose_W. wrr compose_W. wrr fun_on_quotient_pr4. app composable_fun_projcs. aw. red. eee. aw. ue. Qed. Lemma compose_fun_proj_ev: forall r f b x, is_equivalence r -> compatible_with_equiv (BL f (substrate r) b) r -> inc x (substrate r) -> transf_axioms f (substrate r) b -> W x (compose (function_on_quotient r f b) (canon_proj r)) = f x. Proof. ir. assert (inc (class r x) (quotient r)). gprops. aw. rww foq_W. red in H0. ee. assert (related r (rep (class r x)) x). app symmetricity_e. app related_rep_class. pose (H5 _ _ H6). awii e. fprops. app composable_fun_proj. aw. Qed. Lemma compose_fun_proj_ev2: forall r r' f x, is_equivalence r -> is_equivalence r' -> compatible_with_equivs (BL f (substrate r) (substrate r')) r r' -> transf_axioms f (substrate r) (substrate r') -> inc x (substrate r) -> inc (f x) (substrate r') -> W (f x) (canon_proj r') = W x (compose (function_on_quotients r r' f) (canon_proj r)). Proof. ir. aw. set (xx:= (W x (canon_proj r))). assert (W xx (function_on_quotients r r' f) = (W xx (fun_on_quotients r r' (BL f (substrate r) (substrate r'))))). assert (inc xx (quotient r)). uf xx. aw. gprops. rww foqs_W. rww foqcs_W. aw. uf xx. aw. app inc_rep_substrate. gprops. app bl_function. aw. aw. aw. ufi xx H5. wri fun_on_quotient_pr5 H5. awii H5. sy; am. aw. am. am. am. am. app composable_fun_projs. aw. Qed. Lemma compose_fun_proj_eq: forall r f b, is_equivalence r -> compatible_with_equiv (BL f (substrate r) b) r -> transf_axioms f (substrate r) b -> compose (function_on_quotient r f b) (canon_proj r) = BL f (substrate r) b. Proof. ir. app function_exten. ap compose_function. app composable_fun_proj. app bl_function. uf fun_on_quotient. aw. uf function_on_quotient. aw. aw. aw. ir. rww compose_fun_proj_ev. aw. Qed. Lemma compose_fun_proj_eq2: forall r r' f, is_equivalence r -> is_equivalence r' -> transf_axioms f (substrate r) (substrate r') -> compatible_with_equivs (BL f (substrate r) (substrate r')) r r'-> compose (function_on_quotients r r' f) (canon_proj r) = compose (canon_proj r') (BL f (substrate r) (substrate r')). Proof. ir. assert (is_function (function_on_quotients r r' f)). app foqs_function. assert(is_function (BL f (substrate r) (substrate r'))). app bl_function. assert (composable (function_on_quotients r r' f) (canon_proj r)). red. eee. uf function_on_quotients. aw. assert (composable (canon_proj r') (BL f (substrate r) (substrate r'))). red. eee. aw. app function_exten. fct_tac. fct_tac. aw. uf function_on_quotients. aw. ir. awi H7. assert (inc (f x) (substrate r')). app H1. wrr compose_fun_proj_ev2. aw. Qed. Lemma compatible_ea: forall f, is_function f -> compatible_with_equiv f (equivalence_associated f). Proof. ir. red. ee. am. rww graph_ea_substrate. ir. rwii ea_related H0. ee. am. Qed. Lemma ea_foq_injective: forall f, is_function f -> injective (fun_on_quotient (equivalence_associated f) f). Proof. ir. set (g:= equivalence_associated f). assert (is_equivalence g). uf g. app graph_ea_equivalence. assert(source f = substrate g). uf g. rww graph_ea_substrate. red. ee. app foqc_function. assert (source (fun_on_quotient g f) = (quotient g)). uf fun_on_quotient. uf section_canon_proj. aw. rw H2; clear H2. ir. rwii foqc_W H4. rwii foqc_W H4. pose (inc_rep_substrate H0 H2). pose (inc_rep_substrate H0 H3). assert (related g (rep x) (rep y)). uf g. rw ea_related. rw H1. intuition. am. rwii related_rep_rep H5. Qed. Lemma ea_foq_on_im_bijective: forall f, is_function f -> bijective (restriction2 (fun_on_quotient (equivalence_associated f) f) (quotient (equivalence_associated f)) (range (graph f))). Proof. ir. set (g:= equivalence_associated f). set (h:= fun_on_quotient g f). assert(is_equivalence g). uf g. app graph_ea_equivalence. assert(source f = substrate g). uf g. rww graph_ea_substrate. assert (injective h). uf h. uf g. app ea_foq_injective. assert (Ha: is_function h). fct_tac. assert (quotient g = source h). uf h. uf fun_on_quotient. uf section_canon_proj. aw. assert (range (graph f) = image_by_fun h (source h)). uf h. simpl. set_extens. awi H4. nin H4. assert (inc x0 (source f)). graph_tac. rwi H1 H5. assert (inc (class g x0) (quotient g)). gprops. aw. exists (class g x0). ee. fold h. ue. rww foqc_W. wr (W_pr H H4). assert (related g x0 (rep (class g x0))). app related_rep_class. cp (ea_related x0 (rep (class g x0)) H). fold g in H8. rwi H8 H7. eee. fprops. fprops. awi H4. nin H4. nin H4. rwii foqc_W H5. wr H5. aw. exists (rep x0). graph_tac. rw H1. app inc_rep_substrate. ue. fprops. ue. fprops. fprops. rw H4. rw H3. rww restriction1_pr. app restriction1_bijective. fprops. Qed. (** Canonical decomposition of a function as a surjection, a bijection and an ionjection *) Lemma canonical_decompositiona: forall f, is_function f -> let r:= equivalence_associated f in is_function (compose (restriction2 (fun_on_quotient r f) (quotient r) (range (graph f))) (canon_proj r)). Proof. ir. set (g:= canon_proj r). set (a:=range (graph f)). set (j:=canonical_injection a (target f)). set (k:=restriction2 (fun_on_quotient r f) (quotient r) a). assert (is_equivalence r). uf r. app graph_ea_equivalence. assert (source f = substrate r). uf r. rww graph_ea_substrate. assert (sub a (target f)). uf a. red in H;eee. assert (is_function j). uf j. app ci_function. assert (is_function (fun_on_quotient r f)). app foqc_function. assert(restriction2_axioms (fun_on_quotient r f) (quotient r) a). red. eee. uf fun_on_quotient. aw. uf section_canon_proj. aw. fprops. uf fun_on_quotient. aw. red. ir. ufi image_by_fun H5. awi H5. nin H5. ee. red in H6. pose (W_pr H4 H6). rwii foqc_W e. uf a. rww range_inc_rw. exists (rep x0). eee. assert (is_function k). uf k. app restriction2_function. assert (composable k g). uf k; uf g. red. ee. app restriction2_function. fprops. aw. uf restriction2. aw. fct_tac. Qed. Lemma canonical_decomposition: forall f, is_function f -> let r:= equivalence_associated f in f = compose (canonical_injection (range (graph f))(target f)) (compose (restriction2 (fun_on_quotient r f) (quotient r) (range (graph f))) (canon_proj r)). Proof. ir. set (g:= canon_proj r). set (a:=range (graph f)). set (j:=canonical_injection a (target f)). set (k:=restriction2 (fun_on_quotient r f) (quotient r) a). assert (is_equivalence r). uf r. app graph_ea_equivalence. assert(source f = substrate r). uf r. rww graph_ea_substrate. assert (sub a (target f)). uf a. red in H;eee. assert (is_function j). uf j. app ci_function. assert (is_function (fun_on_quotient r f)). app foqc_function. assert(restriction2_axioms (fun_on_quotient r f) (quotient r) a). red. eee. uf fun_on_quotient. uf section_canon_proj. aw. fprops. uf fun_on_quotient. aw. red. ir. awi H5. nin H5. ee. wr H6. rw foqc_W. uf a. app inc_W_range_graph. rw H1. fprops. am. am. am. am. am. uf fun_on_quotient. aw. uf section_canon_proj. fprops. aw. fprops. assert (is_function k). uf k. app restriction2_function. assert (composable k g). uf k; uf g. red. ee. app restriction2_function. fprops. uf restriction2. aw. assert (Ha: source f = source g). uf g. aw. assert (is_function (compose k g)). fct_tac. assert (composable j (compose k g)). red. eee. uf j. uf k. uf canonical_injection. uf restriction2. aw. app function_exten. fct_tac. aw. uf j. uf canonical_injection. aw. ir. rwi Ha H10. cp H10. wri Ha H10. rwi H1 H10. assert (inc (W x g) (quotient r)). assert (quotient r = target g). uf g. aw. rw H12. app inc_W_target. uf g. fprops. aw. uf j. rww ci_W. uf k. rww restriction2_W. rww foqc_W. uf g. aw. assert (related r x (rep (class r x))). app related_rep_class. cp (ea_related x (rep (class r x)) H). fold r in H14. rwi H14 H13. ee. am. assert (a = target k). uf k. uf restriction2. aw. rw H13. app inc_W_target. uf k. uf restriction2. aw. Qed. Lemma surjective_pr7: forall f, surjective f -> canonical_injection (range (graph f))(target f) = identity (target f). Proof. ir. red in H; ee. assert (source f = domain (graph f)). red in H; eee. ufi image_of_fun H0. rwi H1 H0. assert (Ha: is_graph (graph f)). fprops. rwii image_by_graph_domain H0. app function_exten. app ci_function. rw H0; fprops. app identity_function. uf canonical_injection. aw. uf canonical_injection. aw. ir. ufi canonical_injection H2. awi H2. nin H2. assert ( inc x (range (graph f))). aw. ex_tac. rw ci_W. rww identity_W. wrr H0. ue. am. am. Qed. Lemma canonical_decomposition_surj: forall f, surjective f -> let r:= equivalence_associated f in f = (compose (restriction2 (fun_on_quotient r f) (quotient r) (target f)) (canon_proj r)). Proof. ir. cp (surjective_pr7 H). cp (surjective_pr3 H). nin H. cp (canonical_decomposition H). simpl in H3. rwi H0 H3. fold r in H3. rwi H1 H3. set (g:= (restriction2 (fun_on_quotient r f) (quotient r) (target f))) in *. set (h:= compose g (canon_proj r)) in *. rw H3. assert (target f = target h). uf h. uf g. uf restriction2. aw. rw H4. app compose_identity_left. assert(is_function h). uf h. uf g. uf r. wr H1. app canonical_decompositiona. red in H5. ee. am. Qed. Lemma canonical_decompositionb: forall f, is_function f -> let r:= equivalence_associated f in restriction2 (fun_on_quotient r f) (quotient r) (target f) = (fun_on_quotient r f). Proof. ir. set (k:=restriction2 (fun_on_quotient r f) (quotient r) (target f)). assert (is_equivalence r). uf r. app graph_ea_equivalence. assert(source f = substrate r). uf r. rww graph_ea_substrate. assert (is_function (fun_on_quotient r f)). app foqc_function. assert(restriction2_axioms (fun_on_quotient r f) (quotient r) (target f)). red. eee. uf fun_on_quotient. aw. uf section_canon_proj. aw. fprops. uf fun_on_quotient. aw. fprops. red. ir. ufi image_by_fun H3. assert (target f = target (fun_on_quotient r f)). uf fun_on_quotient. aw. rw H4. change (inc x (image_by_fun (fun_on_quotient r f) (quotient r))) in H3. assert (quotient r = source (fun_on_quotient r f)). uf fun_on_quotient. aw. uf section_canon_proj. aw. rwi H5 H3. rwi (image_by_fun_source H2) H3. app f_range_graph. assert (is_function k). uf k. app restriction2_function. app function_exten. ir. uf k. uf restriction2. uf fun_on_quotient. uf section_canon_proj. aw. uf k. uf restriction2. uf fun_on_quotient. aw. ir. uf k. rww restriction2_W. ufi k H5. ufi restriction2 H5. awi H5. am. Qed. Lemma canonical_decomposition_surj2: forall f, surjective f -> let r:= equivalence_associated f in f = (compose (fun_on_quotient r f) (canon_proj r)). Proof. ir. cp (canonical_decomposition_surj H). red in H. ee. cp (canonical_decompositionb H). set (g:= fun_on_quotient r f). rw H0. rww H2. Qed. (** ** EII-6-6 Inverse image of an equivalence relation; induced equivalence relation *) (** We have an equivalence on the source induced by the equivalence on the target*) Definition inv_image_relation f r := equivalence_associated (compose (canon_proj r) f). Definition iirel_axioms f r := is_function f & is_equivalence r & target f = substrate r. Lemma iirel_function: forall f r, iirel_axioms f r -> is_function (compose (canon_proj r) f). Proof. ir. red in H. ee. fprops. assert (is_function (canon_proj r)). fprops. fct_tac. sy. aw. Qed. Lemma iirel_relation: forall f r, iirel_axioms f r -> is_equivalence (inv_image_relation f r). Proof. ir. uf inv_image_relation. app graph_ea_equivalence. app iirel_function. Qed. Lemma iirel_substrate: forall f r, iirel_axioms f r -> substrate (inv_image_relation f r) = source f. Proof. ir. uf inv_image_relation. rw graph_ea_substrate. aw. app iirel_function. Qed. Lemma iirel_related: forall f r x y, iirel_axioms f r -> related (inv_image_relation f r) x y = (inc x (source f) & inc y (source f) & related r (W x f) (W y f)). Proof. ir. assert (Ha:is_function (compose (canon_proj r) f)). app iirel_function. uf inv_image_relation. red in H. ee. assert(composable (canon_proj r) f). red. eee. aw. rww ea_related. simpl. assert (forall u, inc u (source f) -> inc (W u f) (substrate r)). ir. wr H1; fprops. assert (source (compose (canon_proj r) f) = source f). aw. rw H4. clear H4. app iff_eq; ir; nin H4; nin H5; cp (H3 _ H4); cp (H3 _ H5); eee. awii H6. rww related_class_eq. equiv_tac. aw. app related_class_eq1. Qed. Lemma iirel_class: forall f r x, iirel_axioms f r -> is_class (inv_image_relation f r) x = exists y, is_class r y & nonempty (intersection2 y (range (graph f))) & x = inv_image_by_fun f y. Proof. ir. assert(Ha:=H). red in H; ee. app iff_eq. ir. rwi is_class_rw H2. ee. rwi iirel_substrate H3. nin H2. assert (inc (W y f) (substrate r)). wr H1. cp (H3 _ H2). fprops. exists (class r (W y f)). ee. app is_class_class. exists (W y f). inter2tac. bw. equiv_tac. aw. exists y. graph_tac. fprops. set_extens. cp H6. rwi (H4 y x0) H7. rwi iirel_related H7. ee. uf inv_image_by_fun. aw. exists (W x0 f). ee. bw. graph_tac. am. am. ufi inv_image_by_fun H6. awi H6. nin H6. ee. rw (H4 y x0 H2). rww iirel_related. ee. app H3. graph_tac. red in H7. rw (W_pr H H7). bwi H6. am. am. am. app iirel_relation. ir. nin H2. ee. nin H3. nin (intersection2_both H3). awi H6. nin H6. pose (W_pr H H6). assert (sub x (source f)). rw H4. red. ir. ufi inv_image_by_fun H7. awi H7. nin H7. ee. graph_tac. rw is_class_rw. ee. rw H4. exists x1. uf inv_image_by_fun. aw. ex_tac. rww iirel_substrate. ir. rw iirel_related. app iff_eq. ir. ee. app H7. app H7. rwi H4 H8. ufi inv_image_by_fun H8. awi H8. nin H8. ee. red in H10. rw (W_pr H H10). rwi H4 H9. ufi inv_image_by_fun H9. awi H9. nin H9. ee. red in H11. rw (W_pr H H11). rw in_class_related. exists x0. intuition. am. ir. ee. rwi H4 H8. ufi inv_image_by_fun H8. awi H8. nin H8. ee. red in H12. rwi (W_pr H H12) H11. rw H4. uf inv_image_by_fun. aw. exists (W z f). ee. rwi is_class_rw H2. ee. wri (H14 x2 (W z f) H8) H11. am. am. graph_tac. am. app iirel_relation. fprops. Qed. (** Equivalence induced on a subset of the substrate *) Definition induced_relation (r a:Set) := inv_image_relation (canonical_injection a (substrate r)) r. Definition induced_rel_axioms(r a :Set) := is_equivalence r & sub a (substrate r). Lemma induced_rel_iirel_axioms : forall r a, induced_rel_axioms r a -> iirel_axioms (canonical_injection a (substrate r)) r. Proof. ir. red. red in H. eee. uf canonical_injection. aw. Qed. Lemma induced_rel_equivalence: forall r a, induced_rel_axioms r a -> is_equivalence (induced_relation r a). Proof. ir. uf induced_relation. app iirel_relation. app induced_rel_iirel_axioms. Qed. Lemma induced_rel_substrate: forall r a, induced_rel_axioms r a -> substrate (induced_relation r a) = a. Proof. ir. uf induced_relation. rww iirel_substrate. uf canonical_injection. aw. app induced_rel_iirel_axioms. Qed. Lemma induced_rel_related: forall r a u v, induced_rel_axioms r a -> related (induced_relation r a) u v = (inc u a & inc v a & related r u v). Proof. ir. cp (induced_rel_iirel_axioms H). red in H; ee. uf induced_relation. rw iirel_related. assert (source (canonical_injection a (substrate r)) = a). uf canonical_injection. aw. rw H2. clear H2. app iff_eq. ir. eee. rwii ci_W H4. rwii ci_W H4. ir. eee. rww ci_W. rww ci_W. am. Qed. Lemma induced_rel_class: forall r a x, induced_rel_axioms r a -> is_class (induced_relation r a) x = exists y, is_class r y & nonempty (intersection2 y a) & x = (intersection2 y a). Proof. ir. cp (induced_rel_iirel_axioms H). uf induced_relation. rww iirel_class. red in H; ee. rw ci_range. uf inv_image_by_fun. uf canonical_injection. aw. assert (forall y,inv_image_by_graph (identity_g a) y = intersection2 y a). ir. set_extens. awi H2. nin H2. ee. rwi inc_pair_diagonal H3. ee. wri H4 H2. inter2tac. aw. exists x0. ee. inter2tac. rw inc_pair_diagonal. ee. inter2tac. tv. app iff_eq. ir. nin H3. exists x0. eee;wr (H2 x0). ir. nin H3. ee. exists x0. eee; rw (H2 x0). am. Qed. Lemma compatible_injection_induced_rel: forall r a, induced_rel_axioms r a -> compatible_with_equivs (canonical_injection a (substrate r)) (induced_relation r a) r. Proof. ir. cp H. red in H; ee. app compatible_with_pr2. app induced_rel_equivalence. app ci_function. uf canonical_injection. aw. uf canonical_injection. aw. rww induced_rel_substrate. ir. rwi induced_rel_related H2. ee. rww ci_W. rww ci_W. am. Qed. Lemma foq_induced_rel_injective: forall r a, induced_rel_axioms r a -> injective (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))). Proof. ir. set (f := (canonical_injection a (substrate r))). cp H. cp (induced_rel_equivalence H). red in H; ee. assert(is_function f). uf f. app ci_function. assert (Ha: target f = substrate r). uf f. uf canonical_injection. aw. assert (source f = substrate (induced_relation r a)). uf f. rww induced_rel_substrate. uf canonical_injection. aw. red. ee. app foqcs_function. assert (source (fun_on_quotients (induced_relation r a) r f) = quotient (induced_relation r a) ). uf fun_on_quotients. aw. uf section_canon_proj. aw. rw H5. clear H5. ir. rwii foqcs_W H7. rwii foqcs_W H7. ufi f H7. set (s:= (induced_relation r a)). fold s in H5; fold s in H6. assert (a = substrate s). uf s. rww induced_rel_substrate. assert (inc (rep x) a). rw H8. fprops. assert (inc (rep y) a). rw H8. fprops. rwii ci_W H7. rwii ci_W H7. assert (related s (rep x) (rep y)). uf s. rw induced_rel_related. eee. rw related_rw. ee. app H2. app H2. am. am. am. rwii related_rep_rep H11. Qed. Lemma foq_induced_rel_image: forall r a, induced_rel_axioms r a -> image_by_fun (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))) (quotient (induced_relation r a)) = image_by_fun (canon_proj r) a. Proof. ir. cp H. red in H0; ee. uf image_by_fun. set (ci := canonical_injection a (substrate r)). assert (Hd: is_function ci). uf ci. app ci_function. assert (He:source ci = substrate (induced_relation r a)). rww induced_rel_substrate. uf ci. uf canonical_injection. aw. set (f:= fun_on_quotients (induced_relation r a) r ci). cp (foq_induced_rel_injective H). fold ci in H2. fold f in H2. assert (is_function f). fct_tac. clear H2. assert (Ha: is_equivalence (induced_relation r a)). app induced_rel_equivalence. assert (Hb:is_graph (graph f)). fprops. assert (Hf : target ci = substrate r). uf ci. uf canonical_injection. aw. assert (is_function (canon_proj r)). fprops. set_extens. awi H4. nin H4. ee. rwii inc_quotient H4. rwii induced_rel_class H4. nin H4. ee. cp (W_pr H3 H5). ufi f H8. rwi foqcs_W H8. ufi ci H8. assert(inc (rep x0) (intersection2 x1 a)). wr H7. app nonempty_rep. rw H7. am. nin (intersection2_both H9). clear H9. rwi ci_W H8. aw. nin H6. exists y. ee. inter2tac. assert (x = W y (canon_proj r)). aw. wr H8. assert (inc y x1). inter2tac. assert (related r (rep x0) y). rw in_class_related. exists x1. eee. am. app related_class_eq1. app H1. inter2tac. rw H9. graph_tac. aw. app H1. inter2tac. am. am. am. am. am. am. am. rwii foqcs_W H8. ufi ci H8. rwii ci_W H8. rw inc_quotient. rw induced_rel_class. exists x1. eee. am. am. assert (inc (rep x0) (intersection2 x1 a)). wr H7. app nonempty_rep. rww H7. inter2tac. pose (inc_pr1graph_source H3 H5). ufi f i. ufi fun_on_quotients i. awi i. ufi section_canon_proj i. awi i. am. awi H4. nin H4. ee. red in H5. pose (W_pr H2 H5). awi e. clear H5. aw. assert (Hv: inc x0 x). wr e. bw. cp (H1 _ H4). equiv_tac. set (y:= intersection2 x a). assert (Hw : nonempty y). uf y. exists x0. inter2tac. assert (inc y (quotient (induced_relation r a))). rww inc_quotient. rww induced_rel_class. exists x. ee. wr e. app is_class_class. app H1. am. tv. ex_tac. assert (inc (rep y) (intersection2 x a)). uf y. app nonempty_rep. assert (x = W (intersection2 x a) f). uf f. rww foqcs_W. uf ci. rww ci_W. fold y. wr e. assert (related r x0 (rep y)). rw in_class_related. exists x. ee. wr e. app is_class_class. app H1. am. inter2tac. am. rwi related_rw H7. ee. am. am. fold y. inter2tac. rw H7. fold y. graph_tac. uf f. uf fun_on_quotients. aw. uf section_canon_proj. aw. am. app H1. Qed. Definition canonical_foq_induced_rel r a := restriction2 (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))) (quotient (induced_relation r a)) (image_by_fun (canon_proj r) a). Lemma canonical_foq_induced_rel_bijective: forall r a, induced_rel_axioms r a -> bijective (canonical_foq_induced_rel r a). Proof. ir. assert (Ha: source (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))) = quotient (induced_relation r a)). uf fun_on_quotients. uf section_canon_proj. aw. assert( restriction2_axioms (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))) (quotient (induced_relation r a)) (image_by_fun (canon_proj r) a)). red. simpl. ee. nin (foq_induced_rel_injective H). am. rw Ha. fprops. uf fun_on_quotients. aw. red in H. ee. red. ir. app (sub_im_canon_proj_quotient H H0 H1). rww foq_induced_rel_image. fprops. uf canonical_foq_induced_rel. red. ee. app restriction2_injective. app foq_induced_rel_injective. app restriction2_surjective. uf fun_on_quotients. aw. uf section_canon_proj. aw. wrr foq_induced_rel_image. uf image_of_fun. aw. Qed. (** ** EII-6-7 Quotients of equivalence relations *) (** Definition of a finer equivalence *) Definition finer_equivalence (s r:Set):= forall x y, related s x y -> related r x y. Definition finer_axioms(s r:Set):= is_equivalence s & is_equivalence r & substrate r = substrate s. Lemma finer_sub_equiv: forall s r, finer_axioms s r -> (finer_equivalence s r) = (sub s r). Proof. ir. red in H; ee. app iff_eq. ir. red. ir. assert (is_graph s). fprops. cp (H4 _ H3). wr (pair_recov H5). app H2. red. rww (pair_recov H5). ir. red. ir. red. app H2. Qed. Lemma finer_sub_equiv2: forall s r, finer_axioms s r -> (finer_equivalence s r) = (forall x, exists y, sub(class s x)(class r y)). Proof. ir. red in H; ee. app iff_eq. ir. exists x. red. ir. bw. bwi H3. app H2. am. ir. red. ir. nin (H2 x). assert (inc x (substrate s)). substr_tac. assert(inc x (class s x)). bw. equiv_tac. cp (H4 _ H6). bwi H7. assert (inc y (class s x)). bw. cp (H4 _ H8). bwi H9. equiv_tac. am. am. Qed. Lemma finer_sub_equiv3: forall s r, finer_axioms s r -> (finer_equivalence s r) = (forall y, saturated s (class r y)). Proof. ir. assert (Ha:= H). red in H. ee. app iff_eq. ir. rww saturated_pr. ir. rwii finer_sub_equiv2 H2. nin (H2 y0). assert (class r x = class r y). assert (inc y0 (substrate r)). bwi H3. substr_tac. am. rwi H1 H5. assert (inc y0 (class r x)). app H4. bw. equiv_tac. bwi H6. bwi H3. assert (related r x y). assert (related r y0 y). equiv_tac. equiv_tac. wrr related_class_eq. assert (inc x (substrate r)). substr_tac. equiv_tac. am. am. ue. wr H1. app sub_class_substrate. ir. red. ir. cp (H2 x). rwii saturated_pr H4. assert (inc x (substrate s)). substr_tac. assert (inc x (class r x)). bw. wri H1 H5. equiv_tac. cp (H4 _ H6). assert (inc y (class s x)). bw. cp (H7 _ H8). bwi H9. am. am. wr H1. app sub_class_substrate. Qed. Lemma finest_equivalence: forall r, is_equivalence r -> finer_equivalence (identity_g (substrate r)) r. Proof. ir. red. ir. ufi related H0. awi H0. ee. wr H1. equiv_tac. Qed. Lemma coarsest_equivalence: forall r, is_equivalence r -> finer_equivalence r (coarse (substrate r)). Proof. ir. red. ir. rw coarse_related. rwii related_rw H0. intuition. Qed. Lemma compatible_with_finer: forall s r, finer_axioms s r -> finer_equivalence s r -> compatible_with_equiv (canon_proj r) s. Proof. ir. red in H. ee. red. eee. aw. ir. pose (H0 _ _ H3). rwi related_rw r0. ee. aw. am. Qed. Lemma foq_finer_function: forall s r, finer_axioms s r -> finer_equivalence s r -> is_function(fun_on_quotient s (canon_proj r)). Proof. ir. red in H. ee. app foqc_function. fprops. aw. Qed. Lemma foq_finer_W: forall s r x, finer_axioms s r -> finer_equivalence s r -> inc x (quotient s) -> W x (fun_on_quotient s (canon_proj r)) = class r (rep x). Proof. ir. red in H. ee. rww foqc_W. aw. rw H3. fprops. fprops. aw. Qed. Lemma foq_finer_surjective: forall s r, finer_axioms s r -> finer_equivalence s r -> surjective(fun_on_quotient s (canon_proj r)). Proof. ir. app surjective_pr6. app foq_finer_function. aw. ir. assert (inc (rep y) (substrate r)). red in H. ee. ufi fun_on_quotient H1. awi H1. fprops. assert (source (fun_on_quotient s (canon_proj r)) = (quotient s)). uf fun_on_quotient. aw. uf section_canon_proj. aw. set (x := class s (rep y)). assert (inc x (quotient s)). uf x. red in H. ee. rwi H5 H2. gprops. rw H3. ex_tac. rww foq_finer_W. red in H0. red in H; ee. assert (class r (rep y) = y). app class_rep. ufi fun_on_quotient H1. awi H1. am. wr H7. app related_class_eq1. app H0. rwii inc_quotient H4. rwii is_class_rw H4. ee. wrr H9. uf x. bw. rwi H6 H2. equiv_tac. app nonempty_rep. Qed. (** Quotient of a relation by a finer one *) Definition quotient_of_relations (r s:Set):= equivalence_associated (fun_on_quotient s (canon_proj r)). Lemma quotient_of_relations_equivalence: forall r s, finer_axioms s r -> finer_equivalence s r -> is_equivalence (quotient_of_relations r s). Proof. ir. uf quotient_of_relations. app graph_ea_equivalence. cp (foq_finer_surjective H H0). fct_tac. Qed. Lemma quotient_of_relations_substrate: forall r s, finer_axioms s r -> finer_equivalence s r -> substrate (quotient_of_relations r s) = (quotient s). Proof. ir. uf quotient_of_relations. rww graph_ea_substrate. uf fun_on_quotient. aw. uf section_canon_proj. aw. ap (surj_is_function (foq_finer_surjective H H0)). Qed. Lemma quotient_of_relations_related: forall r s x y, finer_axioms s r -> finer_equivalence s r -> related (quotient_of_relations r s) x y = (inc x (quotient s) & inc y (quotient s) & related r (rep x) (rep y)). Proof. ir. assert (is_function (fun_on_quotient s (canon_proj r))). cp (foq_finer_surjective H H0). fct_tac. uf quotient_of_relations. rww ea_related. simpl. red in H; ee. assert (Ha:is_function (canon_proj r)). fprops. assert (Hc: source (fun_on_quotient s (canon_proj r)) = quotient s). uf fun_on_quotient. uf section_canon_proj. aw. rw Hc. assert(Hb:source (canon_proj r) = substrate s). aw. app iff_eq. ir. eee. assert (inc (rep x) (substrate r)). rw H3. fprops. assert (inc (rep y) (substrate r)). rw H3. fprops. rwii foqc_W H6. rwii foqc_W H6. awii H6. rw related_rw. intuition. am. ir. eee. assert (inc (rep x) (substrate r)). rw H3. fprops. assert (inc (rep y) (substrate r)). rw H3. fprops. rww foqc_W. rww foqc_W. rwi related_rw H6. ee. aw. am. Qed. Lemma quotient_of_relations_related_bis: forall r s x y, finer_axioms s r -> finer_equivalence s r -> inc x (substrate s) -> inc y (substrate s) -> related (quotient_of_relations r s) (class s x) (class s y) = related r x y. Proof. ir. rww quotient_of_relations_related. red in H. ee. assert (related r x (rep (class s x))). app H0. app related_rep_class. assert (related r y (rep (class s y))). app H0. app related_rep_class. app iff_eq. ir. ee. apply transitivity_e with (rep (class s x)). am. am. apply transitivity_e with (rep (class s y)). am. am. equiv_tac. ir. ee. gprops. gprops. apply transitivity_e with x. am. app symmetricity_e. equiv_tac. Qed. Lemma nonempty_image: forall f x, is_function f -> nonempty x -> sub x (source f) -> nonempty (image_by_fun f x). Proof. ir. nin H0. exists (W y f). uf image_by_fun. aw. ex_tac. graph_tac. Qed. Lemma cqr_aux: forall s x y u, is_equivalence s -> sub y (substrate s) -> x = image_by_fun (canon_proj s) y -> inc u x = (exists v, inc v y & u = class s v). Proof. ir. app iff_eq. ir. rwi H1 H2. ufi image_by_fun H2. cp (sub_im_canon_proj_quotient H H0 H2). awi H2. nin H2. ee. rwi related_graph_canon_proj H4. ex_tac. assert (class s (rep u) = u). app class_rep. wr H5. assert (related s (rep u) x0). wrr inc_class. rww H5. rwi related_rw H6. ee. am. am. am. app H0. am. assert (is_function (canon_proj s)). fprops. fprops. ir. nin H2. ee. rw H1. uf image_by_fun. aw. nin H3. nin H3. ex_tac. rw related_graph_canon_proj. rw H6. app inc_itself_class. app H0. am. app H0. rw inc_quotient. rw H6. app is_class_class. app H0. am. Qed. Lemma quotient_of_relations_class_bis: forall r s x, finer_axioms s r -> finer_equivalence s r -> inc x (quotient (quotient_of_relations r s)) = exists y, inc y (quotient r) & x = image_by_fun (canon_proj s) y. Proof. ir. cp (quotient_of_relations_equivalence H H0). assert (Hb:=H). assert (Hc:=H0). red in H; ee; red in H0. rww inc_quotient. assert (Ha:is_function (canon_proj s)). fprops. app iff_eq. ir. cp H4. rwi is_class_rw H4. ee. rwi quotient_of_relations_substrate H6. set(y:= Zo (substrate r) (fun v => exists u, inc u x & inc v u)). assert (nonempty y). nin H4. assert (inc (rep y0) y0). assert (inc y0 (quotient s)). app H6. app (inc_rep_itself H H8). exists (rep y0). uf y. Ztac. assert (inc y0 (quotient s)). app H6. rw H3. fprops. ex_tac. assert(sub y (substrate r)). red. ir. unfold y in H9. Ztac. am. exists y. ee. rww inc_quotient. rww is_class_rw. ee. am. am. ir. ufi y H10. Ztac. clear H10. nin H12. app iff_eq. ir. ufi y H12. Ztac. clear H12. nin H14. ee. pose (H7 x0 x1 H10). rwi quotient_of_relations_related e. rwi e H12. ee. apply transitivity_e with (rep x0). am. app Hc. rw in_class_related. exists x0. ee. rwi inc_quotient H12. am. am. am. app nonempty_rep. app (non_empty_in_quotient H H12). am. apply transitivity_e with (rep x1). am. am. app Hc. rw in_class_related. exists x1. ee. rwi inc_quotient H16. am. am. app nonempty_rep. app (non_empty_in_quotient H H16). am. am. am. am. ir. ee. cp (inc_arg2_substrate H12). wri (quotient_of_relations_related_bis (r:=r) (s:=s)) H12; try am. wri H7 H12. uf y. Ztac. exists (class s z). ee. am. app inc_itself_class. ue. assert (inc x0 (quotient s)). app H6. pose (is_class_pr H H13 H15). wrr e. ue. ue. set(xx := image_by_fun (canon_proj s) y). rwi H3 H9. set_extens. rw (cqr_aux x0 H H9 (refl_equal xx)). assert (inc x0 (quotient s)). app H6. exists (rep x0). ee. uf y. Ztac. rw H3. fprops. ex_tac. app (inc_rep_itself H H11). app is_class_pr. app (inc_rep_itself H H11). rwi (cqr_aux x0 H H9 (refl_equal xx)) H10. nin H10. ee. ufi y H10. Ztac. nin H13. ee. assert (inc x2 (quotient s)). app H6. assert (related s (rep x2) x1). app (related_rep_in_class H H15 H14). rwi related_rw H16. ee. cp (class_rep H H15). rw H11. wr H18. rw H19. am. am. am. am. am. ir. nin H4. ee. rwii inc_quotient H4. rwii is_class_rw H4. ee. assert (Hd:=H6). rwi H3 Hd. nin H4. assert (inc y (substrate s)). wr H3. app H6. rw is_class_rw. ee. rw H5. app nonempty_image. ex_tac. aw. rw quotient_of_relations_substrate. rw H5. red. ir. app (sub_im_canon_proj_quotient H Hd H9). am. am. ir. app iff_eq. ir. rwi (cqr_aux y0 H Hd H5) H9. rwi (cqr_aux z H Hd H5) H10. nin H9; nin H10. ee. rw H12; rw H11. rw quotient_of_relations_related_bis. wr (H7 x1 x2 H9). am. am. am. app Hd. app Hd. ir. rwi (cqr_aux y0 H Hd H5) H9. rw (cqr_aux z H Hd H5). nin H9. ee. rwi quotient_of_relations_related H10. ee. exists (rep z). ee. rw (H7 x1 (rep z) H9). apply transitivity_e with (rep y0). am. app Hc. rw in_class_related. exists y0. ee. rw H11. app is_class_class. app Hd. rw H11. app inc_itself_class. app Hd. app nonempty_rep. app (non_empty_in_quotient H H10). am. am. sy. app class_rep. am. am. am. Qed. Lemma quotient_canonical_decomposition: forall r s, let f := fun_on_quotient s (canon_proj r) in let qr := quotient_of_relations r s in finer_axioms s r -> finer_equivalence s r -> f = (compose (fun_on_quotient qr f) (canon_proj qr)). Proof. ir. assert (surjective f). uf f. app foq_finer_surjective. app (canonical_decomposition_surj2 H1). Qed. Lemma quotient_of_relations_pr: forall s t, let r := inv_image_relation (canon_proj s) t in is_equivalence s -> is_equivalence t -> substrate t = quotient s -> t = quotient_of_relations r s. Proof. ir. assert (iirel_axioms (canon_proj s) t). red. ee. fprops. am. sy. aw. assert (is_equivalence r). uf r. app iirel_relation. assert (finer_axioms s r). red. eee. uf r. rww iirel_substrate. aw. assert (finer_equivalence s r). red. ir. uf r. rw iirel_related. ir. assert (inc x (substrate s)). substr_tac. assert (inc y (substrate s)). substr_tac. aw. ee. am. am. assert (class s x =class s y). wr related_class_eq. am. am. equiv_tac. rw H8. app reflexivity_e. rw H1. gprops. am. assert (is_equivalence (quotient_of_relations r s)). app quotient_of_relations_equivalence. rw graph_exten. ir. rww quotient_of_relations_related. app iff_eq. ir. assert (inc u (quotient s)). wr H1. substr_tac. assert (inc v (quotient s)). wr H1. substr_tac. assert(inc (rep u) (substrate s)). fprops. assert(inc (rep v) (substrate s)). fprops. eee. uf r. rw iirel_related. aw. eee. aw. rw class_rep. rw class_rep. tv. am. am. am. am. am. ir. ee. ufi r H9. rwi iirel_related H9. ee. awi H11. rwi class_rep H11. rwi class_rep H11. am. am. am. am. am. am. awi H10. am. am. awi H9. am. am. fprops. fprops. Qed. (** ** EII-6-8 Product of two equivalence relations *) Definition substrate_for_prod(r r':Set) := product(substrate r)(substrate r'). Definition prod_of_relation(r r':Set):= Zo(product(substrate_for_prod r r')(substrate_for_prod r r')) (fun y=> inc (J(P (P y))(P (Q y))) r & inc (J(Q (P y))(Q (Q y))) r'). Lemma prod_of_rel_is_rel: forall r r', is_graph (prod_of_relation r r'). Proof. ir. red. ir. ufi prod_of_relation H. Ztac. ee. pose (product_pr H0). ee. am. Qed. Lemma substrate_prod_of_rel1: forall r r', sub (substrate (prod_of_relation r r'))(substrate_for_prod r r'). Proof. ir. red. ir. assert(is_graph (prod_of_relation r r')). app prod_of_rel_is_rel. pose (inc_substrate_rw x H0). rwi e H. induction H. nin H. ufi prod_of_relation H. Ztac. pose (product_pair_pr H1). ee. am. nin H. ufi prod_of_relation H. Ztac. pose (product_pair_pr H1). ee. am. Qed. Lemma prod_of_rel_pr: forall r r' a b, related (prod_of_relation r r') a b = ( is_pair a & is_pair b & related r (P a) (P b) & related r' (Q a) (Q b)). Proof. ir. app iff_eq. ir. red in H. ufi prod_of_relation H. Ztac. awi H1. awi H0. ufi substrate_for_prod H0. ee. awi H3; ee;am. awi H4; eee. am. am. ir. red. ee. uf prod_of_relation. Ztac. uf substrate_for_prod. aw. ee. fprops. am. substr_tac. substr_tac. am. substr_tac. substr_tac. aw. eee. Qed. Lemma substrate_prod_of_rel2: forall r r', is_symmetric r -> is_symmetric r' -> substrate (prod_of_relation r r') = substrate_for_prod r r'. Proof. ir. app extensionality. app substrate_prod_of_rel1. red. ir. ufi substrate_for_prod H1. awi H1. ee. red in H; red in H0. ee. set (r'':=prod_of_relation r r'). nin H1. nin H1. rwi H1 H2. awi H2. rwi H1 H3. awi H3. assert (exists u, inc (J x0 u) r). rwi (inc_substrate_rw x0 H) H2. nin H2; nin H2; exists x2; [am | app H5]. nin H6. assert (exists u, inc (J x1 u) r'). rwi (inc_substrate_rw x1 H0) H3. nin H3; nin H3; exists x3; [am | app H4]. nin H7. assert (related r'' x (J x2 x3)). uf r''. rw prod_of_rel_pr. rw H1. aw. eee. substr_tac. Qed. Lemma prod_of_rel_refl: forall r r', is_reflexive r -> is_reflexive r' -> is_reflexive (prod_of_relation r r'). Proof. ir. red. ee. app prod_of_rel_is_rel. ir. assert (inc y (substrate_for_prod r r')). app substrate_prod_of_rel1. ufi substrate_for_prod H2. pose (product_pr H2). red in H ; red in H0; ee. pose (H7 _ H4). pose (H6 _ H5). rw prod_of_rel_pr. eee. Qed. Lemma prod_of_rel_sym: forall r r', is_symmetric r -> is_symmetric r' -> is_symmetric (prod_of_relation r r'). Proof. ir. red. ee. app prod_of_rel_is_rel. ir. rwi prod_of_rel_pr H1. ee. red in H ; red in H0; ee. pose (H5 _ _ H4). pose (H6 _ _ H3). rw prod_of_rel_pr. eee. Qed. Lemma prod_of_rel_trans: forall r r', is_transitive r -> is_transitive r' -> is_transitive (prod_of_relation r r'). Proof. ir. red. ee. app prod_of_rel_is_rel. ir. rwi prod_of_rel_pr H1. rwi prod_of_rel_pr H2. ee. red in H ; red in H0; ee. pose (H10 _ _ _ H7 H4). pose (H9 _ _ _ H8 H5). rw prod_of_rel_pr. eee. Qed. Lemma substrate_prod_of_rel: forall r r', is_equivalence r ->is_equivalence r' -> substrate (prod_of_relation r r') = product(substrate r)(substrate r'). Proof. ir. red in H; red in H0; ee. app (substrate_prod_of_rel2 H4 H2). Qed. Lemma equivalence_prod_of_rel: forall r r', is_equivalence r -> is_equivalence r' -> is_equivalence (prod_of_relation r r'). Proof. uf is_equivalence. ir. ee. app prod_of_rel_refl. app prod_of_rel_trans. app prod_of_rel_sym. Qed. Lemma related_prod_of_rel1: forall r r' x x' v, is_equivalence r -> is_equivalence r' -> inc x (substrate r) -> inc x' (substrate r') -> related (prod_of_relation r r') (J x x') v = (exists y, exists y', v = J y y' & related r x y & related r' x' y'). Proof. ir. rw prod_of_rel_pr. app iff_eq. ir. ee. exists (P v). exists (Q v). ee. aw. awi H5. am. awi H6. am. ir. nin H3. nin H3. nin H3. rw H3. aw. fprops. Qed. Lemma related_prod_of_rel2: forall r r' x x' v, is_equivalence r -> is_equivalence r' -> inc x (substrate r) -> inc x' (substrate r') -> related (prod_of_relation r r') (J x x') v = inc v (product (im_singleton r x) (im_singleton r' x')). Proof. ir. rww related_prod_of_rel1. aw. app iff_eq. ir. nin H3; nin H3; ee. rw H3. fprops. rw H3. aw. rw H3. aw. ir. ee. exists (P v). exists (Q v). aw. au. Qed. Lemma class_prod_of_rel2: forall r r' x, is_equivalence r -> is_equivalence r' -> is_class (prod_of_relation r r') x = exists u, exists v, is_class r u & is_class r' v & x = product u v. Proof. ir. assert (Ha:=equivalence_prod_of_rel H H0). app iff_eq. ir. rwii is_class_rw H1. ee. nin H1. rwii substrate_prod_of_rel H2. assert (inc y (product (substrate r) (substrate r'))). app H2. awi H4. ee. exists (class r (P y)). exists (class r' (Q y)). ee. app is_class_class. app is_class_class. set_extens. rwi (H3 y x0 H1) H7. rwi prod_of_rel_pr H7. ee. aw. ee. am. bw. bw. awi H7. ee. rw (H3 y x0 H1). rw prod_of_rel_pr. eee. wr inc_class. am. am. wrr inc_class. ir. nin H1. nin H1. ee. rwii is_class_rw H1. rwii is_class_rw H2. ee. nin H1; nin H2. rw is_class_rw. ee. exists (J y y0). rw H3. aw. aw. ee. fprops. am. am. rw substrate_prod_of_rel. rw H3. app product_monotone. am. am. ir. rwi H3 H8. awi H8. ee. rw prod_of_rel_pr. rw H3. aw. app iff_eq. ir. eee. wr H7. am. am. wr H5. am. am. ir. ee. am. wri H7 H13. am. am. wri H5 H14. am. am. am. Qed. Lemma ext_to_prod_rel_function: forall r r', is_equivalence r -> is_equivalence r' -> is_function (ext_to_prod(canon_proj r)(canon_proj r')). Proof. ir. app ext_to_prod_function. fprops. fprops. Qed. Lemma ext_to_prod_rel_W: forall r r' x x', is_equivalence r -> is_equivalence r' -> inc x (substrate r) -> inc x' (substrate r') -> W (J x x') (ext_to_prod(canon_proj r)(canon_proj r')) = J (class r x) (class r' x'). Proof. ir. rw ext_to_prod_W. aw. fprops. fprops. aw. aw. Qed. Lemma compatible_ext_to_prod: forall r r', is_equivalence r -> is_equivalence r' -> compatible_with_equiv (ext_to_prod (canon_proj r) (canon_proj r')) (prod_of_relation r r'). Proof. ir. red. assert (is_function (canon_proj r)). fprops. assert (is_function (canon_proj r')). fprops. ee. app ext_to_prod_function. rww substrate_prod_of_rel. uf ext_to_prod. aw. ir. rwi prod_of_rel_pr H3. ee. rwii related_rw H5. ee. rwii related_rw H6. ee. assert (J (P x)(Q x) = x). aw. assert (J (P x')(Q x') = x'). aw. wr H11. wr H12. rww ext_to_prod_W. rww ext_to_prod_W. aw. rw H8; rw H10; tv. aw. aw. aw. aw. Qed. Lemma compatible_ext_to_prod_inv: forall r r' x x', is_equivalence r -> is_equivalence r' -> is_pair x -> inc (P x) (substrate r) -> inc (Q x) (substrate r') -> is_pair x' -> inc (P x') (substrate r) -> inc (Q x') (substrate r') -> W x (ext_to_prod (canon_proj r) (canon_proj r')) = W x' (ext_to_prod (canon_proj r) (canon_proj r')) -> related (prod_of_relation r r') x x'. Proof. ir. assert (J (P x) (Q x) = x). aw. assert (J (P x') (Q x') = x'). aw. wri H8 H7; wri H9 H7. rwii ext_to_prod_rel_W H7. rwii ext_to_prod_rel_W H7. rw prod_of_rel_pr. eee. pose (pr1_def H7). rw related_rw. intuition. am. pose (pr2_def H7). rw related_rw. intuition. am. Qed. Lemma related_ext_to_prod_rel: forall r r', is_equivalence r -> is_equivalence r' -> equivalence_associated (ext_to_prod(canon_proj r)(canon_proj r')) = prod_of_relation r r'. Proof. ir. cp (compatible_ext_to_prod H H0). red in H1. ee. rw graph_exten. ir. rw ea_related. simpl. app iff_eq. ir. ee. ufi ext_to_prod H4. awi H4. ufi ext_to_prod H5. awi H5. assert(Ha:is_function (canon_proj r)). fprops. assert(Hb:is_function (canon_proj r')). fprops. ee. assert (J (P u)(Q u) = u). aw. assert (J (P v)(Q v) = v). aw. wri H11 H6. wri H12 H6. rwii ext_to_prod_W H6. rwii ext_to_prod_W H6. awi H6; try am. assert (class r (P u) = class r (P v)). assert (P (J (class r (P u)) (class r' (Q u))) = P (J (class r (P v)) (class r' (Q v)))). rw H6. tv. awi H13. am. assert (class r' (Q u) = class r' (Q v)). assert (Q (J (class r (P u)) (class r' (Q u))) = Q (J (class r (P v)) (class r' (Q v)))). rw H6. tv. awi H14. am. rw prod_of_rel_pr. rw related_rw. rw related_rw. eee. am. am. fprops. fprops. aw. aw. aw. aw. ir. cp H4. rwi prod_of_rel_pr H4. rwi related_rw H4. rwi related_rw H4. ee. aw. au. aw. uf ext_to_prod. aw. au. uf ext_to_prod. aw. au. app H3. am. am. am. assert (is_equivalence (equivalence_associated (ext_to_prod (canon_proj r) (canon_proj r')))). ap graph_ea_equivalence. ap ext_to_prod_function. fprops. fprops. fprops. assert(is_equivalence (prod_of_relation r r')). app equivalence_prod_of_rel. fprops. Qed. Lemma decomposable_ext_to_prod_rel:forall r r', is_equivalence r -> is_equivalence r' -> exists h, bijective h & source h = quotient (prod_of_relation r r') & target h = product (quotient r) (quotient r')& compose h (canon_proj (prod_of_relation r r')) = ext_to_prod(canon_proj r)(canon_proj r'). Proof. ir. set (r'':=prod_of_relation r r'). set (f'':=ext_to_prod (canon_proj r) (canon_proj r')). pose (h:=fun_on_quotient r'' f''). assert (is_equivalence r''). uf r''. app equivalence_prod_of_rel. assert(compatible_with_equiv f'' r''). uf f''; uf r''. app compatible_ext_to_prod. cp (compose_foq_proj H1 H2). fold h in H3. assert (source h = quotient r''). uf h. uf fun_on_quotient. uf section_canon_proj. aw. assert (target h = product (quotient r) (quotient r')). uf h. uf fun_on_quotient. uf f''. aw. uf ext_to_prod. aw. exists h. eee. assert (is_function h). uf h. app foqc_function. uf f''. app ext_to_prod_function. fprops. fprops. uf f''. simpl. aw. uf r''. rw substrate_prod_of_rel. uf ext_to_prod. aw. am. am. red. ee. red. ee. am. rw H4. uf h. ir. rwi foqc_W H9. rwi foqc_W H9. ufi f'' H9. cp (inc_rep_substrate H1 H7). unfold r'' in H10. rwi substrate_prod_of_rel H10. awi H10. ee. cp (inc_rep_substrate H1 H8). unfold r'' in H13. rwi substrate_prod_of_rel H13. awi H13. ee. cp (compatible_ext_to_prod_inv H H0 H10 H11 H12 H13 H14 H15 H9). fold r'' in H16. rwi related_rep_rep H16. am. am. am. am. am. am. am. am. am. uf f''. app ext_to_prod_rel_function. red in H2; eee. am. am. uf f''. app ext_to_prod_rel_function. red in H2; eee. am. app surjective_pr6. ir. rwi H5 H7. awi H7. ee. assert (inc (J (rep (P y)) (rep (Q y))) (substrate r'')). uf r''. rw substrate_prod_of_rel. aw. aw. ee. app pair_is_pair. fprops. fprops. am. am. set (x:= class r'' (J (rep (P y)) (rep (Q y)))). assert (inc x (quotient r'')). uf x. fprops. gprops. assert (inc (rep x) (substrate r'')). fprops. cp (related_rep_class H1 H10). fold x in H13. ufi r'' H13. rwi related_prod_of_rel1 H13. nin H13. nin H13. ee. exists x. ee. rww H4. uf h. rw foqc_W. ufi r'' H12. rwi substrate_prod_of_rel H12. awi H12. ee. assert (J (P (rep x)) (Q (rep x)) = (rep x)). aw. wr H18. uf f''. rww ext_to_prod_rel_W. assert (J (P y) (Q y) = y). aw. wr H19. assert (P y = class r (P (rep x))). app is_class_pr. rw H13. aw. rwi inc_quotient H8. rwi is_class_rw H8. ee. assert (inc (rep (P y)) (P y)). app nonempty_rep. rw (H21 (rep (P y)) x0 H22). am. am. am. wr H20. ap uneq. sy. app is_class_pr. rw H13. aw. rwi inc_quotient H9. rwi is_class_rw H9. ee. assert (inc (rep (Q y)) (Q y)). app nonempty_rep. rw (H22 (rep (Q y)) x1 H23). am. am. am. am. am. am. uf f''. app ext_to_prod_rel_function. red in H2; eee. am. am. am. fprops. fprops. Qed. End Relation. Export Relation.