feat(topology/homotopy/basic): add homotopic for continuous_maps. (…

…#9865)

src/topology/homotopy/basic.lean

@@ -20,7 +20,7 @@ formalisation in HOL-Analysis, we define `homotopy_with f₀ f₁ P`, for homoto
 
 ## Definitions
 
-* `homotopy f₀ f₁ P` is the type of homotopies between `f₀` and `f₁`.
+* `homotopy f₀ f₁` is the type of homotopies between `f₀` and `f₁`.
 * `homotopy_with f₀ f₁ P` is the type of homotopies between `f₀` and `f₁`, where the intermediate
   maps satisfy the predicate `P`.
 * `homotopy_rel f₀ f₁ S` is the type of homotopies between `f₀` and `f₁` which are fixed on `S`.
@@ -33,16 +33,26 @@ For each of the above, we have
 * `trans F G`, which concatenates the homotopies `F` and `G`. For example, if `F : homotopy f₀ f₁`
   and `G : homotopy f₁ f₂`, then `F.trans G : homotopy f₀ f₂`.
 
+We also define the relations
+
+* `homotopic f₀ f₁` is defined to be `nonempty (homotopy f₀ f₁)`
+* `homotopic_with f₀ f₁ P` is defined to be `nonempty (homotopy_with f₀ f₁ P)`
+* `homotopic_rel f₀ f₁ P` is defined to be `nonempty (homotopy_rel f₀ f₁ P)`
+
+and for `homotopic` and `homotopic_rel`, we also define the `setoid` and `quotient` in `C(X, Y)` by
+these relations.
+
 ## References
 
 - [HOL-Analysis formalisation](https://isabelle.in.tum.de/library/HOL/HOL-Analysis/Homotopy.html)
 -/
 
 noncomputable theory
 
-universes u v
+universes u v w
 
-variables {X : Type u} {Y : Type v} [topological_space X] [topological_space Y]
+variables {X : Type u} {Y : Type v} {Z : Type w}
+variables [topological_space X] [topological_space Y] [topological_space Z]
 
 open_locale unit_interval
 
@@ -141,7 +151,6 @@ Given a continuous function `f`, we can define a `homotopy f f` by `F (t, x) = f
 @[simps]
 def refl (f : C(X, Y)) : homotopy f f :=
 { to_fun := λ x, f x.2,
-  continuous_to_fun := by continuity,
   to_fun_zero := λ _, rfl,
   to_fun_one := λ _, rfl }
 
@@ -154,7 +163,6 @@ Given a `homotopy f₀ f₁`, we can define a `homotopy f₁ f₀` by reversing
 @[simps]
 def symm {f₀ f₁ : C(X, Y)} (F : homotopy f₀ f₁) : homotopy f₁ f₀ :=
 { to_fun := λ x, F (σ x.1, x.2),
-  continuous_to_fun := by continuity,
   to_fun_zero := by norm_num,
   to_fun_one := by norm_num }
 
@@ -219,12 +227,49 @@ Casting a `homotopy f₀ f₁` to a `homotopy g₀ g₁` where `f₀ = g₀` and
 def cast {f₀ f₁ g₀ g₁ : C(X, Y)} (F : homotopy f₀ f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
   homotopy g₀ g₁ :=
 { to_fun := F,
-  continuous_to_fun := by continuity,
   to_fun_zero := by simp [←h₀],
   to_fun_one := by simp [←h₁] }
 
+/--
+If we have a `homotopy f₀ f₁` and a `homotopy g₀ g₁`, then we can compose them and get a
+`homotopy (g₀.comp f₀) (g₁.comp f₁)`.
+-/
+@[simps]
+def hcomp {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (F : homotopy f₀ f₁) (G : homotopy g₀ g₁) :
+  homotopy (g₀.comp f₀) (g₁.comp f₁) :=
+{ to_fun := λ x, G (x.1, F x),
+  to_fun_zero := by simp,
+  to_fun_one := by simp }
+
 end homotopy
 
+/--
+Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic if there exists a
+`homotopy f₀ f₁`.
+-/
+def homotopic (f₀ f₁ : C(X, Y)) : Prop :=
+nonempty (homotopy f₀ f₁)
+
+namespace homotopic
+
+@[refl]
+lemma refl (f : C(X, Y)) : homotopic f f := ⟨homotopy.refl f⟩
+
+@[symm]
+lemma symm ⦃f g : C(X, Y)⦄ (h : homotopic f g) : homotopic g f := ⟨h.some.symm⟩
+
+@[trans]
+lemma trans ⦃f g h : C(X, Y)⦄ (h₀ : homotopic f g) (h₁ : homotopic g h) : homotopic f h :=
+⟨h₀.some.trans h₁.some⟩
+
+lemma hcomp {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (h₀ : homotopic f₀ f₁) (h₁ : homotopic g₀ g₁) :
+  homotopic (g₀.comp f₀) (g₁.comp f₁) :=
+⟨h₀.some.hcomp h₁.some⟩
+
+lemma equivalence : equivalence (@homotopic X Y _ _) := ⟨refl, symm, trans⟩
+
+end homotopic
+
 /--
 The type of homotopies between `f₀ f₁ : C(X, Y)`, where the intermediate maps satisfy the predicate
 `P : C(X, Y) → Prop`
@@ -358,6 +403,31 @@ def cast {f₀ f₁ g₀ g₁ : C(X, Y)} (F : homotopy_with f₀ f₁ P) (h₀ :
 
 end homotopy_with
 
+/--
+Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic with respect to the
+predicate `P` if there exists a `homotopy_with f₀ f₁ P`.
+-/
+def homotopic_with (f₀ f₁ : C(X, Y)) (P : C(X, Y) → Prop) : Prop :=
+nonempty (homotopy_with f₀ f₁ P)
+
+namespace homotopic_with
+
+variable {P : C(X, Y) → Prop}
+
+@[refl]
+lemma refl (f : C(X, Y)) (hf : P f) : homotopic_with f f P :=
+⟨homotopy_with.refl f hf⟩
+
+@[symm]
+lemma symm ⦃f g : C(X, Y)⦄ (h : homotopic_with f g P) : homotopic_with g f P := ⟨h.some.symm⟩
+
+@[trans]
+lemma trans ⦃f g h : C(X, Y)⦄ (h₀ : homotopic_with f g P) (h₁ : homotopic_with g h P) :
+  homotopic_with f h P :=
+⟨h₀.some.trans h₁.some⟩
+
+end homotopic_with
+
 /--
 A `homotopy_rel f₀ f₁ S` is a homotopy between `f₀` and `f₁` which is fixed on the points in `S`.
 -/
@@ -442,4 +512,31 @@ def cast {f₀ f₁ g₀ g₁ : C(X, Y)} (F : homotopy_rel f₀ f₁ S) (h₀ :
 
 end homotopy_rel
 
+/--
+Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic relative to a set `S` if
+there exists a `homotopy_rel f₀ f₁ S`.
+-/
+def homotopic_rel (f₀ f₁ : C(X, Y)) (S : set X) : Prop :=
+nonempty (homotopy_rel f₀ f₁ S)
+
+namespace homotopic_rel
+
+variable {S : set X}
+
+@[refl]
+lemma refl (f : C(X, Y)) : homotopic_rel f f S := ⟨homotopy_rel.refl f S⟩
+
+@[symm]
+lemma symm ⦃f g : C(X, Y)⦄ (h : homotopic_rel f g S) : homotopic_rel g f S := ⟨h.some.symm⟩
+
+@[trans]
+lemma trans ⦃f g h : C(X, Y)⦄ (h₀ : homotopic_rel f g S) (h₁ : homotopic_rel g h S) :
+  homotopic_rel f h S :=
+⟨h₀.some.trans h₁.some⟩
+
+lemma equivalence : equivalence (λ f g : C(X, Y), homotopic_rel f g S) :=
+⟨refl, symm, trans⟩
+
+end homotopic_rel
+
 end continuous_map

src/topology/homotopy/path.lean

@@ -28,9 +28,6 @@ In this file, we define a `homotopy` between two `path`s. In addition, we define
 * `path.homotopic.setoid x₀ x₁` is the setoid on `path`s from `path.homotopic`
 * `path.homotopic.quotient x₀ x₁` is the quotient type from `path x₀ x₀` by `path.homotopic.setoid`
 
-## Todos
-
-Define the fundamental group(oid).
 -/
 
 universes u v