Theorems · Theorem · category theory

CategoryTheory.Presieve.IsSeparatedFor.ext

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X},
  CategoryTheory.Presieve.IsSeparatedFor P R →
    ∀ {t₁ t₂ : P.obj (Opposite.op X)},
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          R f →
            (CategoryTheory.ConcreteCategory.hom (P.map f.op)) t₁ =
              (CategoryTheory.ConcreteCategory.hom (P.map f.op)) t₂) →
        t₁ = t₂

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

29 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category