mathlib documentation

category_theory.full_subcategory

@[nolint]
def category_theory.induced_category {C : Type u₁} (D : Type u₂) [category_theory.category D] :
(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) (a : 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} :