Theorems · Theorem · category theory

CategoryTheory.Adjunction.CoreHomEquiv.mk.sizeOf_spec

∀ {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} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (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),
  sizeOf
      { homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
        homEquiv_naturality_right := homEquiv_naturality_right } =
    1

Defined in

Mathlib.CategoryTheory.Adjunction.Basic

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategorySizeOfSizeOf