Theorems · Definition · category theory

CategoryTheory.Functor.PreOneHypercoverDenseData.f

{C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} → (self : F.PreOneHypercoverDenseData S) → (i : self.I₀) → F.obj (self.X i) ⟶ S

the morphisms in the covering of S

Defined in

Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Cited by

33 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category