:: J\'onsson Theorem about Representation of Modular Lattices
:: by Mariusz {\L}api\'nski
::
:: Received June 29, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDERS_2, XBOOLE_0, STRUCT_0, EQREL_1, SUBSET_1,
FINSEQ_1, LATTICE5, LATTICES, WAYBEL_0, ZFMISC_1, GROUP_6, FUNCT_1,
RELAT_1, XXREAL_0, FINSET_1, ABIAN, CARD_1, ARYTM_3, CAT_1, YELLOW_0,
ORDINAL2, ORDINAL1, TARSKI, WELLORD1, SEQM_3, LATTICE3, WAYBEL_1,
MCART_1, VALUED_0, RELAT_2, PARTFUN1, FUNCOP_1, FUNCT_6, NAT_1, FUNCT_2,
LATTICE8, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
ORDINAL2, MCART_1, DOMAIN_1, PARTFUN1, FUNCOP_1, STRUCT_0, ORDERS_2,
EQREL_1, FINSEQ_1, LATTICE3, BINOP_1, YELLOW_0, YELLOW_2, LATTICE5,
YELLOW11, WAYBEL_1, WAYBEL_0, ABIAN, XXREAL_0;
constructors ORDINAL2, FUNCT_6, RFUNCT_3, ABIAN, REALSET2, ORDERS_3, WAYBEL_1,
LATTICE5, YELLOW11, RELSET_1, XTUPLE_0, NUMBERS, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1,
XREAL_0, INT_1, CARD_1, FINSEQ_1, EQREL_1, ABIAN, STRUCT_0, LATTICE3,
YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL10, LATTICE5, YELLOW11, WAYBEL21,
LATTICE7, ZFMISC_1, FUNCT_1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
definition
let L be RelStr;
attr L is finitely_typed means
:: LATTICE8:def 1
ex A being non empty set st
(for e being object
st e in the carrier of L holds e is Equivalence_Relation of A) & ex o
being Element of NAT st
for e1,e2 being Equivalence_Relation of A, x,y being object
st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2
holds ex F being non empty FinSequence of A st len F = o & x,y are_joint_by F,
e1,e2;
end;
definition
let L be lower-bounded LATTICE;
let n be Element of NAT;
pred L has_a_representation_of_type<= n means
:: LATTICE8:def 2
ex A being non trivial
set, f be Homomorphism of L,EqRelLATT A st f is one-to-one & Image f is
finitely_typed & (ex e being Equivalence_Relation of A st e in the carrier of
Image f & e <> id A) & type_of Image f <= n;
end;
registration
cluster lower-bounded distributive finite for LATTICE;
end;
registration
let A be non trivial set;
cluster non trivial finitely_typed full for
non empty Sublattice of EqRelLATT A;
end;
theorem :: LATTICE8:1
for A be non empty set for L be lower-bounded LATTICE for d be
distance_function of A,L holds succ {} c= DistEsti(d);
theorem :: LATTICE8:2
for L being trivial Semilattice holds L is modular;
theorem :: LATTICE8:3
for A being non empty set for L being non empty Sublattice of
EqRelLATT A holds L is trivial or ex e being Equivalence_Relation of A st e in
the carrier of L & e <> id A;
theorem :: LATTICE8:4
for L1,L2 be lower-bounded LATTICE for f being Function of L1,L2
st f is infs-preserving sups-preserving holds f is meet-preserving
join-preserving;
theorem :: LATTICE8:5
for L1,L2 be lower-bounded LATTICE st L1,L2 are_isomorphic & L1
is modular holds L2 is modular;
theorem :: LATTICE8:6
for S being lower-bounded non empty Poset for T being non empty
Poset for f being monotone Function of S,T holds Image f is lower-bounded;
theorem :: LATTICE8:7
for L being lower-bounded LATTICE for x,y being Element of L for
A being non empty set for f be Homomorphism of L,EqRelLATT A st f is one-to-one
holds (corestr f).x <= (corestr f).y implies x <= y;
begin
theorem :: LATTICE8:8
for A being non trivial set for L being finitely_typed full non
empty Sublattice of EqRelLATT A for e being Equivalence_Relation of A st e in
the carrier of L & e <> id A holds type_of L <= 2 implies L is modular;
theorem :: LATTICE8:9
for L be lower-bounded LATTICE holds L
has_a_representation_of_type<= 2 implies L is modular;
:: <= :: L is modular implies L has_a_representation_of_type<= 2
definition
let A be set;
func new_set2 A -> set equals
:: LATTICE8:def 3
A \/ {{A}, {{A}}};
end;
registration
let A be set;
cluster new_set2 A -> non empty;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun2(d,q) -> BiFunction of new_set2 A,L means
:: LATTICE8:def 4
(for u,v being Element of A holds it.(u,v) = d.(u,v)) &
it.({A},{A}) = Bottom L & it.({{A}},{{A}}) = Bottom L &
it.({A},{{A}}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) &
it.({{A}
},{A}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) &
for u being Element of A
holds it.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) &
it.({A},u) = d.(u,q`1_4)"\/"(q`3_4) &
it.(u,{{A}}) = d.(u,q`2_4) "\/"(q`3_4) &
it.({{A}},u) = d.(u,q`2_4)"\/"(q`3_4);
end;
theorem :: LATTICE8:10
for A being non empty set for L being lower-bounded LATTICE for
d being BiFunction of A,L st d is zeroed for q being Element of [:A,A,the
carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is zeroed;
theorem :: LATTICE8:11
for A being non empty set for L being lower-bounded LATTICE for
d being BiFunction of A,L st d is symmetric for q being Element of [:A,A,the
carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is symmetric;
theorem :: LATTICE8:12
for A being non empty set for L being lower-bounded LATTICE st L
is modular for d being BiFunction of A,L st d is symmetric & d is u.t.i. for q
being Element of [:A,A,the carrier of L,the carrier of L:]
st d.(q`1_4,q`2_4) <= (q`3_4)"\/"(q`4_4) holds new_bi_fun2(d,q) is u.t.i.;
theorem :: LATTICE8:13
for A being non empty set for L being lower-bounded LATTICE for
d be BiFunction of A,L for q be Element of [:A,A,the carrier of L,the carrier
of L:] holds d c= new_bi_fun2(d,q);
reserve x for set,
C for Ordinal,
L0 for Sequence;
definition
let A be non empty set;
let O be Ordinal;
func ConsecutiveSet2(A,O) -> set means
:: LATTICE8:def 5
ex L0 being Sequence st it = last
L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal st succ C in succ O
holds L0.succ C = new_set2(L0.C)) & for C being Ordinal st C in succ O & C <>
0 & C is limit_ordinal holds L0.C = union rng (L0|C);
end;
theorem :: LATTICE8:14
for A being non empty set holds ConsecutiveSet2(A,0) = A;
theorem :: LATTICE8:15
for A being non empty set for O being Ordinal holds
ConsecutiveSet2(A,succ O) = new_set2 ConsecutiveSet2(A,O);
theorem :: LATTICE8:16
for A being non empty set for O being Ordinal for T being
Sequence holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being
Ordinal st O1 in O holds T.O1 = ConsecutiveSet2(A,O1)) implies ConsecutiveSet2(
A,O) = union rng T;
reserve O1,O2 for Ordinal;
registration
let A be non empty set;
let O be Ordinal;
cluster ConsecutiveSet2(A,O) -> non empty;
end;
theorem :: LATTICE8:17
for A being non empty set for O being Ordinal holds A c= ConsecutiveSet2(A,O)
;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume
O in dom q;
func Quadr2(q,O) -> Element of [:ConsecutiveSet2(A,O),ConsecutiveSet2(A,O),
the carrier of L,the carrier of L:] equals
:: LATTICE8:def 6
q.O;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta2(q,O) -> set means
:: LATTICE8:def 7
ex L0 being Sequence st it = last
L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal st succ C in succ O
holds L0.succ C = new_bi_fun2(BiFun(L0.C,ConsecutiveSet2(A,C),L),Quadr2(q,C)))
& for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C
= union rng(L0|C);
end;
theorem :: LATTICE8:18
for A being non empty set for L be lower-bounded LATTICE for d
being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta2(q,0)
= d;
theorem :: LATTICE8:19
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds
ConsecutiveDelta2(q,succ O) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O),
ConsecutiveSet2(A,O),L),Quadr2(q,O));
theorem :: LATTICE8:20
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for T being Sequence for O
being Ordinal holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being
Ordinal st O1 in O holds T.O1 = ConsecutiveDelta2(q,O1)) implies
ConsecutiveDelta2(q,O) = union rng T;
theorem :: LATTICE8:21
for A being non empty set for O,O1,O2 being Ordinal holds O1 c=
O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2);
theorem :: LATTICE8:22
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds
ConsecutiveDelta2(q,O) is BiFunction of ConsecutiveSet2(A,O),L;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
redefine func ConsecutiveDelta2(q,O) -> BiFunction of ConsecutiveSet2(A,O),L;
end;
theorem :: LATTICE8:23
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds d c=
ConsecutiveDelta2(q,O);
theorem :: LATTICE8:24
for A being non empty set for L be lower-bounded LATTICE for d
being BiFunction of A,L for O1,O2 being Ordinal for q being QuadrSeq of d st O1
c= O2 holds ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2);
theorem :: LATTICE8:25
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L st d is zeroed for q being QuadrSeq of d for O being
Ordinal holds ConsecutiveDelta2(q,O) is zeroed;
theorem :: LATTICE8:26
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L st d is symmetric for q being QuadrSeq of d for O being
Ordinal holds ConsecutiveDelta2(q,O) is symmetric;
theorem :: LATTICE8:27
for A being non empty set for L being lower-bounded LATTICE st L
is modular for d be BiFunction of A,L st d is symmetric u.t.i. for O being
Ordinal for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta2(q
,O) is u.t.i.;
theorem :: LATTICE8:28
for A being non empty set for L being lower-bounded modular LATTICE
for d being distance_function of A,L for O being Ordinal for q being QuadrSeq
of d st O c= DistEsti(d) holds ConsecutiveDelta2(q,O) is distance_function of
ConsecutiveSet2(A,O),L;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet2(d) -> set equals
:: LATTICE8:def 8
ConsecutiveSet2(A,DistEsti(d));
end;
registration
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet2(d) -> non empty;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta2(q) -> set equals
:: LATTICE8:def 9
ConsecutiveDelta2(q,DistEsti(d));
end;
definition
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
redefine func NextDelta2(q) -> distance_function of NextSet2(d),L;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set;
let dq be distance_function of Aq,L;
pred Aq, dq is_extension2_of A,d means
:: LATTICE8:def 10
ex q being QuadrSeq of d st Aq = NextSet2(d) & dq = NextDelta2(q);
end;
theorem :: LATTICE8:29
for A being non empty set for L be lower-bounded LATTICE for d
be distance_function of A,L for Aq be non empty set for dq be distance_function
of Aq,L st Aq, dq is_extension2_of A,d for x,y being Element of A, a,b being
Element of L st d.(x,y) <= a "\/" b ex z1,z2 being Element of Aq st dq.(x,z1) =
a & dq.(z1,z2) = (d.(x,y) "\/" a) "/\" b & dq.(z2,y) = a;
definition
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq2 of A,d -> Function means
:: LATTICE8:def 11
dom it = NAT & it.0 = [A
,d] & for n being Nat holds ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension2_of A9,d9 & it.n = [A9,d9] & it.(n+1) = [Aq,dq];
end;
theorem :: LATTICE8:30
for A being non empty set for L be lower-bounded modular LATTICE
for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l
being Nat st k <= l holds (S.k)`1 c= (S.l)`1;
theorem :: LATTICE8:31
for A being non empty set for L be lower-bounded modular LATTICE
for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l
being Nat st k <= l holds (S.k)`2 c= (S.l)`2;
theorem :: LATTICE8:32
for L be lower-bounded modular LATTICE for S being ExtensionSeq2
of the carrier of L, BasicDF(L) for FS being non empty set st FS = union the
set of all (S.i
)`1 where i is Element of NAT holds union the set of all (S.i)`2 where i
is Element of NAT is distance_function of FS,L;
theorem :: LATTICE8:33
for L be lower-bounded modular LATTICE for S being ExtensionSeq2
of the carrier of L, BasicDF(L) for FS being non empty set for FD being
distance_function of FS,L for x,y being Element of FS for a,b being Element of
L st FS = union the set of all (S.i)`1 where i is Element of NAT & FD =
union the set of all (S.i)`2 where i is Element of NAT & FD.(x,y) <= a
"\/"b ex z1,z2 being Element of FS st FD.(x,z1) = a & FD.(z1,z2) = (FD.(x,y)
"\/"a)"/\"b & FD.(z2,y) = a;
theorem :: LATTICE8:34
for L be lower-bounded modular LATTICE for S being ExtensionSeq2
of the carrier of L, BasicDF(L) for FS being non empty set for FD being
distance_function of FS,L for f being Homomorphism of L,EqRelLATT FS for e1,e2
being Equivalence_Relation of FS
for x,y being object st f = alpha FD & FS = union
the set of all (S.i)`1 where i is Element of NAT & FD = union the set of all
(S.i)`2
where i is Element of NAT & e1 in the carrier of Image f &
e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non empty
FinSequence of FS st len F = 2+2 & x,y are_joint_by F,e1,e2;
theorem :: LATTICE8:35
for L be lower-bounded modular LATTICE holds L
has_a_representation_of_type<= 2;
:: <=> :: L has_a_representation_of_type<= 2 iff L is modular
::$N Jonsson Theorem for modular lattices
theorem :: LATTICE8:36
for L be lower-bounded LATTICE holds L has_a_representation_of_type<=
2 iff L is modular;