Theorems · Theorem · category theory

CategoryTheory.Presieve.IsSheafFor.valid_glue

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R)
  {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) (f : Y ⟶ X) (Hf : R f),
  (CategoryTheory.ConcreteCategory.hom (P.map f.op)) (t.amalgamate x hx) = x f Hf

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category