InverseLimitEventualHom.lean

theorem transported_refinement_factorization
    {C : Type v} [Category.{w} C] {X Y U V U' V' A B : C}
    (e₀ : X ≅ U) (f₀ : Y ≅ V) (e₁ : X ≅ U') (f₁ : Y ≅ V')
    (p : U ≅ A) (q : V ≅ B) (r : U' ≅ A) (t : V' ≅ B)
    (a : X ⟶ Y) (b : A ⟶ B)
    (he : e₁.hom ≫ r.hom = e₀.hom ≫ p.hom)
    (hf : f₁.hom ≫ t.hom = f₀.hom ≫ q.hom)
    (hb : p.hom ≫ b = (e₀.inv ≫ a ≫ f₀.hom) ≫ q.hom) :
    a = e₁.hom ≫ (r.hom ≫ b ≫ t.inv) ≫ f₁.inv

theorem comparison_composition_hom_app {i j k : I}
    (hij : i ≤ j) (hjk : j ≤ k) (A : stage D i) :
    (comparison D s (hij.trans hjk)).hom.app A ≫
        (toLimit D s k).map ((compositionIso D hij hjk).hom.app A) =
      (comparison D s hij).hom.app A ≫
        (comparison D s hjk).hom.app ((transition D hij).obj A)

theorem eventualHom
    (i j : I) (A : stage D i) (B : stage D j)
    (f : (toLimit D s i).obj A ⟶ (toLimit D s j).obj B) :
    ∃ (k : I) (hik : i ≤ k) (hjk : j ≤ k)
      (g : (transition D hik).obj A ⟶ (transition D hjk).obj B),
      f = (comparison D s hik).hom.app A ≫ (toLimit D s k).map g ≫
        (comparison D s hjk).inv.app B