Theorems · Theorem · category theory

CategoryTheory.Functor.faithful_of_comp_essSurj

∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor D E) (L : CategoryTheory.Functor C D) [L.EssSurj],
  (∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g) → F.Faithful

Defined in

Mathlib.CategoryTheory.EssentialImage

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.EssSurj