Theorems · Definition · category theory

CategoryTheory.wideSubcategoryInclusion

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : P.IsMultiplicative] → CategoryTheory.Functor (CategoryTheory.WideSubcategory P) C

The forgetful functor from a wide subcategory into the original category ("forgetting" the condition).

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

2 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative