[Merged by Bors] - feat: port CategoryTheory.Adjunction.Lifting

[int-y1]

---

todo:

• constructLeftAdjoint error
  the error likely involves constructLeftAdjointEquiv_apply and @[simps (config := { rhsMd := semireducible })]

[semorrison]

Oh dear! It's an inscrutable block of rewrites that goes bad part way through.

@b-mehta, any chance you'd be able to look at this?

[kbuzzard]

As int-y1 suggests, I think the problem is that the type of constructLeftAdjointEquiv_apply is completely different in Lean 3 than in Lean 4. I don't know what @[simps (config := { rhsMd := semireducible })] did in Lean 3 but I can see that the type of the Lean 3 theorem is

construct_left_adjoint_equiv_apply :
  ∀ {A : Type u_4} {B : Type u_5} {C : Type u_6} [_inst_1 : category A] [_inst_2 : category B]
  [_inst_3 : category C]
  {U : B ⥤ C} {F : C ⥤ B} (R : A ⥤ B) (F' : C ⥤ A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R ⋙ U)
  [_inst_4 : has_reflexive_coequalizers A]
  [_inst_5 : Π (X : B), regular_epi (adj₁.counit.app X)] (Y : A) (X : B)
  (ᾰ : construct_left_adjoint_obj R F' adj₁ adj₂ X ⟶ Y),
    ⇑(construct_left_adjoint_equiv R F' adj₁ adj₂ Y X) ᾰ =
      (⇑((cofork.is_colimit.hom_iso (counit_coequalises adj₁ X) (R.obj Y)).symm) ∘
         ⇑(((cofork.is_colimit.hom_iso
                (colimit.is_colimit
                   (parallel_pair (F'.map (U.map (adj₁.counit.app X))) (other_map R F' adj₁ adj₂ X)))
                Y).trans
               ((adj₂.hom_equiv (U.obj X) Y).subtype_equiv _)).trans
              ((adj₁.hom_equiv (U.obj X) (R.obj Y)).symm.subtype_equiv _)))

which is pretty much what you would expect from the definition. In Lean 4 the type is totally different: it's

CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv_apply.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} {B : Type u₂}
  {C : Type u₃} [inst✝ : Category A] [inst✝¹ : Category B] [inst✝² : Category C] {U : B ⥤ C} {F : C ⥤ B} (R : A ⥤ B)
  (F' : C ⥤ A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R ⋙ U) [inst✝³ : HasReflexiveCoequalizers A]
  [inst✝⁴ : (X : B) → RegularEpi (adj₁.counit.app X)] (Y : A) (X : B)
  (a✝ : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) :
  ↑(constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) a✝ =
    ↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
      {
        val :=
          F.map
              (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                ↑(↑(Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                    a✝)) ≫
            adj₁.counit.app (R.obj Y),
        property :=
          (_ :
            (fun b ↦ F.map (U.map (adj₁.counit.app X)) ≫ b = adj₁.counit.app (F.obj (U.obj X)) ≫ b)
              (F.map
                  (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                    ↑(↑(Cofork.IsColimit.homIso
                            (colimit.isColimit
                              (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                            Y)
                        a✝)) ≫
                adj₁.counit.app (R.obj Y))) }

and so after rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply] the goal is totally different in Lean 3 than in Lean 4. I suspect the path of least resistance here is to figure out how to make Lean 4 simps make the same lemma as Lean 3 simps, or just make the Lean 3 lemma manually. I tried this with

lemma construct_left_adjoint_equiv_apply' [∀ (X : B), RegularEpi (adj₁.counit.app X)] (Y : A) (X : B)
  (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) :
    (constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) a =
      (↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm) ∘
         ⇑(((Cofork.IsColimit.homIso
                (colimit.isColimit
                   (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                Y).trans
               ((adj₂.homEquiv (U.obj X) Y).subtypeEquiv _)).trans
              ((adj₁.homEquiv (U.obj X) (R.obj Y)).symm.subtypeEquiv _))) := sorry

but I couldn't get the statement to typecheck. If there is just some quick way of making simps behave in the same way as Lean 3 then it would save all this bother.

[mattrobball]

Or just bull ahead naively...

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style