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