Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.Point.map_aux

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [F.IsCocontinuous J K] ⦃X : D⦄,
  ∀ R ∈ K X,
    ∀ ⦃u : Φ.fiber.Elements⦄ (f : ((CategoryTheory.CategoryOfElements.π Φ.fiber).comp F).obj u ⟶ X),
      ∃ Y g,
        ∃ (_ : R.arrows g),
          ∃ v q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (F.map ↑q) f

Defined in

Mathlib.CategoryTheory.Sites.Point.Map

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsCocontinuous