Theorems · Theorem · category theory

CategoryTheory.Presheaf.isLocallyInjective_whisker_iff

∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA],
  CategoryTheory.CoverPreserving J K H →
    ∀ [H.IsCocontinuous J K] [H.IsCoverDense K],
      CategoryTheory.Presheaf.IsLocallyInjective J (H.op.whiskerLeft f) ↔ CategoryTheory.Presheaf.IsLocallyInjective K f

Defined in

Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Functor.IsCocontinuousCategoryTheory.Functor.IsCoverDense