:: Commutativeness of Fundamental Groups of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


set I = I[01] ;

set II = [:I[01],I[01]:];

set R = R^1 ;

set RR = [:R^1,R^1:];

set A = R^1 [.0,1.];

set cR = the carrier of R^1;

Lm1: the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:]
by BORSUK_1:def 2;

definition
let A, B be non empty TopSpace;
let C be set ;
let f be Function of [:A,B:],C;
let a be Element of A;
let b be Element of B;
:: original: .
redefine func f . (a,b) -> Element of C;
coherence
f . (a,b) is Element of C
proof end;
end;

definition
let G be multMagma ;
let g be Element of G;
attr g is unital means :Def1: :: TOPALG_7:def 1
g = 1_ G;
end;

:: deftheorem Def1 defines unital TOPALG_7:def 1 :
for G being multMagma
for g being Element of G holds
( g is unital iff g = 1_ G );

registration
let G be multMagma ;
cluster 1_ G -> unital ;
coherence
1_ G is unital
;
end;

registration
let G be unital multMagma ;
cluster unital for Element of the carrier of G;
existence
ex b1 being Element of G st b1 is unital
proof end;
end;

registration
let G be unital multMagma ;
let g be Element of G;
let h be unital Element of G;
reduce g * h to g;
reducibility
g * h = g
proof end;
reduce h * g to g;
reducibility
h * g = g
proof end;
end;

registration
let G be Group;
reduce (1_ G) " to 1_ G;
reducibility
(1_ G) " = 1_ G
by GROUP_1:8;
end;

scheme :: TOPALG_7:sch 1
TopFuncEx{ F1() -> non empty TopSpace, F2() -> non empty TopSpace, F3() -> non empty set , F4( Point of F1(), Point of F2()) -> Element of F3() } :
ex f being Function of [:F1(),F2():],F3() st
for s being Point of F1()
for t being Point of F2() holds f . (s,t) = F4(s,t)
proof end;

scheme :: TOPALG_7:sch 2
TopFuncEq{ F1() -> non empty TopSpace, F2() -> non empty TopSpace, F3() -> non empty set , F4( Point of F1(), Point of F2()) -> Element of F3() } :
for f, g being Function of [:F1(),F2():],F3() st ( for s being Point of F1()
for t being Point of F2() holds f . (s,t) = F4(s,t) ) & ( for s being Point of F1()
for t being Point of F2() holds g . (s,t) = F4(s,t) ) holds
f = g
proof end;

definition
let X be non empty set ;
let T be non empty multMagma ;
let f, g be Function of X,T;
deffunc H1( Element of X) -> Element of the carrier of T = (f . $1) * (g . $1);
func f (#) g -> Function of X,T means :Def2: :: TOPALG_7:def 2
for x being Element of X holds it . x = (f . x) * (g . x);
existence
ex b1 being Function of X,T st
for x being Element of X holds b1 . x = (f . x) * (g . x)
proof end;
uniqueness
for b1, b2 being Function of X,T st ( for x being Element of X holds b1 . x = (f . x) * (g . x) ) & ( for x being Element of X holds b2 . x = (f . x) * (g . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines (#) TOPALG_7:def 2 :
for X being non empty set
for T being non empty multMagma
for f, g, b5 being Function of X,T holds
( b5 = f (#) g iff for x being Element of X holds b5 . x = (f . x) * (g . x) );

theorem :: TOPALG_7:1
for X being non empty set
for T being non empty associative multMagma
for f, g, h being Function of X,T holds (f (#) g) (#) h = f (#) (g (#) h)
proof end;

definition
let X be non empty set ;
let T be non empty commutative multMagma ;
let f, g be Function of X,T;
:: original: (#)
redefine func f (#) g -> Function of X,T;
commutativity
for f, g being Function of X,T holds f (#) g = g (#) f
proof end;
end;

definition
let T be non empty TopGrStr ;
let t be Point of T;
let f, g be Loop of t;
func LoopMlt (f,g) -> Function of I[01],T equals :: TOPALG_7:def 3
f (#) g;
coherence
f (#) g is Function of I[01],T
;
end;

:: deftheorem defines LoopMlt TOPALG_7:def 3 :
for T being non empty TopGrStr
for t being Point of T
for f, g being Loop of t holds LoopMlt (f,g) = f (#) g;

definition
let T be non empty TopSpace-like unital BinContinuous TopGrStr ;
let t be unital Point of T;
let f, g be Loop of t;
:: original: LoopMlt
redefine func LoopMlt (f,g) -> Loop of t;
coherence
LoopMlt (f,g) is Loop of t
proof end;
end;

registration
let T be UnContinuous TopGroup;
cluster inverse_op T -> continuous ;
coherence
inverse_op T is continuous
;
end;

definition
let T be TopGroup;
let t be Point of T;
let f be Loop of t;
func inverse_loop f -> Function of I[01],T equals :: TOPALG_7:def 4
(inverse_op T) * f;
coherence
(inverse_op T) * f is Function of I[01],T
;
end;

:: deftheorem defines inverse_loop TOPALG_7:def 4 :
for T being TopGroup
for t being Point of T
for f being Loop of t holds inverse_loop f = (inverse_op T) * f;

theorem Th2: :: TOPALG_7:2
for x being Point of I[01]
for T being TopGroup
for t being Point of T
for f being Loop of t holds (inverse_loop f) . x = (f . x) "
proof end;

theorem Th3: :: TOPALG_7:3
for x being Point of I[01]
for T being TopGroup
for t being Point of T
for f being Loop of t holds ((inverse_loop f) . x) * (f . x) = 1_ T
proof end;

theorem :: TOPALG_7:4
for x being Point of I[01]
for T being TopGroup
for t being Point of T
for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T
proof end;

definition
let T be UnContinuous TopGroup;
let t be unital Point of T;
let f be Loop of t;
:: original: inverse_loop
redefine func inverse_loop f -> Loop of t;
coherence
inverse_loop f is Loop of t
proof end;
end;

definition
let s, t be Point of I[01];
:: original: *
redefine func s * t -> Point of I[01];
coherence
s * t is Point of I[01]
proof end;
end;

definition
func R^1-TIMES -> Function of [:R^1,R^1:],R^1 means :Def5: :: TOPALG_7:def 5
for x, y being Point of R^1 holds it . (x,y) = x * y;
existence
ex b1 being Function of [:R^1,R^1:],R^1 st
for x, y being Point of R^1 holds b1 . (x,y) = x * y
proof end;
uniqueness
for b1, b2 being Function of [:R^1,R^1:],R^1 st ( for x, y being Point of R^1 holds b1 . (x,y) = x * y ) & ( for x, y being Point of R^1 holds b2 . (x,y) = x * y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines R^1-TIMES TOPALG_7:def 5 :
for b1 being Function of [:R^1,R^1:],R^1 holds
( b1 = R^1-TIMES iff for x, y being Point of R^1 holds b1 . (x,y) = x * y );

registration
cluster R^1-TIMES -> continuous ;
coherence
R^1-TIMES is continuous
proof end;
end;

theorem Th5: :: TOPALG_7:5
[:R^1,R^1:] | [:(R^1 [.0,1.]),(R^1 [.0,1.]):] = [:I[01],I[01]:]
proof end;

definition
func I[01]-TIMES -> Function of [:I[01],I[01]:],I[01] equals :: TOPALG_7:def 6
R^1-TIMES || (R^1 [.0,1.]);
coherence
R^1-TIMES || (R^1 [.0,1.]) is Function of [:I[01],I[01]:],I[01]
proof end;
end;

:: deftheorem defines I[01]-TIMES TOPALG_7:def 6 :
I[01]-TIMES = R^1-TIMES || (R^1 [.0,1.]);

theorem Th6: :: TOPALG_7:6
for x, y being Point of I[01] holds I[01]-TIMES . (x,y) = x * y
proof end;

registration
cluster I[01]-TIMES -> continuous ;
coherence
I[01]-TIMES is continuous
proof end;
end;

theorem Th7: :: TOPALG_7:7
for a, b being Point of I[01]
for N being a_neighborhood of a * b ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st
for x, y being Point of I[01] st x in N1 & y in N2 holds
x * y in N
proof end;

definition
let T be non empty multMagma ;
let F, G be Function of [:I[01],I[01]:],T;
deffunc H1( Point of I[01], Point of I[01]) -> Element of the carrier of T = (F . ($1,$2)) * (G . ($1,$2));
func HomotopyMlt (F,G) -> Function of [:I[01],I[01]:],T means :Def7: :: TOPALG_7:def 7
for a, b being Point of I[01] holds it . (a,b) = (F . (a,b)) * (G . (a,b));
existence
ex b1 being Function of [:I[01],I[01]:],T st
for a, b being Point of I[01] holds b1 . (a,b) = (F . (a,b)) * (G . (a,b))
proof end;
uniqueness
for b1, b2 being Function of [:I[01],I[01]:],T st ( for a, b being Point of I[01] holds b1 . (a,b) = (F . (a,b)) * (G . (a,b)) ) & ( for a, b being Point of I[01] holds b2 . (a,b) = (F . (a,b)) * (G . (a,b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines HomotopyMlt TOPALG_7:def 7 :
for T being non empty multMagma
for F, G, b4 being Function of [:I[01],I[01]:],T holds
( b4 = HomotopyMlt (F,G) iff for a, b being Point of I[01] holds b4 . (a,b) = (F . (a,b)) * (G . (a,b)) );

Lm2: now :: thesis: for T being non empty TopSpace-like unital BinContinuous TopGrStr
for t being unital Point of T
for x being Point of I[01]
for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )
let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis: for t being unital Point of T
for x being Point of I[01]
for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let t be unital Point of T; :: thesis: for x being Point of I[01]
for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let x be Point of I[01]; :: thesis: for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let f1, f2, g1, g2 be Loop of t; :: thesis: for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let F be Homotopy of f1,f2; :: thesis: for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let G be Homotopy of g1,g2; :: thesis: ( f1,f2 are_homotopic & g1,g2 are_homotopic implies ( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t ) )
assume A1: ( f1,f2 are_homotopic & g1,g2 are_homotopic ) ; :: thesis: ( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )
then A2: ( F . (x,0[01]) = f1 . x & G . (x,0[01]) = g1 . x ) by BORSUK_6:def 11;
thus (HomotopyMlt (F,G)) . (x,0) = (F . (x,0[01])) * (G . (x,0[01])) by Def7
.= (LoopMlt (f1,g1)) . x by A2, Def2 ; :: thesis: ( (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )
A3: ( F . (x,1[01]) = f2 . x & G . (x,1[01]) = g2 . x ) by A1, BORSUK_6:def 11;
thus (HomotopyMlt (F,G)) . (x,1) = (F . (x,1[01])) * (G . (x,1[01])) by Def7
.= (LoopMlt (f2,g2)) . x by A3, Def2 ; :: thesis: ( (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )
( F . (0[01],x) = t & G . (0[01],x) = t ) by A1, BORSUK_6:def 11;
hence (HomotopyMlt (F,G)) . (0,x) = t * t by Def7
.= t ;
:: thesis: (HomotopyMlt (F,G)) . (1,x) = t
( F . (1[01],x) = t & G . (1[01],x) = t ) by A1, BORSUK_6:def 11;
hence (HomotopyMlt (F,G)) . (1,x) = t * t by Def7
.= t ;
:: thesis: verum
end;

theorem Th8: :: TOPALG_7:8
for T being non empty TopSpace-like unital BinContinuous TopGrStr
for F, G being Function of [:I[01],I[01]:],T
for M, N being Subset of [:I[01],I[01]:] holds (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)
proof end;

registration
let T be non empty TopSpace-like unital BinContinuous TopGrStr ;
let F, G be continuous Function of [:I[01],I[01]:],T;
cluster HomotopyMlt (F,G) -> continuous ;
coherence
HomotopyMlt (F,G) is continuous
proof end;
end;

theorem Th9: :: TOPALG_7:9
for T being non empty TopSpace-like unital BinContinuous TopGrStr
for t being unital Point of T
for f1, f2, g1, g2 being Loop of t st f1,f2 are_homotopic & g1,g2 are_homotopic holds
LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic
proof end;

theorem :: TOPALG_7:10
for T being non empty TopSpace-like unital BinContinuous TopGrStr
for t being unital Point of T
for f1, f2, g1, g2 being Loop of t
for F being Homotopy of f1,f2
for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds
HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)
proof end;

theorem Th11: :: TOPALG_7:11
for T being non empty TopSpace-like unital BinContinuous TopGrStr
for t being unital Point of T
for f, g being Loop of t
for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))
proof end;

theorem Th12: :: TOPALG_7:12
for T being non empty TopSpace-like unital BinContinuous TopGrStr
for t being unital Point of T
for f, g being Loop of t
for c being constant Loop of t holds LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic
proof end;

definition
let T be TopGroup;
let t be Point of T;
let f, g be Loop of t;
deffunc H1( Point of I[01], Point of I[01]) -> Element of the carrier of T = ((((inverse_loop f) . ($1 * $2)) * (f . $1)) * (g . $1)) * (f . ($1 * $2));
func HopfHomotopy (f,g) -> Function of [:I[01],I[01]:],T means :Def8: :: TOPALG_7:def 8
for a, b being Point of I[01] holds it . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b));
existence
ex b1 being Function of [:I[01],I[01]:],T st
for a, b being Point of I[01] holds b1 . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b))
proof end;
uniqueness
for b1, b2 being Function of [:I[01],I[01]:],T st ( for a, b being Point of I[01] holds b1 . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) ) & ( for a, b being Point of I[01] holds b2 . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines HopfHomotopy TOPALG_7:def 8 :
for T being TopGroup
for t being Point of T
for f, g being Loop of t
for b5 being Function of [:I[01],I[01]:],T holds
( b5 = HopfHomotopy (f,g) iff for a, b being Point of I[01] holds b5 . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) );

registration
let T be TopologicalGroup;
let t be Point of T;
let f, g be Loop of t;
cluster HopfHomotopy (f,g) -> continuous ;
coherence
HopfHomotopy (f,g) is continuous
proof end;
end;

Lm3: now :: thesis: for T being TopologicalGroup
for t being unital Point of T
for f, g being Loop of t
for x being Point of I[01] holds
( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )
let T be TopologicalGroup; :: thesis: for t being unital Point of T
for f, g being Loop of t
for x being Point of I[01] holds
( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let t be unital Point of T; :: thesis: for f, g being Loop of t
for x being Point of I[01] holds
( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let f, g be Loop of t; :: thesis: for x being Point of I[01] holds
( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let x be Point of I[01]; :: thesis: ( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )
set F = HopfHomotopy (f,g);
set i = inverse_loop f;
A1: t = 1_ T by Def1;
A2: t,t are_connected ;
A3: f . 0[01] = t by A2, BORSUK_2:def 2;
A4: f . 1[01] = t by A2, BORSUK_2:def 2;
A5: g . 0[01] = t by A2, BORSUK_2:def 2;
A6: (inverse_loop f) . 0[01] = t by A2, BORSUK_2:def 2;
thus (HopfHomotopy (f,g)) . (x,0) = ((((inverse_loop f) . (x * 0[01])) * (f . x)) * (g . x)) * (f . (x * 0[01])) by Def8
.= (LoopMlt (f,g)) . x by A3, A6, Def2 ; :: thesis: ( (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )
thus (HopfHomotopy (f,g)) . (x,1) = ((((inverse_loop f) . (x * 1[01])) * (f . x)) * (g . x)) * (f . (x * 1[01])) by Def8
.= (t * (g . x)) * (f . x) by A1, Th3
.= (LoopMlt (g,f)) . x by Def2 ; :: thesis: ( (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )
thus (HopfHomotopy (f,g)) . (0,x) = ((((inverse_loop f) . (0[01] * x)) * (f . 0[01])) * (g . 0[01])) * (f . (0[01] * x)) by Def8
.= t by A3, A5, A2, BORSUK_2:def 2 ; :: thesis: (HopfHomotopy (f,g)) . (1,x) = t
thus (HopfHomotopy (f,g)) . (1,x) = ((((inverse_loop f) . (1[01] * x)) * (f . 1[01])) * (g . 1[01])) * (f . (1[01] * x)) by Def8
.= ((((inverse_loop f) . x) * t) * t) * (f . x) by A4, A2, BORSUK_2:def 2
.= t by A1, Th3 ; :: thesis: verum
end;

theorem Th13: :: TOPALG_7:13
for T being TopologicalGroup
for t being unital Point of T
for f, g being Loop of t holds LoopMlt (f,g), LoopMlt (g,f) are_homotopic
proof end;

definition
let T be TopologicalGroup;
let t be unital Point of T;
let f, g be Loop of t;
:: original: HopfHomotopy
redefine func HopfHomotopy (f,g) -> Homotopy of LoopMlt (f,g), LoopMlt (g,f);
coherence
HopfHomotopy (f,g) is Homotopy of LoopMlt (f,g), LoopMlt (g,f)
proof end;
end;

registration
let T be TopologicalGroup;
let t be unital Point of T;
cluster FundamentalGroup (T,t) -> commutative ;
coherence
pi_1 (T,t) is commutative
proof end;
end;