Theorems · Inductive type · category theory

CategoryTheory.LocalizerMorphism

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        CategoryTheory.MorphismProperty C₁ → CategoryTheory.MorphismProperty C₂ → Type (max (max (max u₁ u₂) v₁) v₂)

If W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂, a LocalizerMorphism W₁ W₂ is the datum of a functor C₁ ⥤ C₂ which sends morphisms in W₁ to morphisms in W₂

Defined in

Mathlib.CategoryTheory.Localization.LocalizerMorphism

Cited by

161 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 8 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category