:: On the Lattice of Subspaces of Vector Space
:: by Andrzej Iwaniuk
::
:: Received May 23, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies VECTSP_1, STRUCT_0, GROUP_4, XXREAL_2, LATTICES, RLSUB_2,
RLSUB_1, XBOOLE_0, SUBSET_1, GROUP_2, FUNCT_1, ZFMISC_1, RELAT_1,
SUPINF_2, SETFAM_1, ARYTM_3, PBOOLE, TARSKI, EQREL_1, REWRITE1, LATTICE3,
RLVECT_3, GROUP_6, VECTSP_8, MSSUBFAM, UNIALG_1, LATTICE4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, LATTICE4, SETFAM_1, RLVECT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, VECTSP_1,
LATTICES, VECTSP_5, LATTICE3, VECTSP_4, VECTSP_7, GRCAT_1, MOD_2;
constructors SETFAM_1, BINOP_1, REALSET1, VECTSP_5, VECTSP_7, MOD_2, LATTICE3,
LATTICE4, RELSET_1, GRCAT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES,
VECTSP_2, VECTSP_4, VECTSP_5, RELSET_1, LATTICE4;
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 -> set means
:: VECTSP_8:def 2
for x be set st x in it holds x is Subspace of VS;
end;
registration
let F,VS;
cluster non empty for 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;
redefine 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 object for VS being strict VectSp of F for S being
Subset of VS st S is non empty & S is linearly-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
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 :: VECTSP_8:12
for F being Field for A,B being strict VectSp of F for f be
Function of A, B st f is additive homogeneous 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 Function
of A,B st f is one-to-one additive homogeneous
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 Function of A, B st f is
additive homogeneous & 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;