:: Combinatorial {G}rassmannians
:: by Andrzej Owsiejczuk
::
:: Received April 16, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: COMBGRAS:1
for n being Element of NAT
for a, b being set st a <> b &amp; card a = n &amp; card b = n holds
( card (a /\ b) in n &amp; n + 1 c= card (a \/ b) )
proofend;

theorem Th2: :: COMBGRAS:2
for n, k being Element of NAT
for a, b being set st card a = n + k &amp; card b = n + k holds
( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) )
proofend;

theorem Th3: :: COMBGRAS:3
for X, Y being set holds
( card X c= card Y iff ex f being Function st
( f is one-to-one &amp; X c= dom f &amp; f .: X c= Y ) )
proofend;

theorem Th4: :: COMBGRAS:4
for X being set
for f being Function st f is one-to-one &amp; X c= dom f holds
card (f .: X) = card X
proofend;

theorem Th5: :: COMBGRAS:5
for X, Y, Z being set st X \ Y = X \ Z &amp; Y c= X &amp; Z c= X holds
Y = Z
proofend;

theorem Th6: :: COMBGRAS:6
for X being set
for Y being non empty set
for p being Function of X,Y st p is one-to-one holds
for x1, x2 being Subset of X st x1 <> x2 holds
p .: x1 <> p .: x2
proofend;

theorem Th7: :: COMBGRAS:7
for n being Element of NAT
for a, b, c being set st card a = n - 1 &amp; card b = n - 1 &amp; card c = n - 1 &amp; card (a /\ b) = n - 2 &amp; card (a /\ c) = n - 2 &amp; card (b /\ c) = n - 2 &amp; 2 <= n holds
( ( not 3 <= n or ( card ((a /\ b) /\ c) = n - 2 &amp; card ((a \/ b) \/ c) = n + 1 ) or ( card ((a /\ b) /\ c) = n - 3 &amp; card ((a \/ b) \/ c) = n ) ) &amp; ( n = 2 implies ( card ((a /\ b) /\ c) = n - 2 &amp; card ((a \/ b) \/ c) = n + 1 ) ) )
proofend;

theorem Th8: :: COMBGRAS:8
for P1, P2 being IncProjStr st IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) holds
for A1 being POINT of P1
for A2 being POINT of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 &amp; A1 on L1 holds
A2 on L2
proofend;

theorem Th9: :: COMBGRAS:9
for P1, P2 being IncProjStr st IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) holds
for A1 being Subset of the Points of P1
for A2 being Subset of the Points of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 &amp; A1 on L1 holds
A2 on L2
proofend;

registration
cluster strict with_non-trivial_lines linear up-2-rank for IncProjStr ;
existence
 ex b1 being IncProjStr st
( b1 is with_non-trivial_lines &amp; b1 is linear &amp; b1 is up-2-rank &amp; b1 is strict )
proofend;
end;

begin

definition
mode PartialLinearSpace is with_non-trivial_lines up-2-rank IncProjStr ;
end;

definition
let k be Element of NAT ;
let X be non empty set ;
assume that
B1: 0 < k and
B2: k + 1 c= card X ;
func G_ (k,X) ->  strict PartialLinearSpace means :Def1: :: COMBGRAS:def 1
( the Points of it =  {  A where A is Subset of X : card A = k  }  &amp; the Lines of it =  {  L where L is Subset of X : card L = k + 1  }  &amp; the Inc of it = (RelIncl (bool X)) /\ [: the Points of it, the Lines of it:] );
existence
 ex b1 being strict PartialLinearSpace st
( the Points of b1 =  {  A where A is Subset of X : card A = k  }  &amp; the Lines of b1 =  {  L where L is Subset of X : card L = k + 1  }  &amp; the Inc of b1 = (RelIncl (bool X)) /\ [: the Points of b1, the Lines of b1:] )
proofend;
uniqueness
 for b1, b2 being strict PartialLinearSpace st the Points of b1 =  {  A where A is Subset of X : card A = k  }  &amp; the Lines of b1 =  {  L where L is Subset of X : card L = k + 1  }  &amp; the Inc of b1 = (RelIncl (bool X)) /\ [: the Points of b1, the Lines of b1:] &amp; the Points of b2 =  {  A where A is Subset of X : card A = k  }  &amp; the Lines of b2 =  {  L where L is Subset of X : card L = k + 1  }  &amp; the Inc of b2 = (RelIncl (bool X)) /\ [: the Points of b2, the Lines of b2:] holds
b1 = b2 ;
end;

:: deftheorem Def1 defines G_ COMBGRAS:def_1_:_
 for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for b3 being strict PartialLinearSpace holds
( b3 = G_ (k,X) iff ( the Points of b3 =  {  A where A is Subset of X : card A = k  }  &amp; the Lines of b3 =  {  L where L is Subset of X : card L = k + 1  }  &amp; the Inc of b3 = (RelIncl (bool X)) /\ [: the Points of b3, the Lines of b3:] ) );

theorem Th10: :: COMBGRAS:10
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for A being POINT of (G_ (k,X))
for L being LINE of (G_ (k,X)) holds
( A on L iff A c= L )
proofend;

theorem Th11: :: COMBGRAS:11
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
G_ (k,X) is Vebleian
proofend;

theorem Th12: :: COMBGRAS:12
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))
for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 &amp; A2 on L1 &amp; A3 on L2 &amp; A4 on L2 &amp; A5 on L1 &amp; A5 on L2 &amp; A1 on L3 &amp; A3 on L3 &amp; A2 on L4 &amp; A4 on L4 &amp; not A5 on L3 &amp; not A5 on L4 &amp; L1 <> L2 &amp; L3 <> L4 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 &amp; A6 on L4 &amp; A6 = (A1 /\ A2) \/ (A3 /\ A4) )
proofend;

theorem :: COMBGRAS:13
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
G_ (k,X) is Desarguesian
proofend;

definition
let S be IncProjStr ;
let K be Subset of the Points of S;
attrK is clique  means :Def2: :: COMBGRAS:def 2
 for A, B being POINT of S st A in K &amp; B in K holds
ex L being LINE of S st {A,B} on L;
end;

:: deftheorem Def2 defines clique COMBGRAS:def_2_:_
 for S being IncProjStr
for K being Subset of the Points of S holds
( K is clique iff for A, B being POINT of S st A in K &amp; B in K holds
ex L being LINE of S st {A,B} on L );

definition
let S be IncProjStr ;
let K be Subset of the Points of S;
attrK is maximal_clique  means :Def3: :: COMBGRAS:def 3
( K is clique &amp; ( for U being Subset of the Points of S st U is clique &amp; K c= U holds
U = K ) );
end;

:: deftheorem Def3 defines maximal_clique COMBGRAS:def_3_:_
 for S being IncProjStr
for K being Subset of the Points of S holds
( K is maximal_clique iff ( K is clique &amp; ( for U being Subset of the Points of S st U is clique &amp; K c= U holds
U = K ) ) );

definition
let k be Element of NAT ;
let X be non empty set ;
let T be Subset of the Points of (G_ (k,X));
attrT is STAR  means :Def4: :: COMBGRAS:def 4
 ex S being Subset of X st
( card S = k - 1 &amp; T =  {  A where A is Subset of X : ( card A = k &amp; S c= A )  }  );
attrT is TOP  means :Def5: :: COMBGRAS:def 5
 ex S being Subset of X st
( card S = k + 1 &amp; T =  {  A where A is Subset of X : ( card A = k &amp; A c= S )  }  );
end;

:: deftheorem Def4 defines STAR COMBGRAS:def_4_:_
 for k being Element of NAT
for X being non empty set
for T being Subset of the Points of (G_ (k,X)) holds
( T is STAR iff ex S being Subset of X st
( card S = k - 1 &amp; T =  {  A where A is Subset of X : ( card A = k &amp; S c= A )  }  ) );

:: deftheorem Def5 defines TOP COMBGRAS:def_5_:_
 for k being Element of NAT
for X being non empty set
for T being Subset of the Points of (G_ (k,X)) holds
( T is TOP iff ex S being Subset of X st
( card S = k + 1 &amp; T =  {  A where A is Subset of X : ( card A = k &amp; A c= S )  }  ) );

theorem Th14: :: COMBGRAS:14
for k being Element of NAT
for X being non empty set st 2 <= k &amp; k + 2 c= card X holds
for K being Subset of the Points of (G_ (k,X)) st ( K is STAR or K is TOP ) holds
K is maximal_clique
proofend;

theorem Th15: :: COMBGRAS:15
for k being Element of NAT
for X being non empty set st 2 <= k &amp; k + 2 c= card X holds
for K being Subset of the Points of (G_ (k,X)) holds
( not K is maximal_clique or K is STAR or K is TOP )
proofend;

begin

definition
let S1, S2 be IncProjStr ;
attrc3 is strict ;
struct IncProjMap over S1,S2 -> ;
aggrIncProjMap(# point-map, line-map #) ->  IncProjMap over S1,S2;
sel point-map c3 ->  Function of the Points of S1, the Points of S2;
sel line-map c3 ->  Function of the Lines of S1, the Lines of S2;
end;

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap over S1,S2;
let a be POINT of S1;
funcF . a ->  POINT of S2 equals :: COMBGRAS:def 6
 the point-map of F . a;
coherence
 the point-map of F . a is POINT of S2 ;
end;

:: deftheorem  defines . COMBGRAS:def_6_:_
 for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for a being POINT of S1 holds F . a = the point-map of F . a;

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap over S1,S2;
let L be LINE of S1;
funcF . L ->  LINE of S2 equals :: COMBGRAS:def 7
 the line-map of F . L;
coherence
 the line-map of F . L is LINE of S2 ;
end;

:: deftheorem  defines . COMBGRAS:def_7_:_
 for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for L being LINE of S1 holds F . L = the line-map of F . L;

theorem Th16: :: COMBGRAS:16
for S1, S2 being IncProjStr
for F1, F2 being IncProjMap over S1,S2 st ( for A being POINT of S1 holds F1 . A = F2 . A ) &amp; ( for L being LINE of S1 holds F1 . L = F2 . L ) holds
IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #)
proofend;

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap over S1,S2;
attrF is incidence_preserving  means :Def8: :: COMBGRAS:def 8
 for A1 being POINT of S1
for L1 being LINE of S1 holds
( A1 on L1 iff F . A1 on F . L1 );
end;

:: deftheorem Def8 defines incidence_preserving COMBGRAS:def_8_:_
 for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2 holds
( F is incidence_preserving iff for A1 being POINT of S1
for L1 being LINE of S1 holds
( A1 on L1 iff F . A1 on F . L1 ) );

theorem :: COMBGRAS:17
for S1, S2 being IncProjStr
for F1, F2 being IncProjMap over S1,S2 st IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) &amp; F1 is incidence_preserving holds
F2 is incidence_preserving
proofend;

definition
let S be IncProjStr ;
let F be IncProjMap over S,S;
attrF is automorphism  means :Def9: :: COMBGRAS:def 9
( the line-map of F is bijective &amp; the point-map of F is bijective &amp; F is incidence_preserving );
end;

:: deftheorem Def9 defines automorphism COMBGRAS:def_9_:_
 for S being IncProjStr
for F being IncProjMap over S,S holds
( F is automorphism iff ( the line-map of F is bijective &amp; the point-map of F is bijective &amp; F is incidence_preserving ) );

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap over S1,S2;
let K be Subset of the Points of S1;
funcF .: K ->  Subset of the Points of S2 equals :: COMBGRAS:def 10
 the point-map of F .: K;
coherence
 the point-map of F .: K is Subset of the Points of S2
proofend;
end;

:: deftheorem  defines .: COMBGRAS:def_10_:_
 for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for K being Subset of the Points of S1 holds F .: K = the point-map of F .: K;

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap over S1,S2;
let K be Subset of the Points of S2;
funcF " K ->  Subset of the Points of S1 equals :: COMBGRAS:def 11
 the point-map of F " K;
coherence
 the point-map of F " K is Subset of the Points of S1
proofend;
end;

:: deftheorem  defines " COMBGRAS:def_11_:_
 for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for K being Subset of the Points of S2 holds F " K = the point-map of F " K;

definition
let X be set ;
let A be finite set ;
func ^^ (A,X) ->  Subset of (bool X) equals :: COMBGRAS:def 12
 {  B where B is Subset of X : ( card B = (card A) + 1 &amp; A c= B )  }  ;
coherence
  {  B where B is Subset of X : ( card B = (card A) + 1 &amp; A c= B )  }  is Subset of (bool X)
proofend;
end;

:: deftheorem  defines ^^ COMBGRAS:def_12_:_
 for X being set
for A being finite set holds ^^ (A,X) =  {  B where B is Subset of X : ( card B = (card A) + 1 &amp; A c= B )  }  ;

definition
let k be Element of NAT ;
let X be non empty set ;
assume B1: ( 0 < k &amp; k + 1 c= card X ) ;
let A be finite set ;
assume B2: card A = k - 1 ;
func ^^ (A,X,k) ->  Subset of the Points of (G_ (k,X)) equals :Def13: :: COMBGRAS:def 13
 ^^ (A,X);
coherence
 ^^ (A,X) is Subset of the Points of (G_ (k,X))
proofend;
end;

:: deftheorem Def13 defines ^^ COMBGRAS:def_13_:_
 for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for A being finite set st card A = k - 1 holds
^^ (A,X,k) = ^^ (A,X);

theorem Th18: :: COMBGRAS:18
for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for K being Subset of the Points of S1 holds F .: K =  {  B where B is POINT of S2 : ex A being POINT of S1 st
( A in K &amp; F . A = B )  }
proofend;

theorem :: COMBGRAS:19
for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for K being Subset of the Points of S2 holds F " K =  {  A where A is POINT of S1 : ex B being POINT of S2 st
( B in K &amp; F . A = B )  }
proofend;

theorem Th20: :: COMBGRAS:20
for S being IncProjStr
for F being IncProjMap over S,S
for K being Subset of the Points of S st F is incidence_preserving &amp; K is clique holds
F .: K is clique
proofend;

theorem Th21: :: COMBGRAS:21
for S being IncProjStr
for F being IncProjMap over S,S
for K being Subset of the Points of S st F is incidence_preserving &amp; the line-map of F is onto &amp; K is clique holds
F " K is clique
proofend;

theorem Th22: :: COMBGRAS:22
for S being IncProjStr
for F being IncProjMap over S,S
for K being Subset of the Points of S st F is automorphism &amp; K is maximal_clique holds
( F .: K is maximal_clique &amp; F " K is maximal_clique )
proofend;

theorem Th23: :: COMBGRAS:23
for k being Element of NAT
for X being non empty set st 2 <= k &amp; k + 2 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds
for K being Subset of the Points of (G_ (k,X)) st K is STAR holds
( F .: K is STAR &amp; F " K is STAR )
proofend;

definition
let k be Element of NAT ;
let X be non empty set ;
assume B1: ( 0 < k &amp; k + 1 c= card X ) ;
let s be Permutation of X;
func incprojmap (k,s) ->  strict IncProjMap over G_ (k,X), G_ (k,X) means :Def14: :: COMBGRAS:def 14
( ( for A being POINT of (G_ (k,X)) holds it . A = s .: A ) &amp; ( for L being LINE of (G_ (k,X)) holds it . L = s .: L ) );
existence
 ex b1 being strict IncProjMap over G_ (k,X), G_ (k,X) st
( ( for A being POINT of (G_ (k,X)) holds b1 . A = s .: A ) &amp; ( for L being LINE of (G_ (k,X)) holds b1 . L = s .: L ) )
proofend;
uniqueness
 for b1, b2 being strict IncProjMap over G_ (k,X), G_ (k,X) st ( for A being POINT of (G_ (k,X)) holds b1 . A = s .: A ) &amp; ( for L being LINE of (G_ (k,X)) holds b1 . L = s .: L ) &amp; ( for A being POINT of (G_ (k,X)) holds b2 . A = s .: A ) &amp; ( for L being LINE of (G_ (k,X)) holds b2 . L = s .: L ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines incprojmap COMBGRAS:def_14_:_
 for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for s being Permutation of X
for b4 being strict IncProjMap over G_ (k,X), G_ (k,X) holds
( b4 = incprojmap (k,s) iff ( ( for A being POINT of (G_ (k,X)) holds b4 . A = s .: A ) &amp; ( for L being LINE of (G_ (k,X)) holds b4 . L = s .: L ) ) );

theorem Th24: :: COMBGRAS:24
for k being Element of NAT
for X being non empty set st k = 1 &amp; k + 1 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds
ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
proofend;

theorem Th25: :: COMBGRAS:25
for k being Element of NAT
for X being non empty set st 1 < k &amp; card X = k + 1 holds
for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds
ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
proofend;

theorem Th26: :: COMBGRAS:26
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for T being Subset of the Points of (G_ (k,X))
for S being Subset of X st card S = k - 1 &amp; T =  {  A where A is Subset of X : ( card A = k &amp; S c= A )  }  holds
S = meet T
proofend;

theorem :: COMBGRAS:27
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for T being Subset of the Points of (G_ (k,X)) st T is STAR holds
for S being Subset of X st S = meet T holds
( card S = k - 1 &amp; T =  {  A where A is Subset of X : ( card A = k &amp; S c= A )  }  )
proofend;

theorem Th28: :: COMBGRAS:28
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for T1, T2 being Subset of the Points of (G_ (k,X)) st T1 is STAR &amp; T2 is STAR &amp; meet T1 = meet T2 holds
T1 = T2
proofend;

theorem Th29: :: COMBGRAS:29
for k being Element of NAT
for X being non empty set st k + 1 c= card X holds
for A being finite Subset of X st card A = k - 1 holds
^^ (A,X,k) is STAR
proofend;

theorem Th30: :: COMBGRAS:30
for k being Element of NAT
for X being non empty set st k + 1 c= card X holds
for A being finite Subset of X st card A = k - 1 holds
meet (^^ (A,X,k)) = A
proofend;

theorem Th31: :: COMBGRAS:31
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 3 c= card X holds
for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism &amp; the line-map of H = the point-map of F &amp; ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )
proofend;

theorem Th32: :: COMBGRAS:32
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 3 c= card X holds
for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap over G_ (k,X), G_ (k,X) st the line-map of H = the point-map of F holds
for f being Permutation of X st IncProjMap(# the point-map of H, the line-map of H #) = incprojmap (k,f) holds
IncProjMap(# the point-map of F, the line-map of F #) = incprojmap ((k + 1),f)
proofend;

theorem Th33: :: COMBGRAS:33
for k being Element of NAT
for X being non empty set st 2 <= k &amp; k + 2 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds
ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)
proofend;

theorem Th34: :: COMBGRAS:34
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for s being Permutation of X holds incprojmap (k,s) is automorphism
proofend;

theorem :: COMBGRAS:35
for k being Element of NAT
for X being non empty set st 0 < k &amp; k + 1 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
proofend;