A bijective prefunctor has an inverse: `eq.rec` goal

Stream: maths

[Rémi Bottinelli]

Hey, I'm trying to define isomorphisms of quivers, and a natural thing to prove here is that a prefunctor that is bijective on objects and arrows is an isomorphism. The problem is that to show that its inverse really is an inverse, I face transport on equalities of vertices, and I see no way to attack those. This is the two sorrys in the code below.
What's the proper way to solve those goals? Thanks!

import combinatorics.quiver.basic

universes u v w z

namespace quiver

structure iso (U V : Type*) [quiver.{u+1} U] [quiver.{v+1} V] extends prefunctor U V :=
(inv_prefunctor : V ⥤q U)
(left_inv : to_prefunctor ⋙q inv_prefunctor = 𝟭q _)
(right_inv : inv_prefunctor ⋙q to_prefunctor = 𝟭q _)

infix ` ≃q `:60 := iso

variables {U V W Z : Type*} [quiver.{u+1} U] [quiver.{v+1} V] [quiver.{w+1} W] [quiver.{z+1} Z]

instance : has_coe (iso U V) (prefunctor U V) :=
⟨iso.to_prefunctor⟩


def iso.refl (U : Type*) [quiver.{u+1} U] : iso U U := ⟨𝟭q _, 𝟭q _, rfl, rfl⟩

def iso.symm (φ : iso U V) : iso V U :=
⟨φ.inv_prefunctor, φ.to_prefunctor, φ.right_inv, φ.left_inv⟩

def iso.trans (φ : iso U V) (ψ : iso V W) : iso U W :=
{ to_prefunctor := φ.to_prefunctor ⋙q ψ.to_prefunctor,
  inv_prefunctor := ψ.inv_prefunctor ⋙q φ.inv_prefunctor,
  left_inv := by
  { rw [←prefunctor.comp_assoc, prefunctor.comp_assoc φ.to_prefunctor,
        ψ.left_inv, prefunctor.comp_id, φ.left_inv], },
  right_inv := by
  { rw [←prefunctor.comp_assoc, prefunctor.comp_assoc ψ.inv_prefunctor,
        φ.right_inv, prefunctor.comp_id, ψ.right_inv], }, }

noncomputable def iso.of_bijective (φ : U ⥤q V) (hφobj : function.bijective φ.obj)
  (hφmap : ∀ (x y : U), function.bijective (φ.map : (x ⟶ y) → (φ.obj x ⟶ φ.obj y)) ) :
  iso U V :=
{ to_prefunctor := φ,
  inv_prefunctor :=
  { obj := function.surj_inv hφobj.surjective,
    map := λ (x y : V) (e : x ⟶ y), by
    { rw [←function.right_inverse_surj_inv hφobj.2 x,
          ←function.right_inverse_surj_inv hφobj.2 y] at e,
      exact ((hφmap _ _).2 e).some,  } },
  left_inv := by
  { have : ∀ (X : U), function.surj_inv hφobj.2 (φ.obj X) = X, by
    { rintro x,
      simp only [function.left_inverse_surj_inv hφobj x, prefunctor.comp_obj,
                 prefunctor.id_obj, id.def], },
    fapply prefunctor.ext,
    { exact this, },
    { rintro x y,
      generalize hx : function.surj_inv hφobj.2 (φ.obj x) = x',
      generalize hy : function.surj_inv hφobj.2 (φ.obj y) = y',
      let hx' := this x,
      let hy' := this y,
      simp,
      sorry }, },
  right_inv := by {
    fapply prefunctor.ext,
    { rintro x,
      simp only [function.right_inverse_surj_inv hφobj.2 x, prefunctor.comp_obj,
                 prefunctor.id_obj, id.def], },
    { rintro x y e,
      sorry, }, }, }

@[ext]
lemma iso.ext (φ ψ : iso U V) : φ.to_prefunctor = ψ.to_prefunctor → φ = ψ := sorry

end quiver

[Kevin Buzzard]

Do we have the theorem that a functor is an equivalence if it's bijective on hom sets and essentially surjective on objects? Because you'll see all the same problems there, I should think.

[Rémi Bottinelli]

Good idea, let me see: https://leanprover-community.github.io/mathlib_docs/category_theory/equivalence.html#category_theory.equivalence.of_fully_faithfully_ess_surj

[Kevin Buzzard]

Seems to me that the key difference is that Scott's (presumably it is Scott) definition of full is constructive: docs#category_theory.full (see witness)

[Adam Topaz]

It should be doable with some induction on equalities.... I'll give it a go

[Kevin Buzzard]

yeah it should be messy but doable, but the definition of map in iso.of_bijective is in tactic mode, and Scott can avoid this. I wonder whether it would be easier to prove iso.of_bijective_and_full_in_Scotts_sense first, and then deduce iso.of_bijective from it.

[Rémi Bottinelli]

I had the same problem here and this got solved by Junyan (iirc). I seem to never be able to close these goals.

[Kevin Buzzard]

Basically the same idea: create a little API for the construction which takes a morphism of quivers which is bijective on hom sets and returns the inverse bijection on hom sets, go through the eq.rec pain there, and just use the inverse bijection to make the main proof far less painful (by following Scott's approach, so you don't need the rw in the definition of map)

[Kevin Buzzard]

Rémi Bottinelli said:

I had the same problem here and this got solved by Junyan (iirc). I seem to never be able to close these goals.

Yeah, there is an art to these theorems. Back in the day I remember struggling to prove that a bijection gave an equiv, and this is just the same question but hard mode. The reason I'm cautioning against Adam's approach is that it seems to me that using Scott's trick will localise the pain and ultimately decrease it.

[Rémi Bottinelli]

Yeah, I guess it's always about building the right generic api around your equalities and then applying it in the proof, rather than hopelessely trying to bruteforce things when needed.

[Kevin Buzzard]

Right, which is why I'm trusting Scott's intuition with full (which he makes an API for).

[Adam Topaz]

import combinatorics.quiver.basic
import logic.equiv.basic

universes u v w z

namespace quiver

structure iso (U V : Type*) [quiver.{u+1} U] [quiver.{v+1} V] extends prefunctor U V :=
(inv_prefunctor : V ⥤q U)
(left_inv : to_prefunctor ⋙q inv_prefunctor = 𝟭q _)
(right_inv : inv_prefunctor ⋙q to_prefunctor = 𝟭q _)

infix ` ≃q `:60 := iso

variables {U V W Z : Type*} [quiver.{u+1} U] [quiver.{v+1} V] [quiver.{w+1} W] [quiver.{z+1} Z]

instance : has_coe (iso U V) (prefunctor U V) :=
⟨iso.to_prefunctor⟩


def iso.refl (U : Type*) [quiver.{u+1} U] : iso U U := ⟨𝟭q _, 𝟭q _, rfl, rfl⟩

def iso.symm (φ : iso U V) : iso V U :=
⟨φ.inv_prefunctor, φ.to_prefunctor, φ.right_inv, φ.left_inv⟩

def iso.trans (φ : iso U V) (ψ : iso V W) : iso U W :=
{ to_prefunctor := φ.to_prefunctor ⋙q ψ.to_prefunctor,
  inv_prefunctor := ψ.inv_prefunctor ⋙q φ.inv_prefunctor,
  left_inv := by
  { rw [←prefunctor.comp_assoc, prefunctor.comp_assoc φ.to_prefunctor,
        ψ.left_inv, prefunctor.comp_id, φ.left_inv], },
  right_inv := by
  { rw [←prefunctor.comp_assoc, prefunctor.comp_assoc ψ.inv_prefunctor,
        φ.right_inv, prefunctor.comp_id, ψ.right_inv], }, }

def hom_equiv_of_eq {X X' Y Y' : U} (h1 : X = X') (h2 : Y = Y') :
  (X ⟶ Y) ≃ (X' ⟶ Y') :=
by { subst h1, subst h2 }

lemma hom_equiv_of_eq_eq {X X' Y Y' : U} (h1 : X = X') (h2 : Y = Y') (f : X ⟶ Y) :
  hom_equiv_of_eq h1 h2 f = by { subst h2, subst h1, exact f } :=
by { induction h1, induction h2, refl }

@[simps]
noncomputable
def iso.of_bijective_inverse_aux (φ : U ⥤q V) (hφobj : function.bijective φ.obj)
  (hφmap : ∀ (x y : U), function.bijective (φ.map : (x ⟶ y) → (φ.obj x ⟶ φ.obj y)) ) :
  V ⥤q U :=
let Eobj : U ≃ V := equiv.of_bijective _ hφobj,
    Ehom : Π X Y : U, (X ⟶ Y) ≃ (φ.obj X ⟶ φ.obj Y) := λ X Y, equiv.of_bijective _ (hφmap _ _)
in
{ obj := Eobj.symm,
  map := λ X Y, (Ehom _ _).symm ∘ hom_equiv_of_eq
    (show X = Eobj _, by rw Eobj.apply_symm_apply) (show Y = Eobj _, by rw Eobj.apply_symm_apply) }

noncomputable def iso.of_bijective (φ : U ⥤q V) (hφobj : function.bijective φ.obj)
  (hφmap : ∀ (x y : U), function.bijective (φ.map : (x ⟶ y) → (φ.obj x ⟶ φ.obj y)) ) :
  iso U V :=
{ to_prefunctor := φ,
  inv_prefunctor := iso.of_bijective_inverse_aux φ hφobj hφmap,
  left_inv := begin
    fapply prefunctor.ext,
    { intros X, simp },
    { intros X Y f, dsimp,
      generalize_proofs h _ _ h1 h2,
      induction h1,
      induction h2,
      dsimp,
      change (equiv.of_bijective _ h).symm (φ.map f) = f,
      simp }
  end,
  right_inv := begin
    fapply prefunctor.ext,
    { intros X, dsimp, apply (equiv.of_bijective φ.obj hφobj).apply_symm_apply },
    { intros X Y f, dsimp,
      let Eo := (equiv.of_bijective φ.obj hφobj),
      let E := equiv.of_bijective _ (hφmap (Eo.symm X) (Eo.symm Y)),
      apply E.symm.injective,
      simp,
      generalize_proofs h1 h2,
      apply hom_equiv_of_eq_eq h1 h2 f }
  end }

@[ext]
lemma iso.ext (φ ψ : iso U V) : φ.to_prefunctor = ψ.to_prefunctor → φ = ψ := sorry

end quiver

[Adam Topaz]

Some proofs are sloppy (e.g. I see at least one nonterminal simp)

[Rémi Bottinelli]

Great thanks! I'll try and clean this up and hopefully get the gist of it; Do you reckon iso.ext should be approachable using the same kind of approach ? (I have plenty of similar equalities I need to prove, so hopefully I can base them on your proof here)

[Adam Topaz]

I haven't tried iso.ext yet...

[Adam Topaz]

but it should be easier, I think?

[Adam Topaz]

the rule of thumb with such things is to try to use subst/rcases/induction on the equalities you want to be definitional equalities, and if that doesn't work, pull out an auxiliary lemma which includes these equalities as hypotheses (e.g. I had to do this with hom_equiv_of_eq_eq).

[Rémi Bottinelli]

Adam Topaz said:

I haven't tried iso.ext yet...

I's a good exercise, I'll try it later on!

[Rémi Bottinelli]

Adam Topaz said:

the rule of thumb with such things is to try to use subst/rcases/induction on the equalities you want to be definitional equalities, and if that doesn't work, pull out an auxiliary lemma which includes these equalities as hypotheses (e.g. I had to do this with hom_equiv_of_eq_eq).

I tried doing the first part, but then lean complained about inducting over non-variables, so I tried generalize, in order to revert the equalities to then be able to induct over them, but I think I was running in circles essentially.
And TIL generalize_proofs, which is something I sorely missed until now.

[Rémi Bottinelli]

Haha, finally managed to prove ext. I expect it can be golfed to something very much shorter.
OK, I can't get much shorter than that I guess:

@[ext]
lemma iso.to_prefunctor_ext (φ ψ : iso U V) : φ.to_prefunctor = ψ.to_prefunctor → φ = ψ :=
begin
  rintro h,
  apply iso.ext _ _ h,
  refine prefunctor.ext (λ X, ψ.to_equiv.injective _) (λ X Y f, ψ.to_equiv_hom.injective _),
  { dsimp,
    rw [ψ.obj_inv_obj_eq X, ←h, φ.obj_inv_obj_eq X], },
  { change ψ.map (φ.inv_prefunctor.map f) = ψ.map ((ψ.inv_prefunctor.map f).cast _ _),
    rw [prefunctor.map_cast, ψ.map_inv_map_eq_cast, hom.cast_cast, ←prefunctor.map_cast_eq_of_eq h,
        φ.map_inv_map_eq_cast, hom.cast_cast], },
end