Theorems · Theorem · category theory

CategoryTheory.Subfunctor.to_sheafifyLift

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F) (f : G.toFunctor ⟶ F')
  (h : CategoryTheory.Presieve.IsSheaf J F'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.homOfLe ⋯) (G.sheafifyLift f h) = f

Defined in

Mathlib.CategoryTheory.Sites.Subsheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category