Full and faithful functors

We define typeclasses Full and Faithful, decorating functors.

Main definitions and results

• Use F.map_injective to retrieve the fact that F.map is injective when [Faithful F].
• Similarly, F.map_surjective states that F.map is surjective when [Full F].
• Use F.preimage to obtain preimages of morphisms when [Full F].
• We prove some basic "cancellation" lemmas for full and/or faithful functors, as well as a construction for "dividing" a functor by a faithful functor, see Faithful.div.
• Full F carries data, so definitional properties of the preimage can be used when using F.preimage. To obtain an instance of Full F non-constructively, you can use fullOfExists and fullOfSurjective.

See CategoryTheory.Equivalence.of_fullyFaithful_ess_surj for the fact that a functor is an equivalence if and only if it is fully faithful and essentially surjective.

class CategoryTheory.Full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Type (max (max u₁ v₁) v₂)

A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective. In fact, we use a constructive definition, so the Full F typeclass contains data, specifying a particular preimage of each f : F.obj X ⟶ F.obj Y.

See .

• preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)

  The data of a preimage for every f : F.obj X ⟶ F.obj Y.

• witness : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (CategoryTheory.Full.preimage f) = f

  The property that Full.preimage f of maps to f via F.map.

Instances

• AddCommMonCat.forget₂Full
• CategoryTheory.BundledHom.forget₂Full
• CategoryTheory.Comma.instFullCommaCompCommaCategoryCommaCommaCategoryPreLeft
• CategoryTheory.Comma.instFullCommaCompCommaCategoryCommaCommaCategoryPreRight
• CategoryTheory.CostructuredArrow.instFullCostructuredArrowCompInstCategoryCostructuredArrowCostructuredArrowInstCategoryCostructuredArrowPre
• CategoryTheory.CostructuredArrow.instFullCostructuredArrowInstCategoryCostructuredArrowCostructuredArrowCompObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorInstCategoryCostructuredArrowPost
• CategoryTheory.CostructuredArrow.instFullCostructuredArrowInstCategoryCostructuredArrowOverInstCategoryOverToOver
• CategoryTheory.Coyoneda.coyonedaFull
• CategoryTheory.Equivalence.fullOfEquivalence
• CategoryTheory.Full.comp
• CategoryTheory.Full.id
• CategoryTheory.Full.toEssImage
• CategoryTheory.FullSubcategory.full
• CategoryTheory.FullSubcategory.full_map
• CategoryTheory.Functor.instFullEssImageSubcategoryInstCategoryEssImageSubcategoryEssImageInclusion
• CategoryTheory.Functor.instFullOppositeOppositeOppositeOppositeOp
• CategoryTheory.InducedCategory.full
• CategoryTheory.Limits.Cocones.functorialityFull
• CategoryTheory.Limits.Cones.functorialityFull
• CategoryTheory.StructuredArrow.instFullStructuredArrowCompInstCategoryStructuredArrowStructuredArrowInstCategoryStructuredArrowPre
• CategoryTheory.StructuredArrow.instFullStructuredArrowInstCategoryStructuredArrowStructuredArrowObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCompInstCategoryStructuredArrowPost
• CategoryTheory.StructuredArrow.instFullStructuredArrowInstCategoryStructuredArrowUnderInstCategoryUnderToUnder
• CategoryTheory.Yoneda.yonedaFull
• CategoryTheory.instFullFullSubcategoryCategoryLift
• CategoryTheory.instFullSkeletonInstCategorySkeletonFromSkeleton
• CategoryTheory.instFullTypeTypesCatCategoryTypeToCat
• CategoryTheory.uliftFunctorFull
• CommMonCat.forget₂Full
• CommRingCat.instFullCommRingCatInstCommRingCatLargeCategoryCommSemiRingCatInstCommSemiRingCatLargeCategoryForget₂InstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryInstConcreteCategoryCommSemiRingCatInstCommSemiRingCatLargeCategoryHasForgetToCommSemiRingCat

class CategoryTheory.Faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.

See .

• map_injective : ∀ {X Y : C}, Function.Injective F.map

  F.map is injective for each X Y : C.

Instances

• CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreLeft
• CategoryTheory.Comma.instFaithfulCommaCompCommaCategoryCommaCommaCategoryPreRight
• CategoryTheory.CostructuredArrow.instFaithfulCostructuredArrowCompInstCategoryCostructuredArrowCostructuredArrowInstCategoryCostructuredArrowPre
• CategoryTheory.CostructuredArrow.instFaithfulCostructuredArrowInstCategoryCostructuredArrowCostructuredArrowCompObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorInstCategoryCostructuredArrowPost
• CategoryTheory.CostructuredArrow.instFaithfulCostructuredArrowInstCategoryCostructuredArrowOverInstCategoryOverToOver
• CategoryTheory.CostructuredArrow.proj_faithful
• CategoryTheory.Coyoneda.coyoneda_faithful
• CategoryTheory.Equivalence.faithfulOfEquivalence
• CategoryTheory.Faithful.comp
• CategoryTheory.Faithful.id
• CategoryTheory.Faithful.toEssImage
• CategoryTheory.FullSubcategory.faithful
• CategoryTheory.FullSubcategory.faithful_map
• CategoryTheory.Functor.instFaithfulEssImageSubcategoryInstCategoryEssImageSubcategoryEssImageInclusion
• CategoryTheory.Functor.instFaithfulFunctorCategoryConst
• CategoryTheory.Functor.instFaithfulOppositeOppositeOppositeOppositeOp
• CategoryTheory.Functor.leftOp_faithful
• CategoryTheory.Functor.rightOp_faithful
• CategoryTheory.InducedCategory.faithful
• CategoryTheory.Limits.Cocones.functoriality_faithful
• CategoryTheory.Limits.Cones.functoriality_faithful
• CategoryTheory.Over.forget_faithful
• CategoryTheory.StructuredArrow.instFaithfulStructuredArrowCompInstCategoryStructuredArrowStructuredArrowInstCategoryStructuredArrowPre
• CategoryTheory.StructuredArrow.instFaithfulStructuredArrowInstCategoryStructuredArrowStructuredArrowObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCompInstCategoryStructuredArrowPost
• CategoryTheory.StructuredArrow.instFaithfulStructuredArrowInstCategoryStructuredArrowUnderInstCategoryUnderToUnder
• CategoryTheory.StructuredArrow.proj_faithful
• CategoryTheory.ThinSkeleton.toThinSkeleton_faithful
• CategoryTheory.Under.forget_faithful
• CategoryTheory.Yoneda.yoneda_faithful
• CategoryTheory.faithful_whiskeringRight_obj
• CategoryTheory.forget₂_faithful
• CategoryTheory.instFaithfulFullSubcategoryCategoryLift
• CategoryTheory.instFaithfulSkeletonInstCategorySkeletonFromSkeleton
• CategoryTheory.instFaithfulTypeTypesCatCategoryTypeToCat
• CategoryTheory.uliftFunctor_faithful

theorem CategoryTheory.Functor.map_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (F : CategoryTheory.Functor C D) [CategoryTheory.Faithful F] : Function.Injective F.map

theorem CategoryTheory.Functor.mapIso_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (F : CategoryTheory.Functor C D) [CategoryTheory.Faithful F] : Function.Injective F.mapIso

def CategoryTheory.Functor.preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] (f : F.obj X ⟶ F.obj Y) : X ⟶ Y

The specified preimage of a morphism under a full functor.

Equations

• F.preimage f = CategoryTheory.Full.preimage f

@[simp]

theorem CategoryTheory.Functor.image_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] {X : C} {Y : C} (f : F.obj X ⟶ F.obj Y) : F.map (F.preimage f) = f

theorem CategoryTheory.Functor.map_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] : Function.Surjective F.map

noncomputable def CategoryTheory.Functor.fullOfExists {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (h : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ (p : X ⟶ Y), F.map p = f) : CategoryTheory.Full F

Deduce that F is full from the existence of preimages, using choice.

Equations

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

noncomputable def CategoryTheory.Functor.fullOfSurjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (h : ∀ (X Y : C), Function.Surjective F.map) : CategoryTheory.Full F

Deduce that F is full from surjectivity of F.map, using choice.

Equations

• CategoryTheory.Functor.fullOfSurjective F h = CategoryTheory.Functor.fullOfExists F h

@[simp]

theorem CategoryTheory.preimage_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} : F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.preimage_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} {Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) : F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)

@[simp]

theorem CategoryTheory.preimage_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ⟶ Y) : F.preimage (F.map f) = f

@[simp]

theorem CategoryTheory.Functor.preimageIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) : (CategoryTheory.Functor.preimageIso F f).hom = F.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.preimageIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) : (CategoryTheory.Functor.preimageIso F f).inv = F.preimage f.inv

def CategoryTheory.Functor.preimageIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) : X ≅ Y

If F : C ⥤ D is fully faithful, every isomorphism F.obj X ≅ F.obj Y has a preimage.

Equations

• CategoryTheory.Functor.preimageIso F f = { hom := F.preimage f.hom, inv := F.preimage f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.preimageIso_mapIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ≅ Y) : CategoryTheory.Functor.preimageIso F (F.mapIso f) = f

theorem CategoryTheory.isIso_of_fully_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso f

If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism.

@[simp]

theorem CategoryTheory.equivOfFullyFaithful_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ⟶ F.obj Y) : (CategoryTheory.equivOfFullyFaithful F).symm f = F.preimage f

@[simp]

theorem CategoryTheory.equivOfFullyFaithful_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.equivOfFullyFaithful F) f = F.map f

def CategoryTheory.equivOfFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} : (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)

If F is fully faithful, we have an equivalence of hom-sets X ⟶ Y and F X ⟶ F Y.

Equations

• CategoryTheory.equivOfFullyFaithful F = { toFun := fun (f : X ⟶ Y) => F.map f, invFun := fun (f : F.obj X ⟶ F.obj Y) => F.preimage f, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.isoEquivOfFullyFaithful_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) : (CategoryTheory.isoEquivOfFullyFaithful F).symm f = CategoryTheory.Functor.preimageIso F f

@[simp]

theorem CategoryTheory.isoEquivOfFullyFaithful_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ≅ Y) : (CategoryTheory.isoEquivOfFullyFaithful F) f = F.mapIso f

def CategoryTheory.isoEquivOfFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)

If F is fully faithful, we have an equivalence of iso-sets X ≅ Y and F X ≅ F Y.

Equations

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

@[simp]

theorem CategoryTheory.natTransOfCompFullyFaithful_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (α : CategoryTheory.Functor.comp F H ⟶ CategoryTheory.Functor.comp G H) (X : C) : (CategoryTheory.natTransOfCompFullyFaithful H α).app X = (CategoryTheory.equivOfFullyFaithful H).symm (α.app X)

def CategoryTheory.natTransOfCompFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (α : CategoryTheory.Functor.comp F H ⟶ CategoryTheory.Functor.comp G H) : F ⟶ G

We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.

Equations

• CategoryTheory.natTransOfCompFullyFaithful H α = { app := fun (X : C) => (CategoryTheory.equivOfFullyFaithful H).symm (α.app X), naturality := ⋯ }

@[simp]

theorem CategoryTheory.natIsoOfCompFullyFaithful_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (i : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) (X : C) : (CategoryTheory.natIsoOfCompFullyFaithful H i).hom.app X = H.preimage (i.hom.app X)

@[simp]

theorem CategoryTheory.natIsoOfCompFullyFaithful_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (i : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) (X : C) : (CategoryTheory.natIsoOfCompFullyFaithful H i).inv.app X = H.preimage (i.inv.app X)

def CategoryTheory.natIsoOfCompFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (i : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) : F ≅ G

We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor.

Equations

• CategoryTheory.natIsoOfCompFullyFaithful H i = CategoryTheory.NatIso.ofComponents (fun (X : C) => (CategoryTheory.isoEquivOfFullyFaithful H).symm (i.app X)) ⋯

theorem CategoryTheory.natIsoOfCompFullyFaithful_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (i : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) : (CategoryTheory.natIsoOfCompFullyFaithful H i).hom = CategoryTheory.natTransOfCompFullyFaithful H i.hom

theorem CategoryTheory.natIsoOfCompFullyFaithful_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (i : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) : (CategoryTheory.natIsoOfCompFullyFaithful H i).inv = CategoryTheory.natTransOfCompFullyFaithful H i.inv

@[simp]

theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (α : CategoryTheory.Functor.comp F H ⟶ CategoryTheory.Functor.comp G H) : (CategoryTheory.NatTrans.equivOfCompFullyFaithful H).symm α = CategoryTheory.natTransOfCompFullyFaithful H α

@[simp]

theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (α : F ⟶ G) : (CategoryTheory.NatTrans.equivOfCompFullyFaithful H) α = α ◫ CategoryTheory.CategoryStruct.id H

def CategoryTheory.NatTrans.equivOfCompFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] : (F ⟶ G) ≃ (CategoryTheory.Functor.comp F H ⟶ CategoryTheory.Functor.comp G H)

Horizontal composition with a fully faithful functor induces a bijection on natural transformations.

Equations

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

@[simp]

theorem CategoryTheory.NatIso.equivOfCompFullyFaithful_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (e : F ≅ G) : (CategoryTheory.NatIso.equivOfCompFullyFaithful H) e = CategoryTheory.NatIso.hcomp e (CategoryTheory.Iso.refl H)

@[simp]

theorem CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (i : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) : (CategoryTheory.NatIso.equivOfCompFullyFaithful H).symm i = CategoryTheory.natIsoOfCompFullyFaithful H i

def CategoryTheory.NatIso.equivOfCompFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] : (F ≅ G) ≃ (CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H)

Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms.

Equations

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

instance CategoryTheory.Full.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Full (CategoryTheory.Functor.id C)

Equations

• CategoryTheory.Full.id = { preimage := fun {X Y : C} (f : (CategoryTheory.Functor.id C).obj X ⟶ (CategoryTheory.Functor.id C).obj Y) => f, witness := ⋯ }

instance CategoryTheory.Faithful.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Faithful (CategoryTheory.Functor.id C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Faithful.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Faithful F] [CategoryTheory.Faithful G] : CategoryTheory.Faithful (CategoryTheory.Functor.comp F G)

Equations

• ⋯ = ⋯

theorem CategoryTheory.Faithful.of_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Faithful (CategoryTheory.Functor.comp F G)] : CategoryTheory.Faithful F

def CategoryTheory.Full.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} [CategoryTheory.Full F] (α : F ≅ F') : CategoryTheory.Full F'

If F is full, and naturally isomorphic to some F', then F' is also full.

Equations

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

theorem CategoryTheory.Faithful.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} [CategoryTheory.Faithful F] (α : F ≅ F') : CategoryTheory.Faithful F'

theorem CategoryTheory.Faithful.of_comp_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [CategoryTheory.Faithful H] (h : CategoryTheory.Functor.comp F G ≅ H) : CategoryTheory.Faithful F

theorem CategoryTheory.Iso.faithful_of_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [CategoryTheory.Faithful H] (h : CategoryTheory.Functor.comp F G ≅ H) : CategoryTheory.Faithful F

Alias of CategoryTheory.Faithful.of_comp_iso.

theorem CategoryTheory.Faithful.of_comp_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [ℋ : CategoryTheory.Faithful H] (h : CategoryTheory.Functor.comp F G = H) : CategoryTheory.Faithful F

theorem Eq.faithful_of_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [ℋ : CategoryTheory.Faithful H] (h : CategoryTheory.Functor.comp F G = H) : CategoryTheory.Faithful F

Alias of CategoryTheory.Faithful.of_comp_eq.

def CategoryTheory.Faithful.div {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) (G : CategoryTheory.Functor D E) [CategoryTheory.Faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : CategoryTheory.Functor C D

“Divide” a functor by a faithful functor.

Equations

• CategoryTheory.Faithful.div F G obj h_obj map h_map = { toPrefunctor := { obj := obj, map := map }, map_id := ⋯, map_comp := ⋯ }

theorem CategoryTheory.Faithful.div_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) [CategoryTheory.Faithful F] (G : CategoryTheory.Functor D E) [CategoryTheory.Faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : CategoryTheory.Functor.comp (CategoryTheory.Faithful.div F G obj h_obj map h_map) G = F

theorem CategoryTheory.Faithful.div_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) [CategoryTheory.Faithful F] (G : CategoryTheory.Functor D E) [CategoryTheory.Faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : CategoryTheory.Faithful (CategoryTheory.Faithful.div F G obj h_obj map h_map)

instance CategoryTheory.Full.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Full F] [CategoryTheory.Full G] : CategoryTheory.Full (CategoryTheory.Functor.comp F G)

Equations

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

def CategoryTheory.Full.ofCompFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Full (CategoryTheory.Functor.comp F G)] [CategoryTheory.Faithful G] : CategoryTheory.Full F

If F ⋙ G is full and G is faithful, then F is full.

Equations

• CategoryTheory.Full.ofCompFaithful F G = { preimage := fun {X Y : C} (f : F.obj X ⟶ F.obj Y) => (CategoryTheory.Functor.comp F G).preimage (G.map f), witness := ⋯ }

def CategoryTheory.Full.ofCompFaithfulIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [CategoryTheory.Full H] [CategoryTheory.Faithful G] (h : CategoryTheory.Functor.comp F G ≅ H) : CategoryTheory.Full F

If F ⋙ G is full and G is faithful, then F is full.

Equations

• CategoryTheory.Full.ofCompFaithfulIso h = CategoryTheory.Full.ofCompFaithful F G

def CategoryTheory.fullyFaithfulCancelRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [CategoryTheory.Full H] [CategoryTheory.Faithful H] (comp_iso : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) : F ≅ G

Given a natural isomorphism between F ⋙ H and G ⋙ H for a fully faithful functor H, we can 'cancel' it to give a natural iso between F and G.

Equations

• CategoryTheory.fullyFaithfulCancelRight H comp_iso = CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.Functor.preimageIso H (comp_iso.app X)) ⋯

@[simp]

theorem CategoryTheory.fullyFaithfulCancelRight_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [CategoryTheory.Full H] [CategoryTheory.Faithful H] (comp_iso : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) (X : C) : (CategoryTheory.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)

@[simp]

theorem CategoryTheory.fullyFaithfulCancelRight_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [CategoryTheory.Full H] [CategoryTheory.Faithful H] (comp_iso : CategoryTheory.Functor.comp F H ≅ CategoryTheory.Functor.comp G H) (X : C) : (CategoryTheory.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)