Theorems · Theorem · category theory

CategoryTheory.CatCenter.localization_app

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (r : CategoryTheory.CatCenter C) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_2 : L.IsLocalization W] (X : C), (r.localization L W).app (L.obj X) = L.map (r.app X)

Defined in

Mathlib.CategoryTheory.Center.Localization

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalization