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