Theorems · Inductive type · category theory

CategoryTheory.Functor.IsLocallyFaithful

{C : Type uC} →
  [inst : CategoryTheory.Category.{vC, uC} C] →
    {D : Type uD} →
      [inst_1 : CategoryTheory.Category.{vD, uD} D] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → Prop

A functor G : C ⥤ D is locally faithful w.r.t. a topology on D if for every f₁ f₂ : U ⟶ V whose images in D are equal, the set of G.map gᵢ : G.obj Wᵢ ⟶ G.obj U such that gᵢ ≫ f₁ = gᵢ ≫ f₂ is a coverage of the topology on D.

Defined in

Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Cited by

13 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category