proposition: Lemma Exercise4_9b r (P := E48P r) n: lattice r -> distributive_lattice1 r -> finite_set (substrate r) -> nonempty (substrate r) -> natp n -> order_width (induced_order r P) n -> exists g A f, let r' := (order_product g) in [/\ order_fam g, (allf g total_order), cardinal (domain g) = n, sub A (substrate r') & sublattice r' A /\ order_isomorphism f r (induced_order r' A)].
proof: Proof. move => lr dlr fsr nesr nN eh. move: (proj1 lr) => or. have s1: sub P (substrate r). by rewrite /P/E48P => t /setC1_P [] /Zo_P [ok _] _. move: (iorder_osr or s1) => [orp sr]. move: (Exercise4_5d orp nN eh) => [X1]. rewrite (iorder_sr or s1); move=> [pX1 cX1 aX1]. have aX2: forall x, inc x X1 -> total_order (induced_order r x). move => x x1; move: (aX1 _ x1) => /total_subordersP []; rewrite iorder_sr// => xssxP. by rewrite iorder_trans. move: (the_least_pr (proj1 lr) (Exercise4_7c lr fsr nesr)). set zr := (the_least r); move=> [zrr zrl]. case: (equal_or_not n \0c) => nnz. move: (proj1(proj1 pX1)). rewrite nnz in cX1; rewrite (card_nonempty cX1) setU_0 => pe. have sis: irreds r = singleton zr. rewrite (Exercise4_7f lr fsr nesr); rewrite -/P -pe -/zr. by apply: set1_pr => //; fprops; move => z;case /setU1_P => // /in_set0. have srs: substrate r = singleton zr. apply: set1_pr => // x xr. have pa: (E47S r x) = singleton zr. apply: set1_pr; first by apply Exercise4_7g. move => z /Zo_P [sa [sb _]]. have : inc z (irreds r) by apply: Zo_i. by rewrite sis => /set1_P. move: (Exercise4_7l lr fsr nesr xr); rewrite pa. by rewrite (supremum_singleton or zrr). set g:= Lg emptyset id. have c1: order_fam g by rewrite /g; hnf; aw => x; case; case. have c2: (allf g total_order) by rewrite /g; hnf; aw => x /in_set0. have c3: cardinal (domain g) = n. by rewrite /g nnz; aw; rewrite cardinal_set0. set r' := (order_product g). have srr: substrate r' = singleton emptyset. rewrite /r' (proj2 (order_product_osr _)) //. rewrite /prod_of_substrates /fam_of_substrates /g; aw. by apply: setXb_0'. have or': order r' by apply: (proj1 (order_product_osr _)). have sr1: singletonp (substrate r) by exists zr. have sr2: singletonp (substrate r') by exists emptyset. move: (set1_order_is2 or or' sr1 sr2) => [f isf]. set A := substrate r'. have c4: sub A (substrate r') by fprops. exists g, A, f;split => //; split. have esr: inc emptyset (substrate r') by rewrite srr; fprops. have aux: gle r' emptyset emptyset by order_tac. move => x y; rewrite /A srr => /set1_P -> /set1_P ->. rewrite (sup_comparable1 or' aux) (inf_comparable1 or' aux); split;fprops. by rewrite iorder_substrate. pose Xf i := i +s1 zr. have sXr: forall x, inc x X1 -> sub (Xf x) (substrate r). move => x x1 t;case /setU1_P => xe; last by ue. apply: s1; move: pX1 => [[<- pb] pc]; union_tac. set g:= Lg X1 (fun z => (induced_order r (Xf z))). have c2: (allf g total_order). rewrite /g; hnf; aw; move => s xs;rewrite LgV//. move: (sXr _ xs) => sr'; move: (iorder_osr or sr') => [pa pb]. split => //; rewrite pb. move: (aX2 _ xs) => to1 x y xa ya. suff: gle r x y \/ gle r y x by case => le1;[left | right];apply /iorder_gleP. have sa: sub s (substrate r). apply: sub_trans sr'; move => t; rewrite /Xf; fprops. move: xa ; case /setU1_P. move: ya; case /setU1_P. move: (proj2 to1); rewrite iorder_sr // => h. move => iys ixs; move: (h _ _ ixs iys). case => h1; [left | right]; apply: (iorder_gle1 h1). by move => -> ixs; right; apply: zrl; apply: sa. by move => ->; left; apply: zrl; apply: sr'. have c1: order_fam g by hnf;move => x xd; exact (proj1 (c2 _ xd)). pose Fo i x := Zo (Xf i) (fun z => gle r z x). have Fozr: forall i x, inc x (substrate r) -> inc zr (Fo i x). move => i x xsr; apply: Zo_i; [ by rewrite /Xf; fprops | by apply: zrl]. have Fon: forall i x, inc x (substrate r) -> nonempty (Fo i x). move => i x xsr; exists zr; apply: (Fozr _ _ xsr). have Fos: forall i x, inc i X1 -> sub (Fo i x) (substrate (Vg g i)). move => i x iX; rewrite /g LgV//; rewrite iorder_sr; fprops; apply: Zo_S. have Fof: forall i x, inc i X1 -> finite_set (Fo i x). move => i x iX;apply: sub_finite_set fsr; apply: sub_trans (sXr _ iX). apply: Zo_S. have For: forall i x, inc i X1 -> sub (Fo i x) (substrate r). move => i x iX. have sa: sub (Fo i x) (Xf i) by apply: Zo_S. apply: (sub_trans sa (sXr _ iX)). pose fo i x := the_greatest (induced_order r (Fo i x)). have fop: forall i x, inc i X1 -> inc x (substrate r) -> greatest (induced_order r (Fo i x)) (fo i x). move => i x iX xsr. have idg: inc i (domain g) by rewrite /g; aw. move: (For _ x iX) => sf. move:(c2 _ idg) => tor. have sa: sub (Fo i x) (Xf i) by apply: Zo_S. have so: (induced_order (Vg g i) (Fo i x)) = (induced_order r (Fo i x)). by rewrite /g LgV//; rewrite iorder_trans. have ori: order (induced_order (Vg g i) (Fo i x)). by rewrite so;apply: (proj1 (iorder_osr or _)). move:(the_greatest_pr (ori) (finite_subset_torder_greatest tor (Fof _ _ iX) (Fon _ _ xsr) (Fos _ _ iX))). by rewrite so. pose fp x := Lg X1 (fun i => fo i x). set r' := order_product g. move: (order_product_osr c1) => [ppa ppb]. have ta: forall x, inc x (substrate r) -> inc (fp x) (substrate r'). rewrite ppb /prod_of_substrates /fp/g/fam_of_substrates. move => x xsr; apply/setXf_P;aw;split;fprops. move => i iX1; rewrite !LgV//. move: (fop _ _ iX1 xsr) => [h _]; move: h. move: (sXr _ iX1) => s2. have s3: sub (Fo i x) (Xf i) by apply: Zo_S. rewrite (iorder_sr or (sub_trans s3 s2)) (iorder_sr or s2); apply: s3. set A:= fun_image (substrate r) fp. have c4: sub A (substrate r'). by rewrite /A; move => t /funI_P [z zsr ->]; apply: ta. case: (emptyset_dichot X1) => X1ne. by case: nnz;rewrite - cX1 X1ne cardinal_set0. move: (X1ne) => [repX repXX]. have sxp: forall x, inc x (substrate r) -> E47S r x = unionb (Lg X1 (fun i => Fo i x)). move: pX1 => [[pa pc] pb]. move => x xsr; set_extens t. move /Zo_P => [tsr [si le1]]; apply /setUb_P; aw. case: (equal_or_not t zr). by move => ->; exists repX => //; rewrite LgV//; apply: Fozr. move => ntz. have : inc t P by apply: Zo_i; [ apply: Zo_i | move /set1_P]. rewrite -pa => /setU_P [y ty yx];ex_tac; rewrite LgV//; apply: Zo_i => //. rewrite /Xf; fprops. move => /setUb_P [y ]; rewrite Lgd=> y1; rewrite LgV//; move=>/Zo_P. rewrite /Xf; aw; move => [sa sb]; case/ setU1_P: sa => ty; apply /Zo_P. have: inc t P by rewrite -pa; union_tac. by move => /Zo_P [] /Zo_P [ra rb] _. move: (Exercise4_7d lr fsr nesr) => /Zo_P. by rewrite -/zr; move => [sc sd]; split => //; ue. have sxp1: forall x, inc x (substrate r) -> x = supremum r (fun_image X1 (fun l => supremum r (Fo l x))). move => x xsr; move: (sxp _ xsr) => aux. set X := (Lg X1 (Fo^~ x)). move: (f_equal (supremum r) aux). rewrite (Exercise4_7l lr fsr nesr xsr). have suXdr: sub (unionb X) (substrate r). move =>z /setUb_P; rewrite /X; aw;move => [y yx1]; rewrite LgV// => /Zo_P. by move=> [zb _]; apply: (sXr _ yx1). set h := Lg (unionb X) id. have ra: fgraph h by rewrite /h; fprops. have rx: fgraph X by rewrite /X; fprops. have rb: sub (range h) (substrate r). by rewrite /h =>t /Lg_range_P [b bu ->]; apply: suXdr. have rc: (domain h) = unionb X by rewrite /h /X; aw; split;split;fprops. have rd: (forall l, inc l (domain X) -> has_sup_graph r (restr h (Vg X l))). move => l ld; apply Exercise4_7i => //. have re: fgraph (restr h (Vg X l)) by fprops. have svd: sub (Vg X l) (domain h) by rewrite /h; aw => t tv; union_tac. move => t /(range_gP re); aw; move=> [z ze ->]. have zu: inc z (unionb X) by union_tac. by rewrite restr_ev // /h LgV//;apply: suXdr. have re: has_sup_graph r h by apply Exercise4_7i => //. move: (sup_A2 or ra rb rc rd) => [_ xx]; move: (xx re). rewrite /sup_graph /h -/X Lg_range Lg_range. have -> : (fun_image (unionb X) id) = (unionb X). set_extens t; first by by move /funI_P => [a au ->]. move => tu; apply /funI_P; ex_tac. move => ->. have ww: forall l, inc l X1 -> range (restr (Lg (unionb X) id) (Vg X l)) = (Fo l x). move => l lx1; rewrite {2}/X; aw. have qa: fgraph (restr (Lg (unionb X) id) (Fo l x)) by fprops. have qb: sub (Fo l x) (domain (Lg (unionb X) id)). aw; rewrite /X => s sf; apply /setUb_P; aw; ex_tac; rewrite LgV//. move: (qb); aw => qc; rewrite LgV//. set_extens t. by move /(range_gP qa); aw;move => [u uF ->]; rewrite ! LgV//; apply: qc. by move => tf; apply/(range_gP qa); aw; ex_tac; rewrite !LgV//; apply: qc. move => xv; rewrite {1} xv. rewrite {1} /X; aw; congr (supremum r). by apply: fun_image_exten => t tx; rewrite (ww _ tx). have sxp2: forall x, inc x (substrate r) -> x = supremum r (fun_image X1 (fun i => (fo i x))). move => x xsr; rewrite {1} (sxp1 _ xsr); congr (supremum r). apply: fun_image_exten => i iX. symmetry; apply: (supremum_pr2 or). move: (For _ x iX) => sr1. move: (fop _ _ iX xsr) => []; rewrite (iorder_sr or sr1) => ra rb. apply /(lubP or sr1); split. split; [ apply: (sr1 _ ra) |move => y yf; exact: (iorder_gle1 (rb _ yf)) ]. move => z [z1 z2]; exact: (z2 _ ra). have bla: lf_axiom fp (substrate r) A. by move => t tsr; apply /funI_P; ex_tac. set f := Lf fp (substrate r) A. have bf: bijection f. apply: lf_bijective; [ exact | | by move => y /funI_P]. move => u v usr vsr suv. rewrite (sxp2 _ usr) (sxp2 _ vsr); congr (supremum r _). apply: fun_image_exten => t tx. by move: (f_equal (Vg^~t) suv); rewrite /fp !LgV//. have c3: cardinal (domain g) = n by rewrite /g; aw. have sxp3: forall x, inc x (substrate r) -> sub (fun_image X1 (fo^~ x)) (substrate r). move => x xsr t=> /funI_P [z z1 ->]. move: (fop _ _ z1 xsr) => [h _]; move: h. move: (For _ x z1) => h; rewrite iorder_sr //; apply: h. have c6: order_isomorphism f r (induced_order (order_product g) A). hnf; rewrite /f/bijection_prop /fiso_prop lf_source lf_target. move: (iorder_osr ppa c4) => [pa' pb']. split => //. move => x y xsr ysr; move: (bla _ xsr) (bla _ ysr) => f1a f2a. have f3a: inc (fp x) (prod_of_substrates g) by move: (c4 _ f1a); ue. have f4a: inc (fp y) (prod_of_substrates g) by move: (c4 _ f2a); ue. rewrite ! LfV//; split. move => lexp; apply /iorder_gle0P => //;apply /(order_product_gleP);split => //. move => i; rewrite {1}/g; aw => iX. move: (fop _ _ iX xsr) => []; rewrite (iorder_sr or (For _ _ iX)). move: (fop _ _ iX ysr) => []; rewrite (iorder_sr or (For _ _ iX)). move => qa qb qc qd. have qe: inc (fo i x) (Xf i) by move: qc => /Zo_P []. have qf: inc (fo i y) (Xf i) by move: qa => /Zo_P []. rewrite /g /fp ! LgV//. have xx: inc (fo i x) (Fo i y). apply: Zo_i => //; move: qc => /Zo_P [_ le1]; order_tac. apply /iorder_gle0P => //; exact: (iorder_gle1 (qb _ xx)). aw => le1; move: (iorder_gle1 le1) => /(order_product_gleP) [_ _ ale]. have ale1: forall i, inc i X1 -> gle r (fo i x) y. move: ale; rewrite /g; aw => ale. move => i iX; move: (ale _ iX); rewrite LgV // /fp !LgV// => xx. move: (fop _ _ iX ysr) => []; rewrite (iorder_sr or (For _ _ iX)) =>/Zo_P. move:(iorder_gle1 xx) => le1' [_ le2] _. order_tac. rewrite (sxp2 _ xsr); move: (sxp3 _ xsr) => Xsr. move: (Exercise4_7i lr fsr nesr Xsr) => hsX. move: (supremum_pr1 or hsX) => /(lubP or Xsr) [_]. apply; split; first by exact. by move => t /funI_P [z zi ->]; apply: ale1. have allg: (forall i, inc i (domain g) -> lattice (Vg g i)). move => i idg; move: (c2 _ idg);apply: total_order_lattice. exists g, A, f; simpl; split => //; split => //. move => x y xA yA. move: xA yA (c4 _ xA) (c4 _ yA). move /funI_P => [x1 xsr ->] /funI_P [y1 ysr ->]. move => x2sr y2sr. move: (setX_lattice_sup c1 allg x2sr y2sr); rewrite -/r'. set sxy2 := sup _ _ _; set ixy2 := inf _ _ _. move => [sxy2s ixy2s sxy2p ixy2p]. have dgX: domain g = X1 by rewrite /g; aw. have srp: forall t, inc t (substrate r') -> (fgraph t /\ domain t = domain g). move => t;rewrite ppb /prod_of_substrates /fam_of_substrates. have sa: fgraph (Lg (domain g) (fun i => substrate (Vg i g))) by fprops. move /setXb_P => [sb -> _]; saw. move: (Exercise4_7o lr xsr ysr) => Sinf. move: (lattice_sup_pr lr xsr ysr) (lattice_inf_pr lr xsr ysr). set sxy := sup r x1 y1; set ixy:= inf r x1 y1. move => [qa qb qc][qd qe qf]. have sxyr: inc sxy (substrate r) by order_tac. have ixyr: inc ixy (substrate r) by order_tac. suff: fp sxy = sxy2 /\ fp ixy = ixy2. move => [<- <-]; split; apply /funI_P; [by exists sxy| by exists ixy]. move: (proj1 (distributive_lattice_prop1 lr) dlr) => dlr3. split. move: (srp _ sxy2s) (srp _ (c4 _ (bla _ sxyr))) => [fg1 d1] [fg2 d2]. apply: fgraph_exten => //; rewrite d2; first by symmetry. red; move => i idg;rewrite (sxy2p _ idg);move: (c2 _ idg); rewrite dgX in idg. rewrite /fp !LgV// => toi. have fop1: forall t, inc t (substrate r) -> (inc (fo i t) (Fo i t) /\ forall u, inc u (Fo i t) -> gle r u (fo i t)). move => t tsr; move: (fop _ _ idg tsr) => []. rewrite (iorder_sr or (For _ t idg)) => t1 t2; split; first by exact. by move => u uF; move: (iorder_gle1 (t2 _ uF)). move: (fop1 _ xsr) (fop1 _ ysr) (fop1 _ sxyr). move => [v1 v2][v3 v4][v5 v6]. have sr1: inc (fo i x1) (substrate (Vg g i)) by apply: (Fos _ x1 idg _ v1). have sr2: inc (fo i y1) (substrate (Vg g i)) by apply: (Fos _ y1 idg _ v3). move: v1 => /Zo_P [v11 v12]. move: v3 => /Zo_P [v31 v32]. have le1 : gle r (fo i x1) (fo i sxy). apply: v6; apply: Zo_i => //; order_tac. have le2 : gle r (fo i y1) (fo i sxy). apply: v6; apply: Zo_i => //; order_tac. move: v5 => /Zo_P [v51 v52]. have : inc (fo i sxy) (irreds r). have pi: sub P (irreds r) by apply: sub_setC. move: v51; case /setU1_P. move => fi; apply: pi; move: pX1 => [[<- _]_ ]; union_tac. move => ->; by apply: (Exercise4_7d). move /Zo_P => [_ foi]. move: (Exercise4_8a lr dlr3 foi xsr ysr v52). case => lea. have leb: inc (fo i sxy) (Fo i x1) by apply: Zo_i. move: (v2 _ leb) => lec. have led: (fo i sxy) = (fo i x1) by order_tac. rewrite led ;rewrite led in le2. rewrite sup_C (sup_comparable1 (proj1 toi)) //. by apply/iorder_gleP. have leb: inc (fo i sxy) (Fo i y1) by apply: Zo_i. move: (v4 _ leb) => lec. have led: (fo i sxy) = (fo i y1) by order_tac. rewrite led ;rewrite led in le1. rewrite (sup_comparable1 (proj1 toi)) //. by apply/iorder_gleP. move: (srp _ ixy2s) (srp _ (c4 _ (bla _ ixyr))) => [fg1 d1] [fg2 d2]. apply: fgraph_exten => //; rewrite d2; first by symmetry. red;move => i idg; rewrite (ixy2p _ idg); move: (c2 _ idg); rewrite dgX in idg. rewrite /fp ! LgV// => toi. have fop1: forall t, inc t (substrate r) -> (inc (fo i t) (Fo i t) /\ forall u, inc u (Fo i t) -> gle r u (fo i t)). move => t tsr; move: (fop _ _ idg tsr) => []. rewrite (iorder_sr or (For _ t idg)) => t1 t2; split; first by exact. by move => u uF; move: (iorder_gle1 (t2 _ uF)). move: (fop1 _ xsr) (fop1 _ ysr) (fop1 _ ixyr). move => [v1 v2][v3 v4][v5 v6]. have sr1: inc (fo i x1) (substrate (Vg g i)) by apply: (Fos _ x1 idg _ v1). have sr2: inc (fo i y1) (substrate (Vg g i)) by apply: (Fos _ y1 idg _ v3). move: v1 =>/Zo_P [v11 v12]. move: v3 => /Zo_P [v31 v32]. move: v5 => /Zo_P [v51 v52]. move: toi=> [too]. have ss: sub (Xf i) (substrate r) by apply: sXr. rewrite iorder_sr // => tot. have le1 : gle r (fo i ixy) (fo i x1) by apply: v2; apply: Zo_i => //;order_tac. have le2 : gle r (fo i ixy) (fo i y1) by apply: v4; apply: Zo_i => //;order_tac. have sr11 : inc (fo i x1) (Xf i)by move: sr1; rewrite /g LgV//. have sr22 : inc (fo i y1) (Xf i)by move: sr2; rewrite /g LgV//. case: (tot _ _ sr11 sr22) => le3. rewrite (inf_comparable1 too le3). move: (iorder_gle1 le3) => le4. have le5: gle r (fo i x1) y1 by order_tac. move: (qf _ v12 le5) => l6. have l7: gle r (fo i x1) (fo i ixy) by apply: v6; apply: Zo_i => //. order_tac. rewrite inf_C (inf_comparable1 too le3). move: (iorder_gle1 le3) => le4. have le5: gle r (fo i y1) x1 by order_tac. move: (qf _ le5 v32) => l6. have l7: gle r (fo i y1) (fo i ixy) by apply: v6; apply: Zo_i => //. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)