Documentation

LeanPool.DirectedTopologyLean4.SplitDihomotopy

LeanPool.DirectedTopologyLean4.SplitDihomotopy #

source
@[reducible, inline]
abbrev SplitDihomotopy.DirectedFst (T : ↑unitInterval) :
D(↑unitInterval,↑unitInterval)

For any T: I, we have the directed map I → I given by t ↦ t * T. This is an interpolation from 0 to T

Equations
Instances For
    source
    @[simp]
    theorem SplitDihomotopy.directedFst_apply (T t : ↑unitInterval) :
    (DirectedFst T) t = ⟨↑T * ↑t, ⋯⟩
    source
    @[reducible, inline]
    abbrev SplitDihomotopy.DirectedSnd (T : ↑unitInterval) :
    D(↑unitInterval,↑unitInterval)

    For any T : I we have the directed map I → I given by t ↦ (1 - t) * T + t. This is an interpolation from T to 1

    Equations
    Instances For
      source
      @[simp]
      theorem SplitDihomotopy.directedSnd_apply (T t : ↑unitInterval) :
      (DirectedSnd T) t = ⟨↑(unitInterval.symm T) * ↑t + ↑T, ⋯⟩
      source
      def SplitDihomotopy.FirstPartVerticallyDihomotopy {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (F : γ₁.Dihomotopy γ₂) (T : ↑unitInterval) :
      γ₁.Dihomotopy (F.eval T)

      The first part of a dipath-dihomotopy split vertically at T: a dihomotopy from γ₁ to the slice F.eval T.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem SplitDihomotopy.fpv_apply {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (F : γ₁.Dihomotopy γ₂) (T s t : ↑unitInterval) :
        (FirstPartVerticallyDihomotopy F T) (s, t) = F (T * s, t)
        source
        def SplitDihomotopy.SecondPartVerticallyDihomotopy {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (F : γ₁.Dihomotopy γ₂) (T : ↑unitInterval) :
        (F.eval T).Dihomotopy γ₂

        The second part of a dipath-dihomotopy split vertically at T: a dihomotopy from the slice F.eval T to γ₂.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem SplitDihomotopy.spv_apply {X : dTopCat} {x y : ↑X} {γ₁ γ₂ : Dipath x y} (F : γ₁.Dihomotopy γ₂) (T s t : ↑unitInterval) :
          (SecondPartVerticallyDihomotopy F T) (s, t) = F (⟨↑(unitInterval.symm T) * ↑s + ↑T, ⋯⟩, t)
          source
          def SplitDihomotopy.FirstPartHorizontallyDihomotopy {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T : ↑unitInterval) :
          (SplitDipath.FirstPart (Dipath.ofDirectedMap f) T).toDirectedMap.Dihomotopy (SplitDipath.FirstPart (Dipath.ofDirectedMap g) T).toDirectedMap

          The first part of a dihomotopy split horizontally at T: a dihomotopy between the first parts of f and g as dipaths.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem SplitDihomotopy.fph_apply {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T s t : ↑unitInterval) :
            (FirstPartHorizontallyDihomotopy F T) (s, t) = F (s, T * t)
            source
            def SplitDihomotopy.SecondPartHorizontallyDihomotopy {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T : ↑unitInterval) :
            (SplitDipath.SecondPart (Dipath.ofDirectedMap f) T).toDirectedMap.Dihomotopy (SplitDipath.SecondPart (Dipath.ofDirectedMap g) T).toDirectedMap

            The second part of a dihomotopy split horizontally at T: a dihomotopy between the second parts of f and g as dipaths.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem SplitDihomotopy.sph_apply {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T s t : ↑unitInterval) :
              (SecondPartHorizontallyDihomotopy F T) (s, t) = F (s, ⟨↑(unitInterval.symm T) * ↑t + ↑T, ⋯⟩)
              source
              theorem SplitDihomotopy.fph_eval_0 {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T : ↑unitInterval) :
              (FirstPartHorizontallyDihomotopy F T).evalAtRight 0 = (F.evalAtRight 0).cast ⋯ ⋯
              source
              theorem SplitDihomotopy.fph_eval_1 {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T : ↑unitInterval) :
              (FirstPartHorizontallyDihomotopy F T).evalAtRight 1 = (F.evalAtRight T).cast ⋯ ⋯
              source
              theorem SplitDihomotopy.sph_eval_0 {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T : ↑unitInterval) :
              (SecondPartHorizontallyDihomotopy F T).evalAtRight 0 = (F.evalAtRight T).cast ⋯ ⋯
              source
              theorem SplitDihomotopy.sph_eval_1 {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (T : ↑unitInterval) :
              (SecondPartHorizontallyDihomotopy F T).evalAtRight 1 = (F.evalAtRight 1).cast ⋯ ⋯