chore(CategoryTheory): dualize to right liftings (#40499)

This PR adds api for `RightLift`s, following exactly the case of `LeftLift`s.

Author: FernandoChu

Mathlib/CategoryTheory/Bicategory/Extension.lean

@@ -313,7 +313,7 @@ abbrev mk (h : b ⟶ c) (counit : f ≫ h ⟶ g) : RightExtension f g :=
 /-- To construct a morphism between right extensions, we need a 2-morphism between the extensions,
 and to check that it is compatible with the counits. -/
 abbrev homMk {s t : RightExtension f g} (η : s.extension ⟶ t.extension)
-    (w : f ◁ η ≫ t.counit = s.counit) : s ⟶ t :=
+    (w : f ◁ η ≫ t.counit = s.counit := by cat_disch) : s ⟶ t :=
   CostructuredArrow.homMk η w
 
 @[reassoc (attr := simp)]
@@ -355,22 +355,100 @@ abbrev counit (t : RightLift f g) : t.lift ≫ f ⟶ g := t.hom
 abbrev mk (h : c ⟶ b) (counit : h ≫ f ⟶ g) : RightLift f g :=
   CostructuredArrow.mk counit
 
+variable {s t : RightLift f g}
+
 /-- To construct a morphism between right lifts, we need a 2-morphism between the lifts,
 and to check that it is compatible with the counits. -/
-abbrev homMk {s t : RightLift f g} (η : s.lift ⟶ t.lift) (w : η ▷ f ≫ t.counit = s.counit) :
+abbrev homMk (η : s.lift ⟶ t.lift) (w : η ▷ f ≫ t.counit = s.counit := by cat_disch) :
     s ⟶ t :=
   CostructuredArrow.homMk η w
 
 @[reassoc (attr := simp)]
-theorem w {s t : RightLift f g} (h : s ⟶ t) :
-    h.left ▷ f ≫ t.counit = s.counit :=
+theorem w (h : s ⟶ t) : h.left ▷ f ≫ t.counit = s.counit :=
   CostructuredArrow.w h
 
 /-- The right lift along the identity. -/
 def alongId (g : c ⟶ a) : RightLift (𝟙 a) g := .mk _ (ρ_ g).hom
 
 instance : Inhabited (RightLift (𝟙 a) g) := ⟨alongId g⟩
 
+/-- Construct a right lift along `g : c ⟶ a` from a right lift along `𝟙 c ≫ g`. -/
+@[simps!]
+def ofIdComp (t : RightLift f (𝟙 c ≫ g)) : RightLift f g :=
+  mk (lift t) (counit t ≫ (λ_ _).hom)
+
+/-- Whisker a 1-morphism to a lift.
+```
+                    b
+                  ◹ |
+           lift /   |      | counit
+              /     | f    ▽
+            /       ▽
+x - - - ▷ c - - - ▷ a
+     h         g
+```
+-/
+def whisker (t : RightLift f g) {x : B} (h : x ⟶ c) : RightLift f (h ≫ g) :=
+  .mk _ <| (α_ _ _ _).hom ≫ h ◁ t.counit
+
+@[simp]
+theorem whisker_lift (t : RightLift f g) {x : B} (h : x ⟶ c) :
+    (t.whisker h).lift = h ≫ t.lift :=
+  rfl
+
+@[simp]
+theorem whisker_counit (t : RightLift f g) {x : B} (h : x ⟶ c) :
+    (t.whisker h).counit = (α_ h t.lift f).hom ≫ h ◁ t.counit :=
+  rfl
+
+/-- Whiskering a 1-morphism is a functor. -/
+@[simps]
+def whiskering {x : B} (h : x ⟶ c) : RightLift f g ⥤ RightLift f (h ≫ g) where
+  obj t := t.whisker h
+  map η := RightLift.homMk (h ◁ η.left) <| by
+    dsimp only [whisker_lift, whisker_counit]
+    rw [← RightLift.w η]
+    simp [-RightLift.w]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Define a morphism between right lifts by cancelling the whiskered identities. -/
+@[simps! left]
+def whiskerIdCancel
+    (t : RightLift f (𝟙 c ≫ g)) {s : RightLift f g} (τ : s.whisker (𝟙 c) ⟶ t) :
+    s ⟶ t.ofIdComp :=
+  RightLift.homMk ((λ_ _).inv ≫ τ.left)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Construct a morphism between whiskered lifts. -/
+@[simps! left]
+def whiskerHom (i : s ⟶ t) {x : B} (h : x ⟶ c) :
+    s.whisker h ⟶ t.whisker h :=
+  CostructuredArrow.homMk (h ◁ i.left) <| by
+    rw [← cancel_epi (α_ h _ _).inv]
+    calc
+      _ = h ◁ (i.left ▷ f ≫ t.counit) := by simp [-RightLift.w]
+      _ = h ◁ s.counit := congrArg (h ◁ ·) (RightLift.w i)
+      _ = _ := by simp
+
+/-- Construct an isomorphism between whiskered lifts. -/
+def whiskerIso (i : s ≅ t) {x : B} (h : x ⟶ c) :
+    s.whisker h ≅ t.whisker h :=
+  Iso.mk (whiskerHom i.hom h) (whiskerHom i.inv h)
+    (CostructuredArrow.hom_ext _ _ <|
+      calc
+        _ = h ◁ (i.hom ≫ i.inv).left := by simp [-Iso.hom_inv_id]
+        _ = 𝟙 _ := by simp [Iso.hom_inv_id])
+    (CostructuredArrow.hom_ext _ _ <|
+      calc
+        _ = h ◁ (i.inv ≫ i.hom).left := by simp [-Iso.inv_hom_id]
+        _ = 𝟙 _ := by simp [Iso.inv_hom_id])
+
+set_option backward.defeqAttrib.useBackward true in
+/-- The isomorphism between right lifts induced by a left unitor. -/
+@[simps! hom_left inv_left]
+def whiskerOfIdCompIsoSelf (t : RightLift f g) : (t.whisker (𝟙 c)).ofIdComp ≅ t :=
+  CostructuredArrow.isoMk (λ_ (lift t))
+
 end RightLift
 
 end Bicategory

Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean

@@ -248,6 +248,88 @@ variable {f : b ⟶ a} {g : c ⟶ a}
 /-- A right Kan lift of `g` along `f` is a terminal object in `RightLift f g`. -/
 abbrev IsKan (t : RightLift f g) := t.IsUniversal
 
+/-- An absolute right Kan lift is a Kan lift such that every 1-morphism commutes with it. -/
+abbrev IsAbsKan (t : RightLift f g) :=
+  ∀ {x : B} (h : x ⟶ c), IsKan (t.whisker h)
+
+namespace IsKan
+
+variable {s t : RightLift f g}
+
+/-- To show that a right lift `t` is a Kan lift, we need to show that for every right lift `s`
+there is a unique morphism `s ⟶ t`. -/
+abbrev mk (desc : ∀ s, s ⟶ t) (w : ∀ s τ, τ = desc s) :
+    IsKan t :=
+  .ofUniqueHom desc w
+
+/-- The family of 2-morphisms into a right Kan lift. -/
+abbrev desc (H : IsKan t) (s : RightLift f g) : s.lift ⟶ t.lift :=
+  CostructuredArrow.IsUniversal.lift H s
+
+@[reassoc (attr := simp)]
+theorem fac (H : IsKan t) (s : RightLift f g) :
+    H.desc s ▷ f ≫ t.counit = s.counit :=
+  CostructuredArrow.IsUniversal.fac H s
+
+/-- Two 2-morphisms into a right Kan lift are equal if their compositions with
+each triangle 2-morphism are equal. -/
+theorem hom_ext (H : IsKan t) {k : c ⟶ b} {τ τ' : k ⟶ t.lift}
+    (w : τ ▷ f ≫ t.counit = τ' ▷ f ≫ t.counit) : τ = τ' :=
+  CostructuredArrow.IsUniversal.hom_ext H w
+
+/-- Kan lifts on `g` along `f` are unique up to isomorphism. -/
+def uniqueUpToIso (P : IsKan s) (Q : IsKan t) : s ≅ t :=
+  Limits.IsTerminal.uniqueUpToIso P Q
+
+@[simp]
+theorem uniqueUpToIso_hom_left (P : IsKan s) (Q : IsKan t) :
+    (uniqueUpToIso P Q).hom.left = Q.desc s := rfl
+
+@[simp]
+theorem uniqueUpToIso_inv_left (P : IsKan s) (Q : IsKan t) :
+    (uniqueUpToIso P Q).inv.left = P.desc t := rfl
+
+/-- Transport evidence that a right lift is a Kan lift across an isomorphism of lifts. -/
+def ofIsoKan (P : IsKan s) (i : s ≅ t) : IsKan t :=
+  Limits.IsTerminal.ofIso P i
+
+set_option backward.isDefEq.respectTransparency false in
+/-- If `t : RightLift f (𝟙 c ≫ g)` is a Kan lift, then `t.ofIdComp : RightLift f g` is also
+a Kan lift. -/
+def ofIdComp (t : RightLift f (𝟙 c ≫ g)) (P : IsKan t) : IsKan t.ofIdComp :=
+  .mk (fun s ↦ t.whiskerIdCancel <| P.from (s.whisker (𝟙 c))) <| by
+    intro s τ
+    ext
+    apply P.hom_ext
+    simp [← RightLift.w τ]
+
+/-- If `s ≅ t` and `IsKan (s.whisker h)`, then `IsKan (t.whisker h)`. -/
+def whiskerOfCommute (s t : RightLift f g) (i : s ≅ t) {x : B} (h : x ⟶ c)
+    (P : IsKan (s.whisker h)) :
+    IsKan (t.whisker h) :=
+  P.ofIsoKan <| whiskerIso i h
+
+end IsKan
+
+namespace IsAbsKan
+
+variable {s t : RightLift f g}
+
+/-- The family of 2-morphisms into an absolute right Kan lift. -/
+abbrev desc (H : IsAbsKan t) {x : B} {h : x ⟶ c} (s : RightLift f (h ≫ g)) :
+    s.lift ⟶ h ≫ t.lift :=
+  (H h).desc s
+
+/-- An absolute right Kan lift is a right Kan lift. -/
+def isKan (H : IsAbsKan t) : IsKan t :=
+  ((H (𝟙 c)).ofIdComp _).ofIsoKan <| whiskerOfIdCompIsoSelf t
+
+/-- Transport evidence that a right lift is a Kan lift across an isomorphism of lifts. -/
+def ofIsoAbsKan (P : IsAbsKan s) (i : s ≅ t) : IsAbsKan t :=
+  fun h ↦ (P h).ofIsoKan (whiskerIso i h)
+
+end IsAbsKan
+
 end RightLift
 
 end Bicategory