Pushing quiver along a map: `finish` does the job

Stream: new members

[Rémi Bottinelli]

Hey, given a quiver on V and a map V -> V', I'm trying to define the induced quiver on V' below.
It works, except that one proof uses finish and I have no idea how to extract a meaningful proof out of this.
How should I proceed? Thanks!

import combinatorics.quiver.basic

universes u v u₂ v₂

namespace quiver

/-- The `quiver` instance obtained by pushing arrows of `V` along `σ` -/
def push {V : Type u} [quiver V] {W : Type u₂} (σ : V → W) := W

namespace push

variables {V : Type*} [quiver V] {W : Type*} (σ : V → W)

inductive push_quiver {V : Type u} [quiver.{v} V] {W : Type u₂} (σ : V → W) :
  W → W → Type (max u u₂ v)
| arrow {X Y : V} (f : X ⟶ Y) : push_quiver (σ X) (σ Y)

instance : quiver (push σ) := ⟨λ X Y, push_quiver σ X Y⟩

def of : prefunctor V (push σ) :=
{ obj := σ,
  map := λ X Y f, push_quiver.arrow f}

local postfix ` * ` := of

@[simp] lemma of_obj : ((σ *)).obj = σ := rfl

variables {W' : Type*} [quiver W']
  (φ : prefunctor V W') (τ : W → W') (h : ∀ x, φ.obj x = τ (σ x) )

include φ h
def lift : prefunctor (push σ) W' :=
{ obj := τ,
  map := @push_quiver.rec V _ W σ
    (λ X Y f, τ X ⟶ τ Y)
    (λ X Y f, by {rw [←h X,←h Y], exact φ.map f}) }

lemma lift_spec_obj : (lift σ φ τ h).obj = τ := rfl

lemma lift_spec_comm : (of σ).comp (lift σ φ τ h) = φ :=
begin
  dsimp only [of,lift],
  fapply prefunctor.ext,
  { rintros, simp only [prefunctor.comp_obj], symmetry, exact h X, },
  { rintros _ _ f, simp only [prefunctor.comp_map],
    finish,
     },
  -- no idea how `finish` worked :(
end
lemma lift_unique (Φ : prefunctor (push σ) W') (Φ₀ : Φ.obj = τ) (Φcomm : (of σ).comp Φ = φ) :
  Φ = (lift σ φ τ h) :=
begin
  dsimp only [of,lift],
  fapply prefunctor.ext,
  { rintros, simp_rw [←Φ₀], },
  { rintros _ _ f, induction f, subst_vars, simp only [prefunctor.comp_map, cast_eq], refl, }
end

end push

end quiver

[Junyan Xu]

Here is a proof without finish, and it may be similar to what finish does, because from the (horrible, unreadably long) output of show_term { finish } I also see the use of cast_heq and eq_rec_heq. (by the way shouldn't the name be lift_spec rather than lift_spec_comm?

lemma lift_spec_comm : (of σ).comp (lift σ φ τ h) = φ :=
begin
  dsimp only [of,lift],
  fapply prefunctor.ext,
  { rintros, simp only [prefunctor.comp_obj], symmetry, exact h X, },
  { rintros _ _ f, simp only [prefunctor.comp_map, eq_mpr_eq_cast],
    apply eq_of_heq,
    iterate 2 { apply (cast_heq _ _).trans },
    symmetry,
    iterate 2 { apply (eq_rec_heq _ _).trans },
    refl },
end

[Rémi Bottinelli]

Great, thanks!

Re naming: I'm not sure: there are two properties for the UMP, given by lift_spec_comm and lift_spec_obj, hence the longer name. I could add a lift_spec returning the conjunction of the two.

Also, the iterate 2 { apply (cast_heq _ _).trans }, is quite obscure to me: could you expand on its purpose and how you came up with it?

[Junyan Xu]

The problem is that you want to simplify cast _ something to something using docs#cast_heq, but cast_heq is a heterogeneous equality (==) and rw doesn't work with it. So you need to manually apply docs#heq.trans.

[Rémi Bottinelli]

Ah, OK, I figured it was something along those lines, thanks! Is there a reason some kind of hrw doesn't exist?

[Rémi Bottinelli]

Great, I had two other similar finishs in the code for universal groupoids which I could kill with your trick!

[Junyan Xu]

Re naming: I'm not sure: there are two properties for the UMP, given by lift_spec_comm and lift_spec_obj, hence the longer name. I could add a lift_spec returning the conjunction of the two.

OK I see, I think it's good to keep them separate, and I don't have a better name.

Ah, OK, I figured it was something along those lines, thanks! Is there a reason some kind of hrw doesn't exist?

I think hrw might be more challenging to write. If you compare the signatures of eq.rec (used by rw) and heq.rec:

eq.rec : Π {α : Sort u_7} {a : α} {motive : α → Sort u_6}, motive a → Π {ᾰ : α}, a = ᾰ → motive ᾰ
heq.rec :
  Π {α : Sort u_7} {a : α} {motive : Π {β : Sort u_7}, β → Sort u_6},
    motive a → Π {β : Sort u_7} {ᾰ : β}, a == ᾰ → motive ᾰ

(outputs of #check @eq.rec and #check @heq.rec), you see the motive for heq.rec has one extra argument and is probably harder to fill in. If it can be automatically filled in, I think it may be able to solve some "motive is not type correct" issues that sometimes arises when using rw (though simp_rw already solves some cases).