LATTICE8: J\'onsson Theorem about Representation of Modular Lattices

:: 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

definition

let L be RelStr ;

attr L is finitely_typed means :Def1: :: 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
for 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;

:: deftheorem Def1 defines finitely_typed LATTICE8:def 1 :

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 ex f being Homomorphism of L,(EqRelLATT A) st
( f is V17() & 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;

:: deftheorem defines has_a_representation_of_type<= LATTICE8:def 2 :

registration

cluster non empty finite reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima for RelStr ;

existence

proof end;

end;

Lm1: 1 is odd

proof end;

Lm2: 2 is even

proof end;

registration

let A be non trivial set ;

cluster non empty non trivial full meet-inheriting join-inheriting finitely_typed for SubRelStr of EqRelLATT A;

existence

proof end;

end;

theorem Th1: :: LATTICE8:1

for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d

proof end;

theorem :: LATTICE8:2

for L being trivial Semilattice holds L is modular by STRUCT_0:def 10;

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 ) )

proof end;

theorem :: LATTICE8:4

for L1, L2 being lower-bounded LATTICE
for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds
( f is meet-preserving & f is join-preserving ) ;

theorem Th5: :: LATTICE8:5

for L1, L2 being lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds
L2 is modular

proof end;

theorem Th6: :: LATTICE8:6

for S being non empty lower-bounded Poset
for T being non empty Poset
for f being monotone Function of S,T holds Image f is lower-bounded

proof end;

theorem Th7: :: LATTICE8:7

for L being lower-bounded LATTICE
for x, y being Element of L
for A being non empty set
for f being Homomorphism of L,(EqRelLATT A) st f is V17() & (corestr f) . x <= (corestr f) . y holds
x <= y

proof end;

theorem Th8: :: LATTICE8:8

for A being non trivial set
for L being non empty full finitely_typed Sublattice of EqRelLATT A
for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular

proof end;

theorem Th9: :: LATTICE8:9

for L being lower-bounded LATTICE st L has_a_representation_of_type<= 2 holds
L is modular

proof end;

:: <= :: 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}}};

correctness ;

end;

:: deftheorem defines new_set2 LATTICE8:def 3 :

registration

let A be set ;

cluster new_set2 A -> non empty ;

coherence ;

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 :Def4: :: 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) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines new_bi_fun2 LATTICE8:def 4 :

theorem Th10: :: 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 holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is zeroed

proof end;

theorem Th11: :: 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 holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric

proof end;

theorem Th12: :: LATTICE8:12

for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
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.

proof end;

theorem Th13: :: LATTICE8:13

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun2 (d,q)

proof end;

definition

let A be non empty set ;
let O be Ordinal;

func ConsecutiveSet2 (A,O) -> set means :Def5: :: 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)) ) );

correctness

proof end;

end;

:: deftheorem Def5 defines ConsecutiveSet2 LATTICE8:def 5 :

theorem Th14: :: LATTICE8:14

for A being non empty set holds ConsecutiveSet2 (A,0) = A

proof end;

theorem Th15: :: LATTICE8:15

for A being non empty set
for O being Ordinal holds ConsecutiveSet2 (A,(succ O)) = new_set2 (ConsecutiveSet2 (A,O))

proof end;

theorem Th16: :: LATTICE8:16

for A being non empty set
for O being Ordinal
for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 (A,O1) ) holds
ConsecutiveSet2 (A,O) = union (rng T)

proof end;

registration

let A be non empty set ;
let O be Ordinal;

cluster ConsecutiveSet2 (A,O) -> non empty ;

coherence

proof end;

end;

theorem Th17: :: LATTICE8:17

for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet2 (A,O)

proof 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;
assume A1: 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 :Def6: :: LATTICE8:def 6
q . O;

correctness

proof end;

end;

:: deftheorem Def6 defines Quadr2 LATTICE8:def 6 :

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 :Def7: :: 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)) ) );

correctness

proof end;

end;

:: deftheorem Def7 defines ConsecutiveDelta2 LATTICE8:def 7 :

theorem Th18: :: LATTICE8:18

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta2 (q,0) = d

proof end;

theorem Th19: :: LATTICE8:19

for A being non empty set
for L being lower-bounded LATTICE
for d being 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)))

proof end;

theorem Th20: :: LATTICE8:20

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for T being Sequence
for O being Ordinal st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta2 (q,O1) ) holds
ConsecutiveDelta2 (q,O) = union (rng T)

proof end;

theorem Th21: :: LATTICE8:21

for A being non empty set
for O, O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2)

proof end;

theorem Th22: :: LATTICE8:22

for A being non empty set
for L being lower-bounded LATTICE
for d being 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

proof 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;
:: original: ConsecutiveDelta2
redefine func ConsecutiveDelta2 (q,O) -> BiFunction of (ConsecutiveSet2 (A,O)),L;
coherence by Th22;

end;

theorem Th23: :: LATTICE8:23

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds d c= ConsecutiveDelta2 (q,O)

proof end;

theorem Th24: :: LATTICE8:24

for A being non empty set
for L being 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)

proof end;

theorem Th25: :: LATTICE8:25

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed

proof end;

theorem Th26: :: LATTICE8:26

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric

proof end;

theorem Th27: :: LATTICE8:27

for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.

proof end;

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 by Th25, Th26, Th27;

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));

correctness ;

end;

:: deftheorem defines NextSet2 LATTICE8:def 8 :

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 ;

coherence ;

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));

correctness ;

end;

:: deftheorem defines NextDelta2 LATTICE8:def 9 :

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;
:: original: NextDelta2
redefine func NextDelta2 q -> distance_function of (NextSet2 d),L;
coherence by Th25, Th26, Th27;

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;

:: deftheorem defines is_extension2_of LATTICE8:def 10 :

theorem Th29: :: LATTICE8:29

for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )

proof end;

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 :Def11: :: LATTICE8:def 11
( dom it = NAT & it . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & it . n = [A9,d9] & it . (n + 1) = [Aq,dq] ) ) );

existence

proof end;

end;

:: deftheorem Def11 defines ExtensionSeq2 LATTICE8:def 11 :

theorem Th30: :: LATTICE8:30

for A being non empty set
for L being lower-bounded modular LATTICE
for d being 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

proof end;

theorem Th31: :: LATTICE8:31

for A being non empty set
for L being lower-bounded modular LATTICE
for d being 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

proof end;

theorem Th32: :: LATTICE8:32

for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds
union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L

proof end;

theorem Th33: :: LATTICE8:33

for L being 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 { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )

proof end;

Lm3: for m being Element of NAT holds
( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )

proof end;

Lm4: for j being Nat st 1 <= j & j < 4 & not j = 1 & not j = 2 holds
j = 3

proof end;

theorem Th34: :: LATTICE8:34

for L being 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 { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 2 + 2 & x,y are_joint_by F,e1,e2 )

proof end;

theorem Th35: :: LATTICE8:35

for L being lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2

proof end;

:: <=> :: L has_a_representation_of_type<= 2 iff L is modular
:: WP:

Jonsson Theorem for modular lattices

theorem :: LATTICE8:36

for L being lower-bounded LATTICE holds
( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th35;