![]() |
Metamath
Proof Explorer Theorem List (p. 246 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phtpy01 24501 | Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ (π β ((πΉβ0) = (πΊβ0) β§ (πΉβ1) = (πΊβ1))) | ||
Theorem | isphtpyd 24502* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (πΉ(II Htpy π½)πΊ)) & β’ ((π β§ π β (0[,]1)) β (0π»π ) = (πΉβ0)) & β’ ((π β§ π β (0[,]1)) β (1π»π ) = (πΉβ1)) β β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) | ||
Theorem | isphtpy2d 24503* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β ((II Γt II) Cn π½)) & β’ ((π β§ π β (0[,]1)) β (π π»0) = (πΉβπ )) & β’ ((π β§ π β (0[,]1)) β (π π»1) = (πΊβπ )) & β’ ((π β§ π β (0[,]1)) β (0π»π ) = (πΉβ0)) & β’ ((π β§ π β (0[,]1)) β (1π»π ) = (πΉβ1)) β β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) | ||
Theorem | phtpycom 24504* | Given a homotopy from πΉ to πΊ, produce a homotopy from πΊ to πΉ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (π₯π»(1 β π¦))) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ (π β πΎ β (πΊ(PHtpyβπ½)πΉ)) | ||
Theorem | phtpyid 24505* | A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ πΊ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (πΉβπ₯)) & β’ (π β πΉ β (II Cn π½)) β β’ (π β πΊ β (πΉ(PHtpyβπ½)πΉ)) | ||
Theorem | phtpyco2 24506 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β (π½ Cn πΎ)) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ (π β (π β π») β ((π β πΉ)(PHtpyβπΎ)(π β πΊ))) | ||
Theorem | phtpycc 24507* | Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
β’ π = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π¦ β€ (1 / 2), (π₯πΎ(2 Β· π¦)), (π₯πΏ((2 Β· π¦) β 1)))) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (II Cn π½)) & β’ (π β πΎ β (πΉ(PHtpyβπ½)πΊ)) & β’ (π β πΏ β (πΊ(PHtpyβπ½)π»)) β β’ (π β π β (πΉ(PHtpyβπ½)π»)) | ||
Definition | df-phtpc 24508* | Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
β’ βph = (π₯ β Top β¦ {β¨π, πβ© β£ ({π, π} β (II Cn π₯) β§ (π(PHtpyβπ₯)π) β β )}) | ||
Theorem | phtpcrel 24509 | The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.) |
β’ Rel ( βphβπ½) | ||
Theorem | isphtpc 24510 | The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (πΉ( βphβπ½)πΊ β (πΉ β (II Cn π½) β§ πΊ β (II Cn π½) β§ (πΉ(PHtpyβπ½)πΊ) β β )) | ||
Theorem | phtpcer 24511 | Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof shortened by AV, 1-May-2021.) |
β’ ( βphβπ½) Er (II Cn π½) | ||
Theorem | phtpc01 24512 | Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (πΉ( βphβπ½)πΊ β ((πΉβ0) = (πΊβ0) β§ (πΉβ1) = (πΊβ1))) | ||
Theorem | reparphti 24513* | Lemma for reparpht 24514. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn II)) & β’ (π β (πΊβ0) = 0) & β’ (π β (πΊβ1) = 1) & β’ π» = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (πΉβ(((1 β π¦) Β· (πΊβπ₯)) + (π¦ Β· π₯)))) β β’ (π β π» β ((πΉ β πΊ)(PHtpyβπ½)πΉ)) | ||
Theorem | reparpht 24514 | Reparametrization lemma. The reparametrization of a path by any continuous map πΊ:IIβΆII with πΊ(0) = 0 and πΊ(1) = 1 is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn II)) & β’ (π β (πΊβ0) = 0) & β’ (π β (πΊβ1) = 1) β β’ (π β (πΉ β πΊ)( βphβπ½)πΉ) | ||
Theorem | phtpcco2 24515 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ (π β πΉ( βphβπ½)πΊ) & β’ (π β π β (π½ Cn πΎ)) β β’ (π β (π β πΉ)( βphβπΎ)(π β πΊ)) | ||
Syntax | cpco 24516 | Extend class notation with the concatenation operation for paths in a topological space. |
class *π | ||
Syntax | comi 24517 | Extend class notation with the loop space. |
class Ξ©1 | ||
Syntax | comn 24518 | Extend class notation with the higher loop spaces. |
class Ξ©π | ||
Syntax | cpi1 24519 | Extend class notation with the fundamental group. |
class Ο1 | ||
Syntax | cpin 24520 | Extend class notation with the higher homotopy groups. |
class Οn | ||
Definition | df-pco 24521* | Define the concatenation of two paths in a topological space π½. For simplicity of definition, we define it on all paths, not just those whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ *π = (π β Top β¦ (π β (II Cn π), π β (II Cn π) β¦ (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), (πβ(2 Β· π₯)), (πβ((2 Β· π₯) β 1)))))) | ||
Definition | df-om1 24522* | Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ Ξ©1 = (π β Top, π¦ β βͺ π β¦ {β¨(Baseβndx), {π β (II Cn π) β£ ((πβ0) = π¦ β§ (πβ1) = π¦)}β©, β¨(+gβndx), (*πβπ)β©, β¨(TopSetβndx), (π βko II)β©}) | ||
Definition | df-omn 24523* | Define the n-th iterated loop space of a topological space. Unlike Ξ©1 this is actually a pointed topological space, which is to say a tuple of a topological space (a member of TopSp, not Top) and a point in the space. Higher loop spaces select the constant loop at the point from the lower loop space for the distinguished point. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ Ξ©π = (π β Top, π¦ β βͺ π β¦ seq0(((π₯ β V, π β V β¦ β¨((TopOpenβ(1st βπ₯)) Ξ©1 (2nd βπ₯)), ((0[,]1) Γ {(2nd βπ₯)})β©) β 1st ), β¨{β¨(Baseβndx), βͺ πβ©, β¨(TopSetβndx), πβ©}, π¦β©)) | ||
Definition | df-pi1 24524* | Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ Ο1 = (π β Top, π¦ β βͺ π β¦ ((π Ξ©1 π¦) /s ( βphβπ))) | ||
Definition | df-pin 24525* | Define the n-th homotopy group, which is formed by taking the π-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the π-th loop space, which is the π β 1-th loop space. For π = 0, since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0-th homotopy group is the set of path components of π. (Since the 0-th loop space does not have a group operation, neither does the 0-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ Οn = (π β Top, π β βͺ π β¦ (π β β0 β¦ ((1st β((π Ξ©π π)βπ)) /s if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, ( βphβ(TopOpenβ(1st β((π Ξ©π π)β(π β 1))))))))) | ||
Theorem | pcofval 24526* | The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof shortened by AV, 2-Mar-2024.) |
β’ (*πβπ½) = (π β (II Cn π½), π β (II Cn π½) β¦ (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), (πβ(2 Β· π₯)), (πβ((2 Β· π₯) β 1))))) | ||
Theorem | pcoval 24527* | The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β (πΉ(*πβπ½)πΊ) = (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), (πΉβ(2 Β· π₯)), (πΊβ((2 Β· π₯) β 1))))) | ||
Theorem | pcovalg 24528 | Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ ((π β§ π β (0[,]1)) β ((πΉ(*πβπ½)πΊ)βπ) = if(π β€ (1 / 2), (πΉβ(2 Β· π)), (πΊβ((2 Β· π) β 1)))) | ||
Theorem | pcoval1 24529 | Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ ((π β§ π β (0[,](1 / 2))) β ((πΉ(*πβπ½)πΊ)βπ) = (πΉβ(2 Β· π))) | ||
Theorem | pco0 24530 | The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β ((πΉ(*πβπ½)πΊ)β0) = (πΉβ0)) | ||
Theorem | pco1 24531 | The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β ((πΉ(*πβπ½)πΊ)β1) = (πΊβ1)) | ||
Theorem | pcoval2 24532 | Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) β β’ ((π β§ π β ((1 / 2)[,]1)) β ((πΉ(*πβπ½)πΊ)βπ) = (πΊβ((2 Β· π) β 1))) | ||
Theorem | pcocn 24533 | The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) β β’ (π β (πΉ(*πβπ½)πΊ) β (II Cn π½)) | ||
Theorem | copco 24534 | The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β π» β (π½ Cn πΎ)) β β’ (π β (π» β (πΉ(*πβπ½)πΊ)) = ((π» β πΉ)(*πβπΎ)(π» β πΊ))) | ||
Theorem | pcohtpylem 24535* | Lemma for pcohtpy 24536. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.) |
β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β πΉ( βphβπ½)π») & β’ (π β πΊ( βphβπ½)πΎ) & β’ π = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦))) & β’ (π β π β (πΉ(PHtpyβπ½)π»)) & β’ (π β π β (πΊ(PHtpyβπ½)πΎ)) β β’ (π β π β ((πΉ(*πβπ½)πΊ)(PHtpyβπ½)(π»(*πβπ½)πΎ))) | ||
Theorem | pcohtpy 24536 | Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.) |
β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β πΉ( βphβπ½)π») & β’ (π β πΊ( βphβπ½)πΎ) β β’ (π β (πΉ(*πβπ½)πΊ)( βphβπ½)(π»(*πβπ½)πΎ)) | ||
Theorem | pcoptcl 24537 | A constant function is a path from π to itself. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 19-Mar-2015.) |
β’ π = ((0[,]1) Γ {π}) β β’ ((π½ β (TopOnβπ) β§ π β π) β (π β (II Cn π½) β§ (πβ0) = π β§ (πβ1) = π)) | ||
Theorem | pcopt 24538 | Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
β’ π = ((0[,]1) Γ {π}) β β’ ((πΉ β (II Cn π½) β§ (πΉβ0) = π) β (π(*πβπ½)πΉ)( βphβπ½)πΉ) | ||
Theorem | pcopt2 24539 | Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = ((0[,]1) Γ {π}) β β’ ((πΉ β (II Cn π½) β§ (πΉβ1) = π) β (πΉ(*πβπ½)π)( βphβπ½)πΉ) | ||
Theorem | pcoass 24540* | Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β (πΊβ1) = (π»β0)) & β’ π = (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), if(π₯ β€ (1 / 4), (2 Β· π₯), (π₯ + (1 / 4))), ((π₯ / 2) + (1 / 2)))) β β’ (π β ((πΉ(*πβπ½)πΊ)(*πβπ½)π»)( βphβπ½)(πΉ(*πβπ½)(πΊ(*πβπ½)π»))) | ||
Theorem | pcorevcl 24541* | Closure for a reversed path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (πΉ β (II Cn π½) β (πΊ β (II Cn π½) β§ (πΊβ0) = (πΉβ1) β§ (πΊβ1) = (πΉβ0))) | ||
Theorem | pcorevlem 24542* | Lemma for pcorev 24543. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ1)}) & β’ π» = (π β (0[,]1), π‘ β (0[,]1) β¦ (πΉβif(π β€ (1 / 2), (1 β ((1 β π‘) Β· (2 Β· π ))), (1 β ((1 β π‘) Β· (1 β ((2 Β· π ) β 1))))))) β β’ (πΉ β (II Cn π½) β (π» β ((πΊ(*πβπ½)πΉ)(PHtpyβπ½)π) β§ (πΊ(*πβπ½)πΉ)( βphβπ½)π)) | ||
Theorem | pcorev 24543* | Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ1)}) β β’ (πΉ β (II Cn π½) β (πΊ(*πβπ½)πΉ)( βphβπ½)π) | ||
Theorem | pcorev2 24544* | Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ0)}) β β’ (πΉ β (II Cn π½) β (πΉ(*πβπ½)πΊ)( βphβπ½)π) | ||
Theorem | pcophtb 24545* | The path homotopy equivalence relation on two paths πΉ, πΊ with the same start and end point can be written in terms of the loop πΉ β πΊ formed by concatenating πΉ with the inverse of πΊ. Thus, all the homotopy information in βphβπ½ is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π» = (π₯ β (0[,]1) β¦ (πΊβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ0)}) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ0) = (πΊβ0)) & β’ (π β (πΉβ1) = (πΊβ1)) β β’ (π β ((πΉ(*πβπ½)π»)( βphβπ½)π β πΉ( βphβπ½)πΊ)) | ||
Theorem | om1val 24546* | The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = {π β (II Cn π½) β£ ((πβ0) = π β§ (πβ1) = π)}) & β’ (π β + = (*πβπ½)) & β’ (π β πΎ = (π½ βko II)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(TopSetβndx), πΎβ©}) | ||
Theorem | om1bas 24547* | The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) β β’ (π β π΅ = {π β (II Cn π½) β£ ((πβ0) = π β§ (πβ1) = π)}) | ||
Theorem | om1elbas 24548 | Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) β β’ (π β (πΉ β π΅ β (πΉ β (II Cn π½) β§ (πΉβ0) = π β§ (πΉβ1) = π))) | ||
Theorem | om1addcl 24549 | Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) & β’ (π β π» β π΅) & β’ (π β πΎ β π΅) β β’ (π β (π»(*πβπ½)πΎ) β π΅) | ||
Theorem | om1plusg 24550 | The group operation (which isn't much more than a magma) of the loop space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (*πβπ½) = (+gβπ)) | ||
Theorem | om1tset 24551 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π½ βko II) = (TopSetβπ)) | ||
Theorem | om1opn 24552 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ πΎ = (TopOpenβπ) & β’ (π β π΅ = (Baseβπ)) β β’ (π β πΎ = ((π½ βko II) βΎt π΅)) | ||
Theorem | pi1val 24553 | The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) β β’ (π β πΊ = (π /s ( βphβπ½))) | ||
Theorem | pi1bas 24554 | The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΎ = (Baseβπ)) β β’ (π β π΅ = (πΎ / ( βphβπ½))) | ||
Theorem | pi1blem 24555 | Lemma for pi1buni 24556. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΎ = (Baseβπ)) β β’ (π β ((( βphβπ½) β πΎ) β πΎ β§ πΎ β (II Cn π½))) | ||
Theorem | pi1buni 24556 | Another way to write the loop space base in terms of the base of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΎ = (Baseβπ)) β β’ (π β βͺ π΅ = πΎ) | ||
Theorem | pi1bas2 24557 | The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) β β’ (π β π΅ = (βͺ π΅ / ( βphβπ½))) | ||
Theorem | pi1eluni 24558 | Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) β β’ (π β (πΉ β βͺ π΅ β (πΉ β (II Cn π½) β§ (πΉβ0) = π β§ (πΉβ1) = π))) | ||
Theorem | pi1bas3 24559 | The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) & β’ π = (( βphβπ½) β© (βͺ π΅ Γ βͺ π΅)) β β’ (π β π΅ = (βͺ π΅ / π )) | ||
Theorem | pi1cpbl 24560 | The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) & β’ π = (( βphβπ½) β© (βͺ π΅ Γ βͺ π΅)) & β’ π = (π½ Ξ©1 π) & β’ + = (+gβπ) β β’ (π β ((ππ π β§ ππ π) β (π + π)π (π + π))) | ||
Theorem | elpi1 24561* | The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (πΉ β π΅ β βπ β (II Cn π½)(((πβ0) = π β§ (πβ1) = π) β§ πΉ = [π]( βphβπ½)))) | ||
Theorem | elpi1i 24562 | The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β πΉ β (II Cn π½)) & β’ (π β (πΉβ0) = π) & β’ (π β (πΉβ1) = π) β β’ (π β [πΉ]( βphβπ½) β π΅) | ||
Theorem | pi1addf 24563 | The group operation of Ο1 is a binary operation. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ + = (+gβπΊ) β β’ (π β + :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | pi1addval 24564 | The concatenation of two path-homotopy classes in the fundamental group. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ + = (+gβπΊ) & β’ (π β π β βͺ π΅) & β’ (π β π β βͺ π΅) β β’ (π β ([π]( βphβπ½) + [π]( βphβπ½)) = [(π(*πβπ½)π)]( βphβπ½)) | ||
Theorem | pi1grplem 24565 | Lemma for pi1grp 24566. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ 0 = ((0[,]1) Γ {π}) β β’ (π β (πΊ β Grp β§ [ 0 ]( βphβπ½) = (0gβπΊ))) | ||
Theorem | pi1grp 24566 | The fundamental group is a group. Proposition 1.3 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) β β’ ((π½ β (TopOnβπ) β§ π β π) β πΊ β Grp) | ||
Theorem | pi1id 24567 | The identity element of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ 0 = ((0[,]1) Γ {π}) β β’ ((π½ β (TopOnβπ) β§ π β π) β [ 0 ]( βphβπ½) = (0gβπΊ)) | ||
Theorem | pi1inv 24568* | An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π = (invgβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β πΉ β (II Cn π½)) & β’ (π β (πΉβ0) = π) & β’ (π β (πΉβ1) = π) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β (πβ[πΉ]( βphβπ½)) = [πΌ]( βphβπ½)) | ||
Theorem | pi1xfrf 24569* | Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΌ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΌβ0)) & β’ (π β (πΌβ1) = (πΉβ0)) β β’ (π β πΊ:π΅βΆ(Baseβπ)) | ||
Theorem | pi1xfrval 24570* | The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΌ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΌβ0)) & β’ (π β (πΌβ1) = (πΉβ0)) & β’ (π β π΄ β βͺ π΅) β β’ (π β (πΊβ[π΄]( βphβπ½)) = [(πΌ(*πβπ½)(π΄(*πβπ½)πΉ))]( βphβπ½)) | ||
Theorem | pi1xfr 24571* | Given a path πΉ and its inverse πΌ between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β πΊ β (π GrpHom π)) | ||
Theorem | pi1xfrcnvlem 24572* | Given a path πΉ between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π» = ran (β β βͺ (Baseβπ) β¦ β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β β’ (π β β‘πΊ β π») | ||
Theorem | pi1xfrcnv 24573* | Given a path πΉ between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π» = ran (β β βͺ (Baseβπ) β¦ β¨[β]( βphβπ½), [(πΉ(*πβπ½)(β(*πβπ½)πΌ))]( βphβπ½)β©) β β’ (π β (β‘πΊ = π» β§ β‘πΊ β (π GrpHom π))) | ||
Theorem | pi1xfrgim 24574* | The mapping πΊ between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = (π½ Ο1 (πΉβ0)) & β’ π = (π½ Ο1 (πΉβ1)) & β’ π΅ = (Baseβπ) & β’ πΊ = ran (π β βͺ π΅ β¦ β¨[π]( βphβπ½), [(πΌ(*πβπ½)(π(*πβπ½)πΉ))]( βphβπ½)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (II Cn π½)) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β πΊ β (π GrpIso π)) | ||
Theorem | pi1cof 24575* | Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 π΄) & β’ π = (πΎ Ο1 π΅) & β’ π = (Baseβπ) & β’ πΊ = ran (π β βͺ π β¦ β¨[π]( βphβπ½), [(πΉ β π)]( βphβπΎ)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) = π΅) β β’ (π β πΊ:πβΆ(Baseβπ)) | ||
Theorem | pi1coval 24576* | The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 π΄) & β’ π = (πΎ Ο1 π΅) & β’ π = (Baseβπ) & β’ πΊ = ran (π β βͺ π β¦ β¨[π]( βphβπ½), [(πΉ β π)]( βphβπΎ)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) = π΅) β β’ ((π β§ π β βͺ π) β (πΊβ[π]( βphβπ½)) = [(πΉ β π)]( βphβπΎ)) | ||
Theorem | pi1coghm 24577* | The mapping πΊ between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015.) (Revised by Mario Carneiro, 23-Dec-2016.) |
β’ π = (π½ Ο1 π΄) & β’ π = (πΎ Ο1 π΅) & β’ π = (Baseβπ) & β’ πΊ = ran (π β βͺ π β¦ β¨[π]( βphβπ½), [(πΉ β π)]( βphβπΎ)β©) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) = π΅) β β’ (π β πΊ β (π GrpHom π)) | ||
Syntax | cclm 24578 | Syntax for the class of subcomplex modules. |
class βMod | ||
Definition | df-clm 24579* | Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers βfld, which allows to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng 20323), left modules over such subrings are the same as right modules, see rmodislmod 20540. Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ βMod = {π€ β LMod β£ [(Scalarβπ€) / π][(Baseβπ) / π](π = (βfld βΎs π) β§ π β (SubRingββfld))} | ||
Theorem | isclm 24580 | A subcomplex module is a left module over a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β (π β LMod β§ πΉ = (βfld βΎs πΎ) β§ πΎ β (SubRingββfld))) | ||
Theorem | clmsca 24581 | The ring of scalars πΉ of a subcomplex module is the restriction of the field of complex numbers to the base set of πΉ. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β πΉ = (βfld βΎs πΎ)) | ||
Theorem | clmsubrg 24582 | The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β πΎ β (SubRingββfld)) | ||
Theorem | clmlmod 24583 | A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βMod β π β LMod) | ||
Theorem | clmgrp 24584 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βMod β π β Grp) | ||
Theorem | clmabl 24585 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βMod β π β Abel) | ||
Theorem | clmring 24586 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β πΉ β Ring) | ||
Theorem | clmfgrp 24587 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β πΉ β Grp) | ||
Theorem | clm0 24588 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β 0 = (0gβπΉ)) | ||
Theorem | clm1 24589 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β 1 = (1rβπΉ)) | ||
Theorem | clmadd 24590 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β + = (+gβπΉ)) | ||
Theorem | clmmul 24591 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β Β· = (.rβπΉ)) | ||
Theorem | clmcj 24592 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β βMod β β = (*πβπΉ)) | ||
Theorem | isclmi 24593 | Reverse direction of isclm 24580. (Contributed by Mario Carneiro, 30-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ ((π β LMod β§ πΉ = (βfld βΎs πΎ) β§ πΎ β (SubRingββfld)) β π β βMod) | ||
Theorem | clmzss 24594 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β β€ β πΎ) | ||
Theorem | clmsscn 24595 | The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β πΎ β β) | ||
Theorem | clmsub 24596 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π΄ β πΎ β§ π΅ β πΎ) β (π΄ β π΅) = (π΄(-gβπΉ)π΅)) | ||
Theorem | clmneg 24597 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π΄ β πΎ) β -π΄ = ((invgβπΉ)βπ΄)) | ||
Theorem | clmneg1 24598 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βMod β -1 β πΎ) | ||
Theorem | clmabs 24599 | Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π΄ β πΎ) β (absβπ΄) = ((normβπΉ)βπ΄)) | ||
Theorem | clmacl 24600 | Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βMod β§ π β πΎ β§ π β πΎ) β (π + π) β πΎ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |