Theorems · Theorem · category theory

CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem

∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D)
  [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks],
  (∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)},
      R ∈ K.coverings (F.obj S) →
        CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) →
    F.LocallyCoverDense K.toGrothendieck

Defined in

Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Precoverage.HasIsosCategoryTheory.Precoverage.IsStableUnderBaseChangeCategoryTheory.Precoverage.IsStableUnderCompositionCategoryTheory.Precoverage.HasPullbacks