:: On the Lattice of Subspaces of Vector Space
:: by Andrzej Iwaniuk
::
:: Received May 23, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

definition
let F be Field;
let VS be strict VectSp of F;
func lattice VS ->  strict bounded Lattice equals :: VECTSP_8:def 1
 LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);
coherence
 LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #) is strict bounded Lattice by VECTSP_5:60;
end;

:: deftheorem  defines lattice VECTSP_8:def_1_:_
 for F being Field
for VS being strict VectSp of F holds lattice VS = LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);

definition
let F be Field;
let VS be strict VectSp of F;
mode SubVS-Family of VS ->  set  means :Def2: :: VECTSP_8:def 2
 for x being set st x in it holds
x is Subspace of VS;
existence
 ex b1 being set st
for x being set st x in b1 holds
x is Subspace of VS
proofend;
end;

:: deftheorem Def2 defines SubVS-Family VECTSP_8:def_2_:_
 for F being Field
for VS being strict VectSp of F
for b3 being set holds
( b3 is SubVS-Family of VS iff for x being set st x in b3 holds
x is Subspace of VS );

registration
let F be Field;
let VS be strict VectSp of F;
cluster non empty for SubVS-Family of VS;
existence
 not for b1 being SubVS-Family of VS holds b1 is empty
proofend;
end;

definition
let F be Field;
let VS be strict VectSp of F;
:: original:Subspaces
redefine func Subspaces VS ->  non empty SubVS-Family of VS;
coherence
 Subspaces VS is non empty SubVS-Family of VS
proofend;
let X be non empty SubVS-Family of VS;
:: original:Element
redefine mode Element of X ->  Subspace of VS;
coherence
 for b1 being Element of X holds b1 is Subspace of VS by Def2;
end;

definition
let F be Field;
let VS be strict VectSp of F;
let x be Element of Subspaces VS;
func carr x ->  Subset of VS means :Def3: :: VECTSP_8:def 3
 ex X being Subspace of VS st
( x = X & it = the carrier of X );
existence
 ex b1 being Subset of VS ex X being Subspace of VS st
( x = X & b1 = the carrier of X )
proofend;
uniqueness
 for b1, b2 being Subset of VS st ex X being Subspace of VS st
( x = X & b1 = the carrier of X ) & ex X being Subspace of VS st
( x = X & b2 = the carrier of X ) holds
b1 = b2 ;
end;

:: deftheorem Def3 defines carr VECTSP_8:def_3_:_
 for F being Field
for VS being strict VectSp of F
for x being Element of Subspaces VS
for b4 being Subset of VS holds
( b4 = carr x iff ex X being Subspace of VS st
( x = X & b4 = the carrier of X ) );

definition
let F be Field;
let VS be strict VectSp of F;
func carr VS ->  Function of (Subspaces VS),(bool the carrier of VS) means :Def4: :: VECTSP_8:def 4
 for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
it . h = the carrier of H;
existence
 ex b1 being Function of (Subspaces VS),(bool the carrier of VS) st
for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b1 . h = the carrier of H
proofend;
uniqueness
 for b1, b2 being Function of (Subspaces VS),(bool the carrier of VS) st ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b1 . h = the carrier of H ) & ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b2 . h = the carrier of H ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines carr VECTSP_8:def_4_:_
 for F being Field
for VS being strict VectSp of F
for b3 being Function of (Subspaces VS),(bool the carrier of VS) holds
( b3 = carr VS iff for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b3 . h = the carrier of H );

theorem Th1: :: VECTSP_8:1
for F being Field
for VS being strict VectSp of F
for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty
proofend;

theorem :: VECTSP_8:2
for F being Field
for VS being strict VectSp of F
for H being strict Subspace of VS holds 0. VS in (carr VS) . H
proofend;

definition
let F be Field;
let VS be strict VectSp of F;
let G be non empty Subset of (Subspaces VS);
func meet G ->  strict Subspace of VS means :Def5: :: VECTSP_8:def 5
 the carrier of it = meet ((carr VS) .: G);
existence
 ex b1 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G)
proofend;
uniqueness
 for b1, b2 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G) & the carrier of b2 = meet ((carr VS) .: G) holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def5 defines meet VECTSP_8:def_5_:_
 for F being Field
for VS being strict VectSp of F
for G being non empty Subset of (Subspaces VS)
for b4 being strict Subspace of VS holds
( b4 = meet G iff the carrier of b4 = meet ((carr VS) .: G) );

theorem :: VECTSP_8:3
for F being Field
for VS being strict VectSp of F holds Subspaces VS = the carrier of (lattice VS) ;

theorem :: VECTSP_8:4
for F being Field
for VS being strict VectSp of F holds the L_meet of (lattice VS) = SubMeet VS ;

theorem :: VECTSP_8:5
for F being Field
for VS being strict VectSp of F holds the L_join of (lattice VS) = SubJoin VS ;

theorem Th6: :: VECTSP_8:6
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
proofend;

theorem Th7: :: VECTSP_8:7
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "\/" q = H1 + H2
proofend;

theorem Th8: :: VECTSP_8:8
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "/\" q = H1 /\ H2
proofend;

definition
let L be non empty LattStr ;
redefine attr L is complete  means :: VECTSP_8:def 6
 for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) );
compatibility
 ( L is complete iff for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) )
proofend;
end;

:: deftheorem  defines complete VECTSP_8:def_6_:_
 for L being non empty LattStr holds
( L is complete iff for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) );

theorem :: VECTSP_8:9
for F being Field
for VS being strict VectSp of F holds lattice VS is complete
proofend;

theorem Th10: :: VECTSP_8:10
for F being Field
for x being set
for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
proofend;

definition
let F be Field;
let A, B be strict VectSp of F;
let f be Function of the carrier of A, the carrier of B;
func FuncLatt f ->  Function of the carrier of (lattice A), the carrier of (lattice B) means :Def7: :: VECTSP_8:def 7
 for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
it . S = Lin B0;
existence
 ex b1 being Function of the carrier of (lattice A), the carrier of (lattice B) st
for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b1 . S = Lin B0
proofend;
uniqueness
 for b1, b2 being Function of the carrier of (lattice A), the carrier of (lattice B) st ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b1 . S = Lin B0 ) & ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b2 . S = Lin B0 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines FuncLatt VECTSP_8:def_7_:_
 for F being Field
for A, B being strict VectSp of F
for f being Function of the carrier of A, the carrier of B
for b5 being Function of the carrier of (lattice A), the carrier of (lattice B) holds
( b5 = FuncLatt f iff for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b5 . S = Lin B0 );

definition
let L1, L2 be Lattice;
mode Semilattice-Homomorphism of L1,L2 ->  Function of the carrier of L1, the carrier of L2 means :Def8: :: VECTSP_8:def 8
 for a, b being Element of L1 holds it . (a "/\" b) = (it . a) "/\" (it . b);
existence
 ex b1 being Function of the carrier of L1, the carrier of L2 st
for a, b being Element of L1 holds b1 . (a "/\" b) = (b1 . a) "/\" (b1 . b)
proofend;
end;

:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def_8_:_
 for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "/\" b) = (b3 . a) "/\" (b3 . b) );

definition
let L1, L2 be Lattice;
mode sup-Semilattice-Homomorphism of L1,L2 ->  Function of the carrier of L1, the carrier of L2 means :Def9: :: VECTSP_8:def 9
 for a, b being Element of L1 holds it . (a "\/" b) = (it . a) "\/" (it . b);
existence
 ex b1 being Function of the carrier of L1, the carrier of L2 st
for a, b being Element of L1 holds b1 . (a "\/" b) = (b1 . a) "\/" (b1 . b)
proofend;
end;

:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def_9_:_
 for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is sup-Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "\/" b) = (b3 . a) "\/" (b3 . b) );

theorem :: VECTSP_8:11
for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 holds
( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
proofend;

theorem Th12: :: VECTSP_8:12
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
proofend;

theorem :: VECTSP_8:13
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of lattice A, lattice B
proofend;

theorem :: VECTSP_8:14
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
proofend;

theorem :: VECTSP_8:15
for F being Field
for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of (lattice A)
proofend;