Theorems · Definition · category theory

CategoryTheory.Subobject.underlying

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Functor (CategoryTheory.Subobject X) C

Use choice to pick a representative underlying object in C for any Subobject X. Prefer to use the coercion P : C rather than explicitly writing underlying.obj P.

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

211 results in Mathlib

Foundations

Depth 36 from the axioms, rests on 244 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category