Theorems · Theorem · category theory

CategoryTheory.wideInducedFunctor_map

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative]
  {x x_1 : CategoryTheory.InducedWideCategory D F P} (f : x ⟶ x_1),
  (CategoryTheory.wideInducedFunctor F P).map f = f.hom

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative