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

theorem Th1: :: COMBGRAS:1

for n being 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 k, n being 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 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 :: 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 ;

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 for IncProjStr ;

existence
ex b₁ being IncProjStr st
( b₁ is with_non-trivial_lines & b₁ is linear & b₁ is up-2-rank & b₁ is strict )

proof end;

end;

definition

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

end;

definition

let k be 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 b₁ being strict PartialLinearSpace st
( the Points of b₁ = { A where A is Subset of X : card A = k } & the Lines of b₁ = { L where L is Subset of X : card L = k + 1 } & the Inc of b₁ = (RelIncl (bool X)) /\ [: the Points of b₁, the Lines of b₁:] )

proof end;

uniqueness
for b₁, b₂ being strict PartialLinearSpace st the Points of b₁ = { A where A is Subset of X : card A = k } & the Lines of b₁ = { L where L is Subset of X : card L = k + 1 } & the Inc of b₁ = (RelIncl (bool X)) /\ [: the Points of b₁, the Lines of b₁:] & the Points of b₂ = { A where A is Subset of X : card A = k } & the Lines of b₂ = { L where L is Subset of X : card L = k + 1 } & the Inc of b₂ = (RelIncl (bool X)) /\ [: the Points of b₂, the Lines of b₂:] holds
b₁ = b₂ ;

end;

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

theorem Th10: :: COMBGRAS:10

for k being 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 :: 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 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 :: 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 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 Nat;
let X be non empty set ;
let T be Subset of the Points of (G_ (k,X));

attr T is STAR means :: 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 :: 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 defines STAR COMBGRAS:def 4 :
for k being 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 defines TOP COMBGRAS:def 5 :
for k being 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;

definition

let S1, S2 be IncProjStr ;
attr c₃ is strict ;
struct IncProjMap over S1,S2 -> ;
aggr IncProjMap(# point-map, line-map #) -> IncProjMap over S1,S2;
sel point-map c₃ -> Function of the Points of S1, the Points of S2;
sel line-map c₃ -> 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;

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

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 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 ) & ( 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 over S1,S2;

attr F is incidence_preserving means :: 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 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 #) & F1 is incidence_preserving holds
F2 is incidence_preserving

proof end;

definition

let S be IncProjStr ;
let F be IncProjMap over S,S;

attr F is automorphism means :: COMBGRAS:def 9
( the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving );

end;

:: deftheorem 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 & the point-map of F is bijective & 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;

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

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 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 & 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 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 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 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 & F . A = B ) }

proof end;

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 & F . A = B ) }

proof end;

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 & K is clique holds
F .: K is clique

proof end;

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 & 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 over 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 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 & F " K is STAR )

proof end;

definition

let k be 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 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 ) & ( for L being LINE of (G_ (k,X)) holds it . L = s .: L ) );

existence
ex b₁ being strict IncProjMap over G_ (k,X), G_ (k,X) st
( ( for A being POINT of (G_ (k,X)) holds b₁ . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b₁ . L = s .: L ) )

proof end;

uniqueness
for b₁, b₂ being strict IncProjMap over G_ (k,X), G_ (k,X) st ( for A being POINT of (G_ (k,X)) holds b₁ . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b₁ . L = s .: L ) & ( for A being POINT of (G_ (k,X)) holds b₂ . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b₂ . L = s .: L ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines incprojmap COMBGRAS:def 14 :
for k being Nat
for X being non empty set st 0 < k & k + 1 c= card X holds
for s being Permutation of X
for b₄ being strict IncProjMap over G_ (k,X), G_ (k,X) holds
( b₄ = incprojmap (k,s) iff ( ( for A being POINT of (G_ (k,X)) holds b₄ . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds b₄ . L = s .: L ) ) );

theorem Th24: :: COMBGRAS:24

for k being Nat
for X being non empty set st k = 1 & 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)

proof end;

theorem Th25: :: COMBGRAS:25

for k being Nat
for X being non empty set st 1 < k & 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)

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 Nat
for X being non empty set st 0 < k & 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 & 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 Nat
for X being non empty set st 0 < k & 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)

proof end;

theorem Th33: :: COMBGRAS:33

for k being Nat
for X being non empty set st 2 <= k & 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)

proof end;

theorem Th34: :: COMBGRAS:34

for k being 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 Nat
for X being non empty set st 0 < k & 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) )

proof end;