Locally surjective morphisms of coherent sheaves #
This file characterises locally surjective morphisms of presheaves for the coherent, regular and extensive topologies.
Main results #
regularTopology.isLocallySurjective_iffA morphism of presheavesf : F ⟶ Gis locally surjective for the regular topology iff for every objectXofC, and everyy : G(X), there is an effective epimorphismφ : X' ⟶ Xand anx : F(X)such thatf_{X'}(x) = G(φ)(y).coherentTopology.isLocallySurjective_iffa morphism of sheaves for the coherent topology on a preregular finitary extensive category is locally surjective if and only if it is locally surjective for the regular topology.extensiveTopology.isLocallySurjective_iffa morphism of sheaves for the extensive topology on a finitary extensive category is locally surjective iff it is objectwise surjective.
theorem
CategoryTheory.regularTopology.isLocallySurjective_iff
{C : Type u_1}
(D : Type u_2)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.ConcreteCategory D]
[CategoryTheory.Preregular C]
{F G : CategoryTheory.Functor Cᵒᵖ D}
(f : F ⟶ G)
:
CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f ↔ ∀ (X : C) (y : (CategoryTheory.forget D).obj (G.obj (Opposite.op X))),
∃ (X' : C) (φ : X' ⟶ X) (_ : CategoryTheory.EffectiveEpi φ) (x :
(CategoryTheory.forget D).obj (F.obj (Opposite.op X'))), (f.app (Opposite.op X')) x = (G.map (Opposite.op φ)) y
theorem
CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.FinitaryPreExtensive C]
{F G : CategoryTheory.Functor Cᵒᵖ (Type w)}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts F]
[CategoryTheory.Limits.PreservesFiniteProducts G]
(h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f)
{X : C}
:
Function.Surjective (f.app (Opposite.op X))
@[deprecated CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types]
theorem
CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheafOfTypes
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.FinitaryPreExtensive C]
{F G : CategoryTheory.Functor Cᵒᵖ (Type w)}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts F]
[CategoryTheory.Limits.PreservesFiniteProducts G]
(h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f)
{X : C}
:
Function.Surjective (f.app (Opposite.op X))
Alias of CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types.
theorem
CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff
{C : Type u_1}
(D : Type u_2)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.ConcreteCategory D]
[CategoryTheory.FinitaryPreExtensive C]
{F G : CategoryTheory.Functor Cᵒᵖ D}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts F]
[CategoryTheory.Limits.PreservesFiniteProducts G]
[CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)]
:
CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f ↔ ∀ (X : C), Function.Surjective ⇑(f.app (Opposite.op X))
theorem
CategoryTheory.extensiveTopology.isLocallySurjective_iff
{C : Type u_1}
(D : Type u_2)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.ConcreteCategory D]
[CategoryTheory.FinitaryExtensive C]
{F G : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)]
:
CategoryTheory.Sheaf.IsLocallySurjective f ↔ ∀ (X : C), Function.Surjective ⇑(f.val.app (Opposite.op X))
theorem
CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryPreExtensive C]
{F G : CategoryTheory.Functor Cᵒᵖ (Type w)}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts F]
[CategoryTheory.Limits.PreservesFiniteProducts G]
(h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f)
:
@[deprecated CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types]
theorem
CategoryTheory.regularTopology.isLocallySurjective_sheafOfTypes
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryPreExtensive C]
{F G : CategoryTheory.Functor Cᵒᵖ (Type w)}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts F]
[CategoryTheory.Limits.PreservesFiniteProducts G]
(h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f)
:
Alias of CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types.
theorem
CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff
{C : Type u_1}
(D : Type u_2)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.ConcreteCategory D]
{F G : CategoryTheory.Functor Cᵒᵖ D}
(f : F ⟶ G)
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryPreExtensive C]
[CategoryTheory.Limits.PreservesFiniteProducts F]
[CategoryTheory.Limits.PreservesFiniteProducts G]
[CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)]
:
theorem
CategoryTheory.coherentTopology.isLocallySurjective_iff
{C : Type u_1}
(D : Type u_2)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.ConcreteCategory D]
[CategoryTheory.Preregular C]
[CategoryTheory.FinitaryExtensive C]
{F G : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) D}
(f : F ⟶ G)
[CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)]
: