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