Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.CoversTop.ext

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {I : Type u_1} {Y : I → C},
  J.CoversTop Y →
    ∀ (F : CategoryTheory.Sheaf J A) {c : CategoryTheory.Limits.Cone F.obj} (hc : CategoryTheory.Limits.IsLimit c)
      {X : A} {f g : X ⟶ c.pt},
      (∀ (i : I),
          CategoryTheory.CategoryStruct.comp f (c.π.app (Opposite.op (Y i))) =
            CategoryTheory.CategoryStruct.comp g (c.π.app (Opposite.op (Y i)))) →
        f = g

Defined in

Mathlib.CategoryTheory.Sites.CoversTop.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category