Theorems · Theorem · category theory

CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] (J : Type)
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] [inst_4 : W.IsStableUnderProductsOfShape J]
  [inst_5 : W.ContainsIdentities] [inst_6 : Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C),
  (CategoryTheory.Localization.HasProductsOfShapeAux.adj L W J).counit.app (F.comp L) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).map
        ((CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso L W J).hom.app F))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).hom.app (CategoryTheory.Limits.lim.obj F))
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))

Defined in

Mathlib.CategoryTheory.Localization.FiniteProducts

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Limits.HasProductsOfShapeCategoryTheory.MorphismProperty.IsStableUnderProductsOfShapeCategoryTheory.MorphismProperty.ContainsIdentitiesFinite