Induced categories and full subcategories

Given a category D and a function F : C → D from a type C to the objects of D, there is an essentially unique way to give C a category structure such that F becomes a fully faithful functor, namely by taking $$ Hom_C(X, Y) = Hom_D(FX, FY) $$. We call this the category induced from D along F.

As a special case, if C is a subtype of D, this produces the full subcategory of D on the objects belonging to C. In general the induced category is equivalent to the full subcategory of D on the image of F.

Implementation notes

It looks odd to make D an explicit argument of InducedCategory, when it is determined by the argument F anyways. The reason to make D explicit is in order to control its syntactic form, so that instances like InducedCategory.has_forget₂ (elsewhere) refer to the correct form of D. This is used to set up several algebraic categories like

def CommMon : Type (u+1) := InducedCategory Mon (Bundled.map @CommMonoid.toMonoid) -- not InducedCategory (Bundled Monoid) (Bundled.map @CommMonoid.toMonoid), -- even though MonCat = Bundled Monoid!

def CategoryTheory.InducedCategory {C : Type u₁} (D : Type u₂) (_F : C → D) : Type u₁

InducedCategory 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

• CategoryTheory.InducedCategory D _F = C

instance CategoryTheory.InducedCategory.hasCoeToSort {C : Type u₁} {D : Type u₂} (F : C → D) {α : Sort u_1} [CoeSort D α] : CoeSort (CategoryTheory.InducedCategory D F) α

Equations

• CategoryTheory.InducedCategory.hasCoeToSort F = { coe := fun (c : CategoryTheory.InducedCategory D F) => CoeSort.coe (F c) }

instance CategoryTheory.InducedCategory.category {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : CategoryTheory.Category.{v, u₁} (CategoryTheory.InducedCategory D F)

Equations

• CategoryTheory.InducedCategory.category F = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.inducedFunctor_map {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : ∀ {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y), (CategoryTheory.inducedFunctor F).map f = f

@[simp]

theorem CategoryTheory.inducedFunctor_obj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : ∀ (a : C), (CategoryTheory.inducedFunctor F).obj a = F a

def CategoryTheory.inducedFunctor {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : CategoryTheory.Functor (CategoryTheory.InducedCategory D F) D

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

Equations

• CategoryTheory.inducedFunctor F = { toPrefunctor := { obj := F, map := fun {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y) => f }, map_id := ⋯, map_comp := ⋯ }

instance CategoryTheory.InducedCategory.full {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : CategoryTheory.Full (CategoryTheory.inducedFunctor F)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.InducedCategory.faithful {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) : CategoryTheory.Faithful (CategoryTheory.inducedFunctor F)

Equations

• ⋯ = ⋯

theorem CategoryTheory.FullSubcategory.ext_iff {C : Type u₁} {Z : C → Prop} (x : CategoryTheory.FullSubcategory Z) (y : CategoryTheory.FullSubcategory Z) : x = y ↔ x.obj = y.obj

theorem CategoryTheory.FullSubcategory.ext {C : Type u₁} {Z : C → Prop} (x : CategoryTheory.FullSubcategory Z) (y : CategoryTheory.FullSubcategory Z) (obj : x.obj = y.obj) : x = y

structure CategoryTheory.FullSubcategory {C : Type u₁} (Z : C → Prop) : Type u₁

A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use actual subtypes since the simp-normal form ↑X of X.val does not work well for full subcategories.

See . We do not define 'strictly full' subcategories.

• obj : C

  The category of which this is a full subcategory

• property : Z self.obj

  The predicate satisfied by all objects in this subcategory

instance CategoryTheory.FullSubcategory.category {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) : CategoryTheory.Category.{v, u₁} (CategoryTheory.FullSubcategory Z)

Equations

• CategoryTheory.FullSubcategory.category Z = CategoryTheory.InducedCategory.category CategoryTheory.FullSubcategory.obj

theorem CategoryTheory.FullSubcategory.id_def {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) (X : CategoryTheory.FullSubcategory Z) : CategoryTheory.CategoryStruct.id X = CategoryTheory.CategoryStruct.id X.obj

theorem CategoryTheory.FullSubcategory.comp_def {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) {X : CategoryTheory.FullSubcategory Z✝} {Y : CategoryTheory.FullSubcategory Z✝} {Z : CategoryTheory.FullSubcategory Z✝} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g

def CategoryTheory.fullSubcategoryInclusion {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) : CategoryTheory.Functor (CategoryTheory.FullSubcategory Z) C

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

Equations

• CategoryTheory.fullSubcategoryInclusion Z = CategoryTheory.inducedFunctor CategoryTheory.FullSubcategory.obj

@[simp]

theorem CategoryTheory.fullSubcategoryInclusion.obj {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) {X : CategoryTheory.FullSubcategory Z} : (CategoryTheory.fullSubcategoryInclusion Z).obj X = X.obj

@[simp]

theorem CategoryTheory.fullSubcategoryInclusion.map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) {X : CategoryTheory.FullSubcategory Z} {Y : CategoryTheory.FullSubcategory Z} {f : X ⟶ Y} : (CategoryTheory.fullSubcategoryInclusion Z).map f = f

instance CategoryTheory.FullSubcategory.full {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) : CategoryTheory.Full (CategoryTheory.fullSubcategoryInclusion Z)

Equations

• CategoryTheory.FullSubcategory.full Z = CategoryTheory.InducedCategory.full CategoryTheory.FullSubcategory.obj

instance CategoryTheory.FullSubcategory.faithful {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (Z : C → Prop) : CategoryTheory.Faithful (CategoryTheory.fullSubcategoryInclusion Z)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.FullSubcategory.map_obj_obj {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : C → Prop} {Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) (X : CategoryTheory.FullSubcategory Z) : ((CategoryTheory.FullSubcategory.map h).obj X).obj = X.obj

@[simp]

theorem CategoryTheory.FullSubcategory.map_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : C → Prop} {Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) : ∀ {X Y : CategoryTheory.FullSubcategory Z} (f : X ⟶ Y), (CategoryTheory.FullSubcategory.map h).map f = f

def CategoryTheory.FullSubcategory.map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : C → Prop} {Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) : CategoryTheory.Functor (CategoryTheory.FullSubcategory Z) (CategoryTheory.FullSubcategory Z')

An implication of predicates Z → Z' induces a functor between full subcategories.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.FullSubcategory.full_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : C → Prop} {Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) : CategoryTheory.Full (CategoryTheory.FullSubcategory.map h)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.FullSubcategory.faithful_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : C → Prop} {Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) : CategoryTheory.Faithful (CategoryTheory.FullSubcategory.map h)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.FullSubcategory.map_inclusion {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : C → Prop} {Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) : CategoryTheory.Functor.comp (CategoryTheory.FullSubcategory.map h) (CategoryTheory.fullSubcategoryInclusion Z') = CategoryTheory.fullSubcategoryInclusion Z

@[simp]

theorem CategoryTheory.FullSubcategory.lift_obj_obj {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : ((CategoryTheory.FullSubcategory.lift P F hF).obj X).obj = F.obj X

@[simp]

theorem CategoryTheory.FullSubcategory.lift_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.FullSubcategory.lift P F hF).map f = F.map f

def CategoryTheory.FullSubcategory.lift {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : CategoryTheory.Functor C (CategoryTheory.FullSubcategory P)

A functor which maps objects to objects satisfying a certain property induces a lift through the full subcategory of objects satisfying that property.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FullSubcategory.lift_comp_inclusion_eq {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : CategoryTheory.Functor.comp (CategoryTheory.FullSubcategory.lift P F hF) (CategoryTheory.fullSubcategoryInclusion P) = F

def CategoryTheory.FullSubcategory.lift_comp_inclusion {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : CategoryTheory.Functor.comp (CategoryTheory.FullSubcategory.lift P F hF) (CategoryTheory.fullSubcategoryInclusion P) ≅ F

Composing the lift of a functor through a full subcategory with the inclusion yields the original functor. This is actually true definitionally.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.fullSubcategoryInclusion_obj_lift_obj {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X : C} : (CategoryTheory.fullSubcategoryInclusion P).obj ((CategoryTheory.FullSubcategory.lift P F hF).obj X) = F.obj X

@[simp]

theorem CategoryTheory.fullSubcategoryInclusion_map_lift_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.fullSubcategoryInclusion P).map ((CategoryTheory.FullSubcategory.lift P F hF).map f) = F.map f

instance CategoryTheory.instFaithfulFullSubcategoryCategoryLift {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [CategoryTheory.Faithful F] : CategoryTheory.Faithful (CategoryTheory.FullSubcategory.lift P F hF)

Equations

• ⋯ = ⋯

instance CategoryTheory.instFullFullSubcategoryCategoryLift {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [CategoryTheory.Full F] : CategoryTheory.Full (CategoryTheory.FullSubcategory.lift P F hF)

Equations

• CategoryTheory.instFullFullSubcategoryCategoryLift P F hF = CategoryTheory.Full.ofCompFaithfulIso (CategoryTheory.FullSubcategory.lift_comp_inclusion P F hF)

@[simp]

theorem CategoryTheory.FullSubcategory.lift_comp_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : D → Prop) (Q : D → Prop) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (h : ∀ ⦃X : D⦄, P X → Q X) : CategoryTheory.Functor.comp (CategoryTheory.FullSubcategory.lift P F hF) (CategoryTheory.FullSubcategory.map h) = CategoryTheory.FullSubcategory.lift Q F ⋯