:: Spaces of Pencils, {G}rassmann Spaces, and Generalized {V}eronese
:: Spaces
:: by Adam Naumowicz
::
:: Received November 8, 2004
:: Copyright (c) 2004-2026 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;
definitions TARSKI, XBOOLE_0, PENCIL_1, VECTSP_4;
equalities XBOOLE_0, STRUCT_0, VECTSP_4, RLVECT_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, STRUCT_0, PENCIL_1;
theorems XBOOLE_0, ZFMISC_1, NAT_1, TARSKI, PENCIL_1, CARD_1, XBOOLE_1,
CARD_2, SUBSET_1, VECTSP_5, VECTSP_9, VECTSP_4, RLVECT_1, VECTSP_7,
VECTSP10, VECTSP_1, EULER_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D,
FINSEQ_4;
schemes XBOOLE_0, SUBSET_1;
begin :: Spaces of pencils
theorem Th1:
for k,n being Nat st k < n & 3 <= n holds k+1 < n or 2 <= k
proof
let k,n be Nat such that
A1: k < n and
A2: 3 <= n;
assume
A3: k+1 >= n;
k+1 <= n by A1,NAT_1:13;
then 3 <= k+1 by A2,A3,XXREAL_0:1;
then 3-1 <= k+1-1 by XREAL_1:9;
hence thesis;
end;
Lm1:
for X being finite set for n being Nat st n <= card X ex Y being
Subset of X st card Y = n by FINSEQ_4:72;
theorem Th2:
for F being Field for V being VectSp of F for W being Subspace of
V holds W is Subspace of (Omega).V
proof
let F be Field;
let V be VectSp of F;
let W be Subspace of V;
thus the carrier of W c= the carrier of (Omega).V by VECTSP_4:def 2;
thus 0.W = 0.V by VECTSP_4:def 2
.= 0.(Omega).V;
thus thesis by VECTSP_4:def 2;
end;
theorem Th3:
for F being Field for V being VectSp of F for W being Subspace of
(Omega).V holds W is Subspace of V
proof
let F be Field;
let V be VectSp of F;
let W be Subspace of (Omega).V;
thus the carrier of W c= the carrier of V by VECTSP_4:def 2;
thus 0.W = 0.(Omega).V by VECTSP_4:def 2
.= 0.V;
thus thesis by VECTSP_4:def 2;
end;
theorem Th4:
for F being Field for V being VectSp of F for W being Subspace of
V holds (Omega).W is Subspace of V
proof
let F be Field;
let V be VectSp of F;
let W be Subspace of V;
thus the carrier of (Omega).W c= the carrier of V by VECTSP_4:def 2;
thus 0.(Omega).W = 0.W .= 0.V by VECTSP_4:def 2;
thus thesis by VECTSP_4:def 2;
end;
theorem Th5:
for F being Field for V,W being VectSp of F holds (Omega).W is
Subspace of V implies W is Subspace of V
proof
let F be Field;
let V,W be VectSp of F;
assume
A1: (Omega).W is Subspace of V;
hence the carrier of W c= the carrier of V by VECTSP_4:def 2;
thus 0.W = 0.(Omega).W .= 0.V by A1,VECTSP_4:def 2;
thus thesis by A1,VECTSP_4:def 2;
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:
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;
existence
proof
hereby
defpred P[set] means for W being Subspace of V st W=$1 holds W1 is
Subspace of W & W is Subspace of W2;
set A=Subspaces(V);
assume W1 is Subspace of W2;
consider X being Subset of A such that
A1: for x being set holds x in X iff x in A & P[x] from SUBSET_1:sch
1;
take X;
let W be strict Subspace of V;
thus W in X implies W1 is Subspace of W & W is Subspace of W2 by A1;
assume W1 is Subspace of W & W is Subspace of W2;
then
A2: P[W];
W in Subspaces(V) by VECTSP_5:def 3;
hence W in X by A1,A2;
end;
hereby
reconsider W={} as Subset of Subspaces(V) by XBOOLE_1:2;
assume not W1 is Subspace of W2;
take W;
thus W={};
end;
end;
uniqueness
proof
let S,T be Subset of Subspaces(V);
now
assume W1 is Subspace of W2;
assume that
A3: for W being strict Subspace of V holds W in S iff W1 is Subspace
of W & W is Subspace of W2 and
A4: for W being strict Subspace of V holds W in T iff W1 is Subspace
of W & W is Subspace of W2;
now
let x be object;
thus x in S implies x in T
proof
assume
A5: x in S;
then consider x1 being strict Subspace of V such that
A6: x1=x by VECTSP_5:def 3;
x1 in S iff W1 is Subspace of x1 & x1 is Subspace of W2 by A3;
hence thesis by A4,A5,A6;
end;
assume
A7: x in T;
then consider x1 being strict Subspace of V such that
A8: x1=x by VECTSP_5:def 3;
x1 in T iff W1 is Subspace of x1 & x1 is Subspace of W2 by A4;
hence x in S by A3,A7,A8;
end;
hence S=T by TARSKI:2;
end;
hence thesis;
end;
end;
theorem Th6:
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
let F be Field;
let V be VectSp of F;
let W1,W2,W3,W4 be Subspace of V;
assume that
A1: W1 is Subspace of W2 and
A2: W3 is Subspace of W4 and
A3: (Omega).W1=(Omega).W3 and
A4: (Omega).W2=(Omega).W4;
thus segment(W1,W2) c= segment(W3,W4)
proof
let a be object;
assume
A5: a in segment(W1,W2);
then ex A1 being strict Subspace of V st A1=a by VECTSP_5:def 3;
then reconsider A=a as strict Subspace of V;
A is Subspace of W2 by A1,A5,Def1;
then A is Subspace of (Omega).W2 by Th2;
then
A6: A is Subspace of W4 by A4,Th3;
W1 is Subspace of A by A1,A5,Def1;
then (Omega).W1 is Subspace of A by Th4;
then W3 is Subspace of A by A3,Th5;
hence thesis by A2,A6,Def1;
end;
let a be object;
assume
A7: a in segment(W3,W4);
then ex A1 being strict Subspace of V st A1=a by VECTSP_5:def 3;
then reconsider A=a as strict Subspace of V;
A is Subspace of W4 by A2,A7,Def1;
then A is Subspace of (Omega).W4 by Th2;
then
A8: A is Subspace of W2 by A4,Th3;
W3 is Subspace of A by A2,A7,Def1;
then (Omega).W3 is Subspace of A by Th4;
then W1 is Subspace of A by A3,Th5;
hence thesis by A1,A8,Def1;
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
segment(W1,W2) \ {
(Omega).W1,(Omega).W2};
coherence;
end;
theorem
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 (W1,W2)
/\ (k Subspaces_of V);
coherence by XBOOLE_1:17;
end;
theorem Th8:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
let W1,W2,W be Subspace of V;
assume
A1: W in pencil(W1,W2,k);
then
A2: ex X being strict Subspace of V st W=X & dim X=k by VECTSP_9:def 2;
W in pencil(W1,W2) by A1,XBOOLE_0:def 4;
then
A3: W in segment(W1,W2) by XBOOLE_0:def 5;
then W1 is Subspace of W2 by Def1;
hence thesis by A2,A3,Def1;
end;
theorem
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:
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
proof
defpred P[object] means
ex W1,W2 being Subspace of V st W1 is Subspace of W2
& dim W1+1=k & dim W2=k+1 & $1=pencil(W1,W2,k);
set A = bool (k Subspaces_of V);
consider X being set such that
A1: for x being object holds x in X iff x in A & P[x] from XBOOLE_0:sch 1;
X c= A
by A1;
then reconsider X as Subset-Family of (k Subspaces_of V);
take X;
let x be set;
thus x in X implies 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) by A1;
given W1,W2 being Subspace of V such that
A2: W1 is Subspace of W2 & dim W1+1=k & dim W2=k+1 & x=pencil(W1,W2,k);
thus thesis by A1,A2;
end;
uniqueness
proof
let S,T be Subset-Family of (k Subspaces_of V) such that
A3: for X being set holds X in S 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) and
A4: for X being set holds X in T 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);
now
let x be object;
thus x in S implies x in T
proof
assume x in S;
then
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) by A3;
hence thesis by A4;
end;
assume x in T;
then
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) by A4;
hence x in S by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th10:
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
proof
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
assume that
A1: 1 <= k and
A2: k < dim V;
k+1 <= dim V by A2,NAT_1:13;
then consider W2 being strict Subspace of V such that
A3: dim W2 = k+1 by VECTSP_9:35;
k-'1<=k by NAT_D:35;
then k-'1 <= dim W2 by A3,NAT_1:13;
then consider W1 being strict Subspace of W2 such that
A4: dim W1 = k-'1 by VECTSP_9:35;
reconsider W19=W1 as Subspace of V by VECTSP_4:26;
dim W1+1=k by A1,A4,XREAL_1:235;
then pencil(W19,W2,k) in k Pencils_of V by A3,Def4;
hence thesis;
end;
theorem Th11:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let W1,W2,P0,Q0 be Subspace of V;
let k be Nat such that
A1: dim W1+1=k and
A2: dim W2=k+1 and
A3: P0 in pencil(W1,W2,k) and
A4: Q0 in pencil(W1,W2,k) and
A5: P0<>Q0;
consider Q being strict Subspace of V such that
A6: Q=Q0 and
A7: dim Q = k by A4,VECTSP_9:def 2;
A8: W1 is Subspace of Q by A4,A6,Th8;
consider P being strict Subspace of V such that
A9: P=P0 and
A10: dim P = k by A3,VECTSP_9:def 2;
W1 is Subspace of P by A3,A9,Th8;
then
A11: W1 is Subspace of (P/\Q) by A8,VECTSP_5:19;
P/\Q is Subspace of P by VECTSP_5:15;
then
A12: dim(P/\Q)<=k by A10,VECTSP_9:25;
per cases by A1,A12,A11,NAT_1:9,VECTSP_9:25;
suppose
A13: dim W1 = dim (P/\Q);
then (Omega).W1 = (Omega).(P/\Q) by A11,VECTSP_9:28;
hence P0/\Q0 = (Omega).W1 by A9,A6;
P is Subspace of W2 & Q is Subspace of W2 by A3,A4,A9,A6,Th8;
then
A14: P+Q is Subspace of W2 by VECTSP_5:34;
dim(P+Q)+dim W1-dim W1 = dim P + dim Q - dim W1 by A13,VECTSP_9:32;
then (Omega).(W2) = (Omega).(P+Q) by A1,A2,A10,A7,A14,VECTSP_9:28;
hence thesis by A9,A6;
end;
suppose
A15: dim (P/\Q)=k;
P/\Q is Subspace of Q by VECTSP_5:15;
then
A16: (Omega).(P/\Q) = (Omega).Q by A7,A15,VECTSP_9:28;
P/\Q is Subspace of P by VECTSP_5:15;
then (Omega).(P/\Q) = (Omega).P by A10,A15,VECTSP_9:28;
hence thesis by A5,A9,A6,A16;
end;
end;
theorem Th12:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let v be Vector of V;
assume v <> 0.V;
then
A1: v <> 0.Lin{v} by VECTSP_4:11;
v in {v} by TARSKI:def 1;
then v in Lin{v} by VECTSP_7:8;
then reconsider v0=v as Vector of Lin{v};
Lin{v0}=Lin{v} & (Omega).Lin{v0} = Lin{v0} by VECTSP_9:17;
hence thesis by A1,VECTSP_9:30;
end;
theorem Th13:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let W be Subspace of V;
let v be Vector of V such that
A1: not v in W;
the carrier of (Omega).(W/\Lin{v}) = {0.(W/\Lin{v})}
proof
thus the carrier of (Omega).(W/\Lin{v}) c= {0.(W/\Lin{v})}
proof
let a be object;
assume a in the carrier of (Omega).(W/\Lin{v});
then
A2: a in (the carrier of W)/\the carrier of Lin{v} by VECTSP_5:def 2;
then a in the carrier of Lin{v} by XBOOLE_0:def 4;
then a in Lin{v};
then consider e being Element of F such that
A3: a=e*v by VECTSP10:3;
a in the carrier of W by A2,XBOOLE_0:def 4;
then
A4: a in W;
now
assume e<>0.F;
then v=e"*(e*v) by VECTSP_1:20;
hence contradiction by A1,A4,A3,VECTSP_4:21;
end;
then a=0.V by A3,VECTSP_1:14;
then a = 0.(W/\Lin{v}) by VECTSP_4:11;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {0.(W/\Lin{v})};
then a=0.(W/\Lin{v}) by TARSKI:def 1;
then a=0.V by VECTSP_4:11;
then a in W/\Lin{v} by VECTSP_4:17;
hence thesis;
end;
then (Omega).(W/\Lin{v})=(0).(W/\Lin{v}) by VECTSP_4:def 3;
then
A5: dim(W/\Lin{v})=0 by VECTSP_9:29;
A6: dim(W+Lin{v}) + dim(W/\Lin{v}) = dim W + dim Lin{v} by VECTSP_9:32;
v <> 0.V by A1,VECTSP_4:17;
hence thesis by A5,A6,Th12;
end;
theorem Th14:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let W be Subspace of V;
let v,u be Vector of V such that
A1: v<>u and
A2: {v,u} is linearly-independent and
A3: W/\Lin{v,u}=(0).V;
u in {v,u} by TARSKI:def 2;
then
A4: u in Lin{v,u} by VECTSP_7:8;
v in {v,u} by TARSKI:def 2;
then v in Lin{v,u} by VECTSP_7:8;
then reconsider v1=v,u1=u as Vector of Lin{v,u} by A4;
reconsider L={v1,u1} as linearly-independent Subset of Lin{v,u} by A2,
VECTSP_9:12;
(Omega).Lin{v,u}=Lin L by VECTSP_9:17;
then
A5: dim Lin{v,u}=2 by A1,VECTSP_9:31;
(Omega).(W/\Lin{v,u})=(0).(W/\Lin{v,u}) by A3,VECTSP_4:36;
then dim(W/\Lin{v,u}) = 0 by VECTSP_9:29;
hence dim(W+Lin{v,u}) = dim(W+Lin{v,u}) + dim(W/\Lin{v,u})
.= dim W + 2 by A5,VECTSP_9:32;
end;
theorem Th15:
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)
proof
let F be Field;
let V be finite-dimensional VectSp of F;
let W1,W2 be Subspace of V such that
A1: W1 is Subspace of W2;
let k be Nat such that
A2: dim W1+1=k and
A3: dim W2=k+1;
let v be Vector of V such that
A4: v in W2 and
A5: not v in W1;
set W=W1+Lin{v};
A6: dim W = k by A2,A5,Th13;
then
A7: W in k Subspaces_of V by VECTSP_9:def 2;
v in the carrier of W2 by A4;
then {v} c= the carrier of W2 by ZFMISC_1:31;
then Lin{v} is Subspace of W2 by VECTSP_9:16;
then W1 is Subspace of W & W is Subspace of W2 by A1,VECTSP_5:7,34;
then
A8: W in segment(W1,W2) by A1,Def1;
dim (Omega).W2 = k+1 by A3,VECTSP_9:27;
then
A9: W <> (Omega).W2 by A6;
dim (Omega).W1 + 1 = k by A2,VECTSP_9:27;
then W <> (Omega).W1 by A6;
then not W in {(Omega).W1,(Omega).W2} by A9,TARSKI:def 2;
then W in pencil(W1,W2) by A8,XBOOLE_0:def 5;
hence thesis by A7,XBOOLE_0:def 4;
end;
theorem Th16:
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
proof
let F be Field;
let V be finite-dimensional VectSp of F;
let W1,W2 be Subspace of V;
assume W1 is Subspace of W2;
then reconsider U=W1 as Subspace of W2;
let k be Nat such that
A1: dim W1+1=k & dim W2=k+1;
set W = the Linear_Compl of U;
A2: W2 is_the_direct_sum_of W,U by VECTSP_5:def 5;
then
A3: W /\ U = (0).W2 by VECTSP_5:def 4;
dim W2 = dim U + dim W by A2,VECTSP_9:34;
then consider u,v being Vector of W such that
A4: u <> v and
A5: {u,v} is linearly-independent and
(Omega).W = Lin{u,v} by A1,VECTSP_9:31;
A6: now
assume v in Lin{u};
then ex a being Element of F st v = a*u by VECTSP10:3;
hence contradiction by A4,A5,VECTSP_7:5;
end;
reconsider u,v as Vector of W2 by VECTSP_4:10;
reconsider u1=u,v1=v as Vector of V by VECTSP_4:10;
A7: v in W;
A8: now
assume v in W1;
then v in (0).W2 by A3,A7,VECTSP_5:3;
then v=0.W2 by VECTSP_4:35;
then v=0.W by VECTSP_4:11;
hence contradiction by A5,VECTSP_7:4;
end;
A9: u in W;
A10: now
assume u in W1;
then u in (0).W2 by A3,A9,VECTSP_5:3;
then u=0.W2 by VECTSP_4:35;
then u=0.W by VECTSP_4:11;
hence contradiction by A5,VECTSP_7:4;
end;
v in {v1} by TARSKI:def 1;
then v in Lin{v1} by VECTSP_7:8;
then
A11: v in W1+Lin{v1} by VECTSP_5:2;
A12: not v in Lin{u} by A6,VECTSP10:13;
A13: now
reconsider Wx=W as Subspace of V by VECTSP_4:26;
assume W1+Lin{v1} = W1+Lin{u1};
then consider h,j being Vector of V such that
A14: h in W1 and
A15: j in Lin{u1} and
A16: v1 = h+j by A11,VECTSP_5:1;
consider a being Element of F such that
A17: j=a*u1 by A15,VECTSP10:3;
v1-a*u1=h+(a*u1-a*u1) by A16,A17,RLVECT_1:def 3;
then v1-a*u1=h+0.V by RLVECT_1:15;
then
A18: v1-a*u1=h by RLVECT_1:4;
a*u = a*u1 by VECTSP_4:14;
then
A19: v1-a*u1 = v-a*u by VECTSP_4:16;
a*u in Wx by A9,VECTSP_4:21;
then v-a*u in Wx by A7,VECTSP_4:23;
then v-a*u in W/\U by A14,A18,A19,VECTSP_5:3;
then v-a*u = 0.W2 by A3,VECTSP_4:35;
then h = 0.V by A18,A19,VECTSP_4:11;
then v1 = j by A16,RLVECT_1:4;
hence contradiction by A12,A15,VECTSP10:13;
end;
v in W2;
then
A20: W1+Lin{v1} in pencil(W1,W2,k) by A1,A8,Th15;
u in W2;
then W1+Lin{u1} in pencil(W1,W2,k) by A1,A10,Th15;
then 2 c= card pencil(W1,W2,k) by A13,A20,PENCIL_1:2;
hence thesis by PENCIL_1:4;
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
TopStruct(#k Subspaces_of V
, k Pencils_of V#);
coherence;
end;
theorem Th17:
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
by Th10;
theorem Th18:
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
proof
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat such that
A1: 1 <= k and
A2: k < dim V and
A3: 3 <= dim V;
set S=PencilSpace(V,k);
now
let B be Block of S;
the topology of S is non empty by A1,A2,Th10;
then consider W1,W2 being Subspace of V such that
A4: W1 is Subspace of W2 and
A5: dim W1+1=k and
A6: dim W2=k+1 and
A7: B=pencil(W1,W2,k) by Def4;
A8: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
per cases by A2,A3,Th1;
suppose
k+1 < dim V;
then
A9: (Omega).W2 <> (Omega).V by A6,VECTSP_9:28;
A10: now
assume
A11: the carrier of V = the carrier of W2;
(Omega).W2 is Subspace of V by Th4;
hence contradiction by A9,A11,VECTSP_4:29;
end;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then not the carrier of V c= the carrier of W2 by A10;
then consider v being object such that
A12: v in the carrier of V and
A13: not v in the carrier of W2;
reconsider v as Vector of V by A12;
set X=W1+Lin{v};
A14: now
v in {v} by TARSKI:def 1;
then v in Lin{v} by VECTSP_7:8;
then v in X by VECTSP_5:2;
then
A15: v in the carrier of X;
assume X in B;
then X is Subspace of W2 by A7,Th8;
then the carrier of X c= the carrier of W2 by VECTSP_4:def 2;
hence contradiction by A13,A15;
end;
not v in W2 by A13;
then dim X = k by A4,A5,Th13,VECTSP_4:8;
hence the carrier of S <> B by A14,VECTSP_9:def 2;
end;
suppose
A16: 2 <= k & k+1>=dim V;
set I = the Basis of W1;
reconsider I1=I as finite Subset of W1;
2-1 <= dim W1+1-1 by A5,A16,XREAL_1:9;
then 1 <= card I1 by VECTSP_9:def 1;
then I1 is non empty;
then consider i being object such that
A17: i in I;
reconsider i as Vector of W1 by A17;
reconsider J=I1\{i} as finite Subset of V by A8,XBOOLE_1:1;
I is linearly-independent by VECTSP_7:def 3;
then I\{i} is linearly-independent by VECTSP_7:1,XBOOLE_1:36;
then reconsider JJ=I\{i} as linearly-independent Subset of V by
VECTSP_9:11;
J c= the carrier of Lin J
proof
let a be object;
assume a in J;
then a in Lin J by VECTSP_7:8;
hence thesis;
end;
then reconsider JJJ=JJ as linearly-independent Subset of Lin J by
VECTSP_9:12;
Lin JJJ = Lin J by VECTSP_9:17;
then
A18: J is Basis of Lin J by VECTSP_7:def 3;
A19: card I = dim W1 by VECTSP_9:def 1;
set T = the Linear_Compl of W1;
A20: V is_the_direct_sum_of W1,T by VECTSP_5:38;
then
A21: W1/\T=(0).V by VECTSP_5:def 4;
k+1 <= dim V by A2,NAT_1:13;
then dim V = k+1 by A16,XXREAL_0:1;
then k+1 - (dim W1 + 1) = dim W1 + dim T - (dim W1 + 1) by A20,
VECTSP_9:34;
then consider u,v being Vector of T such that
A22: u<>v and
A23: {u,v} is linearly-independent and
A24: (Omega).T=Lin{u,v} by A5,VECTSP_9:31;
the carrier of T c= the carrier of V & u in the carrier of T by
VECTSP_4:def 2;
then reconsider u1=u,v1=v as Vector of V;
reconsider Y={u,v} as linearly-independent Subset of V by A23,VECTSP_9:11
;
A25: Y={u,v};
Lin (I\{i}) is Subspace of Lin I by VECTSP_7:13,XBOOLE_1:36;
then
A26: Lin J is Subspace of W1 by VECTSP_9:17;
the carrier of ((Lin J)/\Lin{u1,v1}) c= the carrier of (0).V
proof
let a be object;
assume a in the carrier of ((Lin J)/\Lin{u1,v1});
then
A27: a in (Lin J)/\Lin{u1,v1};
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin{u,v} by VECTSP_9:17;
then a in the carrier of the ModuleStr of T by A24;
then
A28: a in T;
a in Lin J by A27,VECTSP_5:3;
then a in W1 by A26,VECTSP_4:8;
then a in W1 /\ T by A28,VECTSP_5:3;
hence thesis by A21;
end;
then
A29: (0).V is Subspace of (Lin J)/\Lin{u1,v1} & (Lin J)/\Lin{u1,v1} is
Subspace of (0).V by VECTSP_4:27,39;
card J = card I1 - card{i} by A17,EULER_1:4
.= dim W1 - 1 by A19,CARD_1:30;
then dim Lin J = dim W1 - 1 by A18,VECTSP_9:def 1;
then
A30: dim ((Lin J)+Lin{u1,v1}) = dim W1 - 1 + 2 by A22,A25,A29,Th14,VECTSP_4:25
;
A31: Lin I = (Omega).W1 by VECTSP_7:def 3;
A32: i in W1;
now
A33: now
reconsider IV=I as Subset of V by A8,XBOOLE_1:1;
assume
A34: i in (Lin J)+Lin{u1,v1};
IV c= the carrier of (Lin J)+Lin{u1,v1}
proof
let a be object;
{i} c= I by A17,ZFMISC_1:31;
then
A35: I\{i}\/{i}=I by XBOOLE_1:45;
assume
A36: a in IV;
per cases by A36,A35,XBOOLE_0:def 3;
suppose
a in J;
then
A37: a in Lin J by VECTSP_7:8;
then a in V by VECTSP_4:9;
then reconsider o=a as Vector of V;
o in (Lin J)+Lin{u1,v1} by A37,VECTSP_5:2;
hence thesis;
end;
suppose
a in {i};
then a=i by TARSKI:def 1;
hence thesis by A34;
end;
end;
then Lin IV is Subspace of (Lin J)+Lin{u1,v1} by VECTSP_9:16;
then Lin I is Subspace of (Lin J)+Lin{u1,v1} by VECTSP_9:17;
then
A38: W1 is Subspace of (Lin J)+Lin{u1,v1} by A31,Th5;
the carrier of (W1/\Lin{u1,v1}) c= the carrier of (0).V
proof
let a be object;
assume a in the carrier of (W1/\Lin{u1,v1});
then
A39: a in W1/\Lin{u1,v1};
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of the ModuleStr of T by A24;
then
A40: a in T;
a in W1 by A39,VECTSP_5:3;
then a in W1 /\ T by A40,VECTSP_5:3;
hence thesis by A21;
end;
then (0).V is Subspace of W1/\Lin{u1,v1} & W1/\Lin{u1,v1} is
Subspace of (0).V by VECTSP_4:27,39;
then
A41: dim (W1+Lin{u1,v1}) = dim W1 + 2 by A22,A25,Th14,VECTSP_4:25;
Lin{u1,v1} is Subspace of (Lin J)+Lin{u1,v1} by VECTSP_5:7;
then W1+Lin{u1,v1} is Subspace of (Lin J)+Lin{u1,v1} by A38,
VECTSP_5:34;
then dim W1 + 1+1 <= dim W1 + 1 by A30,A41,VECTSP_9:25;
hence contradiction by NAT_1:13;
end;
assume (Lin J)+Lin{u1,v1} in B;
then W1 is Subspace of (Lin J)+Lin{u1,v1} by A7,Th8;
hence contradiction by A32,A33,VECTSP_4:8;
end;
hence the carrier of S <> B by A5,A30,VECTSP_9:def 2;
end;
end;
then not the carrier of S is Block of S;
hence S is non degenerated;
end;
theorem Th19:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat such that
A1: 1 <= k & k < dim V;
set S=PencilSpace(V,k);
thus S is with_non_trivial_blocks
proof
let X be Block of S;
S is non void by A1,Th17;
then
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) by Def4;
then X is non trivial by Th16;
hence thesis by PENCIL_1:4;
end;
end;
theorem Th20:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat such that
A1: 1 <= k and
A2: k < dim V;
set S=PencilSpace(V,k);
thus S is identifying_close_blocks
proof
let X,Y be Block of S;
assume 2 c= card(X/\Y);
then consider P,Q being object such that
A3: P in X/\Y & Q in X/\Y and
A4: P<>Q by PENCIL_1:2;
A5: P in X & Q in X by A3,XBOOLE_0:def 4;
A6: P in Y & Q in Y by A3,XBOOLE_0:def 4;
A7: S is non void by A1,A2,Th17;
then consider W1,W2 being Subspace of V such that
A8: W1 is Subspace of W2 and
A9: dim W1+1=k & dim W2=k+1 and
A10: X=pencil(W1,W2,k) by Def4;
the topology of S is non empty by A7;
then X in the topology of S;
then reconsider P,Q as Point of S by A5;
A11: S is non empty by A2,VECTSP_9:36;
then ex P1 being strict Subspace of V st P1=P & dim P1 = k by
VECTSP_9:def 2;
then reconsider P as strict Subspace of V;
ex Q1 being strict Subspace of V st Q1=Q & dim Q1 = k by A11,VECTSP_9:def 2
;
then reconsider Q as strict Subspace of V;
consider U1,U2 being Subspace of V such that
A12: U1 is Subspace of U2 and
A13: dim U1+1=k & dim U2=k+1 and
A14: Y=pencil(U1,U2,k) by A7,Def4;
A15: (Omega).W2=P+Q by A4,A5,A9,A10,Th11
.= (Omega).U2 by A4,A6,A13,A14,Th11;
(Omega).W1=P/\Q by A4,A5,A9,A10,Th11
.= (Omega).U1 by A4,A6,A13,A14,Th11;
hence thesis by A8,A10,A12,A14,A15,Th6;
end;
end;
theorem
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;
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
:Def6:
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
proof
defpred P[object] means ex W being Subspace of V st dim W = n & $1 = m
Subspaces_of W;
set A=bool (m Subspaces_of V);
consider X being set such that
A1: for x being object holds x in X iff x in A & P[x] from XBOOLE_0:sch 1;
X c= A
by A1;
then reconsider X as Subset-Family of m Subspaces_of V;
take X;
let x be set;
thus x in X implies ex W being Subspace of V st dim W=n & x = m
Subspaces_of W by A1;
given W being Subspace of V such that
A2: dim W=n and
A3: x = m Subspaces_of W;
x c= m Subspaces_of V by A3,VECTSP_9:38;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let S,T be Subset-Family of m Subspaces_of V such that
A4: for X being set holds X in S iff ex W being Subspace of V st dim W
= n & X = m Subspaces_of W and
A5: for X being set holds X in T iff ex W being Subspace of V st dim W
= n & X = m Subspaces_of W;
now
let X be object;
thus X in S implies X in T
proof
assume X in S;
then ex W being Subspace of V st dim W = n & X = m Subspaces_of W by A4
;
hence thesis by A5;
end;
assume X in T;
then ex W being Subspace of V st dim W = n & X = m Subspaces_of W by A5;
hence X in S by A4;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th22:
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
proof
let F be Field;
let V be finite-dimensional VectSp of F;
let m,n be Nat;
assume n <= dim V;
then consider W being strict Subspace of V such that
A1: dim W = n by VECTSP_9:35;
m Subspaces_of W in SubspaceSet(V,m,n) by A1,Def6;
hence thesis;
end;
theorem Th23:
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
proof
let F be Field;
let W1,W2 be finite-dimensional VectSp of F such that
A1: (Omega).W1 = (Omega).W2;
let m be Nat;
(Omega).W1 is Subspace of (Omega).W2 by A1,VECTSP_4:24;
then W1 is Subspace of (Omega).W2 by Th5;
then W1 is Subspace of W2 by Th3;
hence m Subspaces_of W1 c= m Subspaces_of W2 by VECTSP_9:38;
(Omega).W2 is Subspace of (Omega).W1 by A1,VECTSP_4:24;
then W2 is Subspace of (Omega).W1 by Th5;
then W2 is Subspace of W1 by Th3;
hence thesis by VECTSP_9:38;
end;
theorem Th24:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let W be Subspace of V;
let m be Nat such that
A1: 1<=m and
A2: m <= dim V and
A3: m Subspaces_of V c= m Subspaces_of W;
hereby
A4: dim W <= dim V by VECTSP_9:25;
assume
A5: (Omega).V <> (Omega).W;
then dim W <> dim V by VECTSP_9:28;
then
A6: dim W < dim V by A4,XXREAL_0:1;
per cases by A2,XXREAL_0:1;
suppose
m=dim V;
then m Subspaces_of W = {} by A6,VECTSP_9:37;
hence contradiction by A2,A3,VECTSP_9:36;
end;
suppose
A7: m < dim V;
A8: now
assume
A9: the carrier of V = the carrier of W;
(Omega).W is strict Subspace of V by Th4;
hence contradiction by A5,A9,VECTSP_4:29;
end;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then not the carrier of V c= the carrier of W by A8;
then consider x being object such that
A10: x in the carrier of V and
A11: not x in the carrier of W;
reconsider x as Vector of V by A10;
0.V in W by VECTSP_4:17;
then x <> 0.V by A11;
then {x} is linearly-independent by VECTSP_7:3;
then consider I being Basis of V such that
A12: {x} c= I by VECTSP_7:19;
reconsider J=I as finite Subset of V;
card J = dim V by VECTSP_9:def 1;
then consider K being Subset of J such that
A13: card K = m by A7,Lm1;
A14: I is linearly-independent by VECTSP_7:def 3;
per cases;
suppose
A15: x in K;
reconsider L=K as finite Subset of V by XBOOLE_1:1;
L c= the carrier of Lin L
proof
let a be object;
assume a in L;
then a in Lin L by VECTSP_7:8;
hence thesis;
end;
then reconsider L9=L as Subset of Lin L;
L is linearly-independent by A14,VECTSP_7:1;
then reconsider LL1 = L9 as linearly-independent Subset of Lin L by
VECTSP_9:12;
Lin LL1 = the ModuleStr of Lin L by VECTSP_9:17;
then L is Basis of Lin L by VECTSP_7:def 3;
then dim Lin L = m by A13,VECTSP_9:def 1;
then Lin L in m Subspaces_of V by VECTSP_9:def 2;
then ex M being strict Subspace of W st M=Lin L & dim M = m by A3,
VECTSP_9:def 2;
then x in W by A15,VECTSP_4:9,VECTSP_7:8;
hence contradiction by A11;
end;
suppose
A16: not x in K;
consider y being object such that
A17: y in K by A1,A13,CARD_1:27,XBOOLE_0:def 1;
(K\{y})\/{x} c= the carrier of V
proof
let a be object;
assume a in (K\{y})\/{x};
then a in (K\{y}) or a in {x} by XBOOLE_0:def 3;
hence thesis by TARSKI:def 3;
end;
then reconsider L=(K\{y})\/{x} as finite Subset of V;
L c= the carrier of Lin L
proof
let a be object;
assume a in L;
then a in Lin L by VECTSP_7:8;
hence thesis;
end;
then reconsider L9=L as Subset of Lin L;
L c= I
proof
let a be object;
assume a in L;
then a in K\{y} or a in {x} by XBOOLE_0:def 3;
hence thesis by A12;
end;
then L is linearly-independent by A14,VECTSP_7:1;
then reconsider LL1 = L9 as linearly-independent Subset of Lin L by
VECTSP_9:12;
Lin LL1 = the ModuleStr of Lin L by VECTSP_9:17;
then
A18: L is Basis of Lin L by VECTSP_7:def 3;
not x in K\{y} by A16,XBOOLE_0:def 5;
then card L = card(K\{y})+1 by CARD_2:41
.= card K - card{y} + 1 by A17,EULER_1:4
.= card K - 1 + 1 by CARD_1:30
.= m by A13;
then dim Lin L = m by A18,VECTSP_9:def 1;
then Lin L in m Subspaces_of V by VECTSP_9:def 2;
then
A19: ex M being strict Subspace of W st M=Lin L & dim M = m by A3,
VECTSP_9:def 2;
x in {x} by TARSKI:def 1;
then x in L by XBOOLE_0:def 3;
then x in W by A19,VECTSP_4:9,VECTSP_7:8;
hence contradiction by A11;
end;
end;
end;
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
TopStruct(#m Subspaces_of V, SubspaceSet(V,m,n)#);
coherence;
end;
theorem Th25:
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
by Th22;
theorem Th26:
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
proof
let F be Field;
let V be finite-dimensional VectSp of F;
let m,n be Nat such that
A1: 1 <= m and
A2: m < n and
A3: n < dim V;
set S=GrassmannSpace(V,m,n);
A4: m < dim V by A2,A3,XXREAL_0:2;
hereby
assume
A5: the carrier of S is Block of S;
the topology of S is non empty by A3,Th22;
then consider W being Subspace of V such that
A6: dim W = n and
A7: m Subspaces_of V = m Subspaces_of W by A5,Def6;
(Omega).V = (Omega).W by A1,A4,A7,Th24;
then dim W = dim (Omega).V by VECTSP_9:27;
hence contradiction by A3,A6,VECTSP_9:27;
end;
end;
theorem Th27:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let m,n be Nat such that
A1: 1 <= m and
A2: m < n and
A3: n <= dim V;
set S=GrassmannSpace(V,m,n);
let B be Block of S;
the topology of S is non empty by A3,Th22;
then consider W being Subspace of V such that
A4: dim W = n and
A5: B = m Subspaces_of W by Def6;
m+1 <= n by A2,NAT_1:13;
then consider U being strict Subspace of W such that
A6: dim U = m+1 by A4,VECTSP_9:35;
set I = the Basis of U;
A7: card I = m+1 by A6,VECTSP_9:def 1;
reconsider I9=I as finite Subset of U;
reconsider m as Element of NAT by ORDINAL1:def 12;
1+1 <= m+1 by A1,XREAL_1:7;
then Segm 2 c= Segm(m+1) by NAT_1:39;
then consider i,j being object such that
A8: i in I and
A9: j in I and
A10: i<>j by PENCIL_1:2,A7;
reconsider I1=I9\{i} as finite Subset of U;
I1 c= the carrier of Lin I1
proof
let a be object;
assume a in I1;
then a in Lin I1 by VECTSP_7:8;
hence thesis;
end;
then reconsider I19=I1 as Subset of Lin I1;
A11: I is linearly-independent by VECTSP_7:def 3;
then I1 is linearly-independent by VECTSP_7:1,XBOOLE_1:36;
then reconsider II1=I19 as linearly-independent Subset of Lin I1 by
VECTSP_9:12;
Lin II1 = the ModuleStr of Lin I1 by VECTSP_9:17;
then
A12: I1 is Basis of Lin I1 by VECTSP_7:def 3;
reconsider I2=I9\{j} as finite Subset of U;
I2 c= the carrier of Lin I2
proof
let a be object;
assume a in I2;
then a in Lin I2 by VECTSP_7:8;
hence thesis;
end;
then reconsider I29=I2 as Subset of Lin I2;
I2 is linearly-independent by A11,VECTSP_7:1,XBOOLE_1:36;
then reconsider II2=I29 as linearly-independent Subset of Lin I2 by
VECTSP_9:12;
Lin II2 = the ModuleStr of Lin I2 by VECTSP_9:17;
then
A13: I2 is Basis of Lin I2 by VECTSP_7:def 3;
card I2 = card I9 - card{j} by A9,EULER_1:4
.= m+1 - 1 by A7,CARD_1:30;
then
A14: dim Lin I2 = m by A13,VECTSP_9:def 1;
Lin I2 is strict Subspace of W by VECTSP_4:26;
then
A15: Lin I2 in B by A5,A14,VECTSP_9:def 2;
card I1 = card I9 - card{i} by A8,EULER_1:4
.= m+1 - 1 by A7,CARD_1:30;
then
A16: dim Lin I1 = m by A12,VECTSP_9:def 1;
Lin I1 is strict Subspace of W by VECTSP_4:26;
then
A17: Lin I1 in B by A5,A16,VECTSP_9:def 2;
not j in {i} by A10,TARSKI:def 1;
then j in I1 by A9,XBOOLE_0:def 5;
then
A18: j in Lin I1 by VECTSP_7:8;
not j in Lin I2 by A11,A9,VECTSP_9:14;
hence thesis by A17,A15,A18,PENCIL_1:2;
end;
theorem Th28:
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
let F be Field;
let V be finite-dimensional VectSp of F;
let m be Nat such that
A1: m+1 <= dim V;
set S = GrassmannSpace(V,m,m+1);
let K,L be Block of S;
A2: the topology of S is non empty by A1,Th22;
then consider W1 being Subspace of V such that
A3: dim W1 = m+1 and
A4: K = m Subspaces_of W1 by Def6;
assume 2 c= card(K/\L);
then consider x,y being object such that
A5: x in K/\L and
A6: y in K/\L and
A7: x <> y by PENCIL_1:2;
y in K by A6,XBOOLE_0:def 4;
then consider Y being strict Subspace of W1 such that
A8: y=Y and
A9: dim Y = m by A4,VECTSP_9:def 2;
consider W2 being Subspace of V such that
A10: dim W2 = m+1 and
A11: L = m Subspaces_of W2 by A2,Def6;
y in L by A6,XBOOLE_0:def 4;
then consider Y9 being strict Subspace of W2 such that
A12: y=Y9 and
dim Y9 = m by A11,VECTSP_9:def 2;
x in L by A5,XBOOLE_0:def 4;
then consider X9 being strict Subspace of W2 such that
A13: x=X9 and
dim X9 = m by A11,VECTSP_9:def 2;
x in K by A5,XBOOLE_0:def 4;
then consider X being strict Subspace of W1 such that
A14: x=X and
A15: dim X = m by A4,VECTSP_9:def 2;
reconsider x,y as strict Subspace of V by A14,A8,VECTSP_4:26;
A16: now
reconsider y9=y as strict Subspace of x+y by VECTSP_5:7;
reconsider x9=x as strict Subspace of x+y by VECTSP_5:7;
assume
A17: dim(x+y)=m;
then (Omega).x9 = (Omega).(x+y) by A14,A15,VECTSP_9:28;
then x = y+x by VECTSP_5:5;
then
A18: y is Subspace of x by VECTSP_5:8;
(Omega).y9 = (Omega).(x+y) by A8,A9,A17,VECTSP_9:28;
then x is Subspace of y by VECTSP_5:8;
hence contradiction by A7,A18,VECTSP_4:25;
end;
x+y is Subspace of W1 by A14,A8,VECTSP_5:34;
then x is Subspace of x+y & dim (x+y) <= m+1 by A3,VECTSP_5:7,VECTSP_9:25;
then
A19: dim (x+y) = m+1 by A14,A15,A16,NAT_1:9,VECTSP_9:25;
X9+Y9=x+y by A13,A12,VECTSP10:12;
then
A20: (Omega).(X9+Y9) = (Omega).W2 by A10,A19,VECTSP_9:28;
A21: X+Y=x+y by A14,A8,VECTSP10:12;
then (Omega).(X+Y) = (Omega).W1 by A3,A19,VECTSP_9:28;
hence thesis by A4,A11,A13,A12,A21,A20,Th23,VECTSP10:12;
end;
theorem
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
let F be Field;
let V be finite-dimensional VectSp of F;
let m be Nat;
assume that
A1: 1 <= m and
A2: m+1 < dim V;
A3: m < m+1 by NAT_1:13;
m <= dim V by A2,NAT_1:13;
hence thesis by A1,A2,A3,Th25,Th26,Th27,Th28,VECTSP_9:36;
end;
begin :: Veronese spaces
definition
let X be set;
func PairSet(X) -> set means
:Def8:
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
proof
defpred P[object] means ex x,y being set st x in X & y in X & $1={x,y};
consider S being set such that
A1: for z being object holds z in S iff z in bool X & P[z] from XBOOLE_0:
sch 1;
take S;
let z be set;
thus z in S implies P[z] by A1;
assume
A2: P[z];
then z c= X by ZFMISC_1:32;
hence thesis by A1,A2;
end;
uniqueness
proof
let p1,p2 be set such that
A3: for z being set holds z in p1 iff ex x,y being set st x in X & y
in X & z={x,y} and
A4: for z being set holds z in p2 iff ex x,y being set st x in X & y
in X & z={x,y};
now
let z be object;
z in p1 iff ex x,y being set st x in X & y in X & z={x,y} by A3;
hence z in p1 iff z in p2 by A4;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let X be non empty set;
cluster PairSet(X) -> non empty;
coherence
proof
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
{x,x} in PairSet(X) by A1,Def8;
hence thesis;
end;
end;
definition
let t be object, X be set;
func PairSet(t,X) -> set means
:Def9:
for z being set holds z in it iff ex y being set st y in X & z={t,y};
existence
proof
t in {t} by TARSKI:def 1;
then
A1: t in X\/{t} by XBOOLE_0:def 3;
defpred P[object] means ex y being set st y in X & $1={t,y};
consider S being set such that
A2: for z being object holds z in S iff z in bool (X\/{t}) & P[z] from
XBOOLE_0:sch 1;
take S;
let z be set;
thus z in S implies P[z] by A2;
assume
A3: P[z];
then consider y being set such that
A4: y in X and
A5: z={t,y};
y in X\/{t} by A4,XBOOLE_0:def 3;
then z c= X\/{t} by A5,A1,ZFMISC_1:32;
hence thesis by A2,A3;
end;
uniqueness
proof
let p1,p2 be set such that
A6: for z being set holds z in p1 iff ex y being set st y in X & z={t, y} and
A7: for z being set holds z in p2 iff ex y being set st y in X & z={t ,y};
now
let z be object;
z in p1 iff ex y being set st y in X & z={t,y} by A6;
hence z in p1 iff z in p2 by A7;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let t be set;
let X be non empty set;
cluster PairSet(t,X) -> non empty;
coherence
proof
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
{t,x} in PairSet(t,X) by A1,Def9;
hence thesis;
end;
end;
registration
let t be set;
let X be non trivial set;
cluster PairSet(t,X) -> non trivial;
coherence
proof
2 c= card X by PENCIL_1:4;
then consider x,y being object such that
A1: x in X & y in X and
A2: x<>y by PENCIL_1:2;
A3: now
assume
A4: {t,x}={t,y};
then y=t by A2,ZFMISC_1:6;
hence contradiction by A2,A4,ZFMISC_1:6;
end;
{t,x} in PairSet(t,X) & {t,y} in PairSet(t,X) by A1,Def9;
then 2 c= card PairSet(t,X) by A3,PENCIL_1:2;
hence thesis by PENCIL_1:4;
end;
end;
definition
let X be set;
let L be Subset-Family of X;
func PairSetFamily(L) -> Subset-Family of PairSet(X) means
:Def10:
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);
existence
proof
set A=PairSet(X);
defpred P[Subset of A] means ex t being set, l being Subset of X st t in X
& l in L & $1=PairSet(t,l);
consider F being Subset-Family of A such that
A1: for B being Subset of A holds B in F iff P[B] from SUBSET_1:sch 3;
take F;
let S be set;
thus S in F implies ex t being set, l being Subset of X st t in X & l in L
& S=PairSet(t,l) by A1;
given t being set, l being Subset of X such that
A2: t in X and
A3: l in L and
A4: S=PairSet(t,l);
S c= PairSet(X)
proof
let a be object;
assume a in S;
then ex y being set st y in l & a={t,y} by A4,Def9;
hence thesis by A2,Def8;
end;
hence thesis by A1,A2,A3,A4;
end;
uniqueness
proof
let p1,p2 be Subset-Family of PairSet(X) such that
A5: for z being set holds z in p1 iff ex t being set, l being Subset
of X st t in X & l in L & z=PairSet(t,l) and
A6: for z being set holds z in p2 iff ex t being set, l being Subset
of X st t in X & l in L & z=PairSet(t,l);
now
let z be object;
z in p1 iff ex t being set, l being Subset of X st t in X & l in L
& z=PairSet(t,l) by A5;
hence z in p1 iff z in p2 by A6;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let X be non empty set;
let L be non empty Subset-Family of X;
cluster PairSetFamily(L) -> non empty;
coherence
proof
consider l being object such that
A1: l in L by XBOOLE_0:def 1;
reconsider l as set by TARSKI:1;
consider t being object such that
A2: t in X by XBOOLE_0:def 1;
PairSet(t,l) in PairSetFamily(L) by A2,A1,Def10;
hence thesis;
end;
end;
definition
let S be TopStruct;
func VeroneseSpace(S) -> strict TopStruct equals
TopStruct(#PairSet(the
carrier of S), PairSetFamily(the topology of S)#);
coherence;
end;
registration
let S be non empty TopStruct;
cluster VeroneseSpace(S) -> non empty;
coherence;
end;
registration
let S be non empty non void TopStruct;
cluster VeroneseSpace(S) -> non void;
coherence;
end;
registration
let S be non empty non void non degenerated TopStruct;
cluster VeroneseSpace(S) -> non degenerated;
coherence
proof
assume the carrier of VeroneseSpace(S) is Block of VeroneseSpace(S);
then consider t being set, l being Subset of S such that
A1: t in the carrier of S and
A2: l in the topology of S and
A3: PairSet(the carrier of S)=PairSet(t,l) by Def10;
not the carrier of S in the topology of S by PENCIL_1:def 5;
then not the carrier of S c= l by A2,XBOOLE_0:def 10;
then consider s being object such that
A4: s in the carrier of S and
A5: not s in l;
now
assume {t,s} in PairSet(t,l);
then
A6: ex z being set st z in l & {t,s}={t,z} by Def9;
then s = t by A5,ZFMISC_1:6;
hence contradiction by A5,A6,ZFMISC_1:6;
end;
hence contradiction by A1,A3,A4,Def8;
end;
end;
registration
let S be non empty non void with_non_trivial_blocks TopStruct;
cluster VeroneseSpace(S) -> with_non_trivial_blocks;
coherence
proof
let L be Block of VeroneseSpace(S);
consider t being set, l being Subset of S such that
t in the carrier of S and
A1: l in the topology of S and
A2: L=PairSet(t,l) by Def10;
2 c= card l by A1,PENCIL_1:def 6;
then reconsider l as non trivial set by PENCIL_1:4;
PairSet(t,l) is non trivial;
hence thesis by A2,PENCIL_1:4;
end;
end;
registration
let S be identifying_close_blocks TopStruct;
cluster VeroneseSpace(S) -> identifying_close_blocks;
coherence
proof
let K,L be Block of VeroneseSpace(S);
assume 2 c= card (K/\L);
then consider a,b being object such that
A1: a in K/\L and
A2: b in K/\L and
A3: a <> b by PENCIL_1:2;
A4: a in K by A1,XBOOLE_0:def 4;
then
A5: the topology of VeroneseSpace(S) is non empty by SUBSET_1:def 1;
then consider t being set, k being Subset of S such that
t in the carrier of S and
A6: k in the topology of S and
A7: K=PairSet(t,k) by Def10;
b in K by A2,XBOOLE_0:def 4;
then consider y being set such that
A8: y in k and
A9: b={t,y} by A7,Def9;
consider x being set such that
A10: x in k and
A11: a={t,x} by A4,A7,Def9;
consider s being set, l being Subset of S such that
s in the carrier of S and
A12: l in the topology of S and
A13: L=PairSet(s,l) by A5,Def10;
a in L by A1,XBOOLE_0:def 4;
then consider z being set such that
A14: z in l and
A15: a={s,z} by A13,Def9;
b in L by A2,XBOOLE_0:def 4;
then consider w being set such that
A16: w in l and
A17: b={s,w} by A13,Def9;
A18: t=s or t=z by A11,A15,ZFMISC_1:6;
now
assume
A19: y<>w;
then y=t by A3,A9,A15,A17,A18,ZFMISC_1:6;
hence contradiction by A9,A17,A19,ZFMISC_1:6;
end;
then
A20: y in k/\l by A8,A16,XBOOLE_0:def 4;
A21: t=s or t=w by A9,A17,ZFMISC_1:6;
now
assume
A22: x<>z;
then x=t by A3,A11,A15,A17,A21,ZFMISC_1:6;
hence contradiction by A11,A15,A22,ZFMISC_1:6;
end;
then x in k/\l by A10,A14,XBOOLE_0:def 4;
then 2 c= card (k/\l) by A3,A11,A9,A20,PENCIL_1:2;
hence thesis by A3,A6,A7,A12,A13,A15,A17,A18,A21,PENCIL_1:def 7;
end;
end;