Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

On the Lattice of Subspaces of a Vector Space

by
Andrzej Iwaniuk

MML identifier: VECTSP_8
[ Mizar article, MML identifier index ]

```environ

vocabulary VECTSP_1, GROUP_4, LATTICES, RLSUB_2, RLSUB_1, BOOLE, GROUP_2,
FUNCT_1, RELAT_1, RLVECT_1, SETFAM_1, BHSP_3, LATTICE3, RLVECT_3,
GROUP_6, PRE_TOPC, INCSP_1, VECTSP_8;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, LATTICE4, SETFAM_1, RLVECT_1,
STRUCT_0, VECTSP_1, PRE_TOPC, LATTICES, VECTSP_5, LATTICE3, VECTSP_4,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, VECTSP_7, MOD_2;
constructors LATTICE4, VECTSP_5, LATTICE3, BINOP_1, VECTSP_7, MOD_2, VECTSP_2;
clusters LATTICES, VECTSP_4, VECTSP_2, STRUCT_0, VECTSP_5, RELSET_1, SUBSET_1,
FUNCT_2, PARTFUN1, XBOOLE_0;
requirements BOOLE, SUBSET;

begin

reserve F for Field;
reserve VS for strict VectSp of F;

definition let F, VS;
func lattice VS -> strict bounded Lattice equals
:: VECTSP_8:def 1
LattStr (# Subspaces(VS), SubJoin(VS), SubMeet(VS) #);
end;

definition let F,VS;
mode SubVS-Family of VS means
:: VECTSP_8:def 2
for x be set st x in it holds x is Subspace of VS;
end;

definition let F,VS;
cluster non empty SubVS-Family of VS;
end;

definition let F,VS;
redefine func Subspaces(VS) -> non empty SubVS-Family of VS;

let X be non empty SubVS-Family of VS;
mode Element of X -> Subspace of VS;
end;

definition
let F,VS;
let x be Element of Subspaces VS;
func carr(x) -> Subset of VS means
:: VECTSP_8:def 3
ex X being Subspace of VS st
x=X & it = the carrier of X;
end;

reserve u,e for set;

definition let F,VS;
func carr VS -> Function of Subspaces(VS),bool the carrier of VS means
:: VECTSP_8:def 4
for h being Element of Subspaces(VS), H being Subspace of VS
st h = H holds it.h = the carrier of H;
end;

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

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

reserve x for set;

definition let F,VS;
let G be non empty Subset of Subspaces(VS);
func meet G -> strict Subspace of VS means
:: VECTSP_8:def 5
the carrier of it = meet ((carr VS).:G);
end;

theorem :: VECTSP_8:3
Subspaces(VS) = the carrier of lattice VS;

theorem :: VECTSP_8:4
the L_meet of lattice VS = SubMeet(VS);

theorem :: VECTSP_8:5
the L_join of lattice VS = SubJoin(VS);

theorem :: VECTSP_8:6
for VS being strict VectSp of F,
p,q being Element of lattice VS,
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;

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

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

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

reserve Z1 for set;

theorem :: VECTSP_8:9
for VS holds lattice VS is complete;

theorem :: VECTSP_8:10
for x being set
for VS being strict VectSp of F
for S being Subset of VS st
S is non empty & S is lineary-closed holds
x in Lin S implies x in S;

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
:: VECTSP_8:def 7
for S being strict Subspace of A, B0 being Subset of B
st B0 = f.:the carrier of S
holds it.S = Lin B0;
end;

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

definition
let L1, L2 be Lattice;
mode sup-Semilattice-Homomorphism of L1, L2 ->
Function of the carrier of L1, the carrier of L2 means
:: VECTSP_8:def 9
for a, b being Element of L1 holds
it.(a "\/" b) = it.a "\/" it.b;
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 :: VECTSP_8:12
for F being Field
for A,B being strict VectSp of F
for f be map of A, B st f is linear holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B;

theorem :: VECTSP_8:13
for F being Field
for A,B being strict VectSp of F
for f be map of A,B st f is one-to-one linear holds
FuncLatt f is Homomorphism of lattice A, lattice B;

theorem :: VECTSP_8:14
for A,B being strict VectSp of F
for f being map of A, B st
f is linear & f is one-to-one holds FuncLatt f is one-to-one;

theorem :: VECTSP_8:15
for A being strict VectSp of F holds
FuncLatt id the carrier of A = id the carrier of lattice A;
```