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


begin

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

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

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 & X c= dom f & f .: X c= Y ) )
proof end;

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

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

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
proof end;

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

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 & A1 on L1 holds
A2 on L2
proof end;

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 & A1 on L1 holds
A2 on L2
proof end;

registration
cluster strict with_non-trivial_lines linear up-2-rank IncProjStr ;
existence
ex b1 being IncProjStr st
( b1 is with_non-trivial_lines & b1 is linear & b1 is up-2-rank & b1 is strict )
proof end;
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
A1: 0 < k and
A2: 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 } & the Lines of it = { L where L is Subset of X : card L = k + 1 } & 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 } & the Lines of b1 = { L where L is Subset of X : card L = k + 1 } & the Inc of b1 = (RelIncl (bool X)) /\ [: the Points of b1, the Lines of b1:] )
proof end;
uniqueness
for b1, b2 being strict PartialLinearSpace st the Points of b1 = { A where A is Subset of X : card A = k } & the Lines of b1 = { L where L is Subset of X : card L = k + 1 } & the Inc of b1 = (RelIncl (bool X)) /\ [: the Points of b1, the Lines of b1:] & the Points of b2 = { A where A is Subset of X : card A = k } & the Lines of b2 = { L where L is Subset of X : card L = k + 1 } & 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 & 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 } & the Lines of b3 = { L where L is Subset of X : card L = k + 1 } & 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 & 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 )
proof end;

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

theorem Th12: :: COMBGRAS:12
for k being Element of NAT
for X being non empty set st 0 < k & 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 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )
proof end;

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

definition
let S be IncProjStr ;
let K be Subset of the Points of S;
attr K is clique means :Def2: :: COMBGRAS:def 2
 for A, B being POINT of S st A in K & 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 & 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;
attr K is maximal_clique means :Def3: :: COMBGRAS:def 3
( K is clique & ( for U being Subset of the Points of S st U is clique & 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 & ( for U being Subset of the Points of S st U is clique & 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));
attr T is STAR means :Def4: :: COMBGRAS:def 4
 ex S being Subset of X st
( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } );
attr T is TOP means :Def5: :: COMBGRAS:def 5
 ex S being Subset of X st
( card S = k + 1 & T = { A where A is Subset of X : ( card A = k & 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 & T = { A where A is Subset of X : ( card A = k & 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 & T = { A where A is Subset of X : ( card A = k & A c= S ) } ) );

theorem Th14: :: COMBGRAS:14
for k being Element of NAT
for X being non empty set st 2 <= k & 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
proof end;

theorem Th15: :: COMBGRAS:15
for k being Element of NAT
for X being non empty set st 2 <= k & 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 )
proof end;

begin

definition
let S1, S2 be IncProjStr ;
attr c3 is strict ;
struct IncProjMap of S1,S2 -> ;
aggr IncProjMap(# point-map, line-map #) -> IncProjMap of 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 of S1,S2;
let a be POINT of S1;
func F . 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 of 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 of S1,S2;
let L be LINE of S1;
func F . 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 of 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 of S1,S2 st ( for A being POINT of S1 holds F1 . A = F2 . A ) & ( 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 #)
proof end;

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap of S1,S2;
attr F 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 of 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 of 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 #) & F1 is incidence_preserving holds
F2 is incidence_preserving
proof end;

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

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

definition
let S1, S2 be IncProjStr ;
let F be IncProjMap of S1,S2;
let K be Subset of the Points of S1;
func F .: 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
proof end;
end;

:: deftheorem defines .: COMBGRAS:def 10 :
for S1, S2 being IncProjStr
for F being IncProjMap of 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 of S1,S2;
let K be Subset of the Points of S2;
func F " 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
proof end;
end;

:: deftheorem defines " COMBGRAS:def 11 :
for S1, S2 being IncProjStr
for F being IncProjMap of 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 & A c= B ) } ;
coherence
{ B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } is Subset of (bool X)
proof end;
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 & A c= B ) } ;

definition
let k be Element of NAT ;
let X be non empty set ;
assume A1: ( 0 < k & k + 1 c= card X ) ;
let A be finite set ;
assume A2: 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))
proof end;
end;

:: deftheorem Def13 defines ^^ COMBGRAS:def 13 :
for k being Element of NAT
for X being non empty set st 0 < k & 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 of 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 & F . A = B ) }
proof end;

theorem :: COMBGRAS:19
for S1, S2 being IncProjStr
for F being IncProjMap of 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 & F . A = B ) }
proof end;

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

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

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

theorem Th23: :: COMBGRAS:23
for k being Element of NAT
for X being non empty set st 2 <= k & k + 2 c= card X holds
for F being IncProjMap of 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 & F " K is STAR )
proof end;

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

:: deftheorem Def14 defines incprojmap COMBGRAS:def 14 :
for k being Element of NAT
for X being non empty set st 0 < k & k + 1 c= card X holds
for s being Permutation of X
for b4 being strict IncProjMap of 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 ) & ( 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 & k + 1 c= card X holds
for F being IncProjMap of 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)
proof end;

theorem Th25: :: COMBGRAS:25
for k being Element of NAT
for X being non empty set st 1 < k & card X = k + 1 holds
for F being IncProjMap of 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)
proof end;

theorem Th26: :: COMBGRAS:26
for k being Element of NAT
for X being non empty set st 0 < k & 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 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds
S = meet T
proof end;

theorem :: COMBGRAS:27
for k being Element of NAT
for X being non empty set st 0 < k & 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 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )
proof end;

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

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
proof end;

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
proof end;

theorem Th31: :: COMBGRAS:31
for k being Element of NAT
for X being non empty set st 0 < k & k + 3 c= card X holds
for F being IncProjMap of G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
ex H being IncProjMap of G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( 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)))) ) )
proof end;

theorem Th32: :: COMBGRAS:32
for k being Element of NAT
for X being non empty set st 0 < k & k + 3 c= card X holds
for F being IncProjMap of G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
for H being IncProjMap of 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)
proof end;

theorem Th33: :: COMBGRAS:33
for k being Element of NAT
for X being non empty set st 2 <= k & k + 2 c= card X holds
for F being IncProjMap of 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)
proof end;

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

theorem :: COMBGRAS:35
for k being Element of NAT
for X being non empty set st 0 < k & k + 1 c= card X holds
for F being IncProjMap of 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) )
proof end;