Theorems · Theorem · category theory

CategoryTheory.Adjunction.CoreHomEquiv.mk.inj

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)}
  {homEquiv_naturality_left_symm :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam}
  {homEquiv_naturality_right :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam}
  {homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)}
  {homEquiv_naturality_left_symm_1 :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv_1 X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv_1 X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam}
  {homEquiv_naturality_right_1 :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv_1 X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv_1 X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam},
  { homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
        homEquiv_naturality_right := homEquiv_naturality_right } =
      { homEquiv := homEquiv_1, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm_1,
        homEquiv_naturality_right := homEquiv_naturality_right_1 } →
    homEquiv = homEquiv_1

Defined in

Mathlib.CategoryTheory.Adjunction.Basic

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound