Library sset3
Theory of Sets: EII-4 Union and intersection of a family of sets
Copyright INRIA (2009-2013) (Apics) Marelle Team (Jose Grimm).Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset2.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module Bunion.
EII-4-1 Definition of the union and intersection of a family of sets
Definition intersectiont (I:Set) (f : I->Set):=
Zo (uniont f) (fun y => forall z : I, inc y (f z)).
Definition unionf (x:Set)(f: fterm) := uniont (fun a:x => f (Ro a)).
Definition unionb g := unionf (domain g)(Vg g).
Definition intersectionf (x:Set)(f: fterm) :=
intersectiont (fun a:x => f (Ro a)).
Definition intersectionb g := intersectionf (domain g) (Vg g).
Basic properties of union
Lemma setUf_P x i f:
inc x (unionf i f) <-> exists2 y, inc y i & inc x (f y).
Proof.
split;first by move/setUt_P=> [z zp]; exists (Ro z) =>//; apply: R_inc.
by move=>[y yi xf]; apply/setUt_P; exists (Bo yi); rewrite B_eq.
Qed.
Lemma setUb_P x f:
inc x (unionb f) <-> exists2 y, inc y (domain f) & inc x (Vg f y).
Proof. exact: setUf_P. Qed.
Lemma setUb_P1 x a f:
inc x (unionb (Lg a f)) <-> exists2 y, inc y a & inc x (f y).
Proof.
split.
move /setUb_P; bw; move => [y ya]; bw => yf; ex_tac.
move => [y ya xf]; apply /setUb_P; bw;ex_tac; bw.
Qed.
Lemma setUt_i (I:Set) (f : I->Set) y x:
inc x (f y) -> inc x (uniont f).
Proof. by move=> h;apply/setUt_P; exists y. Qed.
Lemma setUf_i x y i f:
inc y i -> inc x (f y) -> inc x (unionf i f).
Proof. by move=> yi xf;apply/setUf_P; exists y. Qed.
Lemma setUb_i x y f:
inc y (domain f) -> inc x (Vg f y) -> inc x (unionb f).
Proof. by move=> yd xv; apply/setUb_P; ex_tac. Qed.
Lemma setUf_hi x i f:
inc x (unionf i f) -> exists2 y, inc y i & inc x (f y).
Proof. by move/setUf_P. Qed.
Lemma setUb_hi x f:
inc x (unionb f) -> exists2 y, inc y (domain f) & inc x (Vg f y).
Proof. by move/setUb_P. Qed.
Ltac union_tac:=
match goal with
| H:inc ?x (?f ?y) |- inc ?x (uniont ?f)
=> apply: (setUt_i H)
| Ha : inc ?i (domain ?g), Hb : inc ?x (Vg ?g ?i) |- inc ?x (unionb ?g)
=> apply: (setUb_i Ha Hb)
| Ha : inc ?x ?y, Hb : inc ?y ?a |- inc ?x (union ?a)
=> apply: (setU_i Ha Hb)
| Ha : inc ?y ?i, Hb : inc ?x (?f ?y) |- inc ?x (unionf ?i ?f)
=> apply: (setUf_i _ Ha Hb)
| Ha : inc ?y ?i |- inc ?x (unionf ?i ?f)
=> apply: (setUf_i Ha); fprops
| Hb : inc ?x (?f ?y) |- inc ?x (unionf ?i ?f)
=> apply: (setUf_i _ Hb); fprops
| Ha : inc ?i (domain ?g) |- inc ?x (unionb ?g)
=> apply: (setUb_i Ha); fprops
| Hb : inc ?x (Vg ?g ?i) |- inc ?x (unionb ?g)
=> apply: (setUb_i _ Hb); fprops
| Hb : inc ?z ?X |- inc ?x (union ?X)
=> apply: (setU_i _ Hb); fprops
| Ha : inc ?x ?z |- inc ?x (union ?X)
=> apply: (setU_i Ha); fprops
end.
If the index set is empty so are the union and intersection
Lemma setUt_0 (I:Set) (f:I-> Set): I = emptyset -> uniont f = emptyset.
Proof.
move => ie; apply /set0_P => t /setUt_P [x].
move: (R_inc x); rewrite {2} ie; case; case.
Qed.
Lemma setUf_0 f: unionf emptyset f = emptyset.
Proof. by apply: setUt_0. Qed.
Lemma setUb_0: unionb emptyset = emptyset.
Proof. rewrite /unionb domain_set0; apply/setUf_0. Qed.
Lemma setIt_0 (I:Set) (f:I-> Set):
I = emptyset -> intersectiont f = emptyset.
Proof.
move=> Ie; apply /set0_P => t /Zo_P; rewrite (setUt_0 _ Ie);case; case; case.
Qed.
Lemma setIf_0 f: intersectionf emptyset f = emptyset.
Proof. by apply: setIt_0. Qed.
Lemma setIb_0: intersectionb emptyset = emptyset.
Proof. rewrite /intersectionb domain_set0; apply/setIf_0. Qed.
Basic properties of the intersection in the non-trivial case
Lemma setIt_P (I:Set) (f:I-> Set): nonempty I -> forall x,
(inc x (intersectiont f) <-> (forall j, inc x (f j))).
Proof.
move=> [i [ix _]];split; first by move /Zo_hi.
move => h1; apply: Zo_i => //; move: (h1 ix); apply: setUt_i.
Qed.
Lemma setIf_P I f: nonempty I -> forall x,
(inc x (intersectionf I f) <-> (forall j, inc j I -> inc x (f j))).
Proof.
move => h x; split; first by move/(setIt_P _ h) => aux j [ji <-]; apply: aux.
move => aux; apply/(setIt_P _ h) => j; apply: aux; apply: R_inc.
Qed.
Lemma setIb_P g: nonempty g -> forall x,
(inc x (intersectionb g) <-> (forall i, inc i (domain g) -> inc x (Vg g i))).
Proof. move/domain_set0P => h x; exact: (setIf_P _ h). Qed.
Lemma setI_P y: nonempty y -> forall x,
(inc x (intersection y) <-> (forall i, inc i y -> inc x i)).
Proof.
by move=> ney; split; [ move=> xi iy; apply: setI_hi | apply: setI_i].
Qed.
Lemma setIt_i (I:Set) (f:I-> Set) x: nonempty I ->
(forall j, inc x (f j)) -> inc x (intersectiont f).
Proof. by move=> pa pb; apply/setIt_P. Qed.
Lemma setIt_hi (I:Set) (f:I-> Set) x j:
inc x (intersectiont f) -> inc x (f j).
Proof. move /(setIt_P _ (nonempty_intro (R_inc j))); apply. Qed.
Lemma setIf_i I f x: nonempty I ->
(forall j, inc j I -> inc x (f j)) -> inc x (intersectionf I f).
Proof. by move=> pa pb; apply/setIf_P. Qed.
Lemma setIf_hi I f x j:
inc x (intersectionf I f) -> inc j I -> inc x (f j).
Proof. move => pa pb; move /(setIf_P): pa; apply => //; ex_tac. Qed.
Lemma setIb_i g x: nonempty g ->
(forall i, inc i (domain g) -> inc x (Vg g i)) -> inc x (intersectionb g).
Proof. by move=> neg h; apply/setIb_P. Qed.
Lemma setIb_hi g x i:
inc x (intersectionb g) -> inc i (domain g) -> inc x (Vg g i).
Proof.
by move => /setIb_P pa pb; apply: pa => //; apply /domain_set0P; ex_tac.
Qed.
Lemma setUt_exten (I:Set) (f: I-> Set) (f':I->Set):
f =1 f' -> uniont f = uniont f'.
Proof.
move=> hyp; set_extens t; move/setUt_P=> [z zi]; apply/setUt_P; exists z.
by rewrite -hyp.
by rewrite hyp.
Qed.
Lemma setUf_exten sf f f':
{inc sf, f =1 f'} -> unionf sf f = unionf sf f'.
Proof.
move=> hyp; set_extens t;move/setUf_P=> [z zi tf]; apply/setUf_P; ex_tac.
by rewrite -hyp.
by rewrite hyp.
Qed.
Lemma setIt_exten (I:Set) (f f':I-> Set):
f =1 f' -> (intersectiont f) = (intersectiont f').
Proof.
move=> hyp; case: (emptyset_dichot I) => ie.
by rewrite !(setIt_0 _ ie).
set_extens t; move/(setIt_P _ ie) => h; apply/(setIt_P _ ie) => j.
rewrite - hyp; apply: h.
rewrite hyp; apply: h.
Qed.
Lemma setIf_exten I f f': {inc I, f =1 f'} ->
intersectionf I f = intersectionf I f'.
Proof.
move=> h; apply: setIt_exten => a;apply: h; apply: R_inc.
Qed.
Lemma setUt_s1 (I:Set) (f: I-> Set) i: sub (f i) (uniont f).
Proof. move=> t tf; union_tac. Qed.
Lemma setIt_s1 (I:Set) (f: I-> Set) i: sub (intersectiont f) (f i).
Proof. move=> t; apply: setIt_hi. Qed.
Lemma setUt_s2 (I:Set) (f: I-> Set) x:
(forall i, sub (f i) x) -> sub (uniont f) x.
Proof. by move=> hyp t; move/setUt_P=> [z tfz]; apply: (hyp z). Qed.
Lemma setIt_s2 (I:Set) (f: I-> Set) x:
nonempty I ->
(forall i, sub x (f i)) -> sub x (intersectiont f).
Proof. by move=> ne hyp t tx; apply/setIt_P => // j; apply: hyp. Qed.
Lemma setIt_sub2 (I:Set) (f: I-> Set) x:
(forall i, sub (f i) x) -> sub (intersectiont f) x.
Proof.
move=> hyp t ti.
case: (emptyset_dichot I) => ie.
by move: ti; rewrite setIt_0 // => /in_set0.
case: ie => y; case => z _; apply: (hyp z); move: ti;apply:setIt_s1.
Qed.
Lemma setUt_sub2 (I:Set) (f: I-> Set) x:
nonempty I -> (forall i, sub x (f i)) -> sub x (uniont f).
Proof. by move=> [y yI] hyp t tx; apply/setUt_P; exists (Bo yI);apply: hyp. Qed.
Proposition 1 : union (compose g f) = union g
Theorem setUt_rewrite (I K:Set) (f: K->I) (g:I ->Set):
surjectiveC f ->
uniont g = uniont (g \o f).
Proof.
move=> sf; set_extens t; move/setUt_P=> [z zp]; apply/setUt_P.
by move: (sf z) => [v fv] /=; exists v; ue.
by exists (f z).
Qed.
Theorem setIt_rewrite (I K:Set) (f: K->I) (g:I ->Set):
surjectiveC f ->
intersectiont g = intersectiont (g \o f).
Proof.
move=> sf; case: (emptyset_dichot I) => ei.
rewrite ! setIt_0 =>//; apply /set0_P => y [x _].
move: (f x); rewrite ei; case.
have nek: nonempty K.
move: ei => [k [i]] _; move: (sf i)=> [j _]; exists (Ro j); apply: R_inc.
set_extens t; move/setIt_P=> h; apply/setIt_P => // j; first by apply: (h ei).
move: (sf j) => [k <-]; exact: (h nek k).
Qed.
Lemma setUb_rewrite f g:
fgraph f -> range f = domain g ->
unionb g = unionb (g \cf f).
Proof.
rewrite /composef=> fgf rfsg.
set_extens t; move/setUb_P => [a pa pb]; apply/setUb_P.
move: pa; rewrite- rfsg; move /(range_gP fgf) => [x xd etc].
bw; ex_tac; bw; ue.
move: pa; bw => pa; move: pb; bw; rewrite- rfsg => ta; exists (Vg f a); fprops.
Qed.
Lemma setUb_rewrite1 f g:
function f -> fgraph g -> range (graph f) = domain g ->
unionb g = unionb (g \cf (graph f)).
Proof.
move=> [_ fgf _] fgg rfg.
have fc: g \cfP (graph f) by split => //; ue.
by apply: setUb_rewrite.
Qed.
Lemma setIb_rewrite f g:
fgraph f -> range f = domain g ->
intersectionb g = intersectionb (g \cf f).
Proof.
move=> fgf rfdg.
case: (emptyset_dichot g) => gp.
have -> //: (g \cf f = g).
rewrite gp; apply /set0_P => t /funI_P [z zd _].
have :(inc (Vg f z) (range f)) by fprops.
rewrite rfdg gp domain_set0; apply: in_set0.
have nec: (nonempty (g \cf f)).
move: gp => [x xg].
have : (inc (P x) (range f)) by rewrite rfdg; fprops.
move/(range_gP fgf) => [y ydf etc].
exists (J y (Vg g (Vg f y))); apply/funI_P; ex_tac.
set_extens t.
move/(setIb_P gp) => h; apply/(setIb_P nec); rewrite /composef; bw => j jdf.
bw; apply: h; rewrite - rfdg; apply range_gP => //; ex_tac.
move/(setIb_P nec) => h; apply/(setIb_P gp) => i; rewrite -rfdg.
move/(range_gP fgf) => [x xdf ->]; move: (h x);rewrite /composef; bw.
by apply.
Qed.
Union and intersection of a function with singleton range
Lemma setUt_constant (I:Set) (f:I ->Set) (x:I):
constantp f -> uniont f = f x.
Proof.
move=> cf.
by set_extens t; [move/setUt_P => [z]; rewrite (cf x z) | move=> tp;union_tac].
Qed.
Lemma setIt_constant (I:Set) (f:I ->Set) (x:I):
constantp f -> intersectiont f = f x.
Proof.
have neI: nonempty I by exists (Ro x); apply: R_inc.
move => cf;apply: extensionality; first by apply:setIt_s1.
by move => h j;apply: setIt_i => // k; rewrite (cf k x).
Qed.
Lemma setUt_1 (a:Set) (x:a) (f: singleton (Ro x) -> Set):
uniont f = f (Bo (set1_1 (Ro x))).
Proof.
set_extens t => pt; last by union_tac.
move /setUt_P: pt => [y tfy].
have <- //: (y = (Bo (set1_1 (Ro x)))).
by apply: R_inj; move: (R_inc y) => /set1_P ->; rewrite B_eq.
Qed.
Lemma setIt_1 (a:Set)(x:a) (f: singleton (Ro x) -> Set):
intersectiont f = f (Bo (set1_1 (Ro x))).
Proof.
apply: extensionality; first by apply:setIt_s1.
move => t ti; apply: setIt_i;[by fprops | move=> j].
have -> //: (j = (Bo (set1_1 (Ro x)))).
by apply: R_inj; move: (R_inc j) => /set1_P ->; rewrite B_eq.
Qed.
Lemma setUf_1 f x: unionf (singleton x) f = f x.
Proof.
by set_extens t => tp; [ move: (setUf_hi tp)=> [y /set1_P ->] | union_tac ].
Qed.
Lemma setIf_1 f x: intersectionf (singleton x) f = f x.
Proof.
set_extens t => tx; first by exact :(setIf_hi tx (set1_1 x)).
apply: setIf_i; [ fprops | by move=> j; move/set1_P => ->].
Qed.
Lemma setUg_constant f x: constantgp f -> inc x (domain f) ->
unionb f = Vg f x.
Proof.
move => p1 p2; set_extens t; last by move => p3; union_tac.
by move /setUb_P => [y y1 y2]; rewrite (proj2 p1 _ _ p2 y1).
Qed.
Lemma setIg_constant f x: constantgp f -> inc x (domain f) ->
intersectionb f = Vg f x.
Proof.
move => p1 p2.
have nef: nonempty f by apply /domain_set0P; ex_tac.
set_extens t; first by move /(setIb_P nef); apply.
by move => h; apply /(setIb_P nef) => i idf;rewrite (proj2 p1 _ _ idf p2).
Qed.
Link between union and unionb
Lemma setU_prop x: union x = unionf x id.
Proof. by apply: setUt_exten => t. Qed.
Lemma setI_prop x: intersection x = intersectionf x id.
Proof.
case: (emptyset_dichot x) => xe; first by rewrite xe setI_0 setIf_0.
set_extens t; first by move/(setI_P xe) =>h; apply:setIf_i.
by move/(setIf_P _ xe) =>h;apply:setI_i.
Qed.
Lemma setUb_alt f: fgraph f -> unionb f = union (range f).
Proof.
move=> fgf.
set_extens t; first by move/setUb_P=> [y ty yx]; union_tac.
move/setU_P => [z te]; move/(range_gP fgf) => [x xd eq]; union_tac; ue.
Qed.
Lemma setUb_identity x: unionb (identity_g x) = union x.
Proof.
rewrite /unionb identity_d setU_prop.
by apply: setUf_exten; move=> i ix /=; rewrite identity_ev.
Qed.
Lemma setIb_alt f: fgraph f -> intersectionb f = intersection (range f).
Proof.
move => fgf; case: (emptyset_dichot f) => fe.
by rewrite fe range_set0 setI_0 setIb_0.
set_extens t.
move => ti; apply:setI_i.
move: fe => [w tf]; exists (Q w); apply/funI_P; ex_tac.
move=> y /(range_gP fgf) [x xdf ->]; exact: (setIb_hi ti xdf).
move => ti; apply:setIb_i => // i idf; apply: (setI_hi ti).
apply /(range_gP fgf); ex_tac.
Qed.
Lemma setIb_identity x: intersectionb (identity_g x) = intersection x.
Proof.
rewrite /intersectionb identity_d setI_prop.
by apply: setIf_exten; move=> i ix /=; rewrite identity_ev.
Qed.
Lemma setUt_S (I:Set) (f g:I->Set):
(forall i, sub (f i) (g i)) -> sub (uniont f) (uniont g).
Proof.
by move=> su t /setUt_P [z tf]; apply/setUt_P; exists z; apply: su.
Qed.
Lemma setIt_S (I:Set) (f g:I->Set):
(forall i, sub (f i) (g i)) -> sub (intersectiont f) (intersectiont g).
Proof.
move=> su.
case: (emptyset_dichot I) => i2; first by rewrite !setIt_0.
move=> t/(setIt_P _ i2) hyp; apply/setIt_P => //j; apply: su;apply: hyp.
Qed.
Lemma setUf_S2 f: {compat (unionf ^~ f) : x y / sub x y }.
Proof. move => x y /= sab t /setUf_P [z yA tfy]; union_tac. Qed.
Lemma setIf_S f:
{compat (intersectionf ^~ f) : x y / sub x y /\ nonempty x >-> sub y x}.
Proof.
move=> A B [sAB neA].
have neB: (nonempty B) by move:neA=> [x]; exists x; apply: sAB.
by move=> x /(setIf_P _ neB) p; apply:(setIf_i neA) =>j jA; apply:p; apply: sAB.
Qed.
Associativity of union and intersection
Theorem setUf_A sg f g:
unionf (unionf sg g) f = unionf sg (fun l => unionf (g l) f).
Proof.
set_extens t; move /setUf_P=> [y yu tfy]; [ move: yu | move: tfy];
move/setUf_P => [z zsg ygz]; apply/setUf_P; exists z =>//; union_tac.
Qed.
Theorem setIf_A sg f g:
(alls sg (fun i => (nonempty (g i)))) ->
intersectionf (unionf sg g) f
= intersectionf sg (fun l => intersectionf (g l) f).
Proof.
move=> neall.
case: (emptyset_dichot sg) => sgp.
by rewrite sgp setUf_0 // 2! setIf_0.
have neu: (nonempty (unionf sg g)).
by move: sgp=> [x xsg]; move: (neall _ xsg)=> [y iy]; exists y; union_tac.
set_extens t.
move/(setIf_P _ neu) => h; apply: (setIf_i sgp) => j jsg.
apply: (setIf_i (neall _ jsg)) => k kj; apply: h; union_tac.
move/(setIf_P _ sgp) => h; apply: (setIf_i neu) => j /setUf_P [y ysg jgy].
exact (setIf_hi (h _ ysg) jgy).
Qed.
Theorem dirim_setUt (I:Set) (f:I->Set) g:
direct_image g (uniont f) = uniont (fun i => direct_image g (f i)).
Proof.
set_extens t.
move /dirim_P=> [x /setUt_P [y xfy] Ju]; apply /setUt_P.
exists y; apply/dirim_P; ex_tac.
move /setUt_P => [z /dirim_P [x xf Jg]].
apply /dirim_P;ex_tac; union_tac.
Qed.
Theorem dirim_setIt (I:Set) (f:I->Set) g:
sub (direct_image g (intersectiont f))
(intersectiont (fun i => direct_image g (f i))).
Proof.
move => t /dirim_P [x].
case: (emptyset_dichot I) => neI; first by rewrite (setIt_0 _ neI); case; case.
move => ta tb; apply: (setIt_i neI) => j; apply/dirim_P; ex_tac.
apply: (setIt_hi _ ta).
Qed.
Theorem iim_fun_setIt (I:Set) (f:I->Set) g:
function g ->
(inv_image_by_fun g (intersectiont f)) =
(intersectiont (fun i => inv_image_by_fun g (f i))).
Proof.
move=> fg.
apply: extensionality; first by rewrite iim_fun_pr; apply:dirim_setIt.
case: (emptyset_dichot I) => ie; first by rewrite (setIt_0 _ ie); fprops.
move => t /(setIt_P _ ie) aj.
move: (ie)=> [x [z _]]; move: (aj z) => /iim_fun_P[u ufz Jg].
apply/iim_fun_P; ex_tac; apply: (setIt_i ie) => v.
move: (aj v) => /iim_graph_P [u' ufx Jg'].
by rewrite (Vf_pr fg Jg); rewrite - (Vf_pr fg Jg').
Qed.
Lemma inj_image_setIt (I:Set) (f:I->Set) g:
injection g ->
(image_by_fun g (intersectiont f))
= (intersectiont (fun i => image_by_fun g (f i))).
Proof.
move=> ig; move: (proj1 ig) => fg.
have [_ _ _ _ aux]:= (canonical_decomposition1 fg).
have sf := (iim_fun_r fg).
rewrite sf iim_fun_setIt; last by apply: (bijective_inv_f (aux ig)).
by apply: setIt_exten.
Qed.
Theorem setCUt2 (I:Set) (f:I-> Set) x: nonempty I ->
x -s (uniont f) = intersectiont (fun i=> x -s (f i)).
Proof.
move=>neI; set_extens z.
move /setC_P =>[zx zu];apply:(setIt_i neI) => j; apply setC_i => //.
dneg t; union_tac.
move: neI=> [_ [i _]] xi; move: (setIt_hi i xi) => /setC_P [zx zu].
apply: setC_i => //;move /setUt_P => [j zj].
by move: (setIt_hi j xi) => /setC_P [_].
Qed.
Theorem setCIt2 (I:Set) (f:I-> Set) x: nonempty I ->
x -s (intersectiont f) = uniont (fun i=> x -s (f i)).
Proof.
move=> neI.
set_extens t.
move/setC_P => [tx ti]; apply/setUt_P; ex_middle bad.
case: ti; apply /(setIt_P _ neI) => j; ex_middle bad2.
case: bad; exists j; apply: setC_i => //.
move/setUt_P => [z /setC_P [tx tf]];apply: setC_i => //; dneg h.
exact (setIt_hi z h).
Qed.
Lemma setCUf2 sf f x: nonempty sf ->
x -s (unionf sf f) = intersectionf sf (fun i=> x -s (f i)).
Proof. by apply: setCUt2. Qed.
Lemma setCIf2 sf f x: nonempty sf ->
x -s (intersectionf sf f) = unionf sf (fun i=> x -s (f i)).
Proof. by apply: setCIt2. Qed.
Lemma setUf2f x y f:
unionf (doubleton x y) f = (f x) \cup (f y).
Proof.
set_extens t.
move/setUf_P => [z /set2_P []] -> h; fprops.
case /setU2_P=> tf; union_tac.
Qed.
Lemma setIf2f x y f:
intersectionf (doubleton x y) f = (f x) \cap (f y).
Proof.
move: (set2_ne x y) => ned.
set_extens z.
move /(setIf_P _ ned) => h; apply setI2_i; apply: h; fprops.
by move/setI2_P => [zx zy]; apply: (setIf_i ned) => j; case/set2_P => ->.
Qed.
Lemma setUf2 x y: unionf (doubleton x y) id = x \cup y.
Proof. by rewrite setUf2f. Qed.
Lemma setIf2 x y: intersectionf (doubleton x y) id = x \cap y.
Proof. by rewrite setIf2f. Qed.
Lemma dirim_setU2 g: {morph (direct_image g): x y / x \cup y}.
Proof. by move => x y /=; rewrite - setUf2f - setUf2 dirim_setUt. Qed.
Lemma dirim_setI2 g x y:
sub (direct_image g (x \cap y))
((direct_image g x) \cap (direct_image g y)).
Proof. rewrite - setIf2f - setIf2; apply: dirim_setIt. Qed.
Lemma iim_fun_setI2 g: function g ->
{morph (inv_image_by_fun g): x y / x \cap y}.
Proof.
by move => fg x y /=; rewrite - setIf2f - setIf2; apply iim_fun_setIt.
Qed.
Lemma iim_fun_C1 f: function f ->
{when eq^~ (target f) & sub^~ (target f),
{morph inv_image_by_fun f : a b / a -s b}}.
Proof.
move => ff a b -> btf.
set_extens t.
move/iim_fun_P=> [u /setC_P [utf ux] Jg];apply: setC_i.
apply/iim_fun_P;ex_tac.
by move/iim_fun_P=>[v vx Jvg]; case: ux;rewrite (Vf_pr ff Jg) -(Vf_pr ff Jvg).
move/setC_P => [/iim_fun_P [u ut Jg] ne]; apply/iim_fun_P; ex_tac.
apply/setC_i => //;dneg h; apply/iim_fun_P; ex_tac.
Qed.
Lemma inj_image_C f: injection f ->
{when eq^~ (source f) & sub^~ (source f),
{morph image_by_fun f : a b / a -s b}}.
Proof.
move=> ig a b ->; move: (proj1 ig) => fg.
have [_ fv _ _ aux] := (canonical_decomposition1 fg).
rewrite 3! (iim_fun_r fg).
have ->: source f = target (inverse_fun (restriction_to_image f)).
by rewrite {1} fv; aw.
by apply: iim_fun_C1 => //; apply: (bijective_inv_f (aux ig)).
Qed.
Definition covering f x := fgraph f /\ sub x (unionb f).
Definition covering_s f x := sub x (union f).
Lemma covering_P f x: fgraph f ->
(covering f x <-> covering_s (range f) x).
Proof.
move => fgf; rewrite /covering/covering_s setUb_alt //.
split; [ by case | by split ].
Qed.
Two definitions, second one will be used in set5
Definition coarser_cg f g :=
[/\ fgraph f, fgraph g &
forall j, inc j (domain g)
-> exists2 i, inc i (domain f) & sub (Vg g j) (Vg f i)].
Definition coarser_cs y y':=
forall a, inc a y' -> exists2 b, inc b y & sub a b.
Lemma coarser_cP f g: fgraph f -> fgraph g ->
(coarser_cg f g <-> coarser_cs (range f) (range g)).
Proof.
move => fgf fgg;split.
move=> [_ _ cc j]; move/(range_gP fgg) => [i id ->].
move: (cc _ id) => [k kdf h];exists (Vg f k) => //.
apply/(range_gP fgf); ex_tac.
move => cc; split => // j jdg.
move: (cc _ (inc_V_range fgg jdg)) => [i /(range_gP fgf) [k kdf ->] h].
ex_tac.
Qed.
Lemma sub_covering f I x (g := restr f I):
(sub I (domain f)) -> covering f x -> covering g x ->
coarser_cg f g.
Proof.
move => sd [fgf cf] [fgg cg]; split => // j; rewrite restr_d => jJ.
move: (sd _ jJ) => jdf; ex_tac; rewrite /g restr_ev //.
Qed.
We consider the family of intersections of two families
Definition intersection_covering f g :=
Lg ((domain f) \times (domain g))
(fun z => (Vg f (P z)) \cap (Vg g (Q z))).
Definition intersection_covering2 x y:=
range (intersection_covering (identity_g x) (identity_g y)).
Lemma setI_covering2_P x y z:
inc z (intersection_covering2 x y) <->
exists a b, [/\ inc a x, inc b y & a \cap b = z].
Proof.
rewrite /intersection_covering2 /intersection_covering 2! identity_d.
set g := Lg _ _.
have fgg: fgraph g by rewrite /g; fprops.
rewrite /g;split.
move/Lg_range_P => [b /setX_P [pb Pb Qb] ->].
by rewrite identity_ev // identity_ev //; exists (P b); exists (Q b).
move => [a [b [ax iby <-]]]; apply/Lg_range_P.
exists (J a b); [ fprops | aw;rewrite identity_ev // identity_ev //].
Qed.
Lemma setI_covering E: {compat intersection_covering : x & / covering x E}.
Proof.
move => f g [fgf c1] [fgg c2].
rewrite /intersection_covering; split; first by fprops.
move => u ux; move /setUb_P: (c1 _ ux) => [a af uf].
move/setUb_P:(c2 _ ux)=> [b bg ug].
apply/setUb_P;bw;exists (J a b); [ fprops | bw; aw; fprops].
Qed.
Lemma setI_coarser_cl f g x:
covering f x -> covering g x ->
coarser_cg f (intersection_covering f g).
Proof.
move=> [fgf c1] [fgg c2].
rewrite /intersection_covering; red; bw; split; fprops.
move => j ji; move /setX_P:(ji)=> [pj Pj Qj]; ex_tac => t; bw; apply: setI2_1.
Qed.
Lemma setI_coarser_cr f g x:
covering f x -> covering g x ->
coarser_cg g (intersection_covering f g).
Proof.
move=> [fgf c1] [fgg c2].
rewrite /intersection_covering; red; bw;split; fprops.
move => j ji;move /setX_P: (ji)=> [pj Pj Qj]; ex_tac => t; bw; apply: setI2_2.
Qed.
Lemma setI_coarser_clr h x:
covering h x -> {when covering ^~ x &,
{compat intersection_covering : f & / coarser_cg f h}}.
Proof.
move => c3 f g c1 c2 [fgf fhg cc1] [fgg _ cc2].
rewrite /intersection_covering /coarser_cg; bw.
split;[ fprops | exact | move => u udh ].
move: (cc1 _ udh); move: (cc2 _ udh); move=> [i isg s1] [j jsf s2].
exists (J j i); bw; fprops; aw.
by move=> v vh; apply/setI2_i; [apply: s2 |apply: s1].
Qed.
Next four lemmas are a rewrite of above; they say that
intersection_covering2 is the supremum of both args
Lemma setI_covering2 E:
{compat intersection_covering2 : x & / covering_s x E}.
Proof.
move=> u v c1 c2 z zu.
move /setU_P: (c1 _ zu) =>[y zy yu].
move /setU_P: (c2 _ zu) =>[y' xzy' yv].
apply/setU_P;exists (y \cap y'); first by fprops.
by apply/ setI_covering2_P; exists y, y'.
Qed.
Lemma setI_coarser2_cl f g x:
covering_s f x -> covering_s g x ->
coarser_cs f (intersection_covering2 f g).
Proof.
move=> c1 c2 z; move/setI_covering2_P=> [a [b [af bg <-]]].
ex_tac; apply: subsetI2l.
Qed.
Lemma setI_coarser2_cr f g x:
covering_s f x -> covering_s g x ->
coarser_cs g (intersection_covering2 f g).
Proof.
move=> c1 c2 z; move/setI_covering2_P=> [a [b [af bg <-]]].
ex_tac; apply: subsetI2r.
Qed.
Lemma setI_coarser2_clr h x:
covering_s h x -> {when covering_s ^~ x &,
{compat intersection_covering2 : f & / coarser_cs f h}}.
Proof.
move=> c23 f g c1 c2 cc1 cc2 t th.
move: (cc1 _ th)=> [b bf tb]; move: (cc2 _ th)=> [b' bg tb'].
exists (b \cap b').
by apply/setI_covering2_P; exists b; exists b'.
by apply: setI2_12S.
Qed.
We consider the direct and inverse image of a covering, and the product of two coverings
Lemma image_of_covering f g:
surjection g -> covering f (source g)
-> covering (Lg (domain f) (fun w => image_by_fun g (Vg f w))) (target g).
Proof.
move=> [fg sg] [fgf cf]; split; first by fprops.
move => x xtg; move: (sg _ xtg)=> [y ys vg].
move:(setUf_hi (cf _ ys)) => [z zsf yfz].
apply/setUb_P; bw; ex_tac; bw; rewrite -vg; apply/dirim_P; ex_tac; Wtac.
Qed.
Lemma inv_image_of_covering f g:
function g -> covering f (target g)
-> covering (Lg(domain f) (fun w => inv_image_by_fun g (Vg f w))) (source g).
Proof.
move=> fg [fgf cf]; split; first by fprops.
move => x xs; apply/setUb_P; bw.
have Wt: (inc (Vf g x) (target g)) by fprops.
move /setUb_P: (cf _ Wt) => [y ysf Wf]; ex_tac; bw.
apply/iim_fun_P; ex_tac; Wtac.
Qed.
Lemma product_of_covering f g x y:
covering f x -> covering g y ->
covering (Lg ((domain f) \times (domain g))
(fun z => (Vg f (P z)) \times (Vg g (Q z))))
(x \times y).
Proof.
move=> [fgf c1] [fgg c2]; split; first by fprops.
move => z /setX_P [zp px qy].
move /setUb_P: (c1 _ px) => [a asf pa].
move /setUb_P: (c2 _ qy) => [b bsg ab].
have pc: inc (J a b) ((domain f) \times (domain g)) by fprops.
by apply/setUb_P;exists (J a b); bw; aw;apply:setX_i.
Qed.
If two functions agree on each element of a cobvering of X, they agree on X
Lemma agrees_on_covering f x g g':
covering f x -> function g -> function g' ->
source g = x -> source g' = x ->
(forall i, inc i (domain f) -> agrees_on (x \cap (Vg f i)) g g') ->
agrees_on x g g'.
Proof.
move=> [fgf c] fg fg' sg sg' ag.
hnf; rewrite sg sg';split; fprops.
move=> a ax; move /setUb_P: (c _ ax) => [y ysf afy].
by move: (ag _ ysf)=> [ _ _ ]; apply; apply: setI2_i.
Qed.
We consider the fonction whose source is the union of a family f,
the target is t, the graph is the union of all h i, which are functions
defined V i f with a compatibility condition
Definition common_ext f h t:=
triple (unionb f) t (unionb (Lg (domain f) (fun i => (graph (h i))))).
Definition function_prop_sub f s t:=
[/\ function f, source f = s & sub (target f) t].
Lemma extension_covering f t h
(d:= domain f) (g := common_ext f h t) :
(forall i, inc i d -> function_prop (h i) (Vg f i) t) ->
(forall i j, inc i d -> inc j d ->
agrees_on ((Vg f i) \cap (Vg f j)) (h i) (h j)) ->
[/\ function_prop g (unionb f) t,
graph g = (unionb (Lg d (fun i => (graph (h i))))),
range (graph g) = unionb (Lg d (fun i => (range (graph (h i))))) &
(forall i, inc i d -> agrees_on (Vg f i) g (h i))].
Proof.
move=> afp aag.
have sg: (source g = unionb f) by rewrite /g /common_ext; aw.
have tg: (target g = t) by rewrite /g/common_ext; aw.
set u1:= unionb (Lg _ _).
have gg: graph g = u1 by rewrite /u1/g/common_ext; aw.
have gu: sgraph u1.
move=> z /setUb_P; bw;move=> [y yd]; bw => zd.
by move: (afp _ yd) => [ff _ _]; move: (function_sgraph ff); apply.
have fgf: fgraph u1.
rewrite /u1;split=>//.
move => x y /setUb_P [u usf xghu] /setUb_P [v vsf yghv] sp.
move: usf vsf; bw => usf vsf; move:xghu yghv; bw => xghu yghv.
move:(afp _ usf) => [fu shu _]; move:(afp _ vsf) => [fv shv _].
move: (Vf_pr2 fu xghu) => qx; move: (Vf_pr2 fv yghv)=>qy.
apply: pair_exten=>//.
by apply: (function_sgraph fu).
by apply: (function_sgraph fv).
rewrite qx qy sp; move: (aag _ _ usf vsf)=> [_ _]; apply.
by rewrite - shu - shv; apply: setI2_i ;[ rewrite - sp|]; Wtac.
have fg: function g.
rewrite /g/common_ext; apply: function_pr=>//.
move=> z /funI_P [x /setUb_P]; bw;move=> [y ysf]; bw => Jg ->.
by move: (afp _ ysf)=> [fhy _ <-]; Wtac.
set_extens z.
move /setUb_P=> [y ysf zfy]; apply/(domainP gu); exists (Vf (h y) z).
move: (afp _ ysf) => [fhy shy _].
apply /setUb_P; bw; exists y;bw; apply: Vf_pr3 => //; ue.
move/(domainP gu) => [y]; move/setUb_P; bw;move=> [x xsf]; bw => jg.
move: (afp _ xsf) => [fhx shx _]; apply/setUb_P;ex_tac; rewrite - shx; Wtac.
split => //.
rewrite /g/common_ext; aw; set_extens zs.
move/(rangeP gu)=> [x] /setUb_P; bw; move =>[y ysf]; bw => zfy.
apply/setUb_P;move: (afp _ ysf) => [fhy shy _]; bw; ex_tac; bw;ex_tac.
move/setUb_P; bw; move=> [y ysf]; bw.
move: (afp _ ysf) => [fhy shy _].
move /(rangeP (function_sgraph fhy)) => [x Jg].
apply/(rangeP gu); exists x; apply/setUb_P; bw; exists y; bw.
move=> y ysf; move: (afp _ ysf) => [fhy shy _].
split; first by rewrite sg; move=> x xfy; union_tac.
by rewrite shy; fprops.
move=> a afy /=; symmetry;apply: Vf_pr => //.
rewrite gg; apply /setUb_P; bw; ex_tac; bw; Wtac; ue.
Qed.
Lemma extension_covering_thm f t h (d:= domain f):
(forall i, inc i d -> function_prop (h i) (Vg f i) t) ->
(forall i j, inc i d -> inc j d ->
agrees_on ( (Vg f i) \cap (Vg f j)) (h i) (h j)) ->
fgraph f ->
exists! g, (function_prop g (unionb f) t /\
(forall i, inc i d -> agrees_on (Vg f i) g (h i))).
Proof.
move=> afp aag fgf; apply /unique_existence;split.
move: (extension_covering afp aag)=> [p1 p2 p3 p4].
by exists (common_ext f h t).
rewrite /function_prop=> x y [[fx sx tx] agx] [[fy sy ty] agy].
apply: function_exten=>//; try ue.
have c: (covering f (unionb f)) by split => //.
suff agi: (forall i, inc i d -> agrees_on ((unionb f) \cap (Vg f i)) x y).
move:(agrees_on_covering c fx fy sx sy agi)=>p.
move:p => [_ _]; rewrite sx; apply.
move=> i isf; hnf.
split;first by rewrite sx;apply: subsetI2l.
by rewrite sy;apply: subsetI2l.
move => a /setI2_P; move: (agx _ isf) (agy _ isf).
rewrite /agrees_on; move=> [_ _ p1][_ _ p2] [_ afi].
by rewrite (p1 _ afi) (p2 _ afi).
Qed.
EII-4-7 Partitions
Definition nonempty_fam f := allf f nonempty.
Definition mutually_disjoint f :=
(forall i j, inc i (domain f) -> inc j (domain f) ->
i = j \/ (disjoint (Vg f i) (Vg f j))).
Definition partition_w y x:=
(union y = x) /\
(forall a b, inc a y -> inc b y -> disjointVeq a b).
Definition partition_s y x:= partition_w y x /\ (alls y nonempty).
Definition partition_w_fam f x:=
[/\ fgraph f, mutually_disjoint f & unionb f = x].
Definition partition_s_fam f x:=
partition_w_fam f x /\ nonempty_fam f.
Lemma mutually_disjoint_prop f:
(forall i j y, inc i (domain f) -> inc j (domain f) ->
inc y (Vg f i) -> inc y (Vg f j) -> i = j) ->
mutually_disjoint f.
Proof.
move=> hyp i j idf jdf; mdi_tac nij => u ui uj; case: nij; exact: (hyp _ _ u).
Qed.
Lemma mutually_disjoint_prop1 f: function f ->
(forall i j y, inc i (source f) -> inc j (source f) ->
inc y (Vf f i) -> inc y (Vf f j) -> i = j) ->
mutually_disjoint (graph f).
Proof.
by move=> ff hyp; apply: mutually_disjoint_prop; rewrite f_domain_graph.
Qed.
Lemma mutually_disjoint_prop2 x f:
(forall i j y, inc i x -> inc j x ->
inc y (f i) -> inc y (f j) -> i = j) ->
mutually_disjoint (Lg x f).
Proof.
move=> hyp; apply: mutually_disjoint_prop. bw.
by move=> i j y ix jy; bw; apply: hyp.
Qed.
Lemma partition_same y x:
partition_w y x -> partition_w_fam (identity_g y) x.
Proof.
move=> [un di]; hnf; rewrite setUb_identity.
split => //; first (by apply: identity_fgraph).
hnf; rewrite identity_d; move=> i j iy jy.
by do 2 rewrite identity_ev //; apply: di.
Qed.
Lemma partition_same2 y x:
partition_w_fam y x -> partition_w (range y) x.
Proof.
move=> [fg md uyx]; split; first by rewrite - setUb_alt.
move=> a b /(range_gP fg) [u ud ->] /(range_gP fg) [v vd ->].
by case: (md _ _ ud vd) ;[ move=>->|]; [left | right].
Qed.
Lemma partitions_is_covering y x:
partition_w y x -> covering_s y x.
Proof. by move=> [u d] a ax; ue. Qed.
Lemma partition_fam_is_covering y x:
partition_w_fam y x -> covering y x.
Proof. move=> [fg md uyx];split=>//; rewrite uyx; fprops. Qed.
If f is a partition of x each element of x is uniquely V i f
Definition cover_at f y := select (fun i => inc y (Vg f i)) (domain f).
Lemma cover_at_in f x y (i := cover_at f y):
partition_w_fam f x -> inc y x ->
(inc y (Vg f i) /\ inc i (domain f)).
Proof.
move=> [fg md ufx] yx; apply: select_pr.
by move: yx; rewrite - ufx; move/setUb_P.
move=> k j id yif jd yjf.
have yi: (inc y ((Vg f k) \cap (Vg f j))) by fprops.
case: (md k j id jd)=>// di;empty_tac1 y.
Qed.
Lemma cover_at_pr f x y i:
partition_w_fam f x -> inc i (domain f) -> inc y (Vg f i) ->
cover_at f y = i.
Proof.
move => h idf yv.
move: (h)=> [q1 q2 q3].
have zx: inc y x by rewrite -q3; union_tac.
move: (cover_at_in h zx) => [q4 q5].
case: (q2 _ _ q5 idf) => // di; empty_tac1 y.
Qed.
Lemma same_cover_at f x y z (i := cover_at f y):
partition_w_fam f x -> inc y x -> inc z (Vg f i) -> cover_at f z = i.
Proof.
move => h yx zi.
move: (cover_at_in h yx); rewrite -/i; move => [pa pb].
apply: (cover_at_pr h pb zi).
Qed.
coarser is an ordering of partitions
Lemma coarserT: transitive_r coarser_cs.
Proof.
move=> z x y c1 c2 u uy.
move: (c2 _ uy)=> [v zy uz]; move: (c1 _ zy)=> [t ty zt].
by ex_tac; apply: (sub_trans uz zt).
Qed.
Lemma coarserR: reflexive_r coarser_cs.
Proof. by move=> s x xy; ex_tac. Qed.
Lemma coarserA x:
{when partition_s ^~ x &, antisymmetric_r coarser_cs}.
Proof.
suff: (forall y y', partition_s y x -> partition_s y' x ->
coarser_cs y y' -> coarser_cs y' y -> sub y y').
move=> hyp u v p1 p2 c1 c2.
apply: extensionality; first apply: (hyp _ _ p1 p2 c1 c2).
by apply: (hyp _ _ p2 p1 c2 c1).
move=> y y' [p1 ne] _ c1 c2 t ty.
move: (c2 _ ty) => [b biy tb]; move: (c1 _ biy) => [a ay ba].
move: (ne _ ty)=> [z zt].
case: ((proj2 p1) _ _ ty ay) => eq; last by empty_tac1 z.
have -> //: t = b by apply: extensionality=>//; rewrite eq.
Qed.
We consider that function that associates x to a and y
to anything else. This is generally defined on doubleton a b
Definition variant a x y := (fun z:Set => Yo (z = a) x y).
Definition variantL a b x y := Lg (doubleton a b) (variant a x y).
Lemma variant_true a x y z:
z = a -> variant a x y z = x.
Proof. by move=> za; rewrite /variant Y_true. Qed.
Lemma variant_false a x y z:
z <> a -> variant a x y z = y.
Proof. by move=> za; rewrite /variant Y_false. Qed.
We consider here the functions that maps elements of a to x, anything else to y
Definition varianti x a b := fun z => Yo (inc z x) a b.
Lemma varianti_in z x a b: inc z x -> (varianti x a b z) = a.
Proof. by move=> zx; rewrite /varianti; Ytac0. Qed.
Lemma varianti_out z x a b: ~ inc z x -> (varianti x a b z) = b.
Proof. by move=> zx; rewrite /varianti; Ytac0. Qed.
Lemma variant_V_a a b x y: Vg (variantL a b x y) a = x.
Proof. by rewrite /variantL; bw; fprops; apply: variant_true. Qed.
Lemma variant_V_b a b x y: b <> a -> Vg (variantL a b x y) b = y.
Proof. by rewrite /variantL;bw; fprops; apply: variant_false. Qed.
Lemma variant_fgraph a b x y: fgraph (variantL a b x y).
Proof. rewrite/variantL;fprops. Qed.
Lemma variant_d a b x y: domain (variantL a b x y) = doubleton a b.
Proof. rewrite/variantL; bw. Qed.
Definition variantLc f g:= variantL C0 C1 f g.
Lemma variantLc_fgraph x y: fgraph (variantLc x y).
Proof. rewrite/variantLc/variantL; fprops. Qed.
Hint Resolve variant_fgraph variantLc_fgraph: fprops.
Lemma variantLc_d f g: domain (variantLc f g) = C2.
Proof. rewrite/variantLc/variantL; bw. Qed.
Hint Rewrite variantLc_d: bw.
Lemma variantLc_domain_ne f g: nonempty (domain (variantLc f g)).
Proof. bw; exists C0; fprops. Qed.
Lemma variant_V_ca x y: Vg (variantLc x y) C0 = x.
Proof. by rewrite /variantLc/variantL; bw;[ apply: variant_true |fprops]. Qed.
Lemma variant_V_cb x y: Vg (variantLc x y) C1 = y.
Proof.
rewrite /variantLc/variantL; bw;[ apply: variant_false;apply: TP_ne1 |fprops].
Qed.
Hint Rewrite variant_V_ca variant_V_cb: bw.
Ltac try_lvariant u:= move:u;move/C2_P; case => ->; bw.
Lemma variant_true1 x y: variant C0 x y C0 = x.
Proof. rewrite variant_true //. Qed.
Lemma variant_false1 x y: variant C0 x y C1 = y.
Proof. rewrite variant_false //; apply: TP_ne1. Qed.
Hint Rewrite variant_true1 variant_false1 : bw.
Lemma variantLc_comp a b f:
variantLc (f a) (f b) =
Lg (domain (variantLc a b))(fun z => f (Vg (variantLc a b) z)).
Proof.
apply: fgraph_exten; fprops; bw.
move=> x xtp; try_lvariant xtp; fprops.
Qed.
We have a partition of a set by selecting a subset and its complement
Definition partition_with_complement x j :=
variantLc j (x -s j).
Lemma is_partition_with_complement x j:
sub j x -> partition_w_fam (partition_with_complement x j) x.
Proof.
rewrite /partition_with_complement=> jx; split.
by apply: variantLc_fgraph.
move=> a b; bw;case /C2_P => -> ;case /C2_P => ->; fprops;
right; bw; [ | apply (disjoint_S)];apply:set_I2Cr.
by rewrite/unionb /variantLc variant_d setUf2f; bw; apply:setU2_Cr.
Qed.
Greatest and least partition for covering order
Definition greatest_partition x := fun_image x singleton.
Definition least_partition x := (singleton x).
Lemma least_is_partition x:
nonempty x -> partition_s (least_partition x) x.
Proof.
rewrite /least_partition=>ne.
split; last by move=> a /set1_P ->.
split; first by apply: setU_1.
by move=> a b /set1_P -> /set1_P ->; left.
Qed.
Lemma greatest_partition_P x z:
inc z (greatest_partition x) <-> exists2 w, inc w x & z = singleton w .
Proof. apply/funI_P. Qed.
Lemma greatest_is_partition x: partition_s (greatest_partition x) x.
Proof.
split; last by move=> a /greatest_partition_P [w wx ->]; apply: set1_ne.
split.
set_extens t.
move /setU_P => [y yt /greatest_partition_P [w wx swy]].
by move: yt; rewrite swy; move/set1_P => ->.
move=> tx; apply/setU_P;exists (singleton t); fprops.
apply /greatest_partition_P; ex_tac.
move=> a b/greatest_partition_P [w wx] -> /greatest_partition_P [w' wx'] ->.
mdi_tac ww => u /set1_P -> /set1_P sw; case: ww; ue.
Qed.
A strict partition is an injective functional graph
Definition injective_graph f:=
fgraph f /\ {inc domain f &, injective (Vg f)}.
Lemma injective_partition f x:
partition_s_fam f x -> injective_graph f.
Proof.
move=> [[fgf md ux] hyp]; split=>//.
move=> a b ad bd sV; move: (md _ _ ad bd) (hyp _ bd)=> [] //.
rewrite /disjoint sV setI2_id => -> [_ [[]]].
Qed.
Lemma partition_fam_partition f x:
partition_s_fam f x -> partition_s (range f) x.
Proof.
move=> [pf hyp]; move: (partition_same2 pf)=> [ur di].
move:pf=> [fgf md _]; split=>//.
move=> a /(rangeP (proj1 fgf)) [b bf]; move: (pr2_V fgf bf); aw => ->.
apply: hyp;ex_tac.
Qed.
Lemma inv_image_disjoint g : function g ->
{compat (inv_image_by_fun g) : x y / disjoint x y}.
Proof.
move=> fg x y dxy; rewrite /disjoint -iim_fun_setI2 //.
by apply /set0_P => t /iim_fun_P [u]; rewrite dxy => /in_set0.
Qed.
Given a partition, a function on each subset can be uniquely extended;
We give two variants, in one case the targets may be different
Lemma extension_partition_aux f x t h:
partition_w_fam f x ->
(forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) ->
(forall i j, inc i (domain f) -> inc j (domain f) ->
agrees_on ((Vg f i) \cap (Vg f j)) (h i) (h j)).
Proof.
move=> [fgf mdf ufx] afp.
move=> i j id jd; case: (mdf _ _ id jd).
move=> ->; rewrite setI2_id; move: (afp _ jd)=> [_ shj _].
red; rewrite shj; split;fprops => s //.
rewrite/disjoint=> ->; red; split; try split; fprops.
by move=> a /in_set0.
Qed.
Lemma extension_partition1 f x t h (g := common_ext f h t):
partition_w_fam f x ->
(forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) ->
(function_prop g x t /\
(forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i))).
Proof.
move => pfa afp.
move: (extension_partition_aux pfa afp) => aah.
move: (extension_covering afp aah).
by move: pfa => [fgf mdf ufx]; rewrite -/g - ufx; move => [h1 _ h2 h3].
Qed.
Lemma extension_partition2 f x t h
(g:= common_ext f (fun i => (triple (Vg f i) t (graph (h i)))) t):
partition_w_fam f x ->
(forall i, inc i (domain f) -> function_prop_sub (h i) (Vg f i) t) ->
( function_prop g x t /\
forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i)).
Proof.
move=> pf prop.
pose nh i := triple (Vg f i) t (graph (h i)).
have afp: forall i, inc i (domain f) -> function_prop (nh i) (Vg f i) t.
move=> i id; move: (prop _ id) => [fgh sg th];rewrite /nh;split; aw.
apply: function_pr; fprops.
by apply: sub_trans th; apply: f_range_graph.
by rewrite f_domain_graph.
move: (extension_partition1 pf afp).
move => [fpg aag]; split=>//.
move=> i idf; move: (aag _ idf)=> [aa cc bb];split=>//.
by move: (prop _ idf) => [_ -> _]; fprops.
move=> a aV; move: (bb _ aV) => ->; rewrite /nh /Vf; aw.
Qed.
Theorem extension_partition_thm f x t h:
partition_w_fam f x ->
(forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) ->
exists! g, (function_prop g x t /\
(forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i))).
Proof.
move => pfa afp.
move: (extension_partition_aux pfa afp) => aah.
move: pfa => [fgf mdf <-]; exact: (extension_covering_thm afp aah fgf).
Qed.
EII-4-8 Sum of a family of sets
Definition disjointU_fam f := Lg (domain f)(fun i => (Vg f i) *s1 i).
Definition disjointU f := unionb (disjointU_fam f).
Lemma disjointU_disjoint f:
mutually_disjoint (disjointU_fam f).
Proof.
move=> i j; rewrite /disjointU_fam Lg_domain=> id jd; bw.
by mdi_tac t => u /indexed_P [_ _] qu /indexed_P [_ _]; rewrite qu.
Qed.
Hint Resolve disjointU_disjoint: fprops.
Lemma disjointU_fgraph f: fgraph (disjointU_fam f).
Proof. rewrite /disjointU_fam; fprops. Qed.
Lemma disjointU_d f: domain (disjointU_fam f) = domain f.
Proof. rewrite /disjointU_fam; bw. Qed.
Hint Resolve disjointU_fgraph: fprops.
Theorem disjoint_union_lemma f:
exists g x,
[/\ fgraph g, x = unionb g,
(forall i, inc i (domain f) -> (Vg f i) \Eq (Vg g i))
& mutually_disjoint g].
Proof.
exists (disjointU_fam f), (disjointU f); split;fprops.
move=> i idf; rewrite /disjointU_fam; bw; apply:equipotent_indexed.
Qed.
Lemma partition_disjointU f:
partition_w_fam (disjointU_fam f) (disjointU f).
Proof.
split; [fprops | by apply: disjointU_disjoint | done ].
Qed.
Lemma disjointU_hi f x: inc x (disjointU f) ->
[/\ inc (Q x) (domain f), inc (P x) (Vg f (Q x)) & pairp x].
Proof.
move/setUb_P => [t]; rewrite disjointU_d => td.
by rewrite /disjointU_fam; bw; move /indexed_P => [pa pb ->].
Qed.
Lemma disjointU_P f x: inc x (disjointU f) <->
[/\ inc (Q x) (domain f), inc (P x) (Vg f (Q x)) & pairp x].
Proof.
split; first by apply: disjointU_hi.
move => [pa pb pc]; apply/setUb_P; rewrite disjointU_d; ex_tac.
rewrite /disjointU_fam; bw; rewrite - {1} pc; apply/setXp_i; fprops.
Qed.
Lemma disjointU_pi f x y:
inc y (domain f) -> inc x (Vg f y) ->
inc (J x y) (disjointU f).
Proof. move => ta tb;apply/disjointU_P; aw; split; fprops. Qed.
Lemma disjointU2_rw a b x y: y <> x ->
disjointU (variantL x y a b) = (a *s1 x) \cup (b *s1 y).
Proof.
move=> yx.
rewrite/disjointU /disjointU_fam.
have dv: domain (variantL x y a b) = doubleton x y by rewrite/ variantL; bw.
set_extens z; rewrite dv.
move/setUb_P; bw; move => [u ud]; bw; move/setX_P => [pz Pz Qz].
rewrite -pz; move/set1_P: Qz ->; apply/setU2_P; move: Pz.
case /set2_P: ud=> ->; rewrite ?variant_V_a ? (variant_V_b _ _ yx);
[left | right]; apply: setXp_i => //; fprops.
move=> h.
have Qz: (inc (Q z) (doubleton x y)).
case /setU2_P :h => /setX_P [_ _] /set1_P ->; fprops.
apply/setUb_P; bw; exists (Q z); bw.
by case/setU2_P: h => /setX_P [pz Pz w]; move/set1_P: (w) ->;
apply: setX_i; fprops; rewrite ?variant_V_a ? variant_V_b.
Qed.
Lemma disjointU2_rw1 a b:
disjointU (variantLc a b) = (a *s1 C0) \cup (b *s1 C1).
Proof. rewrite/variantLc disjointU2_rw //; fprops. Qed.
There is a canonical mapping from the disjoint union onto the union; It is bijective if the family is disjoint
Theorem disjointU_pr f
(h := fun i => Lf P ((Vg f i) *s1 i) (unionb f))
(g := common_ext (disjointU_fam f) h (unionb f)):
[/\ source g = disjointU f,
target g = unionb f,
surjection g &
(mutually_disjoint f -> bijection g)].
Proof.
set aux:= (Lg (domain f) (fun i => (Vg f i) *s1 i)).
move: (partition_disjointU f) =>pf.
have da: (domain aux = domain f) by rewrite /aux; bw.
have tap: forall i, inc i (domain aux) -> lf_axiom P ((Vg f i) *s1 i)(unionb f).
by move => i id x; move/setX_P=> [_ pv Qi]; union_tac; ue.
have fpi: (forall i, inc i (domain aux) ->
function_prop (h i) (Vg aux i)(unionb f)).
move=> i id; hnf;rewrite /h/aux; aw; bw; last by ue.
split => //; by apply: lf_function; apply: tap.
move:(extension_partition1 pf fpi).
rewrite -/g; move => [fpg aag].
move: aag; bw; rewrite/disjointU_fam; bw; move=> aag.
move: fpg=> [fg sg tg].
have sug: (surjection g).
apply: surjective_pr5=>//; rewrite /related.
rewrite tg sg; move=> y; move /setUb_P=> [z zdf yg].
set (t:= J y z).
have tsg: inc t (disjointU f) by rewrite /t; apply: disjointU_pi.
exists t => //.
suff: y = Vf g t by move=>->; apply: Vf_pr3 =>//; rewrite sg.
have ps: inc t ((Vg f z) *s1 z) by rewrite /t/indexed ; aw; fprops.
move: (aag _ zdf); bw.
rewrite /agrees_on; move=> [_ _ sv]; move: (sv _ ps).
rewrite /h; aw.
by move=> ->; rewrite /t; aw.
by apply: tap; ue.
split=>//.
move=> mf; split=>//; split => //.
move=> x y; rewrite sg; move=> xsg ysg.
move: (disjointU_hi xsg)=> [qxd pV xp].
move: (disjointU_hi ysg)=> [qyd pyV yp].
move: (aag _ qxd); bw; move=> [ _ _ ax].
move: (aag _ qyd); bw; move=> [ _ _ ay].
have xs: inc x ((Vg f (Q x)) *s1 (Q x)) by apply: setX_i; fprops.
have ys: inc y ((Vg f (Q y)) *s1 (Q y)) by apply: setX_i; fprops.
rewrite (ax _ xs) (ay _ ys).
rewrite/h ;aw ; fprops; try apply: tap; try rewrite da=>//.
move=> sp;move: (mf _ _ qxd qyd).
case=> sq; [by apply: pair_exten | by empty_tac1 (P x);rewrite sp].
Qed.
Definition canonical_du2 a b := disjointU (variantLc a b).
Lemma candu2_rw a b:
canonical_du2 a b = (a *s1 C0) \cup (b *s1 C1).
Proof. by rewrite /canonical_du2 disjointU2_rw1. Qed.
Lemma candu2P a b x:
inc x (canonical_du2 a b) <-> (pairp x /\
((inc (P x) a /\ Q x = C0) \/ (inc (P x) b /\ Q x = C1))).
Proof.
rewrite candu2_rw; split.
case /setU2_P; move /indexed_P => [pa pb]; fprops.
by move => [pa [] [h1 h2]]; apply/setU2_P; [left | right ]; apply /indexed_P.
Qed.
Lemma candu2_pr2 a b x:
inc x (canonical_du2 a b) -> (Q x = C0 \/ Q x = C1).
Proof. by move /candu2P => [_]; case => [] [_]; [left | right]. Qed.
Lemma candu2_pra a b x:
inc x a -> inc (J x C0) (canonical_du2 a b).
Proof. by move=> xa; apply /candu2P; split;fprops; left; aw. Qed.
Lemma candu2_prb a b x:
inc x b -> inc (J x C1) (canonical_du2 a b).
Proof. by move => xb; apply /candu2P; split; fprops ; right; aw. Qed.
EII-5 Product of a family of sets
EII-5-1 The axiom of the set of subsets
Definition extension_to_parts f :=
Lf (image_by_fun f) (powerset (source f)) (powerset (target f)).
Lemma etp_axiom f: correspondence f ->
lf_axiom (image_by_fun f) (powerset (source f)) (powerset (target f)).
Proof.
move=> cf x; move/setP_P => xs; apply/setP_P.
apply: (@sub_trans (range (graph f))); fprops; apply: dirim_Sr.
Qed.
Lemma etp_f f: correspondence f -> function (extension_to_parts f).
Proof.
move => cf; apply: lf_function;by apply: etp_axiom.
Qed.
Lemma etp_V f x:
correspondence f -> sub x (source f)
-> Vf (extension_to_parts f) x = image_by_fun f x.
Proof.
by rewrite /extension_to_parts=> cf s; aw; [apply: etp_axiom | apply/setP_P ].
Qed.
Hint Resolve etp_f : fprops.
Morphism properties of extension
Lemma etp_composable f g:
composableC g f ->
(extension_to_parts g) \coP (extension_to_parts f).
Proof.
move=> [cf cg cfg]; split; fprops.
rewrite /extension_to_parts;aw; ue.
Qed.
Lemma etp_compose:
{when: composableC, {morph extension_to_parts: x y / x \co y }}.
Proof.
move=> g f /= cgf.
move: (etp_composable cgf)=>cegf.
move: cgf=> [cf cg cfg].
have ccg: (correspondence (g \co f)) by apply: compf_correspondence.
symmetry;apply: function_exten; try (fct_tac; fprops); fprops.
by rewrite /extension_to_parts; aw.
by rewrite /extension_to_parts; aw.
aw;move => x xs.
have xs1: sub x (source f).
by move: xs;rewrite /extension_to_parts; aw; move/setP_P.
have xs2: sub x (source (g \co f)) by aw.
symmetry; aw; do 3 rewrite etp_V=>//.
rewrite /compose/image_by_fun ; aw; apply:compg_image.
rewrite cfg /image_by_fun; apply: (@sub_trans (range (graph f))); fprops.
apply: dirim_Sr.
Qed.
Lemma etp_identity x:
extension_to_parts (identity x) = identity (powerset x).
Proof.
move:(@identity_corresp x)=> ic.
apply: function_exten; fprops; try solve [rewrite/extension_to_parts; aw].
move=> y /=; rewrite {1} /extension_to_parts; aw => ys1.
move /setP_P: (ys1) => ys2.
have ys: sub y (source (identity x)) by aw; apply/setP_P.
have fi: (function (identity x)) by fprops.
rewrite etp_V // identity_V //; set_extens t.
by move /(Vf_image_P fi ys) => [u uy]; bw; [ move => -> | apply: ys2].
move => ty;apply /(Vf_image_P fi ys); ex_tac; bw; fprops.
Qed.
Lemma composable_for_function f g:
g \coP f -> composableC g f.
Proof. by move=> [[ fg _ _] [ff _ _ ] eq]. Qed.
Theorem etp_fs f: surjection f -> surjection (extension_to_parts f).
Proof.
move=> sf; apply: surj_if_exists_right_inv.
have [r [cfr cfri]]:= (exists_right_inv_from_surj sf).
have cfr' := (composable_for_function cfr).
exists (extension_to_parts r); split; first by apply: etp_composable.
rewrite - etp_compose // cfri etp_identity /extension_to_parts; aw.
Qed.
Theorem etp_fi f: injection f -> injection (extension_to_parts f).
Proof.
move=> inf.
case: (emptyset_dichot (source f))=> eq.
move: inf=> [[ cf _] _]; split; fprops.
rewrite {1 2} /extension_to_parts=> x y.
by rewrite lf_source eq setP_0; move /set1_P => -> /set1_P ->.
have [r [cfr cfri]] := (exists_left_inv_from_inj inf eq).
have cfr' := (composable_for_function cfr).
apply: inj_if_exists_left_inv.
exists (extension_to_parts r); split; first by apply: etp_composable.
rewrite - etp_compose // cfri etp_identity /extension_to_parts; aw.
Qed.
EII-5-2 Set of mappings of one set into another
Definition functions x y :=
Zo (correspondences x y)
(fun z => fgraph (graph z) /\ x = domain (graph z)).
Definition gfunctions x y:=
Zo (powerset (x \times y))(fun z => fgraph z /\ x = domain z).
Definition permutations E :=
Zo (functions E E) bijection.
Definition sub_functions x y :=
unionf(powerset x)(functions ^~ y).
Lemma fun_set_P x y f:
inc f (functions x y) <-> (function_prop f x y).
Proof.
rewrite/function; split.
move/Zo_P => [/correspondences_P [p1 p2 p3] [p4 p5]]; split => //.
split => //; ue.
by move=> [[qa qb qc] <- pc]; apply: Zo_i; [apply/correspondences_P | split].
Qed.
Lemma sfun_set_P x y f:
inc f (sub_functions x y) <->
[/\ function f, sub (source f) x & target f = y].
Proof.
split.
move/setUf_P => [z /setP_P zx /fun_set_P [pa pb pc]];split => //; ue.
by move => [pa /setP_P pb pc]; apply /setUf_P; ex_tac; apply/fun_set_P.
Qed.
Lemma gfun_set_i f:
function f -> inc (graph f) (gfunctions (source f) (target f)).
Proof. by move=> [[pa pd] pb pc]; apply: Zo_i => //; apply/setP_P. Qed.
Lemma gfun_set_hi x y z:
inc z (gfunctions x y) -> exists f,
[/\ function f, source f = x, target f = y & graph f = z].
Proof.
move/Zo_P => [/setP_P /corr_propcc [_ _ pa] [pb pc]].
exists (triple x y z); aw; split => // ; apply: function_pr=>//.
Qed.
Lemma function_exten5 x y a b:
inc a (functions x y) -> inc b (functions x y) ->
graph a = graph b -> a = b.
Proof.
move /fun_set_P=> [fa sa ta] /fun_set_P [fb sb tb] sg.
apply: function_exten1=>//; ue.
Qed.
Lemma fun_set_small_source y: small_set (functions emptyset y).
Proof.
move=> u v uf vf; apply: (function_exten5 uf vf).
move /fun_set_P: uf => [fa sa _]; move/fun_set_P: vf => [fb sb _].
rewrite !empty_source_graph //.
Qed.
Lemma fun_set_small_target x: small_set (functions x emptyset).
Proof.
move=> u v uf vf; apply: (function_exten5 uf vf).
move /fun_set_P: uf => [fa _ ta]; move/fun_set_P: vf => [fb _ tb].
rewrite !empty_target_graph//.
Qed.
Lemma fun_set_ne x y: (x = emptyset \/ nonempty y) -> nonempty (functions x y).
Proof.
case=> p.
rewrite p;move: (empty_function_tg_function y) => h.
by exists (empty_function_tg y); apply/fun_set_P.
move: p => [p py]; exists (constant_function x py); apply/fun_set_P.
apply constant_prop.
Qed.
Canonical isomorphism between calF(E,F) and F^E
Lemma graph_lf_axiom x y:
lf_axiom graph (functions x y) (gfunctions x y).
Proof. by move=> g /fun_set_P [fg <- <-]; apply: gfun_set_i. Qed.
Lemma graph_fb x y:
bijection (Lf graph (functions x y) (gfunctions x y)).
Proof.
apply: lf_bijective.
- by apply: graph_lf_axiom.
- by move=> u v us vs g; apply: (function_exten5 us vs g).
- move=> z zg ; move: (gfun_set_hi zg) => [f [pa pb pc pd]].
by exists f => //;apply/fun_set_P.
Qed.
Lemma fun_set_equipotent x y:
(functions x y) \Eq (gfunctions x y).
Proof. apply: (equipotent_aux (f:= graph)); aw; apply: graph_fb. Qed.
Isomorphism between calF(E,F) and calF(E',F') for equipotent sets
Definition compose3function u v :=
Lf (fun f => (v \co f) \co u)
(functions (target u) (source v))
(functions (source u) (target v)).
Lemma c3f_axiom u v:
function u -> function v ->
lf_axiom (fun f => (v \co f) \co u)
(functions (target u) (source v))
(functions (source u) (target v)).
Proof.
move=> fu fv x; move /fun_set_P=> [fx sx tx]; apply/fun_set_P; aw.
split=> //; aw; fct_tac ;[fct_tac | aw].
Qed.
Lemma c3f_f u v:
function u -> function v -> function (compose3function u v).
Proof. by move =>fu fv; apply: lf_function; apply: c3f_axiom. Qed.
Lemma c3f_V u v f:
function u -> function v ->
function f -> source f = target u -> target f = source v ->
Vf (compose3function u v) f = (v \co f) \co u.
Proof.
rewrite /compose3function=> fu fv ff sf tf.
by aw; [apply: c3f_axiom=>// | apply/fun_set_P].
Qed.
Theorem c3f_fi u v:
surjection u -> injection v -> injection (compose3function u v).
Proof.
rewrite /compose3function=> su iv.
have fu: function u by fct_tac.
have fv: function v by fct_tac.
apply: lf_injective; first by apply: c3f_axiom.
move=> f g.
case: (emptyset_dichot (source v)) => sve.
by move=> i1 i2 c; apply: (fun_set_small_target (x:= target u)); ue.
move: (exists_right_inv_from_surj su) => [s [cus cusi]].
move: (exists_left_inv_from_inj iv sve).
move=> [r [crv crvi]] /fun_set_P [ff sf tf] /fun_set_P [fg sg tg] ceq.
have cvf: v \coP f by hnf.
have cvg: v \coP g by hnf.
have fvf: function (v \co f) by fct_tac.
have fvg: function (v \co g) by fct_tac.
have cvfu: (v \co f) \coP u by hnf; aw.
have cvgu: (v \co g) \coP u by hnf; aw.
move:(f_equal (fun i => i \co s) ceq).
rewrite - compfA // cusi - sf - (compf_s f v) compf_id_r //.
rewrite - compfA // cusi - sg - (compf_s g v) compf_id_r // => eq.
move: (f_equal (fun i => r \co i) eq).
rewrite compfA // crvi - tf compf_id_l //.
rewrite compfA // crvi - tg compf_id_l //.
Qed.
Theorem c3f_fs u v:
(nonempty (source u) \/ (nonempty (source v)) \/ (nonempty (target v))
\/ target u = emptyset) ->
injection u -> surjection v -> surjection (compose3function u v).
Proof.
move=> nehyp iu sv.
have fu: function u by fct_tac.
have fv: function v by fct_tac.
move: (c3f_f fu fv); set (c3f:= compose3function u v) => c3ff.
split => //; rewrite /c3f/compose3function; aw => y ys.
case: (emptyset_dichot (source u)) => nesu.
have p:(target u = emptyset \/ nonempty (source v)).
case: nehyp.
by rewrite nesu=> [] [h] [x]; case: x.
case; [by right | case; last by left].
by move=> [w wt]; move: (surjective_pr sv wt)=> [x xs _];right; ex_tac.
have: (nonempty (functions (target u) (source v))).
by apply: (fun_set_ne p).
move=> [f fsp]; ex_tac; move/fun_set_P:(fsp) => [ff sf tf].
rewrite c3f_V //.
apply: (fun_set_small_source (y:=target v)); rewrite - nesu //.
by apply: c3f_axiom.
move: (exists_right_inv_from_surj sv)=> [s [cvs cvsi]].
move: (exists_left_inv_from_inj iu nesu) => [r [cru crui]].
have Hb: function s by fct_tac.
have Hc: function r by fct_tac.
move/fun_set_P:ys=> [fy sy ty].
set (f:= (s \co y) \co r).
have sf: source f = target u by move: cru=> [_ _]; rewrite /f; aw.
have tf: target f = source v by move: cvs=> [_ _]; rewrite /f; aw.
have sytr: source y = target r by rewrite sy; move: (f_equal target crui); aw.
have tytr: source s = target y by rewrite ty; move: (f_equal source cvsi); aw.
have csy: s \coP y by [].
have fcyr: function (y \co r) by fct_tac.
have csyr: s \coP (y \co r) by hnf; aw.
have tcyr : (target (y \co r) = target v) by aw.
have fcsy: function (s \co y) by fct_tac.
have ff: function f by rewrite/f; fct_tac=>//; aw.
exists f; first by apply/fun_set_P.
rewrite c3f_V //.
rewrite/f -(@compfA s y r) // (@compfA v s (y \co r)) //.
rewrite cvsi -tcyr compf_id_l // -compfA //.
rewrite crui - sy compf_id_r //.
Qed.
Lemma c3f_fb u v:
bijection u -> bijection v -> bijection (compose3function u v).
Proof.
move=> [iu su][iv sv]; split; first by apply: c3f_fi=>//.
apply: c3f_fs=>//.
case: (emptyset_dichot (target u)); first by right; right; right.
move=> [y yt]; move: (surjective_pr su yt)=> [x xs _]; left; ex_tac.
Qed.
Isomorphism between calF(BxC,A) and calF(C, calF(B,A)) and calF(B, calF(C,A))
Definition partial_fun_axiom f :=
function f /\ exists a b, source f = a \times b.
Lemma partial_fun_axiom_pr f:
partial_fun_axiom f ->
source f = (domain (source f)) \times (range (source f)).
Proof.
move=> [ff [a [b sf]]]; rewrite sf.
case: (emptyset_dichot a); first by move => ->; rewrite setX_0l; bw.
case: (emptyset_dichot b); first by move => ->; rewrite setX_0r; bw.
by move=> h1 h2; bw.
Qed.
Definition first_partial_fun f y:=
Lf (fun x => Vf f (J x y)) (domain (source f)) (target f).
Definition second_partial_fun f x:=
Lf (fun y => Vf f (J x y)) (range (source f)) (target f).
Definition first_partial_function f:=
Lf (fun y => first_partial_fun f y) (range (source f))
(functions (domain (source f)) (target f)).
Definition second_partial_function f:=
Lf (fun x => second_partial_fun f x) (domain (source f))
(functions (range (source f)) (target f)).
Definition first_partial_map b c a:=
Lf (fun f=> first_partial_function f)
(functions (b \times c) a)
(functions c (functions b a)).
Definition second_partial_map b c a:=
Lf (fun f=> second_partial_function f)
(functions (b \times c) a)
(functions b (functions c a)).
Lemma fpf_axiom f y:
partial_fun_axiom f -> inc y (range (source f)) ->
lf_axiom (fun x => Vf f (J x y)) (domain (source f)) (target f).
Proof.
move=> pfa; move: (partial_fun_axiom_pr pfa)=> pfb.
move=> yr x xs; move: pfa=>[ff _]; Wtac;ue.
Qed.
Lemma spf_axiom f x:
partial_fun_axiom f -> inc x (domain (source f)) ->
lf_axiom (fun y => Vf f (J x y)) (range (source f)) (target f).
Proof.
move=> pfa; move: (partial_fun_axiom_pr pfa)=> pfb.
move=> yr t xs; move: pfa=>[ff _]; Wtac; ue.
Qed.
Lemma fpf_f f y:
partial_fun_axiom f -> inc y (range (source f)) ->
function (first_partial_fun f y).
Proof.
rewrite/first_partial_fun=> pfa yr.
by apply: lf_function; apply: fpf_axiom.
Qed.
Lemma spf_f f x:
partial_fun_axiom f -> inc x (domain (source f)) ->
function (second_partial_fun f x).
Proof.
rewrite/second_partial_fun=> pfa yr.
by apply: lf_function; apply: spf_axiom.
Qed.
Lemma fpf_V f x y:
partial_fun_axiom f -> inc x (domain (source f)) ->
inc y (range (source f)) ->
Vf (first_partial_fun f y) x = Vf f (J x y).
Proof.
rewrite/first_partial_fun=> pfa xd yr.
by rewrite lf_V //; apply: fpf_axiom.
Qed.
Lemma spf_V f x y:
partial_fun_axiom f -> inc x (domain (source f)) ->
inc y (range (source f)) ->
Vf (second_partial_fun f x) y = Vf f (J x y).
Proof.
rewrite/first_partial_fun=> pfa xd yr.
by rewrite lf_V //; apply: spf_axiom.
Qed.
Lemma fpfa_axiom f:
partial_fun_axiom f ->
lf_axiom (fun y => (first_partial_fun f y))(range (source f))
(functions (domain (source f)) (target f)).
Proof.
move=> pfa x xr; apply /fun_set_P; rewrite /first_partial_fun;red; aw.
by split => //;apply: fpf_f.
Qed.
Lemma spfa_axiom f:
partial_fun_axiom f ->
lf_axiom (fun x => second_partial_fun f x) (domain (source f))
(functions (range (source f)) (target f)).
Proof.
move=> pfa x xr; apply /fun_set_P;rewrite /second_partial_fun; red;aw.
split => //; by apply: spf_f.
Qed.
Lemma fpfa_f f:
partial_fun_axiom f -> function (first_partial_function f).
Proof.
rewrite /first_partial_function=> fpa.
by apply: lf_function; apply: fpfa_axiom.
Qed.
Lemma spfa_f f:
partial_fun_axiom f -> function (second_partial_function f).
Proof.
rewrite /second_partial_function=> fpa.
by apply: lf_function; apply: spfa_axiom.
Qed.
Lemma fpfa_V f y:
partial_fun_axiom f -> inc y (range (source f)) ->
Vf (first_partial_function f) y = first_partial_fun f y.
Proof.
rewrite /first_partial_function=> pfa yr.
by rewrite lf_V //; apply: fpfa_axiom.
Qed.
Lemma spfa_V f x:
partial_fun_axiom f -> inc x (domain (source f)) ->
Vf (second_partial_function f) x = second_partial_fun f x.
Proof.
rewrite /second_partial_function=> pfa yr.
by rewrite lf_V //; apply: spfa_axiom.
Qed.
Lemma fpfb_axiom a b c:
nonempty b -> nonempty c ->
lf_axiom (fun f=> first_partial_function f)
(functions (b \times c) a)
(functions c (functions b a)).
Proof.
move=> neb nec x; move/fun_set_P=>[fx sx tx]; apply/fun_set_P.
red;rewrite {2 3} /first_partial_function;aw; rewrite sx tx; bw.
by split => //; apply: fpfa_f; split=>//; rewrite sx;exists b, c.
Qed.
Lemma spfb_axiom a b c:
nonempty b -> nonempty c ->
lf_axiom (fun f=> second_partial_function f)
(functions (b \times c) a)
(functions b (functions c a)).
Proof.
move=> neb nec x; move/fun_set_P=>[fx sx tx]; apply/fun_set_P.
red;rewrite {2 3} /second_partial_function; aw; rewrite sx tx; bw.
by split => //; apply: spfa_f; split=>//; rewrite sx;exists b, c.
Qed.
Lemma fpfb_f a b c:
nonempty a -> nonempty b -> function (first_partial_map a b c).
Proof.
by rewrite /first_partial_map=> nea neb;apply: lf_function; apply: fpfb_axiom.
Qed.
Lemma spfb_f a b c:
nonempty a -> nonempty b -> function (second_partial_map a b c).
Proof.
by rewrite /second_partial_map=> nea neb; apply: lf_function; apply: spfb_axiom.
Qed.
Lemma fpfb_V a b c f:
nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
Vf (first_partial_map a b c) f = first_partial_function f.
Proof.
by rewrite/first_partial_map=> nea neb fs; aw; apply: fpfb_axiom.
Qed.
Lemma spfb_V a b c f:
nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
Vf (second_partial_map a b c) f = second_partial_function f.
Proof.
by rewrite/second_partial_map=> nea neb fs; aw; apply: spfb_axiom.
Qed.
Lemma fpfb_VV a b c f x:
nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
inc x (a \times b) ->
Vf (Vf (Vf (first_partial_map a b c) f) (Q x)) (P x) = Vf f x.
Proof.
move=> nea neb fs xp; rewrite fpfb_V=>//.
move /fun_set_P: fs => [fs sf tf].
have pfaf: (partial_fun_axiom f) by split=>//; exists a, b.
move /setX_P: xp =>[xp px qx].
have qxr: (inc (Q x) (range (source f))) by rewrite sf; bw.
have pxr: (inc (P x) (domain (source f))) by rewrite sf; bw.
by rewrite fpfa_V // fpf_V // xp.
Qed.
Lemma spfb_VV a b c f x:
nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
inc x (a \times b) ->
Vf (Vf (Vf (second_partial_map a b c) f) (P x)) (Q x) = Vf f x.
Proof.
move=> nea neb fs xp; rewrite spfb_V=>//.
move /fun_set_P: fs => [fs sf tf].
have pfaf: (partial_fun_axiom f) by split=>//; exists a, b.
move /setX_P: xp =>[xp px qx].
have qxr: (inc (Q x) (range (source f))) by rewrite sf; bw.
have pxr: (inc (P x) (domain (source f))) by rewrite sf; bw.
by rewrite spfa_V // spf_V // xp.
Qed.
Theorem fpfa_fb a b c:
nonempty a -> nonempty b -> bijection (first_partial_map a b c).
Proof.
move=> nea neb.
set f:= _ a b c.
have sf:source f = functions (a \times b) c.
by rewrite /f /first_partial_map; aw.
have tf: target f = functions b (functions a c)
by rewrite /f /first_partial_map; aw.
have ff: function f by apply: (fpfb_f _ nea neb).
split.
split=>//.
move=> x y; rewrite sf=> xs ys eq.
have sx: source x = a \times b by move /fun_set_P: xs => [_ ].
have sy: source y = a \times b by move /fun_set_P: ys => [_ ].
have ha: forall z, inc z (source x) -> Vf x z = Vf y z.
rewrite sx => z zp.
by rewrite -(fpfb_VV nea neb xs zp) -(fpfb_VV nea neb ys zp) eq.
move: xs ys => /fun_set_P [fx _ tx] /fun_set_P [fy _ ty].
by apply: function_exten=>//; try ue.
split=>//; move=> y yt.
set (g:= Lf (fun x => Vf (Vf y (Q x)) (P x)) (a \times b) c).
have ta: lf_axiom (fun x => Vf (Vf y (Q x) ) (P x)) (a \times b) c.
move=> x /setX_P [xp pa qb].
move: yt; rewrite tf; move /fun_set_P => [fy sy ty].
have: (inc (Vf y (Q x)) (target y)) by Wtac.
by rewrite ty; move /fun_set_P=> [fW sW <-]; Wtac.
have gsf: (inc g (source f)).
by rewrite /g sf; apply /fun_set_P; red;aw; split => //; apply: lf_function.
ex_tac.
have: inc (Vf f g) (target f) by Wtac.
move:yt; rewrite tf;move=> /fun_set_P [fy sy ty] /fun_set_P [fW sW tw].
apply: function_exten=>//; try ue; move => x; rewrite sW=> xs.
have: inc (Vf (Vf f g) x) (target (Vf f g)) by Wtac.
have: inc (Vf y x) (target y) by Wtac.
rewrite tw ty; move=> /fun_set_P [fy1 sy1 ty1] /fun_set_P [fW1 sW1 tw1].
apply: function_exten=>//; try ue; rewrite sW1=> z zs.
have psg: (inc (J z x) (source g)) by rewrite /g; aw; fprops.
rewrite/g lf_source in psg; rewrite sf in gsf.
move: (fpfb_VV nea neb gsf psg); aw; move=> ->.
by rewrite /g lf_V; first by aw.
Qed.
Theorem spfa_fb a b c:
nonempty a -> nonempty b -> bijection (second_partial_map a b c).
Proof.
move=> nea neb.
set f:= _ a b c.
have sf:source f = functions (a \times b) c.
by rewrite /f /second_partial_map; aw.
have tf: target f = functions a (functions b c).
by rewrite /f /second_partial_map; aw.
have ff: function f by apply: (spfb_f _ nea neb).
split.
split=>//.
move=> x y; rewrite sf=> xs ys eq.
have sx: source x = a \times b by move /fun_set_P: xs => [_ ].
have sy: source y = a \times b by move /fun_set_P: ys => [_ ].
have ha: forall z, inc z (source x) -> Vf x z = Vf y z.
rewrite sx => z zp.
by rewrite -(spfb_VV nea neb xs zp) -(spfb_VV nea neb ys zp) eq.
move: xs ys => /fun_set_P [fx _ tx] /fun_set_P [fy _ ty].
by apply: function_exten=>//; try ue.
split=>//; move=> y yt.
pose (g:= Lf (fun x => Vf (Vf y (P x)) (Q x)) (a \times b) c).
have ta: lf_axiom (fun x => Vf (Vf y (P x)) (Q x)) (a \times b) c.
move=> x /setX_P [xp pa qb].
move: yt; rewrite tf; move /fun_set_P => [fy sy ty].
have : (inc (Vf y (P x)) (target y)) by Wtac.
by rewrite ty; move /fun_set_P=> [fW sW <-]; Wtac.
have gsf: (inc g (source f)).
by rewrite /g sf; apply /fun_set_P; red;aw; split => //; apply: lf_function.
ex_tac.
have: inc (Vf f g) (target f) by Wtac.
move:yt; rewrite tf;move=> /fun_set_P [fy sy ty] /fun_set_P [fW sW tw].
apply: function_exten=>//; try ue; move => x; rewrite sW=> xs.
have: inc (Vf (Vf f g) x) (target (Vf f g)) by Wtac.
have: inc (Vf y x) (target y) by Wtac.
rewrite tw ty; move=> /fun_set_P [fy1 sy1 ty1] /fun_set_P [fW1 sW1 tw1].
apply: function_exten=>//; try ue; rewrite sW1=> z zs.
have psg: (inc (J x z) (source g)) by rewrite /g; aw; fprops.
rewrite/g lf_source in psg; rewrite sf in gsf.
move: (spfb_VV nea neb gsf psg); aw; move=> ->.
by rewrite /g lf_V; first by aw.
Qed.
End Bunion.
Export Bunion.
Module Bproduct.
EII-5-3 Definition of the product of a family of sets
Definition productb f:=
Zo (powerset ((domain f) \times (unionb f)))
(fun z => [/\ fgraph z, domain z = domain f
& forall i, inc i (domain f) -> inc (Vg z i) (Vg f i)]).
Definition productf sf f:= productb (Lg sf f).
Lemma setXb_P f x:
inc x (productb f) <->
[/\ fgraph x, domain x = domain f &
forall i, inc i (domain f) -> inc (Vg x i) (Vg f i)].
Proof.
split; first by move/Zo_P => [] //.
move => [pa pb pc]; apply: Zo_i => //; apply/setP_P => t tx.
have gx: (sgraph x) by fprops.
have aux: inc (P t) (domain f) by rewrite - pb; apply: domain_i1.
rewrite - (gx _ tx); apply: setXp_i => //.
by apply /setUb_P; ex_tac; rewrite (pr2_V pa tx); apply: pc.
Qed.
Lemma setXf_P sf f x:
inc x (productf sf f) <->
[/\ fgraph x, domain x = sf & forall i, inc i sf -> inc (Vg x i) (f i)].
Proof.
split.
move/setXb_P; bw; move => [pa pb pc];split => //.
move => i isf; move: (pc _ isf); bw.
move => [pa pb pc]; apply/setXb_P;bw;split => //.
by move => i isf; bw; apply: pc.
Qed.
Lemma setXb_exten f x x':
inc x (productb f) -> inc x' (productb f) -> {inc (domain f), x =1g x'} ->
x = x'.
Proof.
move=> /setXb_P [fx dx px] /setXb_P [fx' dx' px'] sv.
apply: fgraph_exten=>//; ue.
Qed.
Lemma setXf_exten sf f x x':
inc x (productf sf f) -> inc x' (productf sf f) -> {inc sf, x =1g x'} ->
x = x'.
Proof.
move => pa pb pc; apply: (setXb_exten pa pb); bw.
Qed.
This lemma says that we may always assume that x is a functional graph
Lemma productb_gr x: productb (Lg (domain x) (Vg x)) = productb x.
Proof.
set_extens t; move /setXb_P => [p1]; bw => p2 p3;apply /setXb_P; bw;
split => // i idg; move: (p3 _ idg); bw.
Qed.
Lemma unionb_gr X : unionb (Lg (domain X) (Vg X)) = unionb X.
Proof.
set_extens t => /setUb_P; bw; move => [y ya]; bw => yb;
apply/setUb_P;bw; ex_tac; bw.
Qed.
Proof.
set_extens t; move /setXb_P => [p1]; bw => p2 p3;apply /setXb_P; bw;
split => // i idg; move: (p3 _ idg); bw.
Qed.
Lemma unionb_gr X : unionb (Lg (domain X) (Vg X)) = unionb X.
Proof.
set_extens t => /setUb_P; bw; move => [y ya]; bw => yb;
apply/setUb_P;bw; ex_tac; bw.
Qed.
Projection function to component i
Definition pr_i f i:= Lf (Vg ^~ i) (productb f) (Vg f i).
Lemma pri_axiom f i:
inc i (domain f) ->
lf_axiom (Vg ^~ i) (productb f) (Vg f i).
Proof. by move=> id x /setXb_P [fx dx]; apply. Qed.
Lemma pri_f f i: inc i (domain f) -> function (pr_i f i).
Proof. by move=> id; apply: lf_function; apply: pri_axiom. Qed.
Lemma pri_V f i x:
inc i (domain f) -> inc x (productb f) ->
Vf (pr_i f i) x = Vg x i.
Proof. by rewrite/pr_i=> id xp; aw; apply: pri_axiom. Qed.
Hint Resolve pri_f : fprops.
Special case where the domain is empty
Lemma setXb_0 : productb emptyset = singleton emptyset.
Proof.
move: fgraph_set0 => h.
apply: set1_pr.
by apply/setXb_P;split => //; rewrite domain_set0 => i /in_set0.
by move => z /setXb_P [_]; rewrite domain_set0; move/domain_set0_P.
Qed.
Lemma setXb_0' f: productb (Lg emptyset f) = singleton emptyset.
Proof. rewrite /Lg funI_set0; apply: setXb_0. Qed.
a product is empty iff all factors are empty
Lemma setXb_ne f: nonempty_fam f -> nonempty (productb f).
Proof.
move=> hyp.
exists (Lg (domain f)(fun i=> rep (Vg f i))).
by apply/setXb_P; split; fprops; bw => i id; bw; apply: rep_i; apply: hyp.
Qed.
Lemma setXb_ne2 f: nonempty (productb f) -> nonempty_fam f.
Proof.
move=> [x] /setXb_P [fg _ h i id]; move:(h _ id) => w; ex_tac.
Qed.
The set of graphs is a product
Lemma graphset_P1 a b z:
inc z (gfunctions a b) <->
[/\ fgraph z, domain z = a & sub z (a \times b)].
Proof.
split; first by move/Zo_P => [/setP_P pa [pb pc]].
move => [pa pb pc]; apply: Zo_i; [by apply/setP_P | done].
Qed.
Lemma graphset_P2 a b z:
inc z (gfunctions a b) <->
[/\ fgraph z, domain z = a & sub (range z) b].
Proof.
split; first by move/graphset_P1 => [pa pb] /corr_propcc [_ _ pc].
move => [pa pb pc]; apply/graphset_P1;split => //.
apply/corr_propcc;rewrite pb;split; fprops.
Qed.
Lemma setXb_sub_graphset f x:
sub (unionb f) x ->
sub (productb f) (gfunctions (domain f) x).
Proof.
move=> su t /setXb_P [ft dt hyp]; apply/graphset_P2;split => //.
move=> a /(range_gP ft) [b bt]->; apply: su.
rewrite dt in bt;union_tac.
Qed.
Lemma setXb_eq_graphset f x:
(forall i, inc i (domain f) -> Vg f i = x) ->
productb f = gfunctions (domain f) x.
Proof.
move=> prop; apply: extensionality.
apply: setXb_sub_graphset =>//.
by move=> y /setUb_P [z zd zV]; rewrite - (prop _ zd).
move=> y /graphset_P2 [fy dy sr]; apply/setXb_P;split => //.
move=> i id; rewrite (prop _ id); apply: sr.
rewrite - dy in id; fprops.
Qed.
Product of a single set
Definition product1 x a := productb (cst_graph (singleton a) x).
Lemma cst_graph_pr x y: productb (cst_graph x y) = gfunctions x y.
Proof.
have xd: x = domain (cst_graph x y) by bw.
rewrite xd - setXb_eq_graphset - xd // => i ix; bw.
Qed.
Lemma setX1_pr x a:
product1 x a = gfunctions (singleton a) x.
Proof. apply: cst_graph_pr. Qed.
Lemma setX1_P x a y:
inc y (product1 x a) <->
[/\ fgraph y, domain y = singleton a & inc (Vg y a) x].
Proof.
apply: (iff_trans (setXf_P _ _ _)); split; move=> [pa pb pc];split => //.
apply: pc; fprops.
by move => i /set1_P ->.
Qed.
Lemma setX1_pr2 f x: domain f = singleton x ->
product1 (Vg f x) x = productb f.
Proof.
move=> df.
rewrite setX1_pr -df (setXb_eq_graphset (x:= (Vg f x))) //.
by rewrite df => i /set1_P ->.
Qed.
Canonical bijection between x and product1 x a
Definition product1_canon x a :=
Lf (fun i => cst_graph (singleton a) i) x (product1 x a).
Lemma setX1_canon_axiom x a:
lf_axiom (fun i => cst_graph (singleton a) i) x (product1 x a).
Proof. move=> y yx; apply /setX1_P;split; bw;fprops. Qed.
Lemma setX1_canon_f x a: function (product1_canon x a).
Proof. apply: lf_function; apply: setX1_canon_axiom. Qed.
Lemma setX1_canon_V x a i:
inc i x -> Vf (product1_canon x a) i = cst_graph (singleton a) i.
Proof.
by rewrite /product1_canon=> iw; aw; apply: setX1_canon_axiom.
Qed.
Lemma setX1_canon_fb x a: bijection (product1_canon x a).
Proof.
apply: lf_bijective.
+ by apply: setX1_canon_axiom.
+ move=> u v ux vx eq; move: (f_equal (Vg ^~a) eq); bw; fprops.
+ move=> y /setX1_P [fy dy Vx]; ex_tac.
rewrite -dy; apply: fgraph_exten; fprops; bw.
by rewrite dy ;move=> z zd /=; bw; move /set1_P: zd => ->.
Qed.
A product of n sets (with n=2) is isomorphic to the product of two sets
Definition product2 x y := productf C2 (variant C0 x y).
Definition product2_canon x y :=
Lf (fun z => (variantLc (P z) (Q z))) (x \times y) (product2 x y).
Lemma setX2_P x y z:
inc z (product2 x y) <->
[/\ fgraph z, domain z = C2 , inc (Vg z C0) x & inc (Vg z C1) y].
Proof.
split.
move /(setXf_P) => [fa fb fc]; split => //.
move: (fc _ inc_C0_2); bw; fprops.
move: (fc _ inc_C1_2); bw; fprops.
move => [pa pb pc pd]; apply/(setXf_P); split ; bw => i ind; try_lvariant ind.
Qed.
Lemma setX2_canon_axiom x y:
lf_axiom (fun z => variantLc (P z) (Q z))
(x \times y) (product2 x y).
Proof. move=> t /setX_P [pt px qy]; apply/setX2_P;bw; split;fprops. Qed.
Lemma setX2_canon_f x y: function (product2_canon x y).
Proof. apply: lf_function; apply: setX2_canon_axiom. Qed.
Lemma setX2_canon_V x y z:
inc z (x \times y) -> Vf (product2_canon x y) z = variantLc (P z) (Q z).
Proof. rewrite /product2_canon => zp; aw; by apply: setX2_canon_axiom. Qed.
Lemma product2_canon_fb x y:
bijection (product2_canon x y).
Proof.
rewrite /product2_canon.
move: (setX2_canon_axiom (x:=x) (y:=y)) => pa.
apply: lf_bijective=>//.
move => u v /setX_P [up pux quy] /setX_P [vp pvx qvy] eq.
move: (f_equal (Vg ^~ C0) eq)(f_equal (Vg ^~ C1) eq); bw.
by apply: pair_exten=>//.
move=> z /setX2_P [fz dz Va Vb].
exists (J (Vg z C0) (Vg z C1)); aw; first fprops.
symmetry;apply: fgraph_exten;fprops; bw;try ue.
move=> t td; try_lvariant td.
Qed.
The product of singletons is a singleton
Lemma setX_set1 f: (allf f singletonp) -> singletonp (productb f).
Proof.
move=> als; apply/singletonP; split.
by apply: setXb_ne => i idf; move /singletonP: (als _ idf) => [].
move=> a b ap bp; apply: (setXb_exten ap bp)=> i id.
move /singletonP: (als _ id) => [ne eq]; apply: eq.
by move/setXb_P: ap => [_ _ ]; apply.
by move/setXb_P: bp => [_ _ ]; apply.
Qed.
Some properties of constant graphs
Definition diagonal_graphp e i :=
Zo (gfunctions i e) constantgp.
Lemma diagonal_graph_P e i x:
inc x (diagonal_graphp e i) <->
[/\ constantgp x, domain x = i & sub (range x) e].
Proof.
split; first by move /Zo_P => [] /graphset_P2 [pa pb pc] pd.
move => [pa pb pc]; apply/Zo_i => //; apply/graphset_P2; split => //.
by move: pa => [].
Qed.
Definition constant_functor i e:=
Lf (fun x => cst_graph i x) e (gfunctions i e).
Lemma cf_injective i e:
nonempty i -> injection (constant_functor i e).
Proof.
rewrite /constant_functor;move=> [x xi].
apply: lf_injective.
move=> t te; rewrite /cst_graph; apply/graphset_P2.
split; fprops; bw.
by move=> y /Lg_range_P [b be ->].
move=> u v ue ve eq;move: (f_equal (Vg ^~ x) eq); bw.
Qed.
Change of variables in a product
Definition product_compose f u :=
Lf (fun x => x \cg (graph u))
(productb f) (productf (source u) (fun k => Vg f (Vf u k))).
Section ProductCompose.
Variables (f u: Set).
Hypotheses (bu: bijection u) (tudf: target u = domain f).
Lemma pc_axiom0 c
(g:= ((triple (domain c) (range c) c)) \co u):
inc c (productb f) ->
[/\ function g, c \cg (graph u) = graph g &
(forall i, inc i (source u) ->
Vg (graph g) i = Vg c (Vg (graph u) i))].
Proof.
move=> /setXb_P [fc dc eq].
have fu: function u by fct_tac.
have cg: (c \cg (graph u) = graph g) by rewrite/g /compose; aw.
have fg: function g.
by rewrite/g; fct_tac; [ apply: function_pr; fprops| aw; ue].
split=>//.
move=> i iu; rewrite/g/compose; aw.
have id: inc i (domain (c \cg graph u)) by rewrite cg /g; fprops; aw.
have fgc: fgraph (c \cg graph u) by ue.
have fgv: fgraph (graph u) by fprops.
move/(compg_pP):(fdomain_pr1 fgc id) => [y Jv Ju].
move:(pr2_V fgv Jv); aw => <-.
move:(pr2_V fc Ju); aw.
Qed.
Lemma pc_axiom:
lf_axiom (fun x => x \cg (graph u))
(productb f) (productf (source u) (fun k => Vg f (Vf u k))).
Proof.
move=> x xp; move: (pc_axiom0 xp) => [fg cg VV].
have fu: function u by fct_tac.
apply/setXb_P; [ rewrite cg; split; bw; [ fprops | aw; bw | ]].
move => i isu;bw; rewrite (VV _ isu) -/(Vf u i).
move /setXb_P: xp => [_ _]; apply; Wtac.
Qed.
Lemma pc_f: function (product_compose f u).
Proof. by apply: lf_function; apply: pc_axiom. Qed.
Lemma pc_V x: inc x (productb f) ->
Vf (product_compose f u) x = x \cg (graph u).
Proof. by rewrite /product_compose=> xp; aw; apply: pc_axiom. Qed.
Lemma pc_VV x i:
inc x (productb f) -> inc i (source u) ->
Vg (Vf (product_compose f u) x) i = Vg x (Vf u i).
Proof.
move=> xp iu; rewrite pc_V //; move:(pc_axiom0 xp) => [fg -> ->] //.
Qed.
Lemma pc_fb: bijection (product_compose f u).
Proof.
move: (pc_f)=> fpc.
have su: surjection u by move: bu=> [_].
have spc: (source (product_compose f u) = productb f).
by rewrite /product_compose; aw.
split.
split=>//.
rewrite spc=> x y xs ys eq.
apply: (setXb_exten xs ys).
rewrite -tudf; move=> i iu; move: ((proj2 su) _ iu) => [z zs <-].
by rewrite - (pc_VV xs zs) -(pc_VV ys zs) eq.
split => //.
set nf:= Lg (source u) (fun k => Vg f (Vf u k)).
have tpc:target (product_compose f u) = productb nf.
rewrite /product_compose; aw.
rewrite tpc spc => y yp.
set x:= Lg (domain f) (fun i => Vg y (Vf (inverse_fun u) i)).
have xp: (inc x (productb f)).
apply /setXb_P; rewrite /x; bw; split; fprops.
move=> i id; bw.
rewrite -tudf in id; move: ((proj2 su) _ id) => [z zsu wz].
rewrite -wz (inverse_V2 bu zsu).
move/setXb_P: yp => [fy dy iVV].
by move: (iVV z); rewrite /nf; bw; apply.
ex_tac.
have Wt: inc (Vf (product_compose f u) x) (productb nf).
by rewrite - spc in xp; move: (Vf_target fpc xp); rewrite tpc.
apply: (setXb_exten Wt yp) => i; rewrite /nf; bw=> id.
have Wd: inc (Vf u i)(domain f) by rewrite -tudf; Wtac; fct_tac.
rewrite pc_VV // (LVg_E _ Wd) (inverse_V2 bu id) //.
Qed.
End ProductCompose.
Lemma restriction_graph2 f j:
fgraph f -> sub j (domain f) ->
Lg j (Vg f) = f \cg (diagonal j).
Proof.
move=> fgj sj.
rewrite diagonal_is_identity - compg_composef.
by rewrite/composef identity_d; apply: Lg_exten => i idx; rewrite identity_ev.
red;rewrite identity_r;split => //; apply: identity_fgraph.
Qed.
Product of f, with indices restricted to j
Definition restriction_product f j := productb (Lg j (Vg f)).
Definition pr_j f j :=
Lf (fun z => restr z j) (productb f)(restriction_product f j).
Section RestrictionProduct.
Variables (f j: Set).
Hypothesis (jdf: sub j (domain f)).
Lemma restriction_productE :
restriction_product f j = productb (restr f j).
Proof. done. Qed.
Lemma prj_axiom:
lf_axiom (fun z => restr z j)
(productb f)(restriction_product f j).
Proof.
rewrite /restriction_product=> x /setXb_P [fx dx iVV].
have sx: sub j (domain x) by rewrite dx.
apply/setXb_P; bw; split; fprops.
by move=> i ij; bw; apply: iVV; apply: jdf.
Qed.
Lemma prj_f : function (pr_j f j).
Proof. apply: lf_function; apply: prj_axiom. Qed.
Lemma prj_V x: inc x (productb f) -> Vf (pr_j f j) x = (restr x j).
Proof. by rewrite /pr_j =>ix; aw; apply: prj_axiom. Qed.
Lemma prj_VV x i:
inc x (productb f) -> inc i j
-> Vg (Vf (pr_j f j) x) i = Vg x i.
Proof.
move=> xp ij; rewrite prj_V //.
by move /setXb_P: xp => [fw dd _]; bw; ue.
Qed.
End RestrictionProduct.
If f is a family of non-empty sets, any g defined on a subset of
the domain of f with values in the partial product can be extended to the
whole product; thus pr_i and pr_j are sujective
Theorem extension_psetX f j g:
nonempty_fam f ->
fgraph g -> domain g = j -> sub j (domain f) ->
(forall i, inc i j -> inc (Vg g i) (Vg f i)) ->
exists h, [/\ domain h = domain f, fgraph h,
(forall i, inc i (domain f) -> inc (Vg h i) (Vg f i)) &
{inc j, h =1g g} ].
Proof.
move=> alne fg dg sjdf iVV.
set (h:= g \cup (unionf ((domain f) -s j)
(fun i => (singleton (J i (rep (Vg f i))))))).
have hg: sgraph h.
move=>t;case /setU2_P; first by move: fg=> [gg _]; apply: gg.
move/setUf_P=> [y _ /set1_P ->]; fprops.
have dh: domain h = domain f.
set_extens t.
move /(domainP hg) => [y /setU2_P []].
move=> Jg; apply: sjdf; rewrite -dg; bw; fprops; ex_tac.
move /setUf_P => [y' yc /set1_P Js].
by rewrite (pr1_def Js); move /setC_P: yc => [].
move => tdf; apply/(domainP hg);case: (inc_or_not t j).
by rewrite -dg; move/(domainP (proj1 fg)) => [y jg];exists y; apply:setU2_1.
move=> ntj; exists (rep (Vg f t)).
apply:setU2_2; apply /setUf_P; exists t;fprops.
have fgh: fgraph h.
split =>//.
move => x y; case /setU2_P => x1; case /setU2_P => y1.
- by move: fg=> [_ ]; apply.
- move/setUf_P: y1 => [z /setC_P [_ nzj] /set1_P eq1] eq2.
move: (domain_i1 x1); rewrite dg eq2 eq1; aw; contradiction.
- move/setUf_P: x1 => [z/setC_P [_ nzj] /set1_P eq1] eq2.
move: (domain_i1 y1); rewrite dg - eq2 eq1; aw; contradiction.
- move/setUf_P: x1 => [x1 _ /set1_P ->]; aw.
by move/setUf_P: y1 => [y1 _ /set1_P ->]; aw => ->.
have sV: forall i, inc i j -> Vg h i = Vg g i.
have sgh: (sub g h) by move=> t; rewrite /h; aw; fprops.
by move=> i; rewrite -dg=> ij; symmetry; apply: (sub_graph_ev fgh sgh ij).
exists h; split => // i id.
case: (inc_or_not i j)=> hyp; first by rewrite sV //; apply: iVV.
have ic: (inc i ((domain f) -s j)) by fprops.
have Jh: (inc (J i (rep (Vg f i))) h).
by rewrite /h; apply: setU2_2; union_tac.
by move: (pr2_V fgh Jh); aw; move=> <-; apply: rep_i; apply: alne.
Qed.
Theorem prj_fs f j: nonempty_fam f -> sub j (domain f) ->
surjection (pr_j f j).
Proof.
move=> alne sjd;split; first by apply: prj_f.
rewrite /pr_j=> y; aw; move/setXb_P.
bw;move => [fy dy iVVy].
have iVV: (forall i, inc i j -> inc (Vg y i) (Vg f i)).
by move => i ij; move: (iVVy _ ij); bw.
move: (extension_psetX alne fy dy sjd iVV) => [h [dh fgh iVVh sv]].
have hp: (inc h (productb f)) by apply/setXb_P.
ex_tac; rewrite prj_V //; rewrite -dh in sjd; symmetry.
by apply: fgraph_exten; bw;fprops=> x; rewrite dy => xd /=; bw; rewrite sv.
Qed.
Lemma pri_fs f k: nonempty_fam f ->
inc k (domain f) -> surjection (pr_i f k).
Proof.
move=> alne kd.
set (j:= singleton k).
have sjd: (sub j (domain f)) by move=> t; move/set1_P => ->.
have cpc: (product1_canon (Vg f k) k) \coP (pr_i f k).
split; first by apply: setX1_canon_f.
by apply: pri_f.
by rewrite /product1_canon /pr_i; aw.
have fcpx:(function ((product1_canon (Vg f k) k) \co (pr_i f k))).
by fct_tac.
have prjc: (pr_j f j = (product1_canon (Vg f k) k) \co (pr_i f k)).
apply: function_exten => //.
- by apply: prj_f=>//.
- by rewrite /pr_j/pr_i; aw.
- rewrite /pr_j/pr_i/product1_canon/product1; aw.
- rewrite/restriction_product.
have: (Lg j (Vg f)) = cst_graph (singleton k) (Vg f k).
by apply: Lg_exten => t /set1_P ->.
by rewrite/restriction_product; move->.
- move=> x xs.
have xp: inc x (productb f) by move: xs;rewrite /pr_j lf_source.
have xsk: inc x (source (pr_i f k)) by rewrite /pr_i lf_source.
have aux1: inc (Vf (pr_i f k) x) (Vg f k).
have : (target (pr_i f k) = Vg f k) by rewrite/pr_i; aw.
by move=> <-; Wtac; apply: pri_f=>//.
aw=>//; rewrite setX1_canon_V //.
rewrite prj_V //.
have xp1: inc x (productb f) by [].
move /setXb_P: xp1 => [fx dx iVVx].
have ssk: sub (singleton k) (domain x).
by move=> xw eq1; bw; rewrite (set1_eq eq1) dx.
rewrite/j; apply: fgraph_exten; rewrite /cst_graph;fprops;bw.
move=> z zk /=; bw;rewrite (set1_eq zk) pri_V //.
apply: (left_compose_fs2 cpc).
by rewrite - prjc; apply: prj_fs.
move: (setX1_canon_fb (Vg f k) k)=> [ h _]; apply: h.
Qed.
if X and Y are functional graphs, with same domain, productb X is a
subset of productb g if and only if the same holds for each component
(for one implication, the small product must be non-empty)
Lemma setXb_monotone1 f g:
domain f = domain g ->
(forall i, inc i (domain f) -> sub (Vg f i) (Vg g i))
-> sub (productb f) (productb g).
Proof.
move=> dfdg sVV x /setXb_P [fx dx iVV].
apply/setXb_P; rewrite -dfdg;split => //; move => i ifg; apply: sVV; fprops.
Qed.
Lemma setXb_monotone2 f g:
domain f = domain g ->
nonempty_fam f ->
sub (productb f) (productb g) ->
(forall i, inc i (domain f) -> sub (Vg f i) (Vg g i)).
Proof.
move=> dfdg alne sfg i id j jV.
have jt: (inc j (target (pr_i f i))) by rewrite/ pr_i; aw.
move:((proj2 (pri_fs alne id)) _ jt) => [x xs <-].
move: xs; rewrite /pr_i lf_source=>xs.
rewrite pri_V //.
by move /setXb_P: (sfg _ xs) => [fx dx]; apply; rewrite -dfdg.
Qed.
EII-5-5 associativity of products of sets
Given a product with domain I, and a partition J of I, we can consider the set of mappings that associate to each j in J the partial product. This is a product. Associativity says that this product of products is isomorphic to the initial product. Implies associativity of cardinal productDefinition prod_assoc_axioms f g :=
partition_w_fam g (domain f).
Definition prod_assoc_map f g :=
Lf(fun z => (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) z)))
(productb f)
(productf (domain g) (fun l => (restriction_product f (Vg g l)))).
Lemma pam_axiom f g:
prod_assoc_axioms f g ->
lf_axiom(fun z => (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) z)))
(productb f)
(productf (domain g) (fun l => (restriction_product f (Vg g l)))).
Proof.
move=> [fg md u] t td; apply/setXb_P; bw; split;fprops.
move=> i id; bw.
have: (restriction_product f (Vg g i) = target (pr_j f (Vg g i))).
by rewrite /pr_j; aw.
move=>->; Wtac; last by rewrite/pr_j lf_source.
apply: prj_f=>//; move=> z; rewrite -u=> tu; union_tac.
Qed.
Lemma pam_f f g:
prod_assoc_axioms f g ->
function (prod_assoc_map f g).
Proof. by move => h; apply: lf_function; apply: pam_axiom. Qed.
Lemma pam_V f g x:
prod_assoc_axioms f g -> inc x (productb f) ->
Vf (prod_assoc_map f g) x = (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) x)).
Proof. by rewrite /prod_assoc_map=> a xp; aw; apply: pam_axiom. Qed.
Lemma pam_fi f g:
prod_assoc_axioms f g ->
injection (prod_assoc_map f g).
Proof.
move=> pa; split; first by apply: pam_f.
have sp:(source (prod_assoc_map f g) = productb f).
by rewrite /prod_assoc_map; aw.
rewrite sp {sp} => x y xs ys.
rewrite (pam_V pa xs)(pam_V pa ys) => sv.
move: pa=> [fg md ugdf].
apply: (@setXb_exten _ x y xs ys) => i; rewrite - ugdf.
move/setUb_P => [z zd iV].
have svf: sub (Vg g z) (domain f) by move=> t tv; rewrite - ugdf; union_tac.
move: (f_equal (Vg ^~ z) sv); bw;rewrite prj_V // prj_V // => sv1.
move/setXb_P: xs => [fx dx _];move/setXb_P: ys => [fy dy _].
move:(f_equal (Vg ^~i) sv1); bw; ue.
Qed.
Theorem pam_fb f g:
prod_assoc_axioms f g ->
bijection (prod_assoc_map f g).
Proof.
move=> pa; split; first by apply: pam_fi.
split; first by apply: pam_f.
have sp: source (prod_assoc_map f g) = productb f
by rewrite /prod_assoc_map; aw.
have tp: target (prod_assoc_map f g) =
(productf (domain g) (fun l => restriction_product f (Vg g l))).
by rewrite /prod_assoc_map; aw.
rewrite sp tp; move=> y yp; move /setXf_P: (yp); bw; move => [fy dy iVr].
move: (pa) => [fg md ugdf].
have sVd: forall i, inc i (domain g) -> sub (Vg g i) (domain f).
by move=> i id v vV; rewrite -ugdf; union_tac.
pose h i := Lf (fun z => (Vg (Vg y i) z)) (Vg g i) (unionb f).
have ta:forall i, inc i (domain g) ->
lf_axiom (fun z => Vg (Vg y i) z) (Vg g i) (unionb f).
move=> i id x xV; move: (sVd _ id) =>sVdi.
apply: (@setUb_i _ x); first by apply: sVdi=>//.
move: (iVr _ id); bw; move/setXb_P => [fgV deq]; bw => rel.
move: (rel _ xV); bw.
have afp: forall i, inc i (domain g) -> function_prop (h i) (Vg g i) (unionb f).
move=> i id; rewrite /h.
by split; first (by apply: lf_function; apply: ta); aw.
move: (extension_partition_thm pa afp) => [x [[[fx sx tx] ag] etc]].
have gxp: inc (graph x) (productb f).
apply/setXb_P; rewrite (f_domain_graph fx) - sx;split; fprops.
move=> i ix; rewrite -/(Vf x i).
move: ix; rewrite sx -ugdf; move/(setUb_P) =>[z zdg iV].
move: (ag _ zdg)=> [_ _ eq]; rewrite (eq _ iV) /h.
aw; last by apply: (ta _ zdg).
move: (iVr _ zdg); bw; move/setXb_P => [qa]; bw => eq1 res.
move: (res _ iV); bw.
have Wt: inc (Vf (prod_assoc_map f g)(graph x))(target (prod_assoc_map f g)).
by Wtac; apply: pam_f.
ex_tac; symmetry; apply: (setXf_exten (x:=y) (x':= Vf _ _ ) yp).
by rewrite - tp.
move=> i id.
have aux2: sub (Vg g i) (domain f) by apply: sVd.
have aux3: sub (Vg g i) (domain (graph x)) by aw; ue.
rewrite pam_V=> //; bw; rewrite prj_V //.
move: (iVr _ id); bw; move/setXb_P=> [fgy]; bw => qa qb.
apply: fgraph_exten; bw; fprops.
move: (ag _ id)=> [ aa bb cc].
move => j; rewrite qa => jd; move: (cc _ jd); bw.
by rewrite -/(Vf x j) => ->; rewrite/h; aw; apply: ta.
Qed.
Case where the domain is partitioned in two sets
Lemma variantLc_prop x y:
variantLc x y = Lg C2 (variant C0 x y).
Proof. by []. Qed.
Lemma prod_assoc_map2 f g:
prod_assoc_axioms f g -> domain g = C2
-> (productb f) \Eq
((restriction_product f(Vg g C0)) \times (restriction_product f (Vg g C1))).
Proof.
move=> pam dg.
eqtrans (productf (domain g) (fun l => (restriction_product f (Vg g l)))).
exists (prod_assoc_map f g).
split; first (by apply: pam_fb); rewrite /prod_assoc_map; aw.
eqsym.
exists (product2_canon (restriction_product f (Vg g C0))
(restriction_product f (Vg g C1))).
rewrite /bijection_prop/product2_canon; aw; split => //.
by apply: product2_canon_fb.
rewrite dg; congr (productb _); apply: Lg_exten.
move=> x xt; try_lvariant xt; fprops.
Qed.
The product of two sets is equipotent to one of them if the other one
is a singleton. Implies that one is a unit for cardinal product.
Lemma first_proj_fb x y:
singletonp y -> bijection (first_proj (x \times y)).
Proof.
move=> sy.
set f:=first_proj (x \times y).
have gp: sgraph (x \times y) by apply: setX_graph.
have sp: source f = (x \times y) by rewrite /f/first_proj; aw.
have tp: target f = domain(x \times y) by rewrite /f/first_proj; aw.
have fp: function (first_proj (x \times y)) by apply: first_proj_f.
move: sy=> [t ty].
split.
split=>//; rewrite sp=> a b ap bp.
do 2 rewrite first_proj_V =>//.
move: ap bp; rewrite ty.
move /setX_P=> [ap _] /set1_P pa /setX_P [bp _ /set1_P qb] peq.
apply: pair_exten=>//; ue.
split => //.
rewrite sp tp; move=>z /(domainP gp) [p px]; ex_tac.
rewrite first_proj_V =>//; aw.
Qed.
A product is isomorphic to a partial product if missing factors are
singletons. Implies that one can be removed in cardinal products.
Lemma prj_fb f j:
sub j (domain f) ->
(forall i, inc i ((domain f) -s j) -> singletonp (Vg f i)) ->
bijection (pr_j f j).
Proof.
set (k:= ((domain f) -s j)) => sjd als.
have sk: sub k (domain f) by apply: sub_setC.
have sr: singletonp (restriction_product f k).
by apply:setX_set1;fprops; red; bw => i ik /=; bw; apply: als.
set (g:= variantLc j ((domain f) -s j)).
have paa: prod_assoc_axioms f g by apply: (is_partition_with_complement sjd).
set (f1:= prod_assoc_map f g).
have bf1: bijection f1 by apply: pam_fb.
have ff1:function f1 by fct_tac.
set (xa:= restriction_product f (Vg g C0)).
set (xb:= restriction_product f (Vg g C1)).
set (f2:= inverse_fun (product2_canon xa xb)).
have dg: domain g = C2 by rewrite /g; bw.
have Va: Vg g C0 = j by rewrite /g; bw.
have Vb: Vg g C1 = k by rewrite /g; bw.
have bf2: bijection f2 by apply: inverse_bij_fb; apply: product2_canon_fb.
have ff2: function f2 by fct_tac.
have sf2tf1: source f2 = target f1.
rewrite lf_target ifun_s lf_target dg; (congr (productb _)).
by apply: Lg_exten=>//; move=> v vt; try_lvariant vt.
set (f3:= first_proj (xa \times xb)).
have sb: singletonp xb.
by rewrite /xb /restriction_product Vb; apply: sr.
have bf3: bijection f3 by apply: first_proj_fb.
have sf3tf2: source f3 = target f2 by rewrite ifun_t ! lf_source.
have cf3f3: f3 \coP f2 by rewrite /f3/f2; split=>//; fct_tac.
have bcf3f2: bijection (f3 \co f2) by apply: compose_fb.
have cf3f2f1: (f3 \co f2) \coP f1 by split; aw=>//; fct_tac.
suff: (pr_j f j = (f3 \co f2) \co f1) by move=> ->; apply: compose_fb=>//.
have sp: source (pr_j f j) = source f1 by rewrite !lf_source.
have nexb: nonempty xb by move/singletonP: sb => [].
apply: function_exten; aw.
by apply: prj_f=>//.
by fct_tac.
by rewrite !lf_target setX_domain // /xa Va.
rewrite sp=> x xs.
move xW: (Vf f1 x) =>y.
move yW: (Vf f2 y)=>z.
have yt: inc y (source f2) by rewrite -xW sf2tf1 ; fprops.
have zt: inc z (target f2) by rewrite -yW; Wtac.
have Jg2: (inc (J y z) (graph f2)) by rewrite -yW; Wtac.
have fp: function (product2_canon xa xb) by apply: setX2_canon_f.
have zs: inc z (source (product2_canon xa xb)) by move: zt; rewrite ifun_t.
have zp: inc z (xa \times xb) by move: zs; rewrite lf_source.
aw; last by rewrite xW.
rewrite xW yW first_proj_V //.
move: Jg2; rewrite /f2; aw; move/igraph_pP => Jg3.
move: (Vf_pr2 fp Jg3); aw; rewrite setX2_canon_V =>//.
move=> eq; move: (f_equal (Vg ^~C0) eq); bw; move => <-.
rewrite -xW /f1 pam_V //; bw; try rewrite Va =>//.
by rewrite dg; fprops.
by move: xs; rewrite lf_source.
Qed.
EII-5-6 distributivity formulae
Given a double family Xij, union over I of intersection over J is intersection of union, and conversely. The new index set is a product.Theorem distrib_union_inter f:
(forall l, inc l (domain f) -> nonempty (domain (Vg f l))) ->
unionf (domain f) (fun l => intersectionb (Vg f l)) =
intersectionf (productf (domain f) (fun l => (domain (Vg f l))))
(fun g => (unionf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
Proof.
move=> alne; set_extens s => xu.
apply: setIf_i.
by apply: setXb_ne; fprops; red; red; bw;move=> i id; bw; apply: alne.
move /setUf_P: xu => [y yf si] j /setXf_P [fgj dj]; bw => aa.
move: (aa _ yf); bw => bb; move: (setIb_hi si bb) => cc; union_tac.
ex_middle nsu.
set gl:= (fun l => Zo (domain (Vg f l)) (fun i => ~ (inc s (Vg (Vg f l) i)))).
have ne: (nonempty (productf (domain f) gl)).
apply: setXb_ne; fprops; red; red;bw=> i id; bw;rewrite /gl; set jl:=Zo _ _ .
case: (emptyset_dichot jl) =>//; move=> je; case: nsu; union_tac.
apply: setIb_i; [by apply /domain_set0P; apply: alne | ].
by move=> j jd; ex_middle hyp; empty_tac1 j; apply: Zo_i.
move: ne=> [y] /setXf_P [fy dy iVz].
have yp: inc y (productf (domain f) (fun l => domain (Vg f l))).
apply/setXf_P; split =>// i id.
by case /Zo_P: (iVz _ id).
by move /setUf_P: (setIf_hi xu yp) => [z zdf sv]; case/Zo_P: (iVz _ zdf).
Qed.
Theorem distrib_inter_union f:
intersectionf (domain f) (fun l => unionb (Vg f l)) =
unionf (productf (domain f) (fun l => (domain (Vg f l))))
(fun g => (intersectionf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
Proof.
set_extens x => xi; last first.
move /setUf_P: xi => [y /setXf_P [_ dy Vd] xi1].
case: (emptyset_dichot (domain f)) => ne.
by move: xi1; rewrite ne setIf_0 => /in_set0.
apply: (setIf_i ne) => j jd; move: (setIf_hi xi1 jd)=> u; union_tac.
pose prop j a := (inc a (domain (Vg f j)) /\ inc x (Vg (Vg f j) a)).
pose yf j:= choose (prop j).
have p1: (forall j, inc j (domain f) -> (prop j (yf j))).
move=> j jd; apply: choose_pr; move /setUb_P:(setIf_hi xi jd).
by move => [y y1 y2];exists y; split.
apply: (@setUf_i _ (Lg (domain f) yf)).
by apply/setXf_P; split;fprops; bw => i id; bw; move: (p1 _ id)=>[].
case: (emptyset_dichot (domain f)) => ne.
by move: xi; rewrite ne setIf_0 => /in_set0.
by apply: (setIf_i ne) => j jd; bw; move: (p1 _ jd) => [].
Qed.
Variants of distributivity of union and intersection of Xij
when one index set has two elements
Lemma distrib_union2_inter f g:
nonempty (domain f) -> nonempty (domain g) ->
(intersectionb f) \cup (intersectionb g) =
intersectionf((domain f) \times (domain g))
(fun z => ((Vg f (P z)) \cup (Vg g (Q z)))).
Proof.
move => nef neg.
have nep:nonempty ((domain f) \times (domain g)).
by move: nef neg=> [x xd][y yd]; exists (J x y); fprops.
set_extens x => xu.
apply: (setIf_i nep)=> j /setX_P [pj p1 p2]; case /setU2_P: xu=>p.
by move: (setIb_hi p p1)=>a; fprops.
by move: (setIb_hi p p2)=>a; fprops.
case: (inc_or_not x (intersectionb f))=> p; [fprops | apply: setU2_2].
move: nef neg; move/domain_set0P => nef1 /domain_set0P neg1.
have [z1 z1d nexv]: (exists2 z1, inc z1 (domain f) & ~ (inc x (Vg f z1))).
ex_middle bad;case: p.
apply: (setIb_i nef1) => i id; ex_middle xx; case: bad; ex_tac.
apply: (setIb_i neg1) => i id; move /(setIf_P _ nep): xu => h.
by move: (h _ (setXp_i z1d id)); aw; case/setU2_P.
Qed.
Lemma distrib_inter2_union f g:
(unionb f) \cap (unionb g) =
unionf((domain f) \times (domain g))
(fun z => ((Vg f (P z)) \cap (Vg g (Q z)))).
Proof.
set_extens x.
move /setI2_P => [] /setUb_P [y yd xf] /setUb_P [z zd xg].
apply/setUf_P; exists (J y z);aw; fprops.
move /setUf_P=> [y /setX_P [yp yf yg] /setI2_P [pa pb]].
apply/setI2_P; split; union_tac.
Qed.
Distributivity of product over union and intersection
Theorem distrib_prod_union f:
productf (domain f) (fun l => unionb (Vg f l)) =
unionf (productf (domain f) (fun l => (domain (Vg f l))))
(fun g => (productf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
Proof.
case: (emptyset_dichot (domain f)) => p.
by rewrite p /productf /Lg !funI_set0 !setXb_0 setUf_1 funI_set0 setXb_0.
case: (p_or_not_p (forall l, inc l (domain f) -> nonempty (domain (Vg f l)))).
move=> alned.
set_extens x => xp; last first.
move: xp => /setUf_P [y /setXf_P [fy dy py] /setXf_P [fx dx px]].
by apply/setXf_P;split => // i idf; apply: (@setUb_i _ (Vg y i)); fprops.
move: xp=> /setXf_P [gx dx px].
have : (nonempty (productf (domain f) (fun l =>
(Zo (domain (Vg f l)) (fun i => (inc (Vg x l) (Vg (Vg f l) i))))))).
apply: setXb_ne; fprops; red;red; bw;move=> i id; bw.
move: (px _ id).
by move /setUb_P=> [y yd iVV]; exists y; apply: Zo_i.
move=> [y] /setXf_P [fy dy py].
by apply: (@setUf_i _ y); apply/setXf_P;
split => // i idf;case /Zo_P: (py _ idf).
move=> special.
have [x xd de]: exists2 l, inc l (domain f) & domain (Vg f l) = emptyset.
ex_middle aux; case: special=> l ld.
case: (emptyset_dichot (domain (Vg f l)))=>//; move=>pp.
case: aux; ex_tac.
have ->: productf (domain f) (fun l => domain (Vg f l)) = emptyset.
apply /set0_P => t/setXf_P [pa pb pc].
by move: (pc _ xd); rewrite de => /in_set0.
rewrite setUf_0;apply /set0_P => t /setXf_P [pa pb pc].
by move: (pc _ xd); move/domain_set0_P: de => ->;rewrite setUb_0 => /in_set0.
Qed.
Theorem distrib_prod_intersection f:
(forall l, inc l (domain f) -> nonempty (domain (Vg f l))) ->
productf (domain f) (fun l => intersectionb (Vg f l)) =
intersectionf (productf (domain f) (fun l => (domain (Vg f l))))
(fun g => (productf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
Proof.
move=> alne.
have nep:(nonempty (productb (Lg (domain f) (fun l => domain (Vg f l))))).
by apply: setXb_ne; fprops;red; red; bw => i id;bw; apply: alne.
set_extens x => xp.
apply: (setIf_i nep) =>j /setXf_P [fj dj iVd].
move /setXf_P: xp=>[fx xd iVi];apply/setXf_P; split => // i id.
move: (iVi _ id) => ivdi; apply: (setIb_hi ivdi (iVd _ id)).
move: nep=> [u up]; move: (setIf_hi xp up) => /setXf_P [fx dx iVx].
apply/setXf_P; split => // i id; apply: setIb_i; [ | move=> j jd].
by apply/domain_set0P; apply: alne.
have: (nonempty (productf (domain f) (fun l =>
(Zo (domain (Vg f l)) (fun jj => l = i -> jj = j))))).
apply: setXb_ne; fprops; red; red;bw=> k kd; bw.
case: (equal_or_not k i)=> ki; first by exists j; apply: Zo_i; ue.
move: (alne _ kd) => [y yd]; exists y; apply: Zo_i=>//.
move=> [y] /setXf_P [fy dy iV]; move: (iV _ id); move/Zo_P => [_ aux].
have yd: (inc y (productf (domain f) (fun l => domain (Vg f l)))).
by apply /setXf_P; split => // k kdf; move /Zo_P: (iV _ kdf) =>[].
move/setXf_P: (setIf_hi xp yd) =>[_ _ rel].
by move: (rel _ id); rewrite aux.
Qed.
A partition on each X_i induces a partition on the product
Lemma partition_product f:
(forall l, inc l (domain f) -> (partition_w_fam (Vg f l) (unionb (Vg f l))))
-> partition_w_fam(Lg(productf (domain f) (fun l => domain (Vg f l)) )
(fun g => (productf (domain f) (fun l => Vg (Vg f l) (Vg g l)))))
( productf (domain f) (fun l => unionb (Vg f l))).
Proof.
move=> alp;split; first (by fprops).
move=> i j; rewrite Lg_domain => ip jp; bw.
case: (equal_or_not i j); first (by left); move=> ij; right.
red; set int:= _ \cap _.
case: (emptyset_dichot int) =>// ei.
case: ij; move: ei=> [xi]; rewrite/int; aw.
move: ip jp => /setXf_P [fi di vi] /setXf_P [fj dj vj]
/setI2_P [] /setXf_P [fx dx eq1] /setXf_P [_ _ eq2].
apply: fgraph_exten =>//; try ue.
move=> x; rewrite di => xd; move: (eq1 _ xd) (eq2 _ xd) (alp _ xd).
rewrite /partition_w_fam; move=> eq3 eq4 [fgV md _].
move: (vi _ xd) (vj _ xd)=> eq5 eq6; case: (md _ _ eq5 eq6) =>// dij.
empty_tac1 (Vg xi x).
rewrite distrib_prod_union /unionb;bw;apply: setUf_exten =>//.
move => i ip /=; bw.
Qed.
Special cases when one index set has only two elements
Lemma distrib_prod2_union f g:
product2 (unionb f)(unionb g) =
unionf((domain f)\times (domain g))
(fun z => (product2 (Vg f (P z)) (Vg g (Q z)))).
Proof.
rewrite /product2; set_extens x.
move /setXf_P => [fx dx iV].
have Tat: inc C0 C2 by fprops.
have Tbt: inc C1 C2 by fprops.
move: (iV _ Tat) (iV _ Tbt); bw.
move=> /setUb_P [u ud uVV] /setUb_P [v vd vVV]; apply/setUf_P.
exists (J u v); fprops; apply/setXf_P;split => //.
move=> i ind; try_lvariant ind; aw.
move/setUf_P=>[y] /setX_P [yp py qy] /setXf_P [fx dx iV]; apply/setXf_P.
split => // i idx; move: (iV _ idx); try_lvariant idx; move=> ?; union_tac.
Qed.
Lemma distrib_prod2_inter f g:
product2 (intersectionb f)(intersectionb g)=
intersectionf((domain f)\times (domain g)) (fun z =>
(product2 (Vg f (P z)) (Vg g (Q z)))).
Proof.
rewrite/product2; set_extens x.
move /setXf_P=> [fx dx iVv].
case: (emptyset_dichot (domain f \times domain g)) => xx.
move: (iVv _ inc_C0_2) (iVv _ inc_C1_2); bw; rewrite /intersectionb.
case: (setX_0 xx) => ->; rewrite setIf_0.
by move => /in_set0.
by move => _ /in_set0.
apply :(setIf_i xx) => j.
move/setX_P => [jp pj qj]; apply/setXf_P;split => // i id.
move: (iVv _ id); try_lvariant id => Vi; first by apply: (setIf_hi Vi pj).
by apply: (setIf_hi Vi qj).
case: (emptyset_dichot (domain f \times domain g)) => xx.
by rewrite xx setIf_0 => /in_set0.
move/(setIf_P _ xx) => h.
move: xx => [j jp]; move: (h _ jp) => /setXf_P [pa pb pc].
move /setX_P: jp => [_ ja jb].
have nef: nonempty f by apply /domain_set0P; ex_tac.
have neg: nonempty g by apply /domain_set0P; ex_tac.
have aux: (forall i j, inc i (domain f) -> inc j (domain g) ->
(inc (Vg x C0) (Vg f i) /\ inc (Vg x C1) (Vg g j))).
move=> i k id kd.
have Jd: (inc (J i k) ((domain f) \times (domain g))) by fprops.
move: (h _ Jd) => /setXf_P [fx dx px].
by move: (px _ inc_C0_2)(px _ inc_C1_2); bw; aw => qa qb; split.
apply/setXf_P;split => // i itp; try_lvariant itp; apply setIb_i => // k kd.
by move: (aux _ _ kd jb) => [].
by by move: (aux _ _ ja kd) => [].
Qed.
Lemma distrib_product2_union f g:
(unionb f) \times (unionb g) =
unionf((domain f) \times (domain g)) (fun z =>
((Vg f (P z)) \times (Vg g (Q z)))).
Proof.
move: (distrib_prod2_union f g); rewrite/product2 => distr.
set_extens x.
move /setX_P=> [xp px qx].
set (v := variantLc (P x) (Q x)).
have: inc v (productb (variantLc (unionb f) (unionb g))).
apply/setXb_P;rewrite/v; bw; split; fprops => i it; try_lvariant it.
rewrite /productf in distr; rewrite variantLc_prop distr.
move /setUf_P => [y p1 p2]; apply/setUf_P; ex_tac.
move /setXf_P: p2=> [fv]; bw => dv p; apply/setX_P.
move: (p _ inc_C0_2) (p _ inc_C1_2); rewrite /v; bw; split;fprops.
move /setUf_P=> [y yp /setX_P [px xp xq]].
set (qx := variantLc (P x) (Q x)).
have:(inc qx (productb (variantLc (unionb f) (unionb g)))).
move: distr; rewrite/productf -variantLc_prop; move=>->.
union_tac; apply/setXf_P;rewrite /qx; bw;split; fprops.
move=> i it; try_lvariant it; fprops.
move/setXf_P=> [fq dx vqx]; apply/setX_P.
move: (vqx _ (set2_1 C0 C1)) (vqx _ (set2_2 C0 C1)).
by rewrite /qx;bw; split.
Qed.
Lemma distrib_product2_inter f g:
(intersectionb f) \times (intersectionb g) =
intersectionf((domain f) \times (domain g)) (fun z =>
((Vg f (P z)) \times (Vg g (Q z)))).
Proof.
move: (distrib_prod2_inter f g); rewrite / product2=> distr.
set_extens x => xp.
set (qx := variantLc (P x) (Q x)).
have: inc qx (productb (variantLc (intersectionb f) (intersectionb g))).
move /setX_P: xp =>[xp pxf qxg]; apply/setXf_P.
rewrite /qx /C2; bw;split; fprops.
by move=> i ind; try_lvariant ind.
move: distr; rewrite /productf -variantLc_prop; move=> -> qxp.
case: (emptyset_dichot (domain f \times domain g)) => xx.
by move: qxp; rewrite xx setIf_0 => /in_set0.
apply /(setIf_P _ xx)=> j jp;move: (setIf_hi qxp jp).
move /setX_P : xp => [pa pb pc].
move => /setXf_P [fgq dq vq]; apply/setX_P.
move: (vq _ inc_C0_2)(vq _ inc_C1_2); rewrite /qx;bw;split;fprops.
set (qx := variantLc (P x) (Q x)).
case: (emptyset_dichot (domain f \times domain g)) => xx.
by move: xp; rewrite xx setIf_0 => /in_set0.
have: inc qx (productb (variantLc (intersectionb f) (intersectionb g))).
move: distr; rewrite /productf variantLc_prop; move =>->.
apply (setIf_i xx)=> j jp; move: (setIf_hi xp jp) => /setX_P [_ Px Qx].
apply/setXf_P; rewrite /qx;split; fprops; bw.
move=> i it; try_lvariant it; fprops.
move/setXf_P => [_ _]; rewrite /qx; bw => qv.
move: xx=> [w wp]; move: (setIf_hi xp wp) => /setX_P [px _ _]; apply /setX_P.
move: (qv _ (set2_1 C0 C1)) (qv _ (set2_2 C0 C1)); bw; split; fprops.
Qed.
A variant of distributivity, valid if the domain of the double family
is a rectangle; works only for intersection.
Theorem distrib_inter_prod f sa sb:
(nonempty sa \/ nonempty sb) ->
intersectionf sb (fun k => productf sa (fun i=> Vg f (J i k))) =
productf sa (fun i => intersectionf sb (fun k=> Vg f (J i k))).
Proof.
move=> aux ; set_extens x => xi.
case: (emptyset_dichot sb) => nb.
by move: xi; rewrite nb setIf_0 => /in_set0.
move: (nb)=> [y yb]; move /setXf_P: (setIf_hi xi yb) => [fx dx px].
apply /setXf_P;split=> // i id; apply: (setIf_i nb).
by move => j jsb; move: (setIf_hi xi jsb) => /setXf_P [_ _]; apply.
move /setXf_P: xi => [fx dx px].
case: (emptyset_dichot sb) => nsb.
case: aux; last by rewrite nsb; case /nonemptyP.
by move => [t ta]; move: (px _ ta); rewrite nsb setIf_0 => /in_set0.
apply: (setIf_i nsb) => j jsb; apply/ setXf_P;split => // i id.
move: (px _ id)=> xi; apply: (setIf_hi xi jsb).
Qed.
Lemma distrib_prod_inter2_prod f g:
fgraph f -> fgraph g -> domain f = domain g ->
(productb f) \cap (productb g) =
productf (domain f) (fun i => (Vg f i) \cap (Vg g i)).
Proof.
move=> ff fg dfdg; set_extens x.
move=> /setI2_P [] /setXb_P [fx dx vx] /setXb_P [ _ dx' vx'].
apply /setXf_P;split => // i id.
by apply: setI2_i; [apply: vx | apply: vx'; ue].
move /setXf_P=> [fx dx vx]; apply: setI2_i.
by apply /setXb_P;split => // i idf; case /setI2_P: (vx _ idf).
by apply /setXb_P; rewrite - dfdg; split => // i idf; case /setI2_P: (vx _ idf).
Qed.
Lemma distrib_inter_prod_inter f g:
domain f = domain g ->
product2 (intersectionb f) (intersectionb g) =
intersectionf (domain f) (fun i => product2 (Vg f i) (Vg g i)).
Proof.
move=> dfdg; set (sb:= domain f).
pose (h:= Lg (product C2 sb)
(fun i => Yo (P i = C0) (Vg f(Q i)) (Vg g (Q i)))).
move: TP_ne1 => ns.
have <-: intersectionf sb(fun k => productf C2 (fun i => Vg h (J i k)))
= intersectionf sb (fun i => product2 (Vg f i) (Vg g i)).
apply: setIf_exten.
move=> i isb /=; congr (productb _ );apply: Lg_exten=> x xp.
rewrite /h; try_lvariant xp; aw; try Ytac0 =>//; apply:setXp_i; fprops.
have aux: nonempty C2 \/ nonempty sb by left; exists C0; fprops.
rewrite (distrib_inter_prod h aux); congr (productb _);apply: Lg_exten=> x xp.
try_lvariant xp; [ | rewrite /intersectionb - dfdg]; apply: setIf_exten;
move => i id; rewrite /h; bw; aw; (try Ytac0 => //); apply:setXp_i; fprops.
Qed.
Lemma distrib_prod2_sum A f:
A \times (unionb f) = unionb (Lg (domain f) (fun x => A \times (Vg f x))).
Proof.
set_extens t.
move=> /setX_P [pt ptA] /setUb_P [y ydf Qv]; apply/setUb_P; bw.
by exists y; bw; apply :setX_i.
move/setUb_P; bw; move=> [y ydf];bw; move=> /setX_P [pr PA QV].
by apply/setX_P; split => //;apply /setUb_P;exists y.
Qed.
Product of two products of family of sets
Definition prod_of_fgraph x x':=
Lg (domain x)(fun i => J (Vg x i) (Vg x' i)).
Definition prod_of_products_canon f f':=
Lf (fun w => prod_of_fgraph (P w) (Q w))
((productb f) \times (productb f'))
(productf (domain f)(fun i => (Vg f i) \times (Vg f' i))).
Definition prod_of_product_aux f f' :=
fun i => ((Vf f i) \times (Vf f' i)).
Definition prod_of_prod_target f f' :=
fun_image(source f)(prod_of_product_aux f f').
Definition prod_of_products f f' :=
Lf (prod_of_product_aux f f')(source f)(prod_of_prod_target f f').
Lemma prod_of_products_f f f':
function (prod_of_products f f').
Proof. apply:lf_function => x xs; apply /funI_P; ex_tac. Qed.
Lemma prod_of_products_V f f' i:
inc i (source f) ->
Vf (prod_of_products f f') i = (Vf f i) \times (Vf f' i).
Proof.
rewrite/prod_of_products => isf; aw => x xs; apply /funI_P; ex_tac.
Qed.
Section ProdProdCanon.
Variables (f f': Set).
Hypotheses (ff:function f) (ff': function f').
Hypothesis (sfsf:source f = source f').
Lemma prod_of_function_axioms x x':
inc (graph x) (productb (graph f)) -> inc (graph x') (productb (graph f')) ->
lf_axiom (fun i => J (Vf x i) (Vf x' i))
(source f) (union (prod_of_prod_target f f')).
Proof.
move=> gp gp' y ys.
apply: (@setU_i _ ((Vf f y) \times (Vf f' y)));
last by apply/funI_P; ex_tac.
apply/setXp_i.
move /setXb_P: gp=> [fgx dgx p1]; apply:p1; rewrite f_domain_graph //.
move /setXb_P: gp'=> [fgx dgx p1]; apply:p1; rewrite f_domain_graph //; ue.
Qed.
Lemma prod_of_function_V x x' i:
inc x (productb (graph f)) -> inc x' (productb (graph f')) ->
inc i (source f) ->
Vg (prod_of_fgraph x x') i = J (Vg x i) (Vg x' i).
Proof.
rewrite /prod_of_fgraph=> xp x'p isf.
by bw; move/setXb_P: xp=> [_ -> _];rewrite f_domain_graph.
Qed.
Lemma prod_of_function_f x x':
inc x (productb (graph f)) -> inc x' (productb (graph f')) ->
inc (prod_of_fgraph x x')
(productb (graph (prod_of_products f f'))).
Proof.
move=> xp x'p.
move: (prod_of_products_f f f') => fp.
move:(f_domain_graph ff) => eq1.
move/setXb_P: (xp)=> [fgd dx]; rewrite eq1 => ivv.
move/setXb_P: x'p=> [fgd' dx'] => ivv'.
apply/setXb_P; rewrite (f_domain_graph fp) lf_source.
rewrite /prod_of_fgraph; split; [ fprops | bw; ue | ].
move=> i idx; bw; last by rewrite dx eq1.
rewrite -/(Vf _ _) (prod_of_products_V _ idx).
apply:setXp_i; first by apply: (ivv i idx).
by apply: ivv'; rewrite (f_domain_graph ff') - sfsf.
Qed.
Lemma popc_target_aux:
productb(Lg (domain (graph f))
(fun i => (Vg (graph f) i) \times (Vg (graph f') i))) =
productb (graph (prod_of_products f f')).
Proof.
congr (productb _).
move: (prod_of_products_f f f') => fp.
apply: fgraph_exten;bw;fprops; first by aw; rewrite lf_source.
move=> x xd /=; bw.
move: xd; rewrite (f_domain_graph ff) => xd.
symmetry; exact: (prod_of_products_V f' xd).
Qed.
Lemma popc_axioms:
lf_axiom(fun w => prod_of_fgraph (P w) (Q w))
((productb (graph f)) \times (productb (graph f')))
(productb (graph (prod_of_products f f'))).
Proof.
move=> x xd /=.
by move/setX_P: xd => [pxd px qx]; apply: prod_of_function_f.
Qed.
Lemma popc_V w:
inc w ((productb (graph f)) \times (productb (graph f'))) ->
Vf (prod_of_products_canon (graph f) (graph f')) w =
prod_of_fgraph (P w) (Q w).
Proof.
by move=> h; rewrite lf_V // /productf popc_target_aux; apply: popc_axioms.
Qed.
Lemma popc_fb:
bijection (prod_of_products_canon (graph f) (graph f')).
Proof.
move: (f_domain_graph ff) (f_domain_graph ff') => fa f'a.
apply: lf_bijective.
- by rewrite/productf popc_target_aux //; apply: popc_axioms=>//.
- move => x y xs ys sv.
move: (xs)(ys) => /setX_P [xp px qx] /setX_P [yp py qy].
have sj: forall i, inc i (source f) ->
J (Vg (P x) i) (Vg (Q x) i) = J (Vg (P y) i) (Vg (Q y) i).
move => j js.
by rewrite -(prod_of_function_V px qx js) -(prod_of_function_V py qy js) sv.
apply: pair_exten => //.
apply: (setXb_exten px py).
move => i; rewrite fa => js; exact (pr1_def (sj _ js)).
apply: (setXb_exten qx qy).
move => i; rewrite f'a - sfsf => js;exact (pr2_def (sj _ js)).
- rewrite /productf popc_target_aux => y.
move: (prod_of_products_f f f') => fc.
move /setXb_P=> [fy]; aw; rewrite lf_source => pa pb.
set (xa:= Lf (fun i => P (Vg y i)) (source f)(union (target f))).
set (xb:= Lf (fun i => Q (Vg y i)) (source f)(union (target f'))).
have ta: lf_axiom (fun i => P (Vg y i)) (source f) (union (target f)).
move=> t tf /=; move:(pb _ tf); rewrite -/(Vf _ _) (prod_of_products_V f' tf).
move/setX_P => [_ iP _]; apply: (@setU_i _ (Vf f t)) => //; Wtac.
have tb: lf_axiom (fun i => Q (Vg y i)) (source f) (union (target f')).
move=> t tf /=; move:(pb _ tf); rewrite -/(Vf _ _) (prod_of_products_V f' tf).
move/setX_P => [_ _ iQ]; apply: (@setU_i _ (Vf f' t)) => //; Wtac.
have fxa: function xa by apply: lf_function.
have fxb: function xb by apply: lf_function.
have sxa: source xa = source f by rewrite /xa; aw.
have sxb: source xb = source f by rewrite /xb; aw.
have ixa :inc (graph xa) (productb (graph f)).
apply /setXb_P;rewrite fa (f_domain_graph fxa);split; fprops.
move => i isf; rewrite /xa -/(Vf _ _) (lf_V ta isf).
move: (pb _ isf); rewrite -/(Vf _ _) (prod_of_products_V f' isf).
by move/setX_P => [_ ].
have ixb :inc (graph xb) (productb (graph f')).
apply /setXb_P;rewrite f'a (f_domain_graph fxb);split; fprops.
by rewrite sxb - sxa - sfsf.
rewrite - sfsf; move => i isf; rewrite /xb -/(Vf _ _) (lf_V tb isf).
move: (pb _ isf); rewrite -/(Vf _ _) (prod_of_products_V f' isf).
by move/setX_P => [_ ].
exists (J (graph xa) (graph xb));fprops; aw.
rewrite /prod_of_fgraph (f_domain_graph fxa) lf_source.
symmetry;apply: fgraph_exten;fprops; bw; first by ue.
move => i isf /=; bw.
rewrite /xa -/(Vf _ _) (lf_V ta isf) /xa -/(Vf _ _) (lf_V tb isf).
move: (pb _ isf); rewrite -/(Vf _ _) (prod_of_products_V f' isf).
by move/setX_P => [-> _].
Qed.
End ProdProdCanon.
Definition ext_map_prod_aux x f := fun i=> Vg (f i) (Vg x i).
Definition ext_map_prod I src trg f :=
Lf (fun x => Lg I (ext_map_prod_aux x f))
(productf I src ) (productf I trg).
Definition ext_map_prod_axioms I src trg f :=
forall i, inc i I ->
[/\ fgraph (f i), domain (f i) = src i & sub (range (f i)) (trg i)].
Section ExtMapProd.
Variables (I: Set) (src trg f: Set-> Set).
Hypothesis ax: ext_map_prod_axioms I src trg f.
Lemma ext_map_prod_taxioms:
lf_axiom (fun x => Lg I (ext_map_prod_aux x f))
(productf I src) (productf I trg).
Proof.
move=> x /setXf_P [pa pb pc]; apply/setXf_P; split; fprops; bw.
rewrite /ext_map_prod_aux => i iI; bw.
move : (ax iI) => [fi dfi sr]; apply: sr.
by apply: inc_V_range=>//;rewrite dfi; apply: pc.
Qed.
Lemma ext_map_prod_f : function (ext_map_prod I src trg f).
Proof. by apply: lf_function; apply: ext_map_prod_taxioms. Qed.
Lemma ext_map_prod_V x: inc x (productf I src) ->
Vf (ext_map_prod I src trg f) x = Lg I (ext_map_prod_aux x f).
Proof. rewrite /ext_map_prod => h; aw; apply: ext_map_prod_taxioms. Qed.
Lemma ext_map_prod_VV x i:
inc x (productf I src) -> inc i I ->
Vg (Vf (ext_map_prod I src trg f) x) i = Vg (f i) (Vg x i) .
Proof. move=> xp iI; rewrite ext_map_prod_V //; bw. Qed.
End ExtMapProd.
Lemma ext_map_prod_composable I p1 p2 p3 g f h:
ext_map_prod_axioms I p1 p2 f ->
ext_map_prod_axioms I p2 p3 g ->
(forall i, inc i I -> h i = (g i) \cf (f i)) ->
(forall i, inc i I -> (g i) \cfP (f i)) ->
ext_map_prod_axioms I p1 p3 h.
Proof.
move=> emp1 emp2 alh alfc x xs.
move: (emp1 _ xs) (emp2 _ xs) => [fgg dg srg] [fgf df srf].
move: (alfc _ xs)(alh _ xs) => fca ->.
have fgc: fgraph ((g x) \cf (f x)) by apply: composef_fgraph.
have dfc :domain((g x) \cf (f x)) = domain (f x) by rewrite /composef; bw.
rewrite dfc dg; split=>//.
move=> y /(range_gP fgc) [z zdg ->];rewrite composef_ev //; last by ue.
apply: srf; apply/(range_gP fgf); exists (Vg (f x) z) => //.
rewrite df; apply: srg; apply: inc_V_range =>//; ue.
Qed.
Lemma ext_map_prod_compose I p1 p2 p3 g f h:
ext_map_prod_axioms I p1 p2 f ->
ext_map_prod_axioms I p2 p3 g ->
(forall i, inc i I -> h i = (g i) \cf (f i)) ->
(forall i, inc i I -> (g i) \cfP (f i)) ->
(ext_map_prod I p2 p3 g) \co (ext_map_prod I p1 p2 f) =
(ext_map_prod I p1 p3 h).
Proof.
move=> emp1 emp2 alh alfc.
set f1:= (ext_map_prod I p2 p3 g).
set f2:= (ext_map_prod I p1 p2 f).
set f3:= (ext_map_prod I p1 p3 h).
move: (ext_map_prod_composable emp1 emp2 alh alfc) => emp3.
have cee: (f1 \coP f2).
split; first by apply: ext_map_prod_f.
by apply: ext_map_prod_f.
rewrite /f1/f2/ext_map_prod; aw.
have fcee: (function (f1 \co f2)) by fct_tac.
apply: function_exten=>//; try solve [ rewrite/f1/f2/f3/ext_map_prod; aw].
by apply: ext_map_prod_f =>//.
aw; move=> x xs/=; aw.
have xp: inc x (productf I p1) by move: xs; rewrite /f2/ext_map_prod; aw.
set (t:= Vf f2 x).
have tv: t = Lg I (ext_map_prod_aux x f) by rewrite /t/f2 ext_map_prod_V //.
have: (Vf f1 t = Lg I (ext_map_prod_aux t g)).
rewrite /f1 ext_map_prod_V //.
have tf2: (target f2 = productf I p2) by rewrite/f2/ext_map_prod; aw.
rewrite/t -tf2; Wtac.
by rewrite/f2; apply: ext_map_prod_f =>//.
have: (Vf f3 x = Lg I (ext_map_prod_aux x h)) by rewrite/f3 ext_map_prod_V //.
move=> -> ->.
apply: Lg_exten.
move => e ei; rewrite tv /ext_map_prod_aux; bw.
move: (alfc _ ei)=> aux.
rewrite (alh _ ei) composef_ev //.
move: (emp1 _ ei)=> [fgg -> srg].
by move /setXf_P: xp => [_ dx]; apply.
Qed.
Lemma ext_map_prod_fi I p1 p2 f:
ext_map_prod_axioms I p1 p2 f ->
(forall i, inc i I -> injective_graph (f i)) ->
injection (ext_map_prod I p1 p2 f).
Proof.
move=> emp alli; split.
by apply: ext_map_prod_f.
rewrite /ext_map_prod; rewrite lf_source; move => x y xp yp eql.
apply: (setXf_exten xp yp).
move=>i iI.
move: (ext_map_prod_VV emp xp iI); move: (ext_map_prod_VV emp yp iI).
rewrite eql; move=> -> aux.
move: (emp _ iI)=> [_ df sr].
move: (alli _ iI); move=> [ff tmp]; apply: tmp=>//.
by rewrite df; move: xp=> /setXf_P [_ dx]; apply.
by rewrite df; move /setXf_P: yp => [_ dx]; apply.
Qed.
Lemma ext_map_prod_fs I p1 p2 f:
ext_map_prod_axioms I p1 p2 f ->
(forall i, inc i I -> range (f i) = p2 i) ->
surjection (ext_map_prod I p1 p2 f).
Proof.
move=> emp als;
set g :=(ext_map_prod I p1 p2 f).
have fg: function g by apply: ext_map_prod_f.
split => //.
have semp: source g = productf I p1 by rewrite /g /ext_map_prod lf_source.
have temp: target g = productf I p2 by rewrite /g /ext_map_prod lf_target.
rewrite semp temp; move=> y yt.
have ext: (forall i, inc i I -> exists2 z, inc z (p1 i) & Vg y i = Vg (f i) z).
move=> i iI; move: (emp _ iI) => [ff df sr].
move /setXf_P : yt => [fy dy ip2]; move: (ip2 _ iI).
by rewrite - (als _ iI); move/(range_gP ff); rewrite df.
pose pr i:= (fun z => inc z (p1 i) /\ Vg y i = Vg (f i) z).
set x:= Lg I (fun i => choose (pr i)).
have xp: forall i, inc i I -> pr i (Vg x i).
move=> i iI; rewrite/x; bw; apply: choose_pr.
by move: (ext _ iI) => [s xa xb]; exists s.
have ixp: (inc x (productf I p1)).
apply /setXf_P; rewrite /x; split; fprops; bw; rewrite -/x.
by move=> i iI; bw; move: (xp _ iI) => [].
have xsq: (inc x (source g)) by ue.
have iWp: (inc (Vf g x)(productf I p2)) by rewrite -temp; Wtac.
ex_tac; apply: (setXf_exten iWp yt); move=> i iI /=.
by rewrite ext_map_prod_VV //;move: (xp _ iI) => [].
Qed.
Lemma fun_set_to_prod1 F f i:
fgraph F -> inc i (domain F) ->
function f -> target f = productb F ->
function_prop (pr_i F i \co f) (source f) (Vg F i) /\
(forall x, inc x (source f) -> Vf (pr_i F i \co f) x = Vg (Vf f x) i).
Proof.
move=> fF id ff tfpF.
have aux: (pr_i F i) \coP f.
split => //; first by apply: pri_f=>//.
symmetry; rewrite /pr_i; aw.
rewrite /function_prop {2 3} /pr_i; aw; split; first split; aw.
fct_tac.
move=> x xs; aw; rewrite pri_V //; rewrite -tfpF; fprops.
Qed.
The two sets (prod Fi)^E and prod (Fi^E) are isomorphic
Definition fun_set_to_prod src F :=
Lf (fun f =>
Lg (domain F)( fun i=> (graph ( (pr_i F i) \co
(triple src (productb F) f)))))
(gfunctions src (productb F))
(productb (Lg (domain F) (fun i=> gfunctions src (Vg F i)))).
Section FunSetToProd.
Variables (src F: Set).
Hypothesis (fF: fgraph F).
Lemma fun_set_to_prod2 f gf:
inc gf (gfunctions src (productb F)) ->
f = (triple src (productb F) gf) -> function_prop f src (productb F).
Proof.
move=> igf eq.
move: (gfun_set_hi igf) => [g [fg sg tg gg]].
have -> // : f = g.
by rewrite eq - sg -tg -gg; apply: corresp_recov1; move: fg=> [ res _].
Qed.
Lemma fun_set_to_prod3:
lf_axiom(fun f =>
Lg (domain F)( fun i=> (graph (compose (pr_i F i)
(triple src (productb F) f)))))
(gfunctions src (productb F))
(productb (Lg (domain F) (fun i=> gfunctions src (Vg F i)))).
Proof.
move=> x xs.
set (f:= triple src (productb F) x).
move: (fun_set_to_prod2 xs (refl_equal f)) => [ff sf tf].
apply/setXf_P;split; fprops; bw => i id; bw.
move: (fun_set_to_prod1 fF id ff tf) => [[fc sc tg] vc].
rewrite -/f - sf - sc -tg; apply: gfun_set_i; fprops.
Qed.
Lemma fun_set_to_prod4 :
function_prop (fun_set_to_prod src F) (gfunctions src (productb F))
(productb (Lg (domain F) (fun i=> gfunctions src (Vg F i)))).
Proof.
rewrite/fun_set_to_prod; red;aw; split => //.
by apply: lf_function; apply: fun_set_to_prod3.
Qed.
Definition fun_set_to_prod5 F f :=
ext_map_prod (domain F) (fun i=> source f)(fun i=> Vg F i)
(fun i => (graph (compose (pr_i F i) f))).
Lemma fun_set_to_prod6 f:
function f -> target f = productb F ->
(function (fun_set_to_prod5 F f) /\
(fun_set_to_prod5 F f) \coP (constant_functor (domain F)(source f) )/\
(fun_set_to_prod5 F f) \co (constant_functor (domain F)(source f)) =f).
Proof.
move=> ff tfpF.
set (tf := fun_set_to_prod5 F f).
have ftf: function tf.
rewrite /tf/fun_set_to_prod5; apply: ext_map_prod_f.
move=> x xs.
move: (fun_set_to_prod1 fF xs ff tfpF) => [[fc sc tc] vc].
by split; fprops; aw; rewrite -tc; apply: f_range_graph.
have ttf:(productb F = target tf).
rewrite /tf/fun_set_to_prod5/ext_map_prod.
aw; rewrite /productf; apply: f_equal; apply: fgraph_exten; fprops; bw.
by move=> x xd /=; bw.
have ctf: tf \coP (constant_functor (domain F)(source f)).
split; fprops.
rewrite /constant_functor; apply: lf_function.
move => x xs /=; apply/graphset_P2.
rewrite/cst_graph; bw;split; fprops.
have aux: fgraph (Lg (domain F) (fun _ : Set => x)) by fprops.
move=> y => /(range_gP aux) [b ]; rewrite Lg_domain => h ->; bw.
set (k:= cst_graph (domain F) (source f)).
have: (domain F = domain k) by rewrite/k; bw.
move=> ->; rewrite /constant_functor; aw.
rewrite - setXb_eq_graphset.
by rewrite /tf/fun_set_to_prod5/ext_map_prod; aw.
rewrite /k; bw => i id; bw.
split=> //; split=>//.
have ta1: lf_axiom [eta cst_graph (domain F)]
(source f) (gfunctions (domain F) (source f)).
move=> y yd; rewrite /gfunctions.
apply: Zo_i; last by bw; split; fprops.
apply /setP_P; move=> t => /funI_P [z zd ->]; fprops.
symmetry; apply: function_exten =>//; try fct_tac.
by rewrite /constant_functor; aw.
rewrite /tf/fun_set_to_prod5/ext_map_prod; aw.
by rewrite /productf tfpF Lg_recovers //.
move=> x xsf; rewrite /constant_functor; aw; bw.
have cgd: inc (cst_graph (domain F) x)
(productf (domain F) (fun _ : Set => source f)).
rewrite/cst_graph; apply/setXf_P.
by split; fprops; bw; move => j jd; bw.
have:inc (Vf f x) (productb F) by rewrite - tfpF; fprops.
have: (inc (Vf tf (cst_graph (domain F) x)) (productb F)).
rewrite ttf; Wtac; rewrite /tf/fun_set_to_prod5/ext_map_prod; aw.
move=> p1 p2; apply: (setXb_exten p2 p1).
move=> i idf /=; rewrite /tf/fun_set_to_prod5 ext_map_prod_V //.
bw; rewrite /ext_map_prod_aux /cst_graph; bw.
set cp:= (pr_i F i) \co f.
rewrite -/(Vf cp x) /cp;aw.
rewrite pri_V //.
split => //; [ by apply: pri_f | by rewrite /pr_i; aw].
move => j jd.
move: (fun_set_to_prod1 fF jd ff tfpF) => [[fcf sc tc] vc].
split; fprops.
by rewrite - sc; fprops; aw.
by rewrite -tc;apply: f_range_graph=>//.
Qed.
Lemma fun_set_to_prod7 f g:
(forall i, inc i (domain F) -> inc (f i) (gfunctions src (Vg F i))) ->
g = ext_map_prod (domain F) (fun i=> src)(Vg F) f ->
(forall i, inc i (domain F) ->
f i = graph ((pr_i F i) \co (g \co (constant_functor (domain F) src) ))).
Proof.
move=> allf geq i idf.
set f1:= (constant_functor (domain F) src).
have fct: function f1.
rewrite /f1 /constant_functor; apply: lf_function.
move=> x xd; apply/ graphset_P2; rewrite /cst_graph.
by split; fprops ; bw; move => w /Lg_range_P [b _ ->].
have fg: (function g).
rewrite geq; apply: ext_map_prod_f.
move=> x xd; move:(gfun_set_hi (allf _ xd))=> [h [? ? th gh]].
rewrite -gh f_domain_graph //; split; fprops.
by rewrite -th; apply: f_range_graph=>//.
have cpa: g \coP f1.
split=>//.
rewrite geq/f1/ext_map_prod/constant_functor; aw.
rewrite /productf.
set (k:= (Lg (domain F) (fun _ : Set => src))).
have dkdf: (domain k = domain F) by rewrite /k;bw.
have aux: (forall i, inc i(domain k) -> Vg k i = src).
by move=> j jd; rewrite /k; bw;ue.
by rewrite -dkdf; apply: (setXb_eq_graphset aux).
have fcf: function (g \co f1) by fct_tac.
have cpb: (pr_i F i) \coP (g \co f1).
split => //; first (by apply: pri_f).
rewrite geq /pr_i/ext_map_prod; aw.
rewrite/productf Lg_recovers //.
have fctr: function ((pr_i F i) \co (g \co f1)) by fct_tac.
move: (allf _ idf) => aux; move: (gfun_set_hi aux).
move=> [h [fh sh th gh]].
have sf1: source f1 = source h by rewrite /f1/pr_i/constant_functor; aw.
have ta1: lf_axiom (fun x0 => cst_graph (domain F) x0)
src (gfunctions (domain F) src).
move=> y yd; rewrite /cst_graph/gfunctions.
apply: Zo_i; last by bw; split; fprops.
apply /setP_P; move=> t /funI_P [z zd ->]; fprops.
suff: (h = (pr_i F i) \co (g \co f1)) by move=> <-; ue.
apply: function_exten =>//.
by rewrite /pr_i/constant_functor; aw.
by rewrite /pr_i/constant_functor; aw.
rewrite /f1; move => x xh.
have xs: inc x src by rewrite - sh.
have xs2: inc x (source (constant_functor (domain F) src)).
by rewrite /constant_functor; aw.
have aax: ext_map_prod_axioms (domain F) (fun _ : Set => src)(Vg F) f.
move=> z zs; move: (allf _ zs) => p;move: (gfun_set_hi p).
move=> [k [fk sk tk gk]].
rewrite -gk - sk -tk f_domain_graph //;split; fprops.
by apply: f_range_graph=>//.
set q:= cst_graph (domain F) x.
have qp: inc q (productf (domain F) (fun _ : Set => src)).
apply/setXf_P; rewrite/q; bw; split; fprops.
by move=> k kd; bw.
have si: Vf (constant_functor (domain F) src) x = q.
by rewrite /Vf/constant_functor /Lf; aw; bw.
have seq: (x = Vg q i) by rewrite /q; bw.
aw; rewrite si geq ext_map_prod_V //.
set s:= (Lg (domain F) (ext_map_prod_aux q f)).
have isp: inc s (productb F).
rewrite /s /ext_map_prod_aux.
apply/setXb_P; split; fprops; bw.
move=> j jd; rewrite /q;bw.
move: (allf _ jd) => p;move: (gfun_set_hi p).
move=> [k [fk sk tk gk]]; rewrite -gk -tk; rewrite -/(Vf _ _ ); Wtac.
aw; rewrite pri_V => //.
by rewrite /s; bw; rewrite /ext_map_prod_aux /Vf gh - seq.
Qed.
Lemma fun_set_to_prod8: bijection (fun_set_to_prod src F).
Proof.
move: (fun_set_to_prod4); set (g :=fun_set_to_prod src F).
move => [fg sg tg].
split.
split =>//; move=> x y; rewrite sg => xs ys.
move :(gfun_set_hi xs) (gfun_set_hi ys).
move=> [x0 [fx0 sx0 tx0 gx]][x1 [fx1 sx1 tx1 gx1]] eq.
move:(fun_set_to_prod3)=> ta.
move: eq; rewrite /g/fun_set_to_prod; aw; clear ta; move => eq.
rewrite - gx - gx1; congr (graph _).
apply: function_exten=>//; (try ue) => x2 x2s.
apply: (setXb_exten (f := F)); [ ue| rewrite sx0 - sx1 in x2s; ue |].
move=> i iF;
move: (fun_set_to_prod1 fF iF fx0 tx0) (fun_set_to_prod1 fF iF fx1 tx1).
move=> [[fc0 sc0 tc0] vc0] [[fc1 sc1 tc1] vc1].
have x0c: (x0 = triple src (productb F) x).
by rewrite - sx0 -tx0 -gx corresp_recov1 //; move: fx0=>[cx0 _].
have x1c: (x1 = triple src (productb F) y).
by rewrite - sx1 -tx1 -gx1 corresp_recov1 //; move: fx1=>[cx1 _].
have cc: ((pr_i F i) \co x0 = (pr_i F i) \co x1).
move: (f_equal (Vg ^~i) eq); bw;rewrite - x0c -x1c => eq1.
apply: function_exten1 =>//; aw.
by rewrite - vc0 //; rewrite sx0 - sx1 in x2s; rewrite cc - vc1 //.
split => // y.
rewrite sg {1} /g /fun_set_to_prod lf_target.
move/setXf_P=> [fy]; bw; move=> dy py.
set (x:= Lf (fun u=> Lg (domain F) (fun i=> Vg (Vg y i) u)) src (productb F)).
have sx: source x = src by rewrite /x; aw.
have tx: target x = productb F by rewrite /x; aw.
have fx: function x.
rewrite /x; apply: lf_function.
move=> t ts; apply/setXb_P; split; fprops; bw.
move => i idf; bw;move: (py _ idf); bw=> xpp.
move: (gfun_set_hi xpp) => [k [fk sk tk gk]].
have ->: (Vg (Vg y i) t = Vf k t) by rewrite /Vf gk.
rewrite -tk; Wtac.
have gs: inc (graph x) (gfunctions src (productb F)).
rewrite - sx -tx; apply: gfun_set_i=> //.
ex_tac.
move: (fun_set_to_prod3) => ax.
rewrite /g/fun_set_to_prod; aw; clear ax.
apply: fgraph_exten; bw;fprops =>//.
move=> z zd; bw;move: (py _ zd); bw; move => Vzg.
have xp: (x = triple src (productb F) (graph x)).
by rewrite - sx -tx corresp_recov1 //; move: fx=>[cx _].
rewrite - xp.
move: (gfun_set_hi Vzg) => [x1 [fx1 sx1 tx1 gx1]].
suff: (x1 = (pr_i F z) \co x) by move => <-.
apply: function_exten =>//; try fct_tac; try (rewrite /pr_i; aw; ue).
by apply: pri_f =>//.
move=> x0 z0s.
have x0s: inc x0 src by ue.
have x0s': inc x0 (source x) by ue.
have cc: (pr_i F z) \coP x.
split => //; [apply: pri_f=>//| rewrite /pr_i; aw; ue].
have Wp: inc (Vf x x0) (productb F) by Wtac.
aw; rewrite pri_V // /x; aw; first by bw; rewrite/Vf; ue.
move=> t ts /=; apply /setXb_P; split;fprops; bw.
move=> i id; bw; move: (py _ id); bw => aux.
move: (gfun_set_hi aux) => [x2 [fx2 sx2 tx2 gx2]].
rewrite -tx2 -gx2; change (inc (Vf x2 t) (target x2)); Wtac.
Qed.
End FunSetToProd.
End Bproduct.
Export Bproduct.