:: Combinatorial {G}rassmannians
:: by Andrzej Owsiejczuk
::
:: Received April 16, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, INCSP_1, SUBSET_1, CARD_1, XBOOLE_0, ARYTM_3, TARSKI,
ORDINAL1, FINSET_1, RELAT_1, ARYTM_1, NAT_1, FUNCT_1, XXREAL_0, FDIFF_1,
WELLORD2, ZFMISC_1, ANPROJ_2, AFF_2, MOD_4, FUNCT_2, PRE_POLY, SETFAM_1,
COMBGRAS;
notations TARSKI, XBOOLE_0, CARD_1, SUBSET_1, ORDINAL1, ENUMSET1, ZFMISC_1,
SETFAM_1, DOMAIN_1, FINSET_1, RELAT_1, RELSET_1, WELLORD2, NUMBERS,
INCSP_1, XXREAL_0, XCMPLX_0, REAL_1, FUNCT_1, FUNCT_2, INCPROJ, NAT_1;
constructors SETFAM_1, WELLORD2, DOMAIN_1, REAL_1, NAT_1, BINOP_2, INCPROJ,
RELSET_1, XREAL_0, INT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1,
XREAL_0, NAT_1, CARD_1, INCSP_1, RELSET_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
reserve
k,n for Nat,
x,y,X,Y,Z for set;
theorem :: COMBGRAS:1
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);
theorem :: COMBGRAS:2
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;
theorem :: COMBGRAS:3
card X c= card Y iff ex f being Function st f is one-to-one & X
c= dom f & f.:X c= Y;
theorem :: COMBGRAS:4
for f being Function st f is one-to-one & X c= dom f holds card(f
.:X) = card X;
theorem :: COMBGRAS:5
X \ Y = X \ Z & Y c= X & Z c= X implies Y = Z;
theorem :: COMBGRAS:6
for Y being non empty set for p being Function of X,Y st p is
one-to-one for x1,x2 being Subset of X holds x1 <> x2 implies p.:x1 <> p.:x2;
theorem :: COMBGRAS:7
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 (3 <= n implies 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 );
theorem :: COMBGRAS:8
for P1,P2 being IncProjStr st the IncProjStr of P1 = the
IncProjStr of P2 for A1 being POINT of P1, A2 being POINT of P2 st A1 = A2 for
L1 being LINE of P1, L2 being LINE of P2 st L1 = L2 holds A1 on L1 implies A2
on L2;
theorem :: COMBGRAS:9
for P1,P2 being IncProjStr st the IncProjStr of P1 = the
IncProjStr of P2 for A1 being Subset of the Points of P1 for A2 being Subset of
the Points of P2 st A1 = A2 for L1 being LINE of P1, L2 being LINE of P2 st L1
= L2 holds A1 on L1 implies A2 on L2;
registration
cluster with_non-trivial_lines linear up-2-rank strict for IncProjStr;
end;
begin :: Configuration G
definition
mode PartialLinearSpace is with_non-trivial_lines up-2-rank IncProjStr;
end;
definition
let k be Nat;
let X be non empty set such that
0 < k and
k + 1 c= card X;
func G_(k,X) -> strict PartialLinearSpace means
:: 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:];
end;
theorem :: COMBGRAS:10
for k being Nat for X being non empty set st 0 < k &
k + 1 c= card X for A being POINT of G_(k,X) for L being LINE of G_(k,X) holds
A on L iff A c= L;
theorem :: 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;
theorem :: 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);
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;
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 ex
L being LINE of S st {A,B} on L;
end;
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;
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;
theorem :: COMBGRAS:14
for k being Element of NAT for X being non empty set st 2 <= k &
k + 2 c= card X for K being Subset of the Points of G_(k,X) holds K is STAR or
K is TOP implies K is maximal_clique;
theorem :: COMBGRAS:15
for k being Element of NAT for X being non empty set st 2 <= k &
k + 2 c= card X for K being Subset of the Points of G_(k,X) holds K is
maximal_clique implies K is STAR or K is TOP;
begin :: Automorphisms
definition
let S1,S2 be IncProjStr;
struct IncProjMap over S1,S2 (#point-map -> Function of the Points of S1,
the Points of S2, line-map -> 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;
end;
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;
end;
theorem :: 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 the IncProjMap of F1 = the IncProjMap of F2;
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;
theorem :: COMBGRAS:17
for S1,S2 being IncProjStr for F1,F2 being IncProjMap over S1,S2 st
the IncProjMap of F1 = the IncProjMap of F2 holds F1 is incidence_preserving
implies F2 is incidence_preserving;
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;
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;
end;
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;
end;
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};
end;
definition
let k be Nat;
let X be non empty set such that
0 < k & k + 1 c= card X;
let A be finite set such that
card A = k - 1;
func ^^(A,X,k) -> Subset of the Points of G_(k,X) equals
:: COMBGRAS:def 13
^^(A,X);
end;
theorem :: 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)};
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)};
theorem :: COMBGRAS:20
for S being IncProjStr for F being IncProjMap over S,S for K
being Subset of the Points of S holds F is incidence_preserving & K is clique
implies F.:K is clique;
theorem :: COMBGRAS:21
for S being IncProjStr for F being IncProjMap over S,S for K
being Subset of the Points of S holds F is incidence_preserving & the line-map
of F is onto & K is clique implies F"K is clique;
theorem :: COMBGRAS:22
for S being IncProjStr for F being IncProjMap over S,S for K
being Subset of the Points of S holds F is automorphism & K is maximal_clique
implies F.:K is maximal_clique & F"K is maximal_clique;
theorem :: COMBGRAS:23
for k being Element of NAT for X being non empty set st 2 <= k &
k + 2 c= card X for F being IncProjMap over G_(k,X), G_(k,X) st F is
automorphism for K being Subset of the Points of G_(k,X) holds K is STAR
implies F.:K is STAR & F"K is STAR;
definition
let k be Nat;
let X be non empty set such that
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
:: 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;
end;
theorem :: COMBGRAS:24
for k being Nat for X being non empty set st k = 1 &
k + 1 c= card X for F being IncProjMap over G_(k,X), G_(k,X) st F is
automorphism holds ex s being Permutation of X st the IncProjMap of F =
incprojmap(k,s);
theorem :: COMBGRAS:25
for k being Nat for X being non empty set st 1 < k &
card X = k + 1 for F being IncProjMap over G_(k,X), G_(k,X) st F is
automorphism holds ex s being Permutation of X st the IncProjMap of F =
incprojmap(k,s);
theorem :: COMBGRAS:26
for k being Element of NAT for X being non empty set st 0 < k &
k + 1 c= card X for T being Subset of the Points of G_(k,X) for S being Subset
of X holds card S = k - 1 & T = {A where A is Subset of X: card A = k & S c= A}
implies S = meet T;
theorem :: COMBGRAS:27 ::LemStarb:
for k being Element of NAT for X being non empty set st 0 < k & k + 1
c= card X for T being Subset of the Points of G_(k,X) st T is STAR for S being
Subset of X holds S = meet T implies card S = k - 1 & T = {A where A is Subset
of X: card A = k & S c= A};
theorem :: COMBGRAS:28
for k being Element of NAT for X being non empty set st 0 < k &
k + 1 c= card X 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;
theorem :: COMBGRAS:29
for k being Element of NAT for X being non empty set st k + 1 c=
card X for A being finite Subset of X st card A = k-1 holds ^^(A,X,k) is STAR
;
theorem :: COMBGRAS:30
for k being Element of NAT for X being non empty set st k + 1 c=
card X for A being finite Subset of X st card A = k-1 holds meet ^^(A,X,k) = A;
theorem :: COMBGRAS:31
for k being Nat for X being non empty set st 0 < k &
k + 3 c= card X for F being IncProjMap over G_(k+1,X), G_(k+1,X) st F is
automorphism 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), B being
finite set st B = A holds H.A = meet(F.:(^^(B,X,k+1)));
theorem :: COMBGRAS:32
for k being Nat for X being non empty set st 0 < k &
k + 3 c= card X for F being IncProjMap over G_(k+1,X), G_(k+1,X) st F is
automorphism for H being IncProjMap over G_(k,X), G_(k,X) st the line-map of H
= the point-map of F for f being Permutation of X st the IncProjMap of H =
incprojmap(k,f) holds the IncProjMap of F = incprojmap(k+1,f);
theorem :: COMBGRAS:33
for k being Nat for X being non empty set st 2 <= k &
k + 2 c= card X for F being IncProjMap over G_(k,X), G_(k,X) st F is
automorphism holds ex s being Permutation of X st the IncProjMap of F =
incprojmap(k,s);
theorem :: COMBGRAS:34
for k being Nat for X being non empty set st 0 < k &
k + 1 c= card X for s being Permutation of X holds incprojmap(k,s) is
automorphism;
theorem :: COMBGRAS:35
for X being non empty set st 0 < k & k + 1 c= card X for F being
IncProjMap over G_(k,X), G_(k,X) holds F is automorphism iff ex s being
Permutation of X st the IncProjMap of F = incprojmap(k,s);