:: About Graph Mappings :: by Sebastian Koch :: :: Received August 29, 2019 :: Copyright (c) 2019-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, RELAT_1, FUNCT_1, TARSKI, CARD_1, XBOOLE_0, GLIB_000, PARTFUN1, ZFMISC_1, FUNCOP_1, ALGSTR_0, FUNCT_2, GLIB_009, MOD_4, WAYBEL_0, RING_3, ORDINAL2, CHORD, CARD_2, SCMYCIEL, GLIB_010, GLIB_011; notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, SETWISEO, EQREL_1, FUNCOP_1, FUNCT_4, PARTFUN2, CARD_1, PBOOLE, CARD_2, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, VALUED_0, FINSEQ_1, BSPACE, GLIB_000, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_6, GLIB_001, CHORD, GLIB_008, GLIB_009, GLIB_010; constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2, FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN, CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2, GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1, GLIB_008, GLIB_009, GLIB_010, FUNCT_7; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, GLIB_000, CARD_1, FUNCT_2, PARTFUN1, RELSET_1, XTUPLE_0, GLIB_006, GLIB_008, GLIB_009, GLIB_010, FUNCT_7; requirements BOOLE, SUBSET; begin :: Vertex Mappings definition let G1, G2 be _Graph; mode PVertexMapping of G1, G2 -> PartFunc of the_Vertices_of G1, the_Vertices_of G2 means :: GLIB_011:def 1 for v,w being Vertex of G1 st v in dom it & w in dom it & v,w are_adjacent holds it/.v, it/.w are_adjacent; end; theorem :: GLIB_011:1 for G1, G2 being _Graph for f being PartFunc of the_Vertices_of G1, the_Vertices_of G2 holds f is PVertexMapping of G1, G2 iff for v,w,e being object st v in dom f & w in dom f & e Joins v,w,G1 ex e9 being object st e9 Joins f.v,f.w,G2; definition let G1, G2 be _Graph, f be PVertexMapping of G1, G2; attr f is directed means :: GLIB_011:def 2 for v,w,e being object st v in dom f & w in dom f & e DJoins v,w,G1 ex e9 being object st e9 DJoins f.v,f.w,G2; attr f is continuous means :: GLIB_011:def 3 for v,w being Vertex of G1 st v in dom f & w in dom f & f/.v, f/.w are_adjacent holds v, w are_adjacent; attr f is Dcontinuous means :: GLIB_011:def 4 for v,w,e9 being object st v in dom f & w in dom f & e9 DJoins f.v,f.w,G2 ex e being object st e DJoins v,w,G1; end; theorem :: GLIB_011:2 for G1, G2 being _Graph, f being PVertexMapping of G1, G2 holds f is continuous iff for v,w,e9 being object st v in dom f & w in dom f & e9 Joins f.v,f.w,G2 ex e being object st e Joins v,w,G1; theorem :: GLIB_011:3 for G1, G2 being _Graph, f being PVertexMapping of G1, G2 holds f is continuous iff for v,w being Vertex of G1 st v in dom f & w in dom f holds v, w are_adjacent iff f/.v, f/.w are_adjacent; registration let G1, G2 be _Graph; cluster Dcontinuous -> continuous for PVertexMapping of G1, G2; cluster empty -> one-to-one Dcontinuous directed continuous for PVertexMapping of G1, G2; cluster total -> non empty for PVertexMapping of G1, G2; cluster onto -> non empty for PVertexMapping of G1, G2; end; registration let G1 be simple _Graph, G2 be _Graph; cluster Dcontinuous -> directed for PVertexMapping of G1, G2; end; registration let G1 be _Graph, G2 be simple _Graph; cluster directed continuous -> Dcontinuous for PVertexMapping of G1, G2; end; registration let G1 be _trivial _Graph, G2 be _Graph; cluster -> directed for PVertexMapping of G1, G2; cluster continuous -> Dcontinuous for PVertexMapping of G1, G2; cluster non empty -> total for PVertexMapping of G1, G2; end; registration let G1 be _Graph, G2 be _trivial _Graph; cluster non empty -> onto for PVertexMapping of G1, G2; end; registration let G1 be _Graph, G2 be _trivial loopless _Graph; cluster -> Dcontinuous continuous for PVertexMapping of G1, G2; end; registration let G1, G2 be _Graph; cluster empty one-to-one directed continuous Dcontinuous for PVertexMapping of G1, G2; end; theorem :: GLIB_011:4 for G1, G2 being _Graph for f being PartFunc of the_Vertices_of G1, the_Vertices_of G2 holds f is directed PVertexMapping of G1, G2 iff for v,w,e being object st v in dom f & w in dom f & e DJoins v,w,G1 ex e9 being object st e9 DJoins f.v,f.w,G2; registration let G1 be loopless _Graph, G2 be _Graph; cluster non empty one-to-one directed for PVertexMapping of G1, G2; end; registration let G1, G2 be loopless _Graph; cluster non empty one-to-one directed continuous Dcontinuous for PVertexMapping of G1, G2; end; registration let G1, G2 be non loopless _Graph; cluster non empty one-to-one directed continuous Dcontinuous for PVertexMapping of G1, G2; end; theorem :: GLIB_011:5 for G being _Graph holds id the_Vertices_of G is directed continuous Dcontinuous PVertexMapping of G, G; theorem :: GLIB_011:6 for G1, G2 being _Graph, f being PVertexMapping of G1, G2 st f is total holds (G2 is loopless implies G1 is loopless) & (G2 is edgeless implies G1 is edgeless); theorem :: GLIB_011:7 for G1, G2 being _Graph, f being continuous PVertexMapping of G1, G2 st f is onto holds (G1 is loopless implies G2 is loopless) & (G1 is edgeless implies G2 is edgeless); definition let G1, G2 be _Graph, f be PVertexMapping of G1, G2; attr f is isomorphism means :: GLIB_011:def 5 f is total one-to-one onto & for v,w being Vertex of G1 holds card G1.edgesBetween({v},{w}) = card G2.edgesBetween({f.v},{f.w}); attr f is Disomorphism means :: GLIB_011:def 6 f is total one-to-one onto & for v,w being Vertex of G1 holds card G1.edgesDBetween({v},{w}) = card G2.edgesDBetween({f.v},{f.w}) & card G1.edgesDBetween({w},{v}) = card G2.edgesDBetween({f.w},{f.v}); end; registration let G1, G2 be _Graph; cluster isomorphism -> total one-to-one onto continuous for PVertexMapping of G1, G2; cluster Disomorphism -> total one-to-one onto isomorphism continuous directed Dcontinuous for PVertexMapping of G1, G2; end; theorem :: GLIB_011:8 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is total one-to-one continuous for v,w being Vertex of G1 holds card G1.edgesBetween({v},{w}) = card G2.edgesBetween({f.v},{f.w}); definition let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2; redefine attr f is isomorphism means :: GLIB_011:def 7 f is total one-to-one onto continuous; end; registration let G1, G2 be non-multi _Graph; cluster total one-to-one onto continuous -> isomorphism for PVertexMapping of G1, G2; end; theorem :: GLIB_011:9 for G1, G2 being non-Dmulti _Graph, f being PVertexMapping of G1, G2 st f is total one-to-one directed Dcontinuous for v,w being Vertex of G1 holds card G1.edgesDBetween({v},{w}) = card G2.edgesDBetween({f.v},{f.w}) & card G1.edgesDBetween({w},{v}) = card G2.edgesDBetween({f.w},{f.v}); definition let G1, G2 be non-Dmulti _Graph, f be PVertexMapping of G1, G2; redefine attr f is Disomorphism means :: GLIB_011:def 8 f is total one-to-one onto directed Dcontinuous; end; registration let G1, G2 be non-Dmulti _Graph; cluster total one-to-one onto directed Dcontinuous -> Disomorphism for PVertexMapping of G1, G2; end; registration let G be_Graph; cluster Disomorphism isomorphism for PVertexMapping of G, G; end; theorem :: GLIB_011:10 for G being _Graph holds id the_Vertices_of G is Disomorphism isomorphism PVertexMapping of G, G; definition let G1, G2 be _Graph, f be PVertexMapping of G1, G2; attr f is invertible means :: GLIB_011:def 9 f is one-to-one continuous; end; registration let G1, G2 be _Graph; cluster invertible -> one-to-one continuous for PVertexMapping of G1, G2; cluster one-to-one continuous -> invertible for PVertexMapping of G1, G2; cluster isomorphism -> invertible for PVertexMapping of G1, G2; cluster Disomorphism -> invertible for PVertexMapping of G1, G2; cluster empty invertible for PVertexMapping of G1, G2; end; registration let G1, G2 be loopless _Graph; cluster non empty directed invertible for PVertexMapping of G1, G2; end; registration let G1, G2 be non loopless _Graph; cluster non empty directed invertible for PVertexMapping of G1, G2; end; definition let G1, G2 be _Graph, f be invertible PVertexMapping of G1, G2; redefine func f" -> PVertexMapping of G2, G1; end; registration let G1, G2 be _Graph, f be invertible PVertexMapping of G1, G2; cluster f" -> one-to-one continuous invertible for PVertexMapping of G2, G1; end; definition let G1, G2, G3 be _Graph; let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3; redefine func g*f -> PVertexMapping of G1, G3; end; theorem :: GLIB_011:11 for G1, G2, G3 being _Graph for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3 st f is continuous & g is continuous holds g*f is continuous; theorem :: GLIB_011:12 for G1, G2, G3 being _Graph for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3 st f is directed & g is directed holds g*f is directed; theorem :: GLIB_011:13 for G1, G2, G3 being _Graph for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3 st f is Dcontinuous & g is Dcontinuous holds g*f is Dcontinuous; theorem :: GLIB_011:14 for G1, G2, G3 being _Graph for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3 st f is isomorphism & g is isomorphism holds g*f is isomorphism; theorem :: GLIB_011:15 for G1, G2, G3 being _Graph for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3 st f is Disomorphism & g is Disomorphism holds g*f is Disomorphism; begin :: The relation between Graph Mappings and Vertex Mappings theorem :: GLIB_011:16 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st for v,w being Vertex of G1 st v in dom F_V & w in dom F_V & v,w are_adjacent ex e being object st e in dom F_E & e Joins v,w,G1 holds F_V is PVertexMapping of G1, G2; theorem :: GLIB_011:17 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st dom F_E = the_Edges_of G1 holds F_V is PVertexMapping of G1, G2; theorem :: GLIB_011:18 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is total holds F_V is PVertexMapping of G1, G2; theorem :: GLIB_011:19 for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2 st for v,w being object st v in dom F_V & w in dom F_V & ex e being object st e DJoins v,w,G1 holds ex e being object st e in dom F_E & e DJoins v,w,G1 holds F_V is directed PVertexMapping of G1, G2; theorem :: GLIB_011:20 for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2 st dom F_E = the_Edges_of G1 holds F_V is directed PVertexMapping of G1, G2; theorem :: GLIB_011:21 for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2 st F is total holds F_V is directed PVertexMapping of G1, G2; theorem :: GLIB_011:22 for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2 st F_V is PVertexMapping of G1, G2 & for v,w being Vertex of G1 st v in dom F_V & w in dom F_V & F_V/.v, F_V/.w are_adjacent ex e9 being object st e9 in rng F_E & e9 Joins F_V.v,F_V.w,G2 holds F_V is continuous PVertexMapping of G1, G2; theorem :: GLIB_011:23 for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2 st dom F_E = the_Edges_of G1 & rng F_E = the_Edges_of G2 holds F_V is continuous PVertexMapping of G1, G2; theorem :: GLIB_011:24 for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2 st F is total onto holds F_V is continuous PVertexMapping of G1, G2; theorem :: GLIB_011:25 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is isomorphism ex f being PVertexMapping of G1, G2 st F_V = f & f is isomorphism; theorem :: GLIB_011:26 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is Disomorphism ex f being directed PVertexMapping of G1, G2 st F_V = f & f is Disomorphism; :: Maybe add that f is continuous implies rng F_E = E2 /\ ... ? :: An example why this isn't always the case is the embedding of P_3 into K_3 theorem :: GLIB_011:27 for G1, G2 being _Graph, f being PVertexMapping of G1, G2 for E1 being RepEdgeSelection of G1, E2 being RepEdgeSelection of G2 ex F being PGraphMapping of G1, G2 st F_V = f & dom F_E = E1 /\ G1.edgesBetween(dom f) & rng F_E c= E2 /\ G2.edgesBetween(rng f); definition let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2; func PVM2PGM(f) -> PGraphMapping of G1, G2 means :: GLIB_011:def 10 it _V = f & dom it _E = G1.edgesBetween(dom f) & rng it _E c= G2.edgesBetween(rng f); end; theorem :: GLIB_011:28 for G1, G2 being non-multi _Graph for f be PVertexMapping of G1, G2 holds (PVM2PGM(f))_V = f; registration let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2; reduce (PVM2PGM f)_V to f; end; :: as above theorem :: GLIB_011:29 for G1, G2 being _Graph, f being directed PVertexMapping of G1, G2 for E1 being RepDEdgeSelection of G1, E2 being RepDEdgeSelection of G2 ex F being directed PGraphMapping of G1, G2 st F_V = f & dom F_E = E1 /\ G1.edgesBetween(dom f) & rng F_E c= E2 /\ G2.edgesBetween(rng f); definition let G1, G2 be non-Dmulti _Graph; let f be directed PVertexMapping of G1, G2; func DPVM2PGM(f) -> directed PGraphMapping of G1, G2 means :: GLIB_011:def 11 it _V = f & dom it _E = G1.edgesBetween(dom f) & rng it _E c= G2.edgesBetween(rng f); end; theorem :: GLIB_011:30 for G1, G2 being non-Dmulti _Graph for f be directed PVertexMapping of G1, G2 holds (DPVM2PGM(f))_V = f; registration let G1, G2 be non-Dmulti _Graph; let f be directed PVertexMapping of G1, G2; reduce (DPVM2PGM f)_V to f; end; theorem :: GLIB_011:31 for G1, G2 being non-multi _Graph for f being directed PVertexMapping of G1, G2 holds PVM2PGM(f) = DPVM2PGM(f); theorem :: GLIB_011:32 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is total holds PVM2PGM(f) is total; theorem :: GLIB_011:33 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is total holds DPVM2PGM(f) is total; theorem :: GLIB_011:34 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is one-to-one holds PVM2PGM(f) is one-to-one; theorem :: GLIB_011:35 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is one-to-one holds DPVM2PGM(f) is one-to-one; theorem :: GLIB_011:36 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is onto continuous holds PVM2PGM(f) is onto; theorem :: GLIB_011:37 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is onto Dcontinuous holds DPVM2PGM(f) is onto; theorem :: GLIB_011:38 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is continuous one-to-one holds PVM2PGM(f) is semi-continuous; theorem :: GLIB_011:39 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is continuous holds PVM2PGM(f) is continuous; theorem :: GLIB_011:40 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is one-to-one holds DPVM2PGM(f) is semi-Dcontinuous semi-continuous; theorem :: GLIB_011:41 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is Dcontinuous holds DPVM2PGM(f) is Dcontinuous; theorem :: GLIB_011:42 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is one-to-one holds PVM2PGM(f) is one-to-one; theorem :: GLIB_011:43 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is one-to-one holds DPVM2PGM(f) is one-to-one; theorem :: GLIB_011:44 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is total one-to-one holds PVM2PGM(f) is weak_SG-embedding; theorem :: GLIB_011:45 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is total one-to-one holds DPVM2PGM(f) is weak_SG-embedding; theorem :: GLIB_011:46 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is total one-to-one continuous holds PVM2PGM(f) is strong_SG-embedding; theorem :: GLIB_011:47 for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2 st f is isomorphism holds PVM2PGM(f) is isomorphism; theorem :: GLIB_011:48 for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2 st f is Disomorphism holds DPVM2PGM(f) is Disomorphism; theorem :: GLIB_011:49 for G1, G2 being non-multi _Graph holds G2 is G1-isomorphic iff ex f being PVertexMapping of G1, G2 st f is isomorphism; theorem :: GLIB_011:50 for G1, G2 being non-Dmulti _Graph holds G2 is G1-Disomorphic iff ex f being directed PVertexMapping of G1, G2 st f is Disomorphism;