feat(CategoryTheory/Adjunction/PartialAdjunction): add symm naturality lemmas for HomEquiv and lift functor (#30143)

Add two lemmas for `partialRightAdjointHomEquiv` to help work with `partialRightAdjointHomEquiv.symm`.

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: staroperator <143908816+staroperator@users.noreply.github.com>
Co-authored-by: Michael Rothgang <10105016+grunweg@users.noreply.github.com>
Co-authored-by: Jeremy Tan Jie Rui <54175463+Parcly-Taxel@users.noreply.github.com>
Co-authored-by: JasperMS <197499579+JasperMS@users.noreply.github.com>
Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <5110976+kebekus@users.noreply.github.com>
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Rado Kirov <rkirov@gmail.com>
Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com>
Co-authored-by: Attila Gáspár <58485900+gasparattila@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Thomas Browning <13339017+tb65536@users.noreply.github.com>
Co-authored-by: SnirBroshi <26556598+SnirBroshi@users.noreply.github.com>
Co-authored-by: Dagur Asgeirsson <25623829+dagurtomas@users.noreply.github.com>
Co-authored-by: Floris van Doorn <vdoorn@math.uni-bonn.de>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: PMKielstra <4313413+PMKielstra@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Zhao Yuyang 赵雨扬 <zhao.yu-yang@foxmail.com>
Co-authored-by: Harald Husum <harald.husum@gmail.com>
Co-authored-by: Yury Kudryashov <162619279+yury-harmonic@users.noreply.github.com>
Co-authored-by: Christian Krause <86738237+Bergschaf@users.noreply.github.com>

Author: 26 people

Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

@@ -103,6 +103,20 @@ lemma partialLeftAdjointHomEquiv_map_comp {X X' : F.PartialLeftAdjointSource} {Y
   rw [partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc,
     ← partialLeftAdjointHomEquiv_comp, id_comp]
 
+@[reassoc]
+lemma partialLeftAdjointHomEquiv_symm_comp {X : F.PartialLeftAdjointSource} {Y Y' : D}
+    (f : X.obj ⟶ F.obj Y) (g : Y ⟶ Y') :
+    F.partialLeftAdjointHomEquiv.symm f ≫ g = F.partialLeftAdjointHomEquiv.symm (f ≫ F.map g) :=
+  CorepresentableBy.homEquiv_symm_comp ..
+
+@[reassoc]
+lemma partialLeftAdjointHomEquiv_comp_symm {X X' : F.PartialLeftAdjointSource} {Y : D}
+    (f : X'.obj ⟶ F.obj Y) (g : X ⟶ X') :
+    F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f =
+    F.partialLeftAdjointHomEquiv.symm (g ≫ f) := by
+  rw [Equiv.eq_symm_apply, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map,
+    assoc, ← partialLeftAdjointHomEquiv_comp, id_comp, Equiv.apply_symm_apply]
+
 /-- Given `F : D ⥤ C`, this is the partial adjoint functor `F.PartialLeftAdjointSource ⥤ D`. -/
 @[simps]
 noncomputable def partialLeftAdjoint : F.PartialLeftAdjointSource ⥤ D where
@@ -244,6 +258,20 @@ lemma partialRightAdjointHomEquiv_map_comp {X : C} {Y Y' : F.PartialRightAdjoint
   rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map,
     ← assoc, ← partialRightAdjointHomEquiv_comp, comp_id]
 
+@[reassoc]
+lemma partialRightAdjointHomEquiv_comp_symm {X X' : C} {Y : F.PartialRightAdjointSource}
+    (f : F.obj X' ⟶ Y.obj) (g : X ⟶ X') :
+    g ≫ F.partialRightAdjointHomEquiv.symm f =
+      F.partialRightAdjointHomEquiv.symm (F.map g ≫ f) :=
+  RepresentableBy.comp_homEquiv_symm ..
+
+@[reassoc]
+lemma partialRightAdjointHomEquiv_symm_comp {X : C} {Y Y' : F.PartialRightAdjointSource}
+    (f : F.obj X ⟶ Y.obj) (g : Y ⟶ Y') :
+    F.partialRightAdjointHomEquiv.symm f ≫ F.partialRightAdjointMap g =
+      F.partialRightAdjointHomEquiv.symm (f ≫ g) := by
+  simp [Equiv.eq_symm_apply, partialRightAdjointHomEquiv_map_comp]
+
 /-- Given `F : C ⥤ D`, this is the partial adjoint functor `F.PartialLeftAdjointSource ⥤ C`. -/
 @[simps]
 noncomputable def partialRightAdjoint : F.PartialRightAdjointSource ⥤ C where