:: Abstract Simplicial Complexes :: by Karol P\c{a}k :: :: Received December 18, 2009 :: Copyright (c) 2009-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 ARYTM_1, XBOOLE_0, CARD_1, CLASSES1, COHSP_1, FINSET_1, FUNCT_1, GROUP_4, INT_1, MATROID0, ORDERS_1, PARTFUN1, PRE_TOPC, RELAT_1, RELAT_2, NUMBERS, SETFAM_1, SGRAPH1, SUBSET_1, TARSKI, TRIANG_1, WELLORD1, ZFMISC_1, SIMPLEX0, XXREAL_0, NAT_1, ORDINAL1, FUNCOP_1, ARYTM_3, RCOMP_1, STRUCT_0, GLIB_000, REAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, WELLORD1, ORDERS_1, FINSET_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0, INT_1, XXREAL_3, NAT_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, PENCIL_1, CLASSES1, MATROID0, RELSET_1, COHSP_1, FUNCOP_1; constructors SETFAM_1, XXREAL_3, REAL_1, TOPS_2, BORSUK_1, WELLORD1, BINOP_2, CLASSES1, COH_SP, MATROID0, COHSP_1, FUNCOP_1, NAT_1; registrations PRE_TOPC, CARD_1, COHSP_1, FIB_NUM2, FINSET_1, FUNCT_1, INT_1, MATROID0, NAT_1, ORDINAL1, PENCIL_1, RELAT_1, SETFAM_1, SUBSET_1, STRUCT_0, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_3, FUNCOP_1, RELSET_1; requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE; begin :: Preliminaries reserve x,y, X,Y,Z for set, D for non empty set, n,k for Nat, i,i1,i2 for Integer; notation let X; antonym X is with_empty_element for X is with_non-empty_elements; end; registration cluster empty -> subset-closed for set; cluster with_empty_element -> non empty for set; cluster non empty subset-closed -> with_empty_element for set; end; registration let X; cluster Sub_of_Fin X -> finite-membered; end; registration let X be subset-closed set; cluster Sub_of_Fin X -> subset-closed; end; theorem :: SIMPLEX0:1 Y is subset-closed iff for X st X in Y holds bool X c= Y; registration let A,B be subset-closed set; cluster A \/ B -> subset-closed; cluster A /\ B -> subset-closed; end; definition let X; func subset-closed_closure_of X -> subset-closed set means :: SIMPLEX0:def 1 X c= it & for Y st X c= Y & Y is subset-closed holds it c= Y; end; theorem :: SIMPLEX0:2 x in subset-closed_closure_of X iff ex y st x c= y & y in X; definition let X; let F be Subset-Family of X; redefine func subset-closed_closure_of F -> subset-closed Subset-Family of X; end; registration cluster subset-closed_closure_of {} -> empty; let X be non empty set; cluster subset-closed_closure_of X -> non empty; end; registration let X be with_non-empty_element set; cluster subset-closed_closure_of X -> with_non-empty_element; end; registration let X be finite-membered set; cluster subset-closed_closure_of X -> finite-membered; end; theorem :: SIMPLEX0:3 X c=Y & Y is subset-closed implies subset-closed_closure_of X c= Y; theorem :: SIMPLEX0:4 subset-closed_closure_of {X} = bool X; theorem :: SIMPLEX0:5 subset-closed_closure_of (X\/Y) = subset-closed_closure_of X \/ subset-closed_closure_of Y; theorem :: SIMPLEX0:6 X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y; theorem :: SIMPLEX0:7 X is subset-closed implies subset-closed_closure_of X = X; theorem :: SIMPLEX0:8 subset-closed_closure_of X c= X implies X is subset-closed; definition let Y,X; let n be set;::Cardinal; func the_subsets_with_limited_card(n,X,Y) -> Subset-Family of Y means :: SIMPLEX0:def 2 for A be Subset of Y holds A in it iff A in X & card A c= n; end; registration let D; cluster finite with_non-empty_element subset-closed finite-membered for Subset-Family of D; end; registration let Y,X; let n be finite Cardinal; cluster the_subsets_with_limited_card(n,X,Y) -> finite-membered; end; registration let Y; let X be subset-closed set; let n be Cardinal; cluster the_subsets_with_limited_card(n,X,Y) -> subset-closed; end; registration let Y; let X be with_empty_element set; let n be Cardinal; cluster the_subsets_with_limited_card(n,X,Y) -> with_empty_element; end; registration let D; let X be with_non-empty_element subset-closed Subset-Family of D; let n be non empty Cardinal; cluster the_subsets_with_limited_card(n,X,D) -> with_non-empty_element; end; notation let X; let Y be Subset-Family of X; let n be set;::Cardinal; synonym the_subsets_with_limited_card(n,Y) for the_subsets_with_limited_card(n,Y,X); end; theorem :: SIMPLEX0:9 X is non empty finite c=-linear implies union X in X; theorem :: SIMPLEX0:10 for X be finite c=-linear set st X is with_non-empty_elements holds card X c= card union X; theorem :: SIMPLEX0:11 X is c=-linear implies X\/{union X\/x} is c=-linear; theorem :: SIMPLEX0:12 for X be non empty set ex Y be Subset-Family of X st Y is with_non-empty_elements c=-linear & X in Y & card X = card Y & for Z st Z in Y & card Z <> 1 ex x st x in Z & Z\{x} in Y; theorem :: SIMPLEX0:13 for Y be Subset-Family of X st Y is finite with_non-empty_elements c=-linear & X in Y ex Y1 be Subset-Family of X st Y c= Y1 & Y1 is with_non-empty_elements c=-linear & card X = card Y1 & for Z st Z in Y1 & card Z <> 1 ex x st x in Z & Z\{x} in Y1; begin :: Simplicial Complexes definition mode SimplicialComplexStr is TopStruct; end; reserve K for SimplicialComplexStr; notation let K; let A be Subset of K; synonym A is simplex-like for A is open; end; notation let K; let S be Subset-Family of K; synonym S is simplex-like for S is open; end; registration let K; cluster empty simplex-like for Subset-Family of K; end; theorem :: SIMPLEX0:14 for S be Subset-Family of K holds S is simplex-like iff S c= the topology of K; definition let K; let v be Element of K; attr v is vertex-like means :: SIMPLEX0:def 3 ex S be Subset of K st S is simplex-like & v in S; end; definition let K; func Vertices K -> Subset of K means :: SIMPLEX0:def 4 for v be Element of K holds v in it iff v is vertex-like; end; definition let K be SimplicialComplexStr; mode Vertex of K is Element of Vertices K; end; definition let K be SimplicialComplexStr; attr K is finite-vertices means :: SIMPLEX0:def 5 Vertices K is finite; end; definition let K; attr K is locally-finite means :: SIMPLEX0:def 6 for v be Vertex of K holds {S where S is Subset of K : S is simplex-like & v in S} is finite; end; definition let K; attr K is empty-membered means :: SIMPLEX0:def 7 the topology of K is empty-membered; attr K is with_non-empty_elements means :: SIMPLEX0:def 8 the topology of K is with_non-empty_elements; end; notation let K; antonym K is with_non-empty_element for K is empty-membered; antonym K is with_empty_element for K is with_non-empty_elements; end; definition let X; mode SimplicialComplexStr of X -> SimplicialComplexStr means :: SIMPLEX0:def 9 [#]it c= X; end; definition let X; let KX be SimplicialComplexStr of X; attr KX is total means :: SIMPLEX0:def 10 [#]KX = X; end; registration cluster with_empty_element -> non void for SimplicialComplexStr; cluster with_non-empty_element -> non void for SimplicialComplexStr; cluster non void empty-membered -> with_empty_element for SimplicialComplexStr; cluster non void subset-closed -> with_empty_element for SimplicialComplexStr; cluster empty-membered-> subset-closed finite-vertices for SimplicialComplexStr; cluster finite-vertices-> locally-finite finite-degree for SimplicialComplexStr; cluster locally-finite subset-closed -> finite-membered for SimplicialComplexStr; end; registration let X; cluster empty void empty-membered strict for SimplicialComplexStr of X; end; registration let D; cluster non empty non void total empty-membered strict for SimplicialComplexStr of D; cluster non empty total with_empty_element with_non-empty_element finite-vertices subset-closed strict for SimplicialComplexStr of D; end; registration cluster non empty with_empty_element with_non-empty_element finite-vertices subset-closed strict for SimplicialComplexStr; end; registration let K be with_non-empty_element SimplicialComplexStr; cluster Vertices K -> non empty; end; registration let K be finite-vertices SimplicialComplexStr; cluster simplex-like -> finite for Subset-Family of K; end; registration let K be finite-membered SimplicialComplexStr; cluster simplex-like -> finite-membered for Subset-Family of K; end; theorem :: SIMPLEX0:15 Vertices K is empty iff K is empty-membered; theorem :: SIMPLEX0:16 Vertices K = union the topology of K; theorem :: SIMPLEX0:17 for S be Subset of K st S is simplex-like holds S c= Vertices K; theorem :: SIMPLEX0:18 K is finite-vertices implies the topology of K is finite; theorem :: SIMPLEX0:19 the topology of K is finite & K is non finite-vertices implies K is non finite-membered; theorem :: SIMPLEX0:20 K is subset-closed & the topology of K is finite implies K is finite-vertices ; begin :: The Simplicial Complex Generated on the Set definition let X; let Y be Subset-Family of X; func Complex_of Y -> strict SimplicialComplexStr of X equals :: SIMPLEX0:def 11 TopStruct(# X,subset-closed_closure_of Y #); end; registration let X; let Y be Subset-Family of X; cluster Complex_of Y -> total subset-closed; end; registration let X; let Y be non empty Subset-Family of X; cluster Complex_of Y -> with_empty_element; end; registration let X; let Y be finite-membered Subset-Family of X; cluster Complex_of Y -> finite-membered; end; registration let X; let Y be finite finite-membered Subset-Family of X; cluster Complex_of Y -> finite-vertices; end; theorem :: SIMPLEX0:21 K is subset-closed implies the TopStruct of K = Complex_of the topology of K; definition let X; mode SimplicialComplex of X is finite-membered subset-closed SimplicialComplexStr of X; end; definition let K be non void SimplicialComplexStr; mode Simplex of K is simplex-like Subset of K; end; registration let K be with_empty_element SimplicialComplexStr; cluster empty -> simplex-like for Subset of K; cluster empty for Simplex of K; end; registration let K be non void finite-membered SimplicialComplexStr; cluster finite for Simplex of K; end; begin :: The Degree of Simplicial Complexes definition let K; func degree K -> ExtReal means :: SIMPLEX0:def 12 (for S be finite Subset of K st S is simplex-like holds card S <= it+1) & ex S be Subset of K st S is simplex-like & card S = it+1 if K is non void finite-degree, it = -1 if K is void otherwise it = +infty; end; registration let K be finite-degree SimplicialComplexStr; cluster degree K + 1 -> natural; cluster degree K -> integer; end; theorem :: SIMPLEX0:22 degree K = -1 iff K is empty-membered; theorem :: SIMPLEX0:23 -1 <= degree K; theorem :: SIMPLEX0:24 for S be finite Subset of K st S is simplex-like holds card S <= degree K+1; theorem :: SIMPLEX0:25 K is non void or i >= -1 implies (degree K <= i iff K is finite-membered & for S be finite Subset of K st S is simplex-like holds card S <= i+1); theorem :: SIMPLEX0:26 for A be finite Subset of X holds degree Complex_of {A} = card A - 1; begin :: Subcomplexes definition let X; let KX be SimplicialComplexStr of X; mode SubSimplicialComplex of KX -> SimplicialComplex of X means :: SIMPLEX0:def 13 [#]it c= [#]KX & the topology of it c= the topology of KX; end; reserve KX for SimplicialComplexStr of X, SX for SubSimplicialComplex of KX; registration let X,KX; cluster empty void strict for SubSimplicialComplex of KX; end; registration let X; let KX be void SimplicialComplexStr of X; cluster -> void for SubSimplicialComplex of KX; end; registration let D; let KD be non void subset-closed SimplicialComplexStr of D; cluster non void for SubSimplicialComplex of KD; end; registration let X; let KX be finite-vertices SimplicialComplexStr of X; cluster -> finite-vertices for SubSimplicialComplex of KX; end; registration let X; let KX be finite-degree SimplicialComplexStr of X; cluster -> finite-degree for SubSimplicialComplex of KX; end; theorem :: SIMPLEX0:27 for S1 be SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX; theorem :: SIMPLEX0:28 for A be Subset of KX for S be finite-membered Subset-Family of A st subset-closed_closure_of S c=the topology of KX holds Complex_of S is strict SubSimplicialComplex of KX; theorem :: SIMPLEX0:29 for KX be subset-closed SimplicialComplexStr of X for A be Subset of KX for S be finite-membered Subset-Family of A st S c= the topology of KX holds Complex_of S is strict SubSimplicialComplex of KX; theorem :: SIMPLEX0:30 for Y1,Y2 be Subset-Family of X st Y1 is finite-membered & Y1 is_finer_than Y2 holds Complex_of Y1 is SubSimplicialComplex of Complex_of Y2; theorem :: SIMPLEX0:31 Vertices SX c= Vertices KX; theorem :: SIMPLEX0:32 degree SX <= degree KX; definition let X,KX,SX; attr SX is maximal means :: SIMPLEX0:def 14 for A be Subset of SX st A in the topology of KX holds A is simplex-like; end; theorem :: SIMPLEX0:33 SX is maximal iff bool[#]SX /\ the topology of KX c= the topology of SX; registration let X,KX; cluster maximal strict for SubSimplicialComplex of KX; end; theorem :: SIMPLEX0:34 for S1 be SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds S1 is maximal SubSimplicialComplex of KX; theorem :: SIMPLEX0:35 for S1 be SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds S1 is maximal; theorem :: SIMPLEX0:36 for K1,K2 be maximal SubSimplicialComplex of KX st [#]K1 = [#]K2 holds the TopStruct of K1 = the TopStruct of K2; definition let X; let KX be subset-closed SimplicialComplexStr of X; let A be Subset of KX such that bool A /\ the topology of KX is finite-membered; func KX|A -> maximal strict SubSimplicialComplex of KX means :: SIMPLEX0:def 15 [#]it = A; end; reserve SC for SimplicialComplex of X; definition let X,SC; let A be Subset of SC; redefine func SC|A means :: SIMPLEX0:def 16 [#]it = A; end; theorem :: SIMPLEX0:37 for A be Subset of SC holds the topology of SC|A = bool A /\ the topology of SC; theorem :: SIMPLEX0:38 for A,B be Subset of SC for B1 be Subset of SC|A st B1 = B holds SC|A|B1 = SC|B; theorem :: SIMPLEX0:39 SC|[#]SC = the TopStruct of SC; theorem :: SIMPLEX0:40 for A,B be Subset of SC st A c= B holds SC|A is SubSimplicialComplex of SC|B; begin :: The Skelton of a Simplicial Complex definition let X,KX; let i be dim-like number; func Skeleton_of(KX,i) -> SimplicialComplexStr of X equals :: SIMPLEX0:def 17 Complex_of the_subsets_with_limited_card(Segm(i+1),the topology of KX); end; definition let n be natural Number; redefine func -n -> integer number; end; registration let X,KX; cluster Skeleton_of(KX,-1) -> empty-membered; let i be dim-like number; cluster Skeleton_of(KX,i) -> finite-degree; end; registration let X; let KX be empty-membered SimplicialComplexStr of X; let i be dim-like number; cluster Skeleton_of(KX,i) -> empty-membered; end; registration let D; let KD be non void subset-closed SimplicialComplexStr of D; let i be dim-like number; cluster Skeleton_of(KD,i) -> non void; end; theorem :: SIMPLEX0:41 for i1,i2 being dim-like number st -1 <= i1 & i1 <= i2 holds Skeleton_of(KX,i1) is SubSimplicialComplex of Skeleton_of(KX,i2); definition let X; let KX be subset-closed SimplicialComplexStr of X; let i be dim-like number; redefine func Skeleton_of(KX,i) -> SubSimplicialComplex of KX; end; theorem :: SIMPLEX0:42 for i being dim-like number st KX is subset-closed & Skeleton_of(KX,i) is empty-membered holds KX is empty-membered or i = -1; theorem :: SIMPLEX0:43 for i being dim-like number holds degree Skeleton_of(KX,i) <= degree KX; theorem :: SIMPLEX0:44 for i being dim-like number st -1 <= i holds degree Skeleton_of(KX,i) <= i; theorem :: SIMPLEX0:45 for i being dim-like number st -1 <= i & Skeleton_of(KX,i) = the TopStruct of KX holds degree KX <= i; theorem :: SIMPLEX0:46 for i being dim-like number st KX is subset-closed & degree KX <= i holds Skeleton_of(KX,i) = the TopStruct of KX; reserve K for non void subset-closed SimplicialComplexStr; definition let K; let i be Real such that i is integer; mode Simplex of i,K -> finite Simplex of K means :: SIMPLEX0:def 18 card it = i+1 if -1 <= i & i <= degree K otherwise it is empty; end; registration let K; cluster -> empty for Simplex of-1,K; end; theorem :: SIMPLEX0:47 for S be Simplex of i,K st S is non empty holds i is natural; theorem :: SIMPLEX0:48 for S be finite Simplex of K holds S is Simplex of card S - 1,K; theorem :: SIMPLEX0:49 for K be non void subset-closed SimplicialComplexStr of D for S be non void SubSimplicialComplex of K for i be Integer,A be Simplex of i,S st A is non empty or i <= degree S or degree S = degree K holds A is Simplex of i,K; definition let K; let i be Real such that i is integer and i <= degree K; let S be Simplex of i,K; mode Face of S -> Simplex of max(i-1,-1),K means :: SIMPLEX0:def 19 it c= S; end; theorem :: SIMPLEX0:50 for S be Simplex of n,K st n<=degree K holds X is Face of S iff ex x st x in S & S\{x} = X; begin :: The Subdivision of a Simplicial Complex reserve P for Function; definition let X,KX,P; func subdivision(P,KX) -> strict SimplicialComplexStr of X means :: SIMPLEX0:def 20 [#]it = [#]KX & for A be Subset of it holds A is simplex-like iff ex S be c=-linear finite simplex-like Subset-Family of KX st A = P.:S; end; registration let X,KX,P; cluster subdivision(P,KX) -> with_empty_element subset-closed finite-membered; end; registration let X; let KX be void SimplicialComplexStr of X; let P; cluster subdivision(P,KX) -> empty-membered; end; theorem :: SIMPLEX0:51 degree subdivision(P,KX) <= degree KX + 1; theorem :: SIMPLEX0:52 dom P is with_non-empty_elements implies degree subdivision(P,KX) <= degree KX; registration let X; let KX be finite-degree SimplicialComplexStr of X; let P; cluster subdivision(P,KX) -> finite-degree; end; registration let X; let KX be finite-vertices SimplicialComplexStr of X; let P; cluster subdivision(P,KX) -> finite-vertices; end; theorem :: SIMPLEX0:53 for KX be subset-closed SimplicialComplexStr of X for P st dom P is with_non-empty_elements & for n st n <= degree KX ex S be Subset of KX st S is simplex-like & card S = n+1 & BOOL S c=dom P & P.:BOOL S is Subset of KX & P|BOOL S is one-to-one holds degree subdivision(P,KX) = degree KX; theorem :: SIMPLEX0:54 Y c=Z implies subdivision(P|Y,KX) is SubSimplicialComplex of subdivision(P|Z,KX); theorem :: SIMPLEX0:55 dom P/\the topology of KX c= Y implies subdivision(P|Y,KX) = subdivision(P,KX); theorem :: SIMPLEX0:56 Y c= Z implies subdivision(Y|`P,KX) is SubSimplicialComplex of subdivision(Z|`P,KX); theorem :: SIMPLEX0:57 P.:(the topology of KX) c= Y implies subdivision(Y|`P,KX) = subdivision(P,KX); theorem :: SIMPLEX0:58 subdivision(P,SX) is SubSimplicialComplex of subdivision(P,KX); theorem :: SIMPLEX0:59 for A be Subset of subdivision(P,KX) st dom P c=the topology of SX & A = [#]SX holds subdivision(P,SX)=subdivision(P,KX)|A; theorem :: SIMPLEX0:60 for K1,K2 be SimplicialComplexStr of X st the TopStruct of K1 = the TopStruct of K2 holds subdivision(P,K1) = subdivision(P,K2); definition let X,KX,P,n; func subdivision(n,P,KX) -> SimplicialComplexStr of X means :: SIMPLEX0:def 21 ex F be Function st F.0 = KX & F.n = it & dom F = NAT & for k for KX1 be SimplicialComplexStr of X st KX1 = F.k holds F.(k+1) = subdivision(P,KX1); end; theorem :: SIMPLEX0:61 subdivision(0,P,KX) = KX; theorem :: SIMPLEX0:62 subdivision(1,P,KX) = subdivision(P,KX); theorem :: SIMPLEX0:63 for n,k be Element of NAT holds subdivision(n+k,P,KX) = subdivision(n,P,subdivision(k,P,KX)); theorem :: SIMPLEX0:64 [#]subdivision(n,P,KX) = [#]KX; theorem :: SIMPLEX0:65 subdivision(n,P,SX) is SubSimplicialComplex of subdivision(n,P,KX);