@[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]
def
category_theory.induced_category.has_coe_to_sort
{C : Type u₁}
{D : Type u₂}
[category_theory.category D]
(F : C → D)
[has_coe_to_sort D] :
Equations
- category_theory.induced_category.has_coe_to_sort F = {S := has_coe_to_sort.S D _inst_2, coe := λ (c : category_theory.induced_category D F), ↥(F c)}
@[instance]
def
category_theory.induced_category.category
{C : Type u₁}
{D : Type u₂}
[category_theory.category D]
(F : C → D) :
Equations
- category_theory.induced_category.category F = {to_category_struct := {to_has_hom := {hom := λ (X Y : category_theory.induced_category D F), F X ⟶ F Y}, id := λ (X : category_theory.induced_category D F), 𝟙 (F X), comp := λ (_x _x_1 _x_2 : category_theory.induced_category D F) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), f ≫ g}, id_comp' := _, comp_id' := _, assoc' := _}
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
- category_theory.induced_functor F = {obj := F, map := λ (x y : category_theory.induced_category D F) (f : x ⟶ y), f, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.induced_functor_obj
{C : Type u₁}
{D : Type u₂}
[category_theory.category D]
(F : C → D)
(a : C) :
(category_theory.induced_functor F).obj a = F a
@[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) :
(category_theory.induced_functor F).map f = f
@[instance]
def
category_theory.induced_category.full
{C : Type u₁}
{D : Type u₂}
[category_theory.category D]
(F : C → D) :
Equations
- category_theory.induced_category.full F = {preimage := λ (x y : category_theory.induced_category D F) (f : (category_theory.induced_functor F).obj x ⟶ (category_theory.induced_functor F).obj y), f, witness' := _}
@[instance]
def
category_theory.induced_category.faithful
{C : Type u₁}
{D : Type u₂}
[category_theory.category D]
(F : C → D) :
@[instance]
def
category_theory.induced_category.groupoid
{C : Type u₁}
(D : Type u₂)
[category_theory.groupoid D]
(F : C → D) :
Equations
- category_theory.induced_category.groupoid D F = {to_category := {to_category_struct := category_theory.category.to_category_struct (category_theory.induced_category.category F), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : category_theory.induced_category D F) (f : X ⟶ Y), category_theory.groupoid.inv f, inv_comp' := _, comp_inv' := _}
@[instance]
def
category_theory.full_subcategory
{C : Type u₂}
[category_theory.category C]
(Z : C → Prop) :
category_theory.category {X // Z X}
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.
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).
@[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} :
@[instance]
def
category_theory.full_subcategory.full
{C : Type u₂}
[category_theory.category C]
(Z : C → Prop) :
@[instance]
def
category_theory.full_subcategory.faithful
{C : Type u₂}
[category_theory.category C]
(Z : C → Prop) :