Theorems · Theorem · category theory

CategoryTheory.coherentTopology.presheafIsLocallySurjective_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]
  {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G) [inst_4 : CategoryTheory.Preregular C]
  [inst_5 : CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.Limits.PreservesFiniteProducts F]
  [CategoryTheory.Limits.PreservesFiniteProducts G]
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)],
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f ↔
    CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f

Defined in

Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.PreregularCategoryTheory.FinitaryPreExtensiveCategoryTheory.Limits.PreservesFiniteProductsCategoryTheory.Limits.PreservesFiniteProductsCategoryTheory.Limits.PreservesFiniteProducts