VECTSP_8: On the Lattice of Subspaces of Vector Space

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

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

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;

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 for SubVS-Family of VS;

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

proof end;

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;

proof end;

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

proof end;

uniqueness by VECTSP_4:29;

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

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

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;

proof end;

proof end;

end;

:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :

definition

let L1, L2 be Lattice;
mode Semilattice-Homomorphism of L1,L2 is "/\"-preserving Function of L1,L2;
mode sup-Semilattice-Homomorphism of L1,L2 is "\/"-preserving Function of L1,L2;

end;

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

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)

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 additive & f is homogeneous 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 additive & f is homogeneous & 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;