:: VECTSP_8 semantic presentation

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 by VECTSP_5:78;

end;

:: deftheorem defines lattice VECTSP_8:def 1 :

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

proof end;

end;

:: deftheorem Def2 defines SubVS-Family VECTSP_8:def 2 :

registration

let F be Field;
let VS be strict VectSp of F;
cluster non empty SubVS-Family of VS;
existence

proof end;

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

proof end;

let X be non empty SubVS-Family of VS;
:: original: Element
redefine mode Element of X -> Subspace of VS;
coherence 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

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines carr VECTSP_8:def 3 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines carr VECTSP_8:def 4 :

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

proof end;

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

proof end;

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

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def5 defines meet VECTSP_8:def 5 :

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

:: deftheorem defines complete VECTSP_8:def 6 :

theorem :: VECTSP_8:9

for F being Field
for VS being strict VectSp of F holds lattice VS is complete

proof end;

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 lineary-closed & x in Lin S holds
x in S

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :

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

proof end;

end;

:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def 8 :

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

proof end;

end;

:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def 9 :

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

proof end;

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 linear holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B

proof end;

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 linear holds
FuncLatt f is Homomorphism of lattice A, lattice B

proof end;

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 linear & f is one-to-one holds
FuncLatt f is one-to-one

proof end;

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)

proof end;