mathlib documentation

category_theory.full_subcategory

@[nolint]
def category_theory.induced_category {C : Type u₁} (D : Type u₂) [category_theory.category D] (F : C → D) :
Type u₁

induced_category D F, 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.

Equations
@[instance]
Equations
def category_theory.induced_functor {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) :

The forgetful functor from an induced category to the original category, forgetting the extra data.

Equations
@[simp]
theorem category_theory.induced_functor_obj {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) (ᾰ : C) :
@[simp]
theorem category_theory.induced_functor_map {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) (x y : category_theory.induced_category D F) (f : x y) :
@[instance]
def category_theory.full_subcategory {C : Type u₂} [category_theory.category C] (Z : C → Prop) :

The category structure on a subtype; morphisms just ignore the property.

See https://stacks.math.columbia.edu/tag/001D. We do not define 'strictly full' subcategories.

Equations
def category_theory.full_subcategory_inclusion {C : Type u₂} [category_theory.category C] (Z : C → Prop) :
{X // Z X} C

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

Equations
@[simp]
theorem category_theory.full_subcategory_inclusion.obj {C : Type u₂} [category_theory.category C] (Z : C → Prop) {X : {X // Z X}} :
@[simp]
theorem category_theory.full_subcategory_inclusion.map {C : Type u₂} [category_theory.category C] (Z : C → Prop) {X Y : {X // Z X}} {f : X Y} :