Theorems · Theorem · category theory

CategoryTheory.regularTopology.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] {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G),
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f ↔
    ∀ (X : C) (y : CategoryTheory.ToType (G.obj (Opposite.op X))),
      ∃ X' φ,
        ∃ (_ : CategoryTheory.EffectiveEpi φ),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X'))) x =
              (CategoryTheory.ConcreteCategory.hom (G.map (Opposite.op φ))) y

Defined in

Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Preregular