Theorems · Theorem · category theory

CategoryTheory.Sheaf.isConstant_iff_forget

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full]
  [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full]
  [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)

Defined in

Mathlib.CategoryTheory.Sites.ConstantSheaf

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.PreservesSheafificationCategoryTheory.GrothendieckTopology.HasSheafComposeCategoryTheory.Functor.FaithfulCategoryTheory.Functor.FullCategoryTheory.Functor.FaithfulCategoryTheory.Functor.FullCategoryTheory.Functor.ReflectsIsomorphisms