Documentation

Mathlib.Topology.Homotopy.Product

Product of homotopies #

In this file, we introduce definitions for the product of homotopies. We show that the products of relative homotopies are still relative homotopies. Finally, we specialize to the case of path homotopies, and provide the definition for the product of path classes. We show various lemmas associated with these products, such as the fact that path products commute with path composition, and that projection is the inverse of products.

Definitions #

General homotopies #

Path products #

@[simp]
theorem ContinuousMap.HomotopyRel.pi_apply {I : Type u_1} {A : Type u_2} {X : IType u_3} [(i : I) → TopologicalSpace (X i)] [TopologicalSpace A] {f : (i : I) → C(A, X i)} {g : (i : I) → C(A, X i)} {S : Set A} (homotopies : (i : I) → (f i).HomotopyRel (g i) S) (a : unitInterval × A) (i : I) :
(ContinuousMap.HomotopyRel.pi homotopies) a i = (homotopies i) a
@[simp]
theorem ContinuousMap.HomotopyRel.pi_toFun {I : Type u_1} {A : Type u_2} {X : IType u_3} [(i : I) → TopologicalSpace (X i)] [TopologicalSpace A] {f : (i : I) → C(A, X i)} {g : (i : I) → C(A, X i)} {S : Set A} (homotopies : (i : I) → (f i).HomotopyRel (g i) S) (a : unitInterval × A) (i : I) :
(ContinuousMap.HomotopyRel.pi homotopies) a i = (homotopies i) a
def ContinuousMap.HomotopyRel.pi {I : Type u_1} {A : Type u_2} {X : IType u_3} [(i : I) → TopologicalSpace (X i)] [TopologicalSpace A] {f : (i : I) → C(A, X i)} {g : (i : I) → C(A, X i)} {S : Set A} (homotopies : (i : I) → (f i).HomotopyRel (g i) S) :
(ContinuousMap.pi f).HomotopyRel (ContinuousMap.pi g) S

The relative product homotopy of homotopies between functions f and g

Equations
Instances For
    @[simp]
    theorem ContinuousMap.Homotopy.prod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Type u_3} [TopologicalSpace A] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) (t : unitInterval × A) :
    (F.prod G) t = (F t, G t)
    def ContinuousMap.Homotopy.prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Type u_3} [TopologicalSpace A] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) :
    (f₀.prodMk g₀).Homotopy (f₁.prodMk g₁)

    The product of homotopies F and G, where F takes f₀ to f₁ and G takes g₀ to g₁

    Equations
    • F.prod G = { toFun := fun (t : unitInterval × A) => (F t, G t), continuous_toFun := , map_zero_left := , map_one_left := }
    Instances For
      @[simp]
      theorem ContinuousMap.HomotopyRel.prod_toFun {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Type u_3} [TopologicalSpace A] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} {S : Set A} (F : f₀.HomotopyRel f₁ S) (G : g₀.HomotopyRel g₁ S) (t : unitInterval × A) :
      (F.prod G) t = (F t, G t)
      @[simp]
      theorem ContinuousMap.HomotopyRel.prod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Type u_3} [TopologicalSpace A] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} {S : Set A} (F : f₀.HomotopyRel f₁ S) (G : g₀.HomotopyRel g₁ S) (t : unitInterval × A) :
      (F.prod G) t = (F t, G t)
      def ContinuousMap.HomotopyRel.prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Type u_3} [TopologicalSpace A] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} {S : Set A} (F : f₀.HomotopyRel f₁ S) (G : g₀.HomotopyRel g₁ S) :
      (f₀.prodMk g₀).HomotopyRel (f₁.prodMk g₁) S

      The relative product of homotopies F and G, where F takes f₀ to f₁ and G takes g₀ to g₁

      Equations
      • F.prod G = { toHomotopy := F.prod G.toHomotopy, prop' := }
      Instances For
        def Path.Homotopic.piHomotopy {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (as i) (bs i)) (H : (i : ι) → (γ₀ i).Homotopy (γ₁ i)) :
        (Path.pi γ₀).Homotopy (Path.pi γ₁)

        The product of a family of path homotopies. This is just a specialization of HomotopyRel.

        Equations
        Instances For
          def Path.Homotopic.pi {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (γ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) :

          The product of a family of path homotopy classes.

          Equations
          Instances For
            theorem Path.Homotopic.pi_lift {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (γ : (i : ι) → Path (as i) (bs i)) :
            (Path.Homotopic.pi fun (i : ι) => γ i) = Path.pi γ
            theorem Path.Homotopic.comp_pi_eq_pi_comp {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} {cs : (i : ι) → X i} (γ₀ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) (γ₁ : (i : ι) → Path.Homotopic.Quotient (bs i) (cs i)) :
            (Path.Homotopic.pi γ₀).comp (Path.Homotopic.pi γ₁) = Path.Homotopic.pi fun (i : ι) => (γ₀ i).comp (γ₁ i)

            Composition and products commute. This is Path.trans_pi_eq_pi_trans descended to path homotopy classes.

            @[reducible, inline]
            abbrev Path.Homotopic.proj {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (i : ι) (p : Path.Homotopic.Quotient as bs) :

            Abbreviation for projection onto the ith coordinate.

            Equations
            • Path.Homotopic.proj i p = p.mapFn { toFun := fun (p : (i : ι) → X i) => p i, continuous_toFun := }
            Instances For
              @[simp]
              theorem Path.Homotopic.proj_pi {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (i : ι) (paths : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) :

              Lemmas showing projection is the inverse of pi.

              @[simp]
              theorem Path.Homotopic.pi_proj {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (p : Path.Homotopic.Quotient as bs) :
              (Path.Homotopic.pi fun (i : ι) => Path.Homotopic.proj i p) = p
              def Path.Homotopic.prodHomotopy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} {p₁ : Path a₁ a₂} {p₁' : Path a₁ a₂} {p₂ : Path b₁ b₂} {p₂' : Path b₁ b₂} (h₁ : p₁.Homotopy p₁') (h₂ : p₂.Homotopy p₂') :
              (p₁.prod p₂).Homotopy (p₁'.prod p₂')

              The product of homotopies h₁ and h₂. This is HomotopyRel.prod specialized for path homotopies.

              Equations
              Instances For
                def Path.Homotopic.prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) :
                Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)

                The product of path classes q₁ and q₂. This is Path.prod descended to the quotient.

                Equations
                Instances For
                  theorem Path.Homotopic.prod_lift {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (p₁ : Path a₁ a₂) (p₂ : Path b₁ b₂) :
                  Path.Homotopic.prod p₁ p₂ = p₁.prod p₂
                  theorem Path.Homotopic.comp_prod_eq_prod_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {a₃ : α} {b₁ : β} {b₂ : β} {b₃ : β} (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) (r₁ : Path.Homotopic.Quotient a₂ a₃) (r₂ : Path.Homotopic.Quotient b₂ b₃) :
                  (Path.Homotopic.prod q₁ q₂).comp (Path.Homotopic.prod r₁ r₂) = Path.Homotopic.prod (q₁.comp r₁) (q₂.comp r₂)

                  Products commute with path composition. This is trans_prod_eq_prod_trans descended to the quotient.

                  @[reducible, inline]
                  abbrev Path.Homotopic.projLeft {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {c₁ : α × β} {c₂ : α × β} (p : Path.Homotopic.Quotient c₁ c₂) :

                  Abbreviation for projection onto the left coordinate of a path class.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Path.Homotopic.projRight {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {c₁ : α × β} {c₂ : α × β} (p : Path.Homotopic.Quotient c₁ c₂) :

                    Abbreviation for projection onto the right coordinate of a path class.

                    Equations
                    Instances For
                      @[simp]
                      theorem Path.Homotopic.projLeft_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) :

                      Lemmas showing projection is the inverse of product.

                      @[simp]
                      theorem Path.Homotopic.projRight_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) :
                      @[simp]
                      theorem Path.Homotopic.prod_projLeft_projRight {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)) :