Theorems · Inductive type · category theory

CategoryTheory.Functor.OneHypercoverDenseData

{C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        CategoryTheory.Functor C₀ C →
          CategoryTheory.GrothendieckTopology C₀ →
            CategoryTheory.GrothendieckTopology C → C → Type (max (max (max u₀ v) v₀) (w + 1))

Given a functor F : C₀ ⥤ C, Grothendieck topologies J₀ on C₀ and J on C, an object S. : C, this structure roughly contains the data of a 1-hypercover of S consisting of objects in C₀.

Defined in

Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Cited by

50 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category