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_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_7, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
[HasForget A]
[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_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_7, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
[HasForget A]
(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_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_7, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
[HasForget A]
(hH : CoverPreserving J K H)
[H.IsCocontinuous J K]
[H.IsCoverDense K]
:
IsLocallyInjective J (whiskerLeft H.op f) ↔ IsLocallyInjective K f
theorem
CategoryTheory.Presheaf.isLocallySurjective_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
[HasForget A]
[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_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
[HasForget A]
(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_4, u_1} C]
[Category.{u_5, u_2} D]
[Category.{u_6, u_3} A]
(J : GrothendieckTopology C)
(K : GrothendieckTopology D)
(H : Functor C D)
{F G : Functor Dᵒᵖ A}
(f : F ⟶ G)
[HasForget A]
(hH : CoverPreserving J K H)
[H.IsCocontinuous J K]
[H.IsCoverDense K]
:
IsLocallySurjective J (whiskerLeft H.op f) ↔ IsLocallySurjective K f