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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_7, 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)
[CategoryTheory.ConcreteCategory A]
[H.IsCocontinuous J K]
[CategoryTheory.Presheaf.IsLocallyInjective K f]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_7, 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)
[CategoryTheory.ConcreteCategory A]
(hH : CategoryTheory.CoverPreserving J K H)
[H.IsCoverDense K]
[CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.whiskerLeft H.op f)]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_whisker_iff
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_7, 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)
[CategoryTheory.ConcreteCategory A]
(hH : CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, 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)
[CategoryTheory.ConcreteCategory A]
[H.IsCocontinuous J K]
[CategoryTheory.Presheaf.IsLocallySurjective K f]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_whisker
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, 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)
[CategoryTheory.ConcreteCategory A]
(hH : CategoryTheory.CoverPreserving J K H)
[H.IsCoverDense K]
[CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.whiskerLeft H.op f)]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_whisker_iff
{C : Type u_1}
{D : Type u_2}
{A : Type u_3}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Category.{u_6, 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)
[CategoryTheory.ConcreteCategory A]
(hH : CategoryTheory.CoverPreserving J K H)
[H.IsCocontinuous J K]
[H.IsCoverDense K]
: