Theorems · Theorem · category theory

CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply

∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B)
  (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U')
  [inst_3 : CategoryTheory.Limits.HasCoreflexiveEqualizers C]
  (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) (Y : C) (X : B)
  (a : Y ⟶ CategoryTheory.LiftRightAdjoint.constructRightAdjointObj L U' adj₁ adj₂ X),
  (CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv L U' adj₁ adj₂ h Y X) a =
    (CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.LiftRightAdjoint.unitEqualises adj₁ h X) (L.obj Y)).symm
      ⟨(adj₁.homEquiv (L.obj Y) (F.obj X))
          ((adj₂.homEquiv Y (F.obj X)).symm
            ↑((CategoryTheory.Limits.Fork.IsLimit.homIso
                  (CategoryTheory.Limits.limit.isLimit
                    (CategoryTheory.Limits.parallelPair (U'.map (F.map (adj₁.unit.app X)))
                      (CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X)))
                  Y)
                a)),
        ⋯⟩

Defined in

Mathlib.CategoryTheory.Adjunction.Lifting.Right

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoreflexiveEqualizers