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.

source

ink

class CategoryTheory.Full {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) :

Type (max(maxu₁v₁)v₂)

The data of a preimage for every f : F.obj X ⟶ F.obj Y⟶ F.obj Y.
preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
The property that Full.preimage f of maps to f via F.map.
witness : autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage X Y f) = f) _auto✝

A functor F : C ⥤ D⥤ 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⟶ F.obj Y.

See https://stacks.math.columbia.edu/tag/001C.

Instances

source

ink

class CategoryTheory.Faithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) :

Prop

F.map is injective for each X Y : C.
map_injective : autoParam (∀ {X Y : C}, Function.Injective (Prefunctor.map F.toPrefunctor)) _auto✝

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

See https://stacks.math.columbia.edu/tag/001C.

Instances

source

ink

theorem CategoryTheory.Functor.map_injective {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {X : C} {Y : C} (F : C ⥤ D) [inst : CategoryTheory.Faithful F] :

Function.Injective (Prefunctor.map F.toPrefunctor)

source

ink

theorem CategoryTheory.Functor.mapIso_injective {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {X : C} {Y : C} (F : C ⥤ D) [inst : CategoryTheory.Faithful F] :

Function.Injective (CategoryTheory.Functor.mapIso F)

source

ink

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

X ⟶ Y

The specified preimage of a morphism under a full functor.

Equations

CategoryTheory.Functor.preimage F f = CategoryTheory.Full.preimage f

source

ink

@[simp]

theorem CategoryTheory.Functor.image_preimage {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] {X : C} {Y : C} (f : F.obj X ⟶ F.obj Y) :

F.map (CategoryTheory.Functor.preimage F f) = f

source

ink

theorem CategoryTheory.Functor.map_surjective {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {X : C} {Y : C} (F : C ⥤ D) [inst : CategoryTheory.Full F] :

Function.Surjective (Prefunctor.map F.toPrefunctor)

source

ink

noncomputable def CategoryTheory.Functor.fullOfExists {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) (h : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ p, 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.

source

ink

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

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

source

ink

@[simp]

theorem CategoryTheory.preimage_id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} :

CategoryTheory.Functor.preimage F (𝟙 (F.obj X)) = 𝟙 X

source

ink

@[simp]

theorem CategoryTheory.preimage_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} {Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) :

CategoryTheory.Functor.preimage F (f ≫ g) = CategoryTheory.Functor.preimage F f ≫ CategoryTheory.Functor.preimage F g

source

ink

@[simp]

theorem CategoryTheory.preimage_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ⟶ Y) :

CategoryTheory.Functor.preimage F (F.map f) = f

source

ink

@[simp]

theorem CategoryTheory.Functor.preimageIso_inv {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) :

(CategoryTheory.Functor.preimageIso F f).inv = CategoryTheory.Functor.preimage F f.inv

source

ink

@[simp]

theorem CategoryTheory.Functor.preimageIso_hom {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) :

(CategoryTheory.Functor.preimageIso F f).hom = CategoryTheory.Functor.preimage F f.hom

source

ink

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

X ≅ Y

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

Equations

CategoryTheory.Functor.preimageIso F f = CategoryTheory.Iso.mk (CategoryTheory.Functor.preimage F f.hom) (CategoryTheory.Functor.preimage F f.inv)

source

ink

@[simp]

theorem CategoryTheory.Functor.preimageIso_mapIso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ≅ Y) :

CategoryTheory.Functor.preimageIso F (CategoryTheory.Functor.mapIso F f) = f

source

ink

theorem CategoryTheory.isIso_of_fully_faithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ⟶ Y) [inst : 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.

source

ink

@[simp]

theorem CategoryTheory.equivOfFullyFaithful_symm_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ⟶ F.obj Y) :

↑(Equiv.symm (CategoryTheory.equivOfFullyFaithful F)) f = CategoryTheory.Functor.preimage F f

source

ink

@[simp]

theorem CategoryTheory.equivOfFullyFaithful_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ⟶ Y) :

↑(CategoryTheory.equivOfFullyFaithful F) f = F.map f

source

ink

def CategoryTheory.equivOfFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : 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⟶ Y and F X ⟶ F Y⟶ F Y.

Equations

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

source

ink

@[simp]

theorem CategoryTheory.isoEquivOfFullyFaithful_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X ≅ Y) :

↑(CategoryTheory.isoEquivOfFullyFaithful F) f = CategoryTheory.Functor.mapIso F f

source

ink

@[simp]

theorem CategoryTheory.isoEquivOfFullyFaithful_symm_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X ≅ F.obj Y) :

↑(Equiv.symm (CategoryTheory.isoEquivOfFullyFaithful F)) f = CategoryTheory.Functor.preimageIso F f

source

ink

def CategoryTheory.isoEquivOfFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) [inst : CategoryTheory.Full F] [inst : 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≅ Y and F X ≅ F Y≅ F Y.

Equations

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

source

ink

@[simp]

theorem CategoryTheory.natTransOfCompFullyFaithful_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F ⋙ H ⟶ G ⋙ H) (X : C) :

(CategoryTheory.natTransOfCompFullyFaithful H α).app X = ↑(Equiv.symm (CategoryTheory.equivOfFullyFaithful H)) (α.app X)

source

ink

def CategoryTheory.natTransOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F ⋙ H ⟶ 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 α = CategoryTheory.NatTrans.mk fun X => ↑(Equiv.symm (CategoryTheory.equivOfFullyFaithful H)) (α.app X)

source

ink

@[simp]

theorem CategoryTheory.natIsoOfCompFullyFaithful_hom_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C) :

(CategoryTheory.natIsoOfCompFullyFaithful H i).hom.app X = CategoryTheory.Functor.preimage H (i.hom.app X)

source

ink

@[simp]

theorem CategoryTheory.natIsoOfCompFullyFaithful_inv_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C) :

(CategoryTheory.natIsoOfCompFullyFaithful H i).inv.app X = CategoryTheory.Functor.preimage H (i.inv.app X)

source

ink

def CategoryTheory.natIsoOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F ⋙ H ≅ 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

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

source

ink

theorem CategoryTheory.natIsoOfCompFullyFaithful_hom {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_2} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F ⋙ H ≅ G ⋙ H) :

(CategoryTheory.natIsoOfCompFullyFaithful H i).hom = CategoryTheory.natTransOfCompFullyFaithful H i.hom

source

ink

theorem CategoryTheory.natIsoOfCompFullyFaithful_inv {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_2} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F ⋙ H ≅ G ⋙ H) :

(CategoryTheory.natIsoOfCompFullyFaithful H i).inv = CategoryTheory.natTransOfCompFullyFaithful H i.inv

source

ink

@[simp]

theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F ⟶ G) :

↑(CategoryTheory.NatTrans.equivOfCompFullyFaithful H) α = α ◫ 𝟙 H

source

ink

@[simp]

theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F ⋙ H ⟶ G ⋙ H) :

↑(Equiv.symm (CategoryTheory.NatTrans.equivOfCompFullyFaithful H)) α = CategoryTheory.natTransOfCompFullyFaithful H α

source

ink

def CategoryTheory.NatTrans.equivOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] :

(F ⟶ G) ≃ (F ⋙ H ⟶ 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.

source

ink

@[simp]

theorem CategoryTheory.NatIso.equivOfCompFullyFaithful_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (e : F ≅ G) :

↑(CategoryTheory.NatIso.equivOfCompFullyFaithful H) e = CategoryTheory.NatIso.hcomp e (CategoryTheory.Iso.refl H)

source

ink

@[simp]

theorem CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F ⋙ H ≅ G ⋙ H) :

↑(Equiv.symm (CategoryTheory.NatIso.equivOfCompFullyFaithful H)) i = CategoryTheory.natIsoOfCompFullyFaithful H i

source

ink

def CategoryTheory.NatIso.equivOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] :

(F ≅ G) ≃ (F ⋙ H ≅ 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.

source

ink

instance CategoryTheory.Full.id {C : Type u₁} [inst : CategoryTheory.Category C] :

CategoryTheory.Full (𝟭 C)

Equations

CategoryTheory.Full.id = CategoryTheory.Full.mk fun {X Y} f => f

source

ink

instance CategoryTheory.Faithful.id {C : Type u₁} [inst : CategoryTheory.Category C] :

CategoryTheory.Faithful (𝟭 C)

Equations

@CategoryTheory.Faithful.id = @CategoryTheory.Faithful.id.proof_1

source

ink

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

CategoryTheory.Faithful (F ⋙ G)

Equations

@CategoryTheory.Faithful.comp = @CategoryTheory.Faithful.comp.proof_1

source

ink

theorem CategoryTheory.Faithful.of_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ D) (G : D ⥤ E) [inst : CategoryTheory.Faithful (F ⋙ G)] :

CategoryTheory.Faithful F

source

ink

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

CategoryTheory.Full F'

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

Equations

CategoryTheory.Full.ofIso α = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.Functor.preimage F ((α.app X).hom ≫ f ≫ (α.app Y).inv)

source

ink

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

CategoryTheory.Faithful F'

source

ink

theorem CategoryTheory.Faithful.of_comp_iso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst : CategoryTheory.Faithful H] (h : F ⋙ G ≅ H) :

CategoryTheory.Faithful F

source

ink

theorem CategoryTheory.Iso.faithful_of_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst : CategoryTheory.Faithful H] (h : F ⋙ G ≅ H) :

CategoryTheory.Faithful F

Alias of CategoryTheory.Faithful.of_comp_iso.

source

ink

theorem CategoryTheory.Faithful.of_comp_eq {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : CategoryTheory.Faithful H] (h : F ⋙ G = H) :

CategoryTheory.Faithful F

source

ink

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

CategoryTheory.Faithful F

Alias of CategoryTheory.Faithful.of_comp_eq.

source

ink

def CategoryTheory.Faithful.div {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ E) (G : D ⥤ E) [inst : 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 X Y f)) (F.map f)) :

C ⥤ D

“Divide” a functor by a faithful functor.

Equations

CategoryTheory.Faithful.div F G obj h_obj map h_map = CategoryTheory.Functor.mk { obj := obj, map := map }

source

ink

theorem CategoryTheory.Faithful.div_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ E) [inst : CategoryTheory.Faithful F] (G : D ⥤ E) [inst : 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 X Y f)) (F.map f)) :

CategoryTheory.Faithful.div F G obj h_obj map h_map ⋙ G = F

source

ink

theorem CategoryTheory.Faithful.div_faithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ E) [inst : CategoryTheory.Faithful F] (G : D ⥤ E) [inst : 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 X Y f)) (F.map f)) :

CategoryTheory.Faithful (CategoryTheory.Faithful.div F G obj h_obj map h_map)

source

ink

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

CategoryTheory.Full (F ⋙ G)

Equations

CategoryTheory.Full.comp F G = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.Functor.preimage F (CategoryTheory.Functor.preimage G f)

source

ink

def CategoryTheory.Full.ofCompFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ D) (G : D ⥤ E) [inst : CategoryTheory.Full (F ⋙ G)] [inst : CategoryTheory.Faithful G] :

CategoryTheory.Full F

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

Equations

CategoryTheory.Full.ofCompFaithful F G = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.Functor.preimage (F ⋙ G) (G.map f)

source

ink

def CategoryTheory.Full.ofCompFaithfulIso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful G] (h : F ⋙ G ≅ H) :

CategoryTheory.Full F

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

Equations

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

source

ink

def CategoryTheory.fullyFaithfulCancelRight {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) :

F ≅ G

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

Equations

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

source

ink

@[simp]

theorem CategoryTheory.fullyFaithfulCancelRight_hom_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} {H : D ⥤ E} [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :

(CategoryTheory.fullyFaithfulCancelRight H comp_iso).hom.app X = CategoryTheory.Functor.preimage H (comp_iso.hom.app X)

source

ink

@[simp]

theorem CategoryTheory.fullyFaithfulCancelRight_inv_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C ⥤ D} {G : C ⥤ D} {H : D ⥤ E} [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :

(CategoryTheory.fullyFaithfulCancelRight H comp_iso).inv.app X = CategoryTheory.Functor.preimage H (comp_iso.inv.app X)