Theorems · Theorem · category theory

CategoryTheory.coherentTopology.isLocallySurjective_iff

∀ {C : Type u_1} (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 : CategoryTheory.Preregular C] [inst_5 : CategoryTheory.FinitaryExtensive C]
  {F G : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) D} (f : F ⟶ G)
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)],
  CategoryTheory.Sheaf.IsLocallySurjective f ↔
    CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f.hom

Defined in

Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.PreregularCategoryTheory.FinitaryExtensiveCategoryTheory.Limits.PreservesFiniteProducts