:: Spaces of Pencils, {G}rassmann Spaces, and Generalized {V}eronese Spaces
:: by Adam Naumowicz
::
:: Received November 8, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users


begin

theorem Th1: :: PENCIL_4:1
for k, n being Nat st k < n & 3 <= n & not k + 1 < n holds
2 <= k
proof end;

theorem :: PENCIL_4:2
canceled;

Lm1: for X being finite set
for n being Nat st n <= card X holds
ex Y being Subset of X st card Y = n
by FINSEQ_4:87;

theorem Th3: :: PENCIL_4:3
for F being Field
for V being VectSp of F
for W being Subspace of V holds W is Subspace of (Omega). V
proof end;

theorem Th4: :: PENCIL_4:4
for F being Field
for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V
proof end;

theorem Th5: :: PENCIL_4:5
for F being Field
for V being VectSp of F
for W being Subspace of V holds (Omega). W is Subspace of V
proof end;

theorem Th6: :: PENCIL_4:6
for F being Field
for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V
proof end;

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 :Def1: :: 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 = {} ;
consistency
for b1 being Subset of (Subspaces V) holds verum ;
existence
( ( W1 is Subspace of W2 implies ex b1 being Subset of (Subspaces V) st
for W being strict Subspace of V holds
( W in b1 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( W1 is not Subspace of W2 implies ex b1 being Subset of (Subspaces V) st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in b1 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in b2 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies b1 = b2 ) & ( W1 is not Subspace of W2 & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
end;

:: deftheorem Def1 defines segment PENCIL_4:def 1 :
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V
for b5 being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 implies ( b5 = segment (W1,W2) iff for W being strict Subspace of V holds
( W in b5 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) ) & ( W1 is not Subspace of W2 implies ( b5 = segment (W1,W2) iff b5 = {} ) ) );

theorem Th7: :: 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
segment (W1,W2) = segment (W3,W4)
proof end;

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)};
coherence
(segment (W1,W2)) \ {((Omega). W1),((Omega). W2)} is Subset of (Subspaces V) ;
end;

:: deftheorem defines pencil PENCIL_4:def 2 :
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V holds pencil (W1,W2) = (segment (W1,W2)) \ {((Omega). W1),((Omega). W2)};

theorem :: PENCIL_4:8
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) by Th7;

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);
coherence
(pencil (W1,W2)) /\ (k Subspaces_of V) is Subset of (k Subspaces_of V) by XBOOLE_1:17;
end;

:: deftheorem defines pencil PENCIL_4:def 3 :
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V
for k being Nat holds pencil (W1,W2,k) = (pencil (W1,W2)) /\ (k Subspaces_of V);

theorem Th9: :: PENCIL_4:9
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 )
proof end;

theorem :: PENCIL_4:10
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) by Th7;

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 :Def4: :: 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) ) );
existence
ex b1 being Subset-Family of (k Subspaces_of V) st
for X being set holds
( X in b1 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) ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (k Subspaces_of V) st ( for X being set holds
( X in b1 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) ) ) ) & ( for X being set holds
( X in b2 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) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Pencils_of PENCIL_4:def 4 :
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for b4 being Subset-Family of (k Subspaces_of V) holds
( b4 = k Pencils_of V iff for X being set holds
( X in b4 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) ) ) );

theorem Th11: :: PENCIL_4:11
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
proof end;

theorem Th12: :: PENCIL_4:12
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 )
proof end;

theorem Th13: :: PENCIL_4:13
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
proof end;

theorem Th14: :: PENCIL_4:14
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
proof end;

theorem Th15: :: PENCIL_4:15
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
proof end;

theorem Th16: :: 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 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
proof end;

theorem Th17: :: PENCIL_4:17
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 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
proof end;

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) #);
coherence
TopStruct(# (k Subspaces_of V),(k Pencils_of V) #) is strict TopStruct ;
end;

:: deftheorem defines PencilSpace PENCIL_4:def 5 :
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat holds PencilSpace (V,k) = TopStruct(# (k Subspaces_of V),(k Pencils_of V) #);

theorem :: PENCIL_4:18
canceled;

theorem Th19: :: 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
not PencilSpace (V,k) is void
proof end;

theorem Th20: :: 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 & 3 <= dim V holds
not PencilSpace (V,k) is degenerated
proof end;

theorem Th21: :: 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 holds
PencilSpace (V,k) is with_non_trivial_blocks
proof end;

theorem Th22: :: PENCIL_4:22
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
proof end;

theorem :: PENCIL_4:23
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 by Th19, Th20, Th21, Th22, VECTSP_9:40;

begin

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 :Def6: :: 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 ) );
existence
ex b1 being Subset-Family of (m Subspaces_of V) st
for X being set holds
( X in b1 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (m Subspaces_of V) st ( for X being set holds
( X in b1 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds
( X in b2 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines SubspaceSet PENCIL_4:def 6 :
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat
for b5 being Subset-Family of (m Subspaces_of V) holds
( b5 = SubspaceSet (V,m,n) iff for X being set holds
( X in b5 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) );

theorem Th24: :: PENCIL_4:24
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not SubspaceSet (V,m,n) is empty
proof end;

theorem Th25: :: PENCIL_4:25
for F being Field
for W1, W2 being finite-dimensional VectSp of F st (Omega). W1 = (Omega). W2 holds
for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
proof end;

theorem Th26: :: PENCIL_4:26
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
proof end;

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)) #);
coherence
TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #) is strict TopStruct ;
end;

:: deftheorem defines GrassmannSpace PENCIL_4:def 7 :
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat holds GrassmannSpace (V,m,n) = TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #);

theorem :: PENCIL_4:27
canceled;

theorem Th28: :: PENCIL_4:28
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not GrassmannSpace (V,m,n) is void
proof end;

theorem Th29: :: PENCIL_4:29
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
not GrassmannSpace (V,m,n) is degenerated
proof end;

theorem Th30: :: PENCIL_4:30
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
proof end;

theorem Th31: :: PENCIL_4:31
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
proof end;

theorem :: PENCIL_4:32
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
proof end;

begin

definition
let X be set ;
func PairSet X -> set means :Def8: :: 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} ) );
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
proof end;
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in b2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :
for X being set
for b2 being set holds
( b2 = PairSet X iff for z being set holds
( z in b2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) );

registration
let X be non empty set ;
cluster PairSet X -> non empty ;
coherence
not PairSet X is empty
proof end;
end;

definition
let t, X be set ;
func PairSet (t,X) -> set means :Def9: :: PENCIL_4:def 9
 for z being set holds
( z in it iff ex y being set st
( y in X & z = {t,y} ) );
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex y being set st
( y in X & z = {t,y} ) )
proof end;
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex y being set st
( y in X & z = {t,y} ) ) ) & ( for z being set holds
( z in b2 iff ex y being set st
( y in X & z = {t,y} ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :
for t, X being set
for b3 being set holds
( b3 = PairSet (t,X) iff for z being set holds
( z in b3 iff ex y being set st
( y in X & z = {t,y} ) ) );

registration
let t be set ;
let X be non empty set ;
cluster PairSet (t,X) -> non empty ;
coherence
not PairSet (t,X) is empty
proof end;
end;

registration
let t be set ;
let X be non trivial set ;
cluster PairSet (t,X) -> non trivial ;
coherence
not PairSet (t,X) is trivial
proof end;
end;

definition
let X be set ;
let L be Subset-Family of X;
func PairSetFamily L -> Subset-Family of (PairSet X) means :Def10: :: PENCIL_4:def 10
 for S being set holds
( S in it iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) );
existence
ex b1 being Subset-Family of (PairSet X) st
for S being set holds
( S in b1 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (PairSet X) st ( for S being set holds
( S in b1 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) & ( for S being set holds
( S in b2 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :
for X being set
for L being Subset-Family of X
for b3 being Subset-Family of (PairSet X) holds
( b3 = PairSetFamily L iff for S being set holds
( S in b3 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) );

registration
let X be non empty set ;
let L be non empty Subset-Family of X;
cluster PairSetFamily L -> non empty ;
coherence
not PairSetFamily L is empty
proof end;
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) #);
coherence
TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #) is strict TopStruct ;
end;

:: deftheorem defines VeroneseSpace PENCIL_4:def 11 :
for S being TopStruct holds VeroneseSpace S = TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);

registration
let S be non empty TopStruct ;
cluster VeroneseSpace S -> non empty strict ;
coherence
not VeroneseSpace S is empty ;
end;

registration
let S be non empty non void TopStruct ;
cluster VeroneseSpace S -> strict non void ;
coherence
not VeroneseSpace S is void
proof end;
end;

registration
let S be non empty non void non degenerated TopStruct ;
cluster VeroneseSpace S -> strict non degenerated ;
coherence
not VeroneseSpace S is degenerated
proof end;
end;

registration
let S be non empty non void with_non_trivial_blocks TopStruct ;
cluster VeroneseSpace S -> strict with_non_trivial_blocks ;
coherence
VeroneseSpace S is with_non_trivial_blocks
proof end;
end;

registration
let S be identifying_close_blocks TopStruct ;
cluster VeroneseSpace S -> strict identifying_close_blocks ;
coherence
VeroneseSpace S is identifying_close_blocks
proof end;
end;