Theorems · Theorem · category theory

CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj.congr_simp

∀ {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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B)
  (F' : CategoryTheory.Functor C A) (adj₁ adj₁_1 : F ⊣ U),
  adj₁ = adj₁_1 →
    ∀ (adj₂ adj₂_1 : F' ⊣ R.comp U),
      adj₂ = adj₂_1 →
        ∀ [inst_3 : CategoryTheory.Limits.HasReflexiveCoequalizers A] (Y Y_1 : B),
          Y = Y_1 →
            CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ Y =
              CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁_1 adj₂_1 Y_1

Defined in

Mathlib.CategoryTheory.Adjunction.Lifting.Left

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasReflexiveCoequalizers