- Fundamental set theory
- Theory of Sets EII-3 Correspondences
- EII-3-1 Graphs et correspondences
- Additional lemmas
- EII-3-2 Inverse of a correspondence
- EII-3-3 Composition of two correspondences
- EII-3-4 Functions
- EII-3-5 Restrictions and extensions of functions
- EII-3-6 Definition of a function by means of a term
- EII-3-7 Composition of two functions. Inverse function
- EII-3-8 Retractions and sections
- EII-3-9 Functions of two arguments
- Theory of Sets: EII-4 Union and intersection of a family of sets
- EII-4-1 Definition of the union and intersection of a family of sets
- EII-4-2 Properties of union and intersection
- EII-4-3 Images of a union and an intersection
- EII-4-4 complement of unions and intersections
- EII-4-5 union and intersection of two sets
- EII-4-6 Coverings
- EII-4-7 Partitions
- EII-4-8 Sum of a family of sets
- EII-5 Product of a family of sets
Library set4
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.
Set Implicit Arguments.
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.
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.
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.
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.
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.
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.
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.
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.
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.