![]() |
Metamath
Proof Explorer Theorem List (p. 251 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phtpyi 25001 | Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → ((0𝐻𝐴) = (𝐹‘0) ∧ (1𝐻𝐴) = (𝐹‘1))) | ||
Theorem | phtpy01 25002 | 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 25003* | 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 25004* | 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 25005* | 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 25006* | 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 25007 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺))) | ||
Theorem | phtpycc 25008* | 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 25009* | 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 25010 | 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 25011 | 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 25012 | 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 25013 | Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐹( ≃ph‘𝐽)𝐺 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1))) | ||
Theorem | reparphti 25014* | Lemma for reparpht 25016. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) Avoid ax-mulf 11238. (Revised by GG, 16-Mar-2025.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn II)) & ⊢ (𝜑 → (𝐺‘0) = 0) & ⊢ (𝜑 → (𝐺‘1) = 1) & ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) ⇒ ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹)) | ||
Theorem | reparphtiOLD 25015* | Obsolete version of reparphti 25014 as of 9-Apr-2025. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn II)) & ⊢ (𝜑 → (𝐺‘0) = 0) & ⊢ (𝜑 → (𝐺‘1) = 1) & ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) ⇒ ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹)) | ||
Theorem | reparpht 25016 | 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 25017 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐹)( ≃ph‘𝐾)(𝑃 ∘ 𝐺)) | ||
Syntax | cpco 25018 | Extend class notation with the concatenation operation for paths in a topological space. |
class *𝑝 | ||
Syntax | comi 25019 | Extend class notation with the loop space. |
class Ω1 | ||
Syntax | comn 25020 | Extend class notation with the higher loop spaces. |
class Ω𝑛 | ||
Syntax | cpi1 25021 | Extend class notation with the fundamental group. |
class π1 | ||
Syntax | cpin 25022 | Extend class notation with the higher homotopy groups. |
class πn | ||
Definition | df-pco 25023* | 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 25024* | 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 25025* | 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 25026* | 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 25027* | 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 25028* | 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 25029* | 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 25030 | 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 25031 | 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 25032 | The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) | ||
Theorem | pco1 25033 | The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) | ||
Theorem | pcoval2 25034 | 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 25035 | 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 25036 | 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 25037* | Lemma for pcohtpy 25038. (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 25038 | 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 25039 | 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 25040 | 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 25041 | Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑃 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹) | ||
Theorem | pcoass 25042* | 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 25043* | 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 25044* | Lemma for pcorev 25045. 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 25045* | 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 25046* | Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)}) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃) | ||
Theorem | pcophtb 25047* | 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 25048* | 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 25049* | The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) | ||
Theorem | om1elbas 25050 | 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 25051 | 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 25052 | 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 25053 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂)) | ||
Theorem | om1opn 25054 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝐾 = (TopOpen‘𝑂) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵)) | ||
Theorem | pi1val 25055 | 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 25056 | 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 25057 | Lemma for pi1buni 25058. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐾 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽))) | ||
Theorem | pi1buni 25058 | 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 25059 | The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽))) | ||
Theorem | pi1eluni 25060 | 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 25061 | The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅)) | ||
Theorem | pi1cpbl 25062 | 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 25063* | 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 25064 | 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 25065 | 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 25066 | 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 25067 | Lemma for pi1grp 25068. (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 25068 | 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 25069 | 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 25070* | 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 25071* | 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 25072* | 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 25073* | 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 25074* | 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 25075* | 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 25076* | 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 25077* | 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 25078* | 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 25079* | 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 25080 | Syntax for the class of subcomplex modules. |
class ℂMod | ||
Definition | df-clm 25081* | 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 20559), left modules over such subrings are the same as right modules, see rmodislmod 20906. 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 25082 | 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 25083 | 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 25084 | 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 25085 | A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) | ||
Theorem | clmgrp 25086 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp) | ||
Theorem | clmabl 25087 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel) | ||
Theorem | clmring 25088 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring) | ||
Theorem | clmfgrp 25089 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp) | ||
Theorem | clm0 25090 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹)) | ||
Theorem | clm1 25091 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹)) | ||
Theorem | clmadd 25092 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹)) | ||
Theorem | clmmul 25093 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹)) | ||
Theorem | clmcj 25094 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹)) | ||
Theorem | isclmi 25095 | Reverse direction of isclm 25082. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod) | ||
Theorem | clmzss 25096 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾) | ||
Theorem | clmsscn 25097 | 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 25098 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵)) | ||
Theorem | clmneg 25099 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → -𝐴 = ((invg‘𝐹)‘𝐴)) | ||
Theorem | clmneg1 25100 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → -1 ∈ 𝐾) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |