TOPALG_7: Commutativeness of Fundamental Groups of Topological Groups

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

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 :

registration

let G be multMagma ;

cluster 1_ G -> unital ;

coherence ;

end;

registration

let G be unital multMagma ;

cluster unital for Element of the carrier of G;

existence

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

proof end;

reduce h * g to g;

reducibility

proof end;

end;

registration

let G be Group;

reduce (1_ G) " to 1_ G;

reducibility by GROUP_1:8;

end;

scheme :: TOPALG_7:sch 1
TopFuncEx{ F₁() -> non empty TopSpace, F₂() -> non empty TopSpace, F₃() -> non empty set , F₄( Point of F₁(), Point of F₂()) -> Element of F₃() } :

ex f being Function of [:F₁(),F₂():],F₃() st
for s being Point of F₁()
for t being Point of F₂() holds f . (s,t) = F₄(s,t)

proof end;

scheme :: TOPALG_7:sch 2
TopFuncEq{ F₁() -> non empty TopSpace, F₂() -> non empty TopSpace, F₃() -> non empty set , F₄( Point of F₁(), Point of F₂()) -> Element of F₃() } :

for f, g being Function of [:F₁(),F₂():],F₃() st ( for s being Point of F₁()
for t being Point of F₂() holds f . (s,t) = F₄(s,t) ) & ( for s being Point of F₁()
for t being Point of F₂() holds g . (s,t) = F₄(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 H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines (#) TOPALG_7:def 2 :

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

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 ;

end;

:: deftheorem defines LoopMlt TOPALG_7:def 3 :

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

proof end;

end;

registration

let T be UnContinuous TopGroup;

cluster inverse_op T -> continuous ;

coherence ;

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 ;

end;

:: deftheorem defines inverse_loop TOPALG_7:def 4 :

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

proof end;

end;

definition

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines R^1-TIMES TOPALG_7:def 5 :

registration

cluster R^1-TIMES -> continuous ;

coherence

proof end;

end;

theorem Th6: :: TOPALG_7:6

for x, y being Point of I[01] holds I[01]-TIMES . (x,y) = x * y

proof 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 H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines HomotopyMlt TOPALG_7:def 7 :

Lm2: now :: thesis:

let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis:
let t be unital Point of T; :: thesis:
let x be Point of I[01]; :: thesis:
let f1, f2, g1, g2 be Loop of t; :: thesis:
let F be Homotopy of f1,f2; :: thesis:
let G be Homotopy of g1,g2; :: thesis:
assume A1: ( f1,f2 are_homotopic & g1,g2 are_homotopic ) ; :: thesis:
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:
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:
( 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:
( 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:

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

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 H₁( 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));