Theorems · Definition · category theory

CategoryTheory.InducedWideCategory

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

InducedWideCategory D F P, where F : C → D, is a typeclass synonym for C, which provides a category structure so that the morphisms X ⟶ Y are the morphisms in D from F X to F Y which satisfy a property P : MorphismProperty D that is multiplicative.

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

12 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative