Theorems · Theorem · category theory

CategoryTheory.Functor.IsLocallyFaithful.ext

∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.IsLocallyFaithful K]
  (ℱ : CategoryTheory.Sheaf K (Type u_2)) {X Y : C} (i₁ i₂ : X ⟶ Y),
  G.map i₁ = G.map i₂ →
    ∀ {s t : ℱ.obj.obj (Opposite.op (G.obj X))},
      (∀ ⦃Z : C⦄ (j : Z ⟶ X),
          CategoryTheory.CategoryStruct.comp j i₁ = CategoryTheory.CategoryStruct.comp j i₂ →
            (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s =
              (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t) →
        s = t

Defined in

Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocallyFaithful