Detecting local equivalences on a covering family #
Local injectivity and local surjectivity of a morphism of additive presheaves can be checked after restriction to a family covering the terminal object. Consequently, when the weak equivalences of a site are the locally bijective morphisms, membership in the class inverted by sheafification can be checked on such a family.
These statements use only a Grothendieck topology and additive presheaves. Scheme charts and module-sheaf tensor products are downstream consumers.
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_coversTop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{P Q : Functor Cᵒᵖ AddCommGrpCat}
(f : P ⟶ Q)
{ι : Type u_1}
(X : ι → C)
(hX : J.CoversTop X)
(h : ∀ (i : ι), IsLocallyInjective (J.over (X i)) ((Over.forget (X i)).op.whiskerLeft f))
:
Local injectivity is detected on a family covering the terminal object.
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_coversTop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{P Q : Functor Cᵒᵖ AddCommGrpCat}
(f : P ⟶ Q)
{ι : Type u_1}
(X : ι → C)
(hX : J.CoversTop X)
(h : ∀ (i : ι), IsLocallySurjective (J.over (X i)) ((Over.forget (X i)).op.whiskerLeft f))
:
Local surjectivity is detected on a family covering the terminal object.
theorem
CategoryTheory.Presheaf.W_of_coversTop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
[J.WEqualsLocallyBijective AddCommGrpCat]
{P Q : Functor Cᵒᵖ AddCommGrpCat}
(f : P ⟶ Q)
{ι : Type u_1}
(X : ι → C)
(hX : J.CoversTop X)
[∀ (i : ι), (J.over (X i)).WEqualsLocallyBijective AddCommGrpCat]
(h : ∀ (i : ι), (J.over (X i)).W ((Over.forget (X i)).op.whiskerLeft f))
:
J.W f
A morphism that is a local weak equivalence on a covering family is one globally.