:: Spaces of Pencils, {G}rassmann Spaces, and Generalized {V}eronese
:: Spaces
:: by Adam Naumowicz
::
:: Received November 8, 2004
:: Copyright (c) 2004-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 NUMBERS, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FINSET_1, CARD_1,
SUBSET_1, TARSKI, XBOOLE_0, VECTSP_1, RLSUB_1, STRUCT_0, SUPINF_2,
RLSUB_2, RLVECT_5, SETFAM_1, ZFMISC_1, RLVECT_3, RELAT_1, PRE_TOPC,
PENCIL_1, PENCIL_4;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, NAT_D, SETFAM_1, DOMAIN_1, STRUCT_0, FINSET_1,
PRE_TOPC, PENCIL_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_7,
MATRLIN, VECTSP_9;
constructors REALSET1, VECTSP_5, VECTSP_7, VECTSP_9, PENCIL_1, NAT_D;
registrations SUBSET_1, FINSET_1, XXREAL_0, XREAL_0, STRUCT_0, MATRLIN,
VECTSP_9, PENCIL_1, ORDINAL1, CARD_1;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
begin :: Spaces of pencils
theorem :: PENCIL_4:1
for k,n being Nat st k < n & 3 <= n holds k+1 < n or 2 <= k;
theorem :: PENCIL_4:2
for F being Field for V being VectSp of F for W being Subspace of
V holds W is Subspace of (Omega).V;
theorem :: PENCIL_4:3
for F being Field for V being VectSp of F for W being Subspace of
(Omega).V holds W is Subspace of V;
theorem :: PENCIL_4:4
for F being Field for V being VectSp of F for W being Subspace of
V holds (Omega).W is Subspace of V;
theorem :: PENCIL_4:5
for F being Field for V,W being VectSp of F holds (Omega).W is
Subspace of V implies W is Subspace of V;
definition
let F be Field;
let V be VectSp of F;
let W1,W2 be Subspace of V;
func segment(W1,W2) -> Subset of Subspaces(V) means
:: PENCIL_4:def 1
for W being
strict Subspace of V holds W in it iff W1 is Subspace of W & W is Subspace of
W2 if W1 is Subspace of W2 otherwise it={};
end;
theorem :: PENCIL_4:6
for F being Field for V being VectSp of F for W1,W2,W3,W4 being
Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega).W1=
(Omega).W3 & (Omega).W2=(Omega).W4 holds segment(W1,W2) = segment(W3,W4);
definition
let F be Field;
let V be VectSp of F;
let W1,W2 be Subspace of V;
func pencil(W1,W2) -> Subset of Subspaces(V) equals
:: PENCIL_4:def 2
segment(W1,W2) \ {
(Omega).W1,(Omega).W2};
end;
theorem :: PENCIL_4:7
for F being Field for V being VectSp of F for W1,W2,W3,W4 being
Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega).W1=
(Omega).W3 & (Omega).W2=(Omega).W4 holds pencil(W1,W2) = pencil(W3,W4);
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let W1,W2 be Subspace of V;
let k be Nat;
func pencil(W1,W2,k) -> Subset of (k Subspaces_of V) equals
:: PENCIL_4:def 3
pencil (W1,W2)
/\ (k Subspaces_of V);
end;
theorem :: PENCIL_4:8
for F being Field for V being finite-dimensional VectSp of F for
k being Nat for W1,W2,W being Subspace of V st W in pencil(W1,W2,k) holds W1 is
Subspace of W & W is Subspace of W2;
theorem :: PENCIL_4:9
for F being Field for V being finite-dimensional VectSp of F for k
being Nat for W1,W2,W3,W4 being Subspace of V st W1 is Subspace of W2 & W3 is
Subspace of W4 & (Omega).W1=(Omega).W3 & (Omega).W2=(Omega).W4 holds pencil(W1,
W2,k) = pencil(W3,W4,k);
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
func k Pencils_of V -> Subset-Family of (k Subspaces_of V) means
:: PENCIL_4:def 4
for
X being set holds X in it iff ex W1,W2 being Subspace of V st W1 is Subspace of
W2 & dim W1+1=k & dim W2=k+1 & X=pencil(W1,W2,k);
end;
theorem :: PENCIL_4:10
for F being Field for V being finite-dimensional VectSp of F for
k being Nat st 1 <= k & k < dim V holds k Pencils_of V is non empty;
theorem :: PENCIL_4:11
for F being Field for V being finite-dimensional VectSp of F for
W1,W2,P,Q being Subspace of V for k being Nat st dim W1+1=k & dim W2=k+1 & P in
pencil(W1,W2,k) & Q in pencil(W1,W2,k) & P<>Q holds P/\Q = (Omega).W1 & P+Q =
(Omega).W2;
theorem :: PENCIL_4:12
for F being Field for V being finite-dimensional VectSp of F for
v being Vector of V st v <> 0.V holds dim Lin{v} = 1;
theorem :: PENCIL_4:13
for F being Field for V being finite-dimensional VectSp of F for
W being Subspace of V for v being Vector of V st not v in W holds dim(W+Lin{v})
=dim W + 1;
theorem :: PENCIL_4:14
for F being Field for V being finite-dimensional VectSp of F for
W being Subspace of V for v,u being Vector of V st v<>u & {v,u} is
linearly-independent & W/\Lin{v,u}=(0).V holds dim(W+Lin{v,u})=dim W + 2;
theorem :: PENCIL_4:15
for F being Field for V being finite-dimensional VectSp of F for
W1,W2 being Subspace of V st W1 is Subspace of W2 for k being Nat st dim W1+1=k
& dim W2=k+1 for v being Vector of V st v in W2 & not v in W1 holds W1+Lin{v}
in pencil(W1,W2,k);
theorem :: PENCIL_4:16
for F being Field for V being finite-dimensional VectSp of F for
W1,W2 being Subspace of V st W1 is Subspace of W2 for k being Nat st dim W1+1=k
& dim W2=k+1 holds pencil(W1,W2,k) is non trivial;
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
func PencilSpace(V,k) -> strict TopStruct equals
:: PENCIL_4:def 5
TopStruct(#k Subspaces_of V
, k Pencils_of V#);
end;
theorem :: PENCIL_4:17
for F being Field for V being finite-dimensional VectSp of F for
k being Nat st 1 <= k & k < dim V holds PencilSpace(V,k) is non void;
theorem :: PENCIL_4:18
for F being Field for V being finite-dimensional VectSp of F for
k being Nat st 1 <= k & k < dim V & 3 <= dim V holds PencilSpace(V,k) is non
degenerated;
theorem :: PENCIL_4:19
for F being Field for V being finite-dimensional VectSp of F for
k being Nat st 1 <= k & k < dim V holds PencilSpace(V,k) is
with_non_trivial_blocks;
theorem :: PENCIL_4:20
for F being Field for V being finite-dimensional VectSp of F for
k being Nat st 1 <= k & k < dim V holds PencilSpace(V,k) is
identifying_close_blocks;
theorem :: PENCIL_4:21
for F being Field for V being finite-dimensional VectSp of F for k
being Nat st 1 <= k & k < dim V & 3 <= dim V holds PencilSpace(V,k) is PLS;
begin :: Grassmann spaces
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let m,n be Nat;
func SubspaceSet(V,m,n) -> Subset-Family of m Subspaces_of V means
:: PENCIL_4:def 6
for X being set holds X in it iff ex W being Subspace of V st dim W = n & X = m
Subspaces_of W;
end;
theorem :: PENCIL_4:22
for F being Field for V being finite-dimensional VectSp of F for
m,n be Nat st n <= dim V holds SubspaceSet(V,m,n) is non empty;
theorem :: PENCIL_4:23
for F being Field for W1,W2 being finite-dimensional VectSp of F
st (Omega).W1 = (Omega).W2 for m being Nat holds m Subspaces_of W1 = m
Subspaces_of W2;
theorem :: PENCIL_4:24
for F being Field for V being finite-dimensional VectSp of F for
W being Subspace of V for m being Nat st 1<=m & m <= dim V & m Subspaces_of V
c= m Subspaces_of W holds (Omega).V = (Omega).W;
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let m,n be Nat;
func GrassmannSpace(V,m,n) -> strict TopStruct equals
:: PENCIL_4:def 7
TopStruct(#m Subspaces_of V, SubspaceSet(V,m,n)#);
end;
theorem :: PENCIL_4:25
for F being Field for V being finite-dimensional VectSp of F for
m,n being Nat st n <= dim V holds GrassmannSpace(V,m,n) is non void;
theorem :: PENCIL_4:26
for F being Field for V being finite-dimensional VectSp of F for
m,n being Nat st 1 <= m & m < n & n < dim V holds GrassmannSpace(V,m,n) is non
degenerated;
theorem :: PENCIL_4:27
for F being Field for V being finite-dimensional VectSp of F for
m,n being Nat st 1 <= m & m < n & n <= dim V holds GrassmannSpace(V,m,n) is
with_non_trivial_blocks;
theorem :: PENCIL_4:28
for F being Field for V being finite-dimensional VectSp of F for
m being Nat st m+1 <= dim V holds GrassmannSpace(V,m,m+1) is
identifying_close_blocks;
theorem :: PENCIL_4:29
for F being Field for V being finite-dimensional VectSp of F for m
being Nat st 1 <= m & m+1 < dim V holds GrassmannSpace(V,m,m+1) is PLS;
begin :: Veronese spaces
definition
let X be set;
func PairSet(X) -> set means
:: PENCIL_4:def 8
for z being set holds z in it iff ex x,y being
set st x in X & y in X & z={x,y};
end;
registration
let X be non empty set;
cluster PairSet(X) -> non empty;
end;
definition
let t be object, X be set;
func PairSet(t,X) -> set means
:: PENCIL_4:def 9
for z being set holds z in it iff ex y being set st y in X & z={t,y};
end;
registration
let t be set;
let X be non empty set;
cluster PairSet(t,X) -> non empty;
end;
registration
let t be set;
let X be non trivial set;
cluster PairSet(t,X) -> non trivial;
end;
definition
let X be set;
let L be Subset-Family of X;
func PairSetFamily(L) -> Subset-Family of PairSet(X) means
:: PENCIL_4:def 10
for S
being set holds S in it iff ex t being set, l being Subset of X st t in X & l
in L & S=PairSet(t,l);
end;
registration
let X be non empty set;
let L be non empty Subset-Family of X;
cluster PairSetFamily(L) -> non empty;
end;
definition
let S be TopStruct;
func VeroneseSpace(S) -> strict TopStruct equals
:: PENCIL_4:def 11
TopStruct(#PairSet(the
carrier of S), PairSetFamily(the topology of S)#);
end;
registration
let S be non empty TopStruct;
cluster VeroneseSpace(S) -> non empty;
end;
registration
let S be non empty non void TopStruct;
cluster VeroneseSpace(S) -> non void;
end;
registration
let S be non empty non void non degenerated TopStruct;
cluster VeroneseSpace(S) -> non degenerated;
end;
registration
let S be non empty non void with_non_trivial_blocks TopStruct;
cluster VeroneseSpace(S) -> with_non_trivial_blocks;
end;
registration
let S be identifying_close_blocks TopStruct;
cluster VeroneseSpace(S) -> identifying_close_blocks;
end;