Preserving and reflecting local injectivity and surjectivity #
This file proves that precomposition with a cocontinuous functor preserves local injectivity and surjectivity of morphisms of presheaves, and that precomposition with a cover preserving and cover dense functor reflects the same properties.
theorem
CategoryTheory.Presheaf.isLocallyInjective_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_6, u_1} C]
[Category.{u_7, u_2} D]
[Category.{u_8, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
{FA : A → A → Type u_4}
{CA : A → Type u_5}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[H.IsCocontinuous J K]
[IsLocallyInjective K f]
:
IsLocallyInjective J (whiskerLeft H.op f)
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_6, u_1} C]
[Category.{u_7, u_2} D]
[Category.{u_8, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
{FA : A → A → Type u_4}
{CA : A → Type u_5}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
(hH : CoverPreserving J K H)
[H.IsCoverDense K]
[IsLocallyInjective J (whiskerLeft H.op f)]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_whisker_iff
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_6, u_1} C]
[Category.{u_7, u_2} D]
[Category.{u_8, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
{FA : A → A → Type u_4}
{CA : A → Type u_5}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
(hH : CoverPreserving J K H)
[H.IsCocontinuous J K]
[H.IsCoverDense K]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_6, u_1} C]
[Category.{u_7, u_2} D]
[Category.{u_8, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
{FA : A → A → Type u_4}
{CA : A → Type u_5}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[H.IsCocontinuous J K]
[IsLocallySurjective K f]
:
IsLocallySurjective J (whiskerLeft H.op f)
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_6, u_1} C]
[Category.{u_7, u_2} D]
[Category.{u_8, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
{FA : A → A → Type u_4}
{CA : A → Type u_5}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
(hH : CoverPreserving J K H)
[H.IsCoverDense K]
[IsLocallySurjective J (whiskerLeft H.op f)]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_whisker_iff
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_6, u_1} C]
[Category.{u_7, u_2} D]
[Category.{u_8, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
{FA : A → A → Type u_4}
{CA : A → Type u_5}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
(hH : CoverPreserving J K H)
[H.IsCocontinuous J K]
[H.IsCoverDense K]
: