Dealing with `Path.cast`

Stream: Is there code for X?

[Sebastian Kumar]

I was formalizing some algebraic topology and I felt I needed lemmas like:

import Mathlib

variable {X : Type*} [TopologicalSpace X]

namespace Path

theorem cast_trans_trans_cast_eq {x₀ x₁ x₂ x₃ x₄ x₅ : X} (h₀ : x₂ = x₁) (h₁ : x₃ = x₄)
    (p₀ : Path x₀ x₁) (p₁ : Path x₂ x₃) (p₂ : Path x₄ x₅) :
    ((p₀.cast rfl h₀).trans p₁).trans (p₂.cast h₁ rfl) =
      (p₀.trans (p₁.cast h₀.symm h₁.symm)).trans p₂ := by
  ext s
  simp [trans_apply]

namespace Homotopic

theorem cast_homotopic_iff_homotopic_cast {x₀ x₁ x₀' x₁' : X} {p : Path x₀ x₁} {p' : Path x₀' x₁'}
    {h₀ : x₀' = x₀} {h₁ : x₁' = x₁} :
    (p.cast h₀ h₁).Homotopic p' ↔ p.Homotopic (p'.cast h₀.symm h₁.symm) := ⟨id, id⟩

However, these seem unreasonably messy. I was wondering if there was a smarter way to do this. Are there any clever dependent type theory constructions to deal with casting objects between different types? My intuition is that Path.trans should only depend on the underlying path and so should be flexible with respect to casting, but I don't know how to formalize this in lean (besides what I gave above).

[Aaron Liu]

try rewriting?

[Aaron Liu]

with the dependent rewrite tactic

[Aaron Liu]

you can also congr!

[Aaron Liu]

import Mathlib

variable {X : Type*} [TopologicalSpace X]

namespace Path

@[simp]
theorem cast_rfl_rfl {x₀ x₁ : X} (p : Path x₀ x₁) : p.cast rfl rfl = p := rfl

theorem cast_trans_trans_cast_eq {x₀ x₁ x₂ x₃ x₄ x₅ : X} (h₀ : x₂ = x₁) (h₁ : x₃ = x₄)
    (p₀ : Path x₀ x₁) (p₁ : Path x₂ x₃) (p₂ : Path x₄ x₅) :
    ((p₀.cast rfl h₀).trans p₁).trans (p₂.cast h₁ rfl) =
      (p₀.trans (p₁.cast h₀.symm h₁.symm)).trans p₂ := by
  rewrite! (castMode := .all) [h₀, h₁]
  dsimp

namespace Homotopic

theorem cast_homotopic_iff_homotopic_cast {x₀ x₁ x₀' x₁' : X} {p : Path x₀ x₁} {p' : Path x₀' x₁'}
    {h₀ : x₀' = x₀} {h₁ : x₁' = x₁} :
    (p.cast h₀ h₁).Homotopic p' ↔ p.Homotopic (p'.cast h₀.symm h₁.symm) := by
  rewrite! (castMode := .all) [h₀, h₁]
  dsimp
  rfl

[Sebastian Kumar]

Thanks for the suggestion. I wasn't familiar with the dependent rewrite tactic. So could something along the lines of the following be added to Mathlib? The example at the end is (more or less) what I am trying to use this for.

namespace Path

variable {X : Type*} [TopologicalSpace X] {x₀ x₀' x₁ x₁' : X}

@[simp] theorem cast_rfl_rfl (p : Path x₀ x₁) : p.cast rfl rfl = p := rfl

theorem cast_eq (h₀ : x₀' = x₀) (h₁ : x₁' = x₁) (p : Path x₀ x₁) :
    p.cast h₀ h₁ = h₀ ▸ h₁ ▸ p  := by
  rewrite! [h₀, h₁]
  rfl

theorem Homotopic.cast_iff (h₀ : x₀' = x₀) (h₁ : x₁' = x₁)
    (p : Path x₀ x₁) (p' : Path x₀' x₁') : (p.cast h₀ h₁).Homotopic p' ↔
      p.Homotopic (p'.cast h₀.symm h₁.symm) := by
  rewrite! (castMode := .all) [h₀, h₁]
  rfl

example {x : X} (h₀ : x₀ = x) (h₁ : x₁ = x) (p : Path x₀ x₁) (q : Path x x)
    (h : p.Homotopic (q.cast h₀ h₁)) :
    ((((refl x).cast rfl h₀).trans p).trans ((Path.refl x).cast h₁ rfl)).Homotopic q := by
  rewrite! (castMode := .all) [h₀, h₁]
  dsimp
  apply Homotopic.trans (Homotopic.trans ⟨Homotopy.transRefl _⟩ ⟨Homotopy.reflTrans _⟩)
  rw [← cast_eq h₀.symm h₁.symm, Homotopic.cast_iff]
  exact h

end Path

Another issue I ran into is that, in the code I was working with, instead of h₀ I have a proof of the form ht₀ ▸ γ.source. For some reason the tactic rewrite! (castMode := .all) [ht₀ ▸ γ.source] doesn't work and I instead have to do have := ht₀ ▸ γ.source; rewrite! (castMode := .all) [this]. Why is this?

[Aaron Liu]

there might be bugs

[Aaron Liu]

what is the error message you got?

[Aaron Liu]

can you provide a #mwe?

[Aaron Liu]

oh btw you can also just cases h₀; cases h₁ since you have a free variable on one side

[Aaron Liu]

import Mathlib

namespace Path

variable {X : Type*} [TopologicalSpace X] {x₀ x₀' x₁ x₁' : X}

@[simp] theorem cast_rfl_rfl (p : Path x₀ x₁) : p.cast rfl rfl = p := rfl

theorem cast_eq (h₀ : x₀' = x₀) (h₁ : x₁' = x₁) (p : Path x₀ x₁) :
    p.cast h₀ h₁ = h₀ ▸ h₁ ▸ p := by
  cases h₀; cases h₁; rfl

theorem Homotopic.cast_iff (h₀ : x₀' = x₀) (h₁ : x₁' = x₁)
    (p : Path x₀ x₁) (p' : Path x₀' x₁') : (p.cast h₀ h₁).Homotopic p' ↔
      p.Homotopic (p'.cast h₀.symm h₁.symm) := by
  cases h₀; cases h₁; simp

@[simp]
theorem Homotopic.trans_refl_left_iff (p q : Path x₀ x₁) :
    (p.trans (Path.refl x₁)).Homotopic q ↔ p.Homotopic q :=
  ⟨.trans ⟨(Homotopy.transRefl p).symm⟩, .trans ⟨Homotopy.transRefl p⟩⟩

@[simp]
theorem Homotopic.refl_trans_left_iff (p q : Path x₀ x₁) :
    ((Path.refl x₀).trans p).Homotopic q ↔ p.Homotopic q :=
  ⟨.trans ⟨(Homotopy.reflTrans p).symm⟩, .trans ⟨Homotopy.reflTrans p⟩⟩

@[simp]
theorem Homotopic.trans_refl_right_iff (p q : Path x₀ x₁) :
    p.Homotopic (q.trans (Path.refl x₁)) ↔ p.Homotopic q :=
  ⟨fun h => h.trans ⟨Homotopy.transRefl q⟩, fun h => h.trans ⟨(Homotopy.transRefl q).symm⟩⟩

@[simp]
theorem Homotopic.refl_trans_right_iff (p q : Path x₀ x₁) :
    p.Homotopic ((Path.refl x₀).trans q) ↔ p.Homotopic q :=
  ⟨fun h => h.trans ⟨Homotopy.reflTrans q⟩, fun h => h.trans ⟨(Homotopy.reflTrans q).symm⟩⟩

example {x : X} (h₀ : x₀ = x) (h₁ : x₁ = x) (p : Path x₀ x₁) (q : Path x x)
    (h : p.Homotopic (q.cast h₀ h₁)) :
    ((((refl x).cast rfl h₀).trans p).trans ((Path.refl x).cast h₁ rfl)).Homotopic q := by
  cases h₀; cases h₁; simpa using h

end Path

[Sebastian Kumar]

Here is an example for the error I was talking about. For me, the first example compiles but the second gives the error tactic 'depRewrite' failed, equality or iff proof expected.

import Mathlib

variable {α : Type*} {a₀ a₁ : α} (ha : a₀ = a₁)
         {X : Type*} [TopologicalSpace X] {x y : X}
         (f : α → X) (hfa₁ : f a₁ = x) (p : Path x y)

example : p.cast (ha ▸ hfa₁) rfl = (ha ▸ hfa₁) ▸ p := by
  have := ha ▸ hfa₁
  rewrite! [this]
  rfl

example : p.cast (ha ▸ hfa₁) rfl = (ha ▸ hfa₁) ▸ p := by
  rewrite! [ha ▸ hfa₁]

[Aaron Liu]

regular rewrite also fails here so it's not dependent rewrite's fault

[Aaron Liu]

maybe it's something about the elaboration

[Aaron Liu]

this works

import Mathlib

variable {α : Type*} {a₀ a₁ : α} (ha : a₀ = a₁)
         {X : Type*} [TopologicalSpace X] {x y : X}
         (f : α → X) (hfa₁ : f a₁ = x) (p : Path x y)

example : p.cast (ha ▸ hfa₁) rfl = (ha ▸ hfa₁) ▸ p := by
  rewrite! [(ha ▸ hfa₁ :)]

[Sebastian Kumar]

thanks for the fix

[Sebastian Kumar]

So should I make a pull request to Mathlib for cast_rfl_rfl, and one for the trans_refl_left_iff lemmas? I am new to Mathilb so I am not quite sure: what would be the convention for giving credit in this case?

[Aaron Liu]

yeah sure, unless you want me to do it

[Aaron Liu]

you can just mention me in the PR description

[Sebastian Kumar]

Okay, thanks for all the help. I should be able to make the prs tomorrow. My end goal is contributing that the n-sphere is simply connected for n > 1, and now I'm getting rather close :)

[Aaron Liu]

ooohhh I'm interested

[Wuyang]

That’s a nice refinement of the casting lemmas: your approach plus cases/rewrite! makes things much cleaner. Looking forward to seeing the PRs!
(P.S. If you want to explore related lemmas or prior work, try LeanFinder at www.leanfinder.org.)

[Wuyang]

@leanfinder casting lemmas for Path and Homotopic in Lean with rewrite! and cases tactics

[leanfinder]

Here’s what I found:

• theorem eq_path_of_eq_image : (πₘ (TopCat.ofHom f)).map ⟦p⟧ = hcast (start_path hfg) ≫ (πₘ (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast (end_path hfg).symm := by rw [conj_eqToHom_iff_heq ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧) (FundamentalGroupoid.ext <| start_path hfg) (FundamentalGroupoid.ext <| end_path hfg)] exact heq_path_of_eq_image hfg "Let $f, g : X \to Y$ be continuous maps between topological spaces, and let $p, q$ be paths in $X$. If $f(p(t)) = g(q(t))$ for all $t$, then the image of the path $p$ under the functor induced by $f$ is equal to the image of the path $q$ under the functor induced by $g$, up to homotopy equivalences at the start and end points. Formally, $(\pi_{\text{}}(f)).map([p]) = \text{hcast}(\text{start extunderscore path}(hfg)) \circ (\pi_{\text{}}(g)).map([q]) \circ \text{hcast}(\text{end extunderscore path}(hfg)^{-1})$ where $\text{hcast}$ represents homotopy casting at the start and end points." (score: 0.708)

• theorem ContinuousMap.Homotopy.apply_zero_path : (πₘ f).map p = hcast (H.apply_zero x₀).symm ≫ (πₘ H.uliftMap).map (prodToProdTopI (𝟙 (@fromTop (TopCat.of _) (ULift.up 0))) p) ≫ hcast (H.apply_zero x₁) := Quotient.inductionOn p fun p' => by apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p') -- This used to be rw, but we need erw after https://github.com/leanprover/lean4/pull/2644 erw [Path.prod_coe]; simp_rw [ulift_apply]; simp "Let $H \colon f \sim g$ be a homotopy between continuous maps $f, g \colon X \to Y$, and let $p \colon x₀ \to x₁$ be a path in the fundamental groupoid $\pi_{\text{}} X$. Then the image of $p$ under the functor induced by $f$ is given by:
  $$
  f_*(p) = \text{hcast}(H(0, x₀)^{-1}) \circ H_*(\text{id}_{0} \times p) \circ \text{hcast}(H(0, x₁))
  $$
  where:

• $\text{hcast}(H(0, x₀)^{-1})$ is the cast morphism for the path $H(0, x₀)^{-1}$,

• $H_*(\text{id}_{0} \times p)$ is the image of the path $\text{id}_{0} \times p$ under the functor induced by $H$ (after appropriate lifting),
• $\text{hcast}(H(0, x₁))$ is the cast morphism for the path $H(0, x₁)$." (score: 0.706)

• definition Path.Homotopy.cast {p₀ p₁ q₀ q₁ : Path x₀ x₁} (F : Homotopy p₀ p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) : Homotopy q₀ q₁ := ContinuousMap.HomotopyRel.cast F (congr_arg _ h₀) (congr_arg _ h₁) "Given a homotopy $F$ between two paths $p_0$ and $p_1$ in a topological space $X$ with fixed endpoints $x_0$ and $x_1$, and given equalities $p_0 = q_0$ and $p_1 = q_1$, this constructs a homotopy between $q_0$ and $q_1$ by casting $F$ to the new pair of paths." (score: 0.704)

• theorem ContinuousMap.Homotopy.apply_one_path : (πₘ g).map p = hcast (H.apply_one x₀).symm ≫ (πₘ H.uliftMap).map (prodToProdTopI (𝟙 (@fromTop (TopCat.of _) (ULift.up 1))) p) ≫ hcast (H.apply_one x₁) := Quotient.inductionOn p fun p' => by apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p') -- This used to be rw, but we need erw after https://github.com/leanprover/lean4/pull/2644 erw [Path.prod_coe]; simp_rw [ulift_apply]; simp "Let $f, g \colon X \to Y$ be continuous maps with a homotopy $H \colon f \sim g$. For any path $p \colon x₀ \to x₁$ in $X$, the image of $p$ under the functor induced by $g$ is given by:
  $$
  g_*(p) = \text{hcast}(H(1, x₀)^{-1}) \circ H_*(\text{id}_{1} \times p) \circ \text{hcast}(H(1, x₁))
  $$
  where:

• $g_*$ is the functor $\pi(X) \to \pi(Y)$ induced by $g$,

• $\text{hcast}$ is the casting isomorphism between equal points in the fundamental groupoid,
• $H_*$ is the functor induced by the lifted homotopy $\text{ULift}\, I \times X \to Y$,
• $\text{id}_{1}$ is the identity path at $1 \in I$,
• $\times$ denotes the product of paths via $\text{prodToProdTopI}$." (score: 0.703)

• theorem eq_diag_path : (πₘ (TopCat.ofHom f)).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧ (⟦H.evalAt x₀⟧ ≫ (πₘ (TopCat.ofHom g)).map p : fromTop (f x₀) ⟶ fromTop (g x₁)) = H.diagonalPath' p := by rw [H.apply_zero_path, H.apply_one_path, H.evalAt_eq] erw [H.evalAt_eq] dsimp only [prodToProdTopI] constructor · slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl] -- Porting note: this ↓ simp didn't do this
  slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
  rfl
  · slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl] -- Porting note: this ↓ simp didn't do this slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp] rfl "Given a homotopy $H$ between continuous maps $f$ and $g$ from a topological space $X$ to another space $Y$, and a path $p$ in the fundamental groupoid, the following equalities hold:
  $$
  (\pi_{\text{m}}(\text{TopCat.ofHom}\ f)).\text{map}(p) \circ [H.\text{evalAt}\ x_1] = H.\text{diagonalPath'}(p)
  $$
  and
  $$
  [H.\text{evalAt}\ x_0] \circ (\pi_{\text{m}}(\text{TopCat.ofHom}\ g)).\text{map}(p) = H.\text{diagonalPath'}(p).
  $$
  This means that the homotopy class of the path evaluated at $x_1$ or $x_0$ is equal to the diagonal path induced by $p$." (score: 0.702)

• definition Path.Homotopy.map {p q : Path x₀ x₁} (F : p.Homotopy q) (f : C(X, Y)) : Homotopy (p.map f.continuous) (q.map f.continuous) where toFun := f ∘ F map_zero_left := by simp map_one_left := by simp prop' t x hx := by cases' hx with hx hx · simp [hx] · rw [Set.mem_singleton_iff] at hx simp [hx] "Given a homotopy $F$ between two paths $p$ and $q$ in a topological space $X$ with fixed endpoints $x_0$ and $x_1$, and a continuous map $f \colon X \to Y$, the composition $f \circ F$ defines a homotopy between the image paths $f \circ p$ and $f \circ q$ in $Y$. This homotopy satisfies:

• $(f \circ F)(t,0) = f(p(t))$ for all $t \in [0,1]$

• $(f \circ F)(t,1) = f(q(t))$ for all $t \in [0,1]$
• $(f \circ F)(0,s) = f(x_0)$ for all $s \in [0,1]$
• $(f \circ F)(1,s) = f(x_1)$ for all $s \in [0,1]$" (score: 0.695)

• theorem Quiver.Path.cast_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) : HEq (p.cast hu hv) p := by rw [Path.cast_eq_cast] exact _root_.cast_heq _ _ "Given a quiver path $p$ from vertex $u$ to vertex $v$ in a quiver $U$, and equalities $hu : u = u'$ and $hv : v = v'$, the transported path $p.\mathrm{cast}\,hu\,hv$ is hereditarily equal to the original path $p$." (score: 0.693)

• theorem Quiver.Path.cast_eq_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) (p' : Path u' v') : p.cast hu hv = p' ↔ HEq p p' := by rw [Path.cast_eq_cast] exact _root_.cast_eq_iff_heq "For any vertices $u, v, u', v'$ in a quiver $U$ with equalities $hu : u = u'$ and $hv : v = v'$, and paths $p : \text{Path}\,u\,v$ and $p' : \text{Path}\,u'\,v'$, the transported path $p.\text{cast}\,hu\,hv$ is equal to $p'$ if and only if $p$ and $p'$ are heterogeneously equal (i.e., equal up to the vertex equalities $hu$ and $hv$)." (score: 0.690)

• theorem Path.Homotopic.proj_pi (i : ι) (paths : ∀ i, Path.Homotopic.Quotient (as i) (bs i)) : proj i (pi paths) = paths i := by induction paths using Quotient.induction_on_pi rw [proj, pi_lift, ← Path.Homotopic.map_lift] congr "For any index $i$ in the index set $\iota$ and any family of path homotopy classes $\{\gamma_j\}_{j \in \iota}$ where each $\gamma_j$ is a homotopy class of paths from $a_j$ to $b_j$ in $X_j$, the projection of the product homotopy class $\prod_{j \in \iota} \gamma_j$ onto the $i$-th coordinate equals $\gamma_i$. In other words, $\text{proj}_i(\prod_{j \in \iota} \gamma_j) = \gamma_i$." (score: 0.689)

• theorem Path.eq_cast_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) (p' : Path u' v') : p' = p.cast hu hv ↔ HEq p' p := ⟨fun h => ((p.cast_eq_iff_heq hu hv p').1 h.symm).symm, fun h => ((p.cast_eq_iff_heq hu hv p').2 h.symm).symm⟩ "For any vertices $u, v, u', v'$ in a quiver $U$ with equalities $hu : u = u'$ and $hv : v = v'$, and paths $p : \text{Path}\,u\,v$ and $p' : \text{Path}\,u'\,v'$, the path $p'$ is equal to the transported path $p.\text{cast}\,hu\,hv$ if and only if $p'$ and $p$ are heterogeneously equal (i.e., equal up to the vertex equalities $hu$ and $hv$)." (score: 0.686)

[Matthew Ballard]

@Wuyang please stop spamming topics with leanfinder.

[Wuyang]

Matthew Ballard said:

Wuyang please stop spamming topics with leanfinder.

@Matthew Ballard Thank you! Sorry for sending many messages! Our team is building basic tools to help mathematicians. Hope these tools could be useful.

[Matthew Ballard]

That is great to hear. Please make a post on #general discussing this so people can interact in a more contained manner and use the tools themselves if they wish.

[Wuyang]

Matthew Ballard said:

That is great to hear. Please make a post on #general discussing this so people can interact in a more contained manner and use the tools themselves if they wish.

@Matthew Ballard Thanks! Will do!

[Sebastian Kumar]

By the way, here is the pull request for the sphere being simply connected #28246. My final approach for dealing with Path.cast was to use cases in the lemma cast_trans_trans_homotopic_of_homotopic_cast and combine that with a dependent rewrite in exists_loops_homotopic_foldTrans_of_open_cover (both in the file SimplyConnectedSphere). I hope that is a sensible approach, but I am of course happy to change it if not.

[Kim Morrison]

Matthew Ballard said:

That is great to hear. Please make a post on #general discussing this so people can interact in a more contained manner and use the tools themselves if they wish.

My suggestion is that you (or any else writing future bots) only ever summon it in "someone else's thread" if you then follow up the bot's response with something useful/constructive/introspective (e.g. "hmm, that wasn't a great answer", or "it looks to me like suggestion 3 was what you're looking for"). Putting in this effort will lessen the impression that you are summoning the bot merely to advertise it.