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

theorem Th1: :: PENCIL_4:1

for k, n being Nat st k < n & 3 <= n & not k + 1 < n holds
2 <= k

proof end;

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

theorem Th2: :: 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

proof end;

theorem Th3: :: 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

proof end;

theorem Th4: :: 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

proof end;

theorem Th5: :: PENCIL_4:5

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 b₁ being Subset of (Subspaces V) holds verum ;
existence
( ( W1 is Subspace of W2 implies ex b₁ being Subset of (Subspaces V) st
for W being strict Subspace of V holds
( W in b₁ iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( W1 is not Subspace of W2 implies ex b₁ being Subset of (Subspaces V) st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in b₁ iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in b₂ iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies b₁ = b₂ ) & ( W1 is not Subspace of W2 & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

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 b₅ being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 implies ( b₅ = segment (W1,W2) iff for W being strict Subspace of V holds
( W in b₅ iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) ) & ( W1 is not Subspace of W2 implies ( b₅ = segment (W1,W2) iff b₅ = {} ) ) );

theorem Th6: :: 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)

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: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) by Th6;

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 Th8: :: 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 )

proof end;

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) by Th6;

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 b₁ being Subset-Family of (k Subspaces_of V) st
for X being set holds
( X in b₁ 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 b₁, b₂ being Subset-Family of (k Subspaces_of V) st ( for X being set holds
( X in b₁ 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 b₂ 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
b₁ = b₂

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 b₄ being Subset-Family of (k Subspaces_of V) holds
( b₄ = k Pencils_of V iff for X being set holds
( X in b₄ 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 Th10: :: 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
not k Pencils_of V is empty

proof end;

theorem Th11: :: 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 )

proof end;

theorem Th12: :: 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

proof end;

theorem Th13: :: 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

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, 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 Th15: :: 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 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 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
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 Th17: :: 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
not PencilSpace (V,k) is void by Th10;

theorem Th18: :: 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
not PencilSpace (V,k) is degenerated

proof end;

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
PencilSpace (V,k) is with_non_trivial_blocks

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 holds
PencilSpace (V,k) is identifying_close_blocks

proof end;

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 by Th17, Th18, Th19, Th20, VECTSP_9:36;

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 b₁ being Subset-Family of (m Subspaces_of V) st
for X being set holds
( X in b₁ iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of (m Subspaces_of V) st ( for X being set holds
( X in b₁ iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds
( X in b₂ iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) holds
b₁ = b₂

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 b₅ being Subset-Family of (m Subspaces_of V) holds
( b₅ = SubspaceSet (V,m,n) iff for X being set holds
( X in b₅ iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) );

theorem Th22: :: PENCIL_4:22

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 Th23: :: PENCIL_4:23

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

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 Th25: :: 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
not GrassmannSpace (V,m,n) is void by Th22;

theorem Th26: :: 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
not GrassmannSpace (V,m,n) is degenerated

proof end;

theorem Th27: :: 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

proof end;

theorem Th28: :: 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

proof end;

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

proof end;

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 b₁ being set st
for z being set holds
( z in b₁ iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for z being set holds
( z in b₁ iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in b₂ iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :
for X, b₂ being set holds
( b₂ = PairSet X iff for z being set holds
( z in b₂ 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 be object ;
let 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 b₁ being set st
for z being set holds
( z in b₁ iff ex y being set st
( y in X & z = {t,y} ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for z being set holds
( z in b₁ iff ex y being set st
( y in X & z = {t,y} ) ) ) & ( for z being set holds
( z in b₂ iff ex y being set st
( y in X & z = {t,y} ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :
for t being object
for X, b₃ being set holds
( b₃ = PairSet (t,X) iff for z being set holds
( z in b₃ 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 b₁ being Subset-Family of (PairSet X) st
for S being set holds
( S in b₁ 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 b₁, b₂ being Subset-Family of (PairSet X) st ( for S being set holds
( S in b₁ 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 b₂ iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :
for X being set
for L being Subset-Family of X
for b₃ being Subset-Family of (PairSet X) holds
( b₃ = PairSetFamily L iff for S being set holds
( S in b₃ 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 ;

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;