:: Introduction to Homotopy Theory
:: by Adam Grabowski
::
:: Received September 10, 1997
:: Copyright (c) 1997-2017 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, XBOOLE_0, PRE_TOPC, CARD_1, XXREAL_0, STRUCT_0,
BORSUK_1, XXREAL_1, REAL_1, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, RCOMP_1,
ORDINAL2, FUNCT_4, TOPS_2, FUNCOP_1, GRAPH_1, RELAT_2, ARYTM_3, ARYTM_1,
TOPMETR, TREAL_1, VALUED_1, SETFAM_1, ZFMISC_1, PCOMPS_1, MCART_1,
CONNSP_2, TOPS_1, BORSUK_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1,
NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, XTUPLE_0,
MCART_1, RCOMP_1, PCOMPS_1, TOPS_1, COMPTS_1, CONNSP_1, CONNSP_2,
TREAL_1, FUNCT_4, BORSUK_1, T_0TOPSP, TOPMETR, BINOP_1, FUNCT_3;
constructors SETFAM_1, FUNCT_3, FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_1,
CONNSP_1, TOPS_2, COMPTS_1, URYSOHN1, T_0TOPSP, TREAL_1, FUNCOP_1,
PCOMPS_1, XXREAL_2, COMPLEX1, XTUPLE_0, BINOP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, XREAL_0, MEMBERED,
STRUCT_0, PRE_TOPC, COMPTS_1, METRIC_1, BORSUK_1, RELAT_1, XXREAL_2,
TOPS_1, CONNSP_1, TOPMETR, RELSET_1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve T,T1,T2,S for non empty TopSpace;
scheme :: BORSUK_2:sch 1
FrCard { A() -> non empty set, X() -> set, F(object) -> set, P[set] }:
card { F
(w) where w is Element of A(): w in X() & P[w] } c= card X();
theorem :: BORSUK_2:1
for f being Function of T1,S, g being Function of T2,S st T1 is
SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is
compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for
p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p ) ex h being Function of
T,S st h = f+*g & h is continuous;
registration
let T be TopStruct;
cluster id T -> open continuous;
end;
registration
let T be TopStruct;
cluster continuous one-to-one for Function of T, T;
end;
theorem :: BORSUK_2:2
for S, T being non empty TopSpace, f being Function of S, T st f is
being_homeomorphism holds f" is open;
begin :: Paths and arcwise connected spaces
theorem :: BORSUK_2:3
for T be non empty TopSpace, a be Point of T ex f be Function of
I[01], T st f is continuous & f.0 = a & f.1 = a;
definition
let T be TopStruct, a,b be Point of T;
pred a,b are_connected means
:: BORSUK_2:def 1
ex f being Function of I[01], T st f is continuous & f.0 = a & f.1 = b;
end;
definition
let T be non empty TopSpace, a,b be Point of T;
redefine pred a,b are_connected;
reflexivity;
end;
definition
let T be TopStruct;
let a, b be Point of T;
assume
a, b are_connected;
mode Path of a, b -> Function of I[01], T means
:: BORSUK_2:def 2
it is continuous & it .0 = a & it.1 = b;
end;
registration
let T be non empty TopSpace;
let a be Point of T;
cluster continuous for Path of a, a;
end;
definition
let T be TopStruct;
attr T is pathwise_connected means
:: BORSUK_2:def 3
for a, b being Point of T holds a, b are_connected;
end;
registration
cluster strict pathwise_connected non empty for TopSpace;
end;
definition
let T be pathwise_connected TopStruct;
let a, b be Point of T;
redefine mode Path of a, b means
:: BORSUK_2:def 4
it is continuous & it.0 = a & it.1 = b;
end;
registration
let T be pathwise_connected TopStruct;
let a, b be Point of T;
cluster -> continuous for Path of a, b;
end;
reserve GY for non empty TopSpace,
r,s for Real;
registration
cluster pathwise_connected -> connected for non empty TopSpace;
end;
begin
definition
let T be non empty TopSpace;
let a, b, c be Point of T;
let P be Path of a, b, Q be Path of b, c such that
a,b are_connected and
b,c are_connected;
func P + Q -> Path of a, c means
:: BORSUK_2:def 5
for t being Point of I[01] holds ( t
<= 1/2 implies it.t = P.(2*t) ) & ( 1/2 <= t implies it.t = Q.(2*t-1) );
end;
registration
let T be non empty TopSpace;
let a be Point of T;
cluster constant for Path of a, a;
end;
::$CT
theorem :: BORSUK_2:5
for T being non empty TopSpace, a being Point of T, P being constant
Path of a, a holds P = I[01] --> a;
theorem :: BORSUK_2:6
for T being non empty TopSpace, a being Point of T, P being
constant Path of a, a holds P + P = P;
registration
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
cluster P + P -> constant;
end;
definition
let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a, b;
assume
a,b are_connected;
func - P -> Path of b, a means
:: BORSUK_2:def 6
for t being Point of I[01] holds it.t = P.(1-t);
end;
theorem :: BORSUK_2:7
for T being non empty TopSpace, a being Point of T, P being
constant Path of a, a holds - P = P;
registration
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
cluster - P -> constant;
end;
begin :: The product of two topological spaces
theorem :: BORSUK_2:8
for X, Y being non empty TopSpace for A being Subset-Family of Y
for f being Function of X, Y holds f"(union A) = union (f"A);
definition
let S1, S2, T1, T2 be non empty TopSpace;
let f be Function of S1, S2, g be Function of T1, T2;
redefine func [:f, g:] -> Function of [:S1, T1:], [:S2, T2:];
end;
theorem :: BORSUK_2:9
for S1, S2, T1, T2 be non empty TopSpace, f be continuous
Function of S1, T1, g be continuous Function of S2, T2, P1, P2 being Subset of
[:T1, T2:] holds (P2 in Base-Appr P1 implies [:f,g:]"P2 is open);
theorem :: BORSUK_2:10
for S1, S2, T1, T2 be non empty TopSpace, f be continuous
Function of S1, T1, g be continuous Function of S2, T2, P2 being Subset of [:T1
, T2:] holds (P2 is open implies [:f,g:]"P2 is open);
registration
let S1, S2, T1, T2 be non empty TopSpace,
f be continuous Function of S1, T1, g be continuous Function of S2, T2;
cluster [:f,g:] -> continuous for Function of [:S1,S2:], [:T1,T2:];
end;
registration
let T1, T2 be T_0 TopSpace;
cluster [:T1, T2:] -> T_0;
end;
registration
let T1, T2 be T_1 TopSpace;
cluster [:T1, T2:] -> T_1;
end;
registration
let T1, T2 be T_2 TopSpace;
cluster [:T1, T2:] -> T_2;
end;
registration
cluster I[01] -> compact T_2;
end;
definition
let T be non empty TopStruct;
let a, b be Point of T;
let P, Q be Path of a, b;
pred P, Q are_homotopic means
:: BORSUK_2:def 7
ex f being Function of [:I[01],I[01]:], T st f
is continuous & for t being Point of I[01] holds f.(t,0) = P.t & f.(t,1) = Q.t
& f.(0,t) = a & f.(1,t) = b;
symmetry;
end;
::$CT
theorem :: BORSUK_2:12
for T being non empty TopSpace, a, b being Point of T, P being
Path of a, b st a,b are_connected holds P, P are_homotopic;
definition
let T be non empty pathwise_connected TopSpace;
let a, b be Point of T;
let P, Q be Path of a, b;
redefine pred P, Q are_homotopic;
reflexivity;
end;
theorem :: BORSUK_2:13
for G being non empty TopSpace, w1,w2,w3 being Point of G, h1,h2 being
Function of I[01],G st h1 is continuous & w1=h1.0 & w2=h1.1 & h2 is continuous
& w2=h2.0 & w3=h2.1 holds ex h3 being Function of I[01],G st h3 is continuous &
w1=h3.0 & w3=h3.1 & rng h3 c= (rng h1) \/ (rng h2);
theorem :: BORSUK_2:14
for T being non empty TopSpace,a,b,c being Point of T, G1 being Path
of a,b, G2 being Path of b,c st G1 is continuous & G2 is continuous & G1.0=a &
G1.1=b & G2.0=b & G2.1=c holds G1+G2 is continuous & (G1+G2).0=a & (G1+G2).1=c;
registration
let T be non empty TopSpace;
cluster non empty compact connected for Subset of T;
end;
:: Moved from BORSUK_5:11, AK, 20.02.2006
theorem :: BORSUK_2:15
for T being non empty TopSpace, a, b being Point of T st (ex f
being Function of I[01], T st f is continuous & f.0 = a & f.1 = b) holds ex g
being Function of I[01], T st g is continuous & g.0 = b & g.1 = a;
registration
cluster I[01] -> pathwise_connected;
end;