Locally surjective morphisms #
Main definitions #
IsLocallySurjective: A morphism of presheaves valued in a concrete category is locally surjective with respect to a Grothendieck topology if every section in the target is locally in the set-theoretic image, i.e. the image sheaf coincides with the target.
Main results #
Presheaf.isLocallySurjective_toSheafify:toSheafifyis locally surjective.Sheaf.isLocallySurjective_iff_epi: a morphism of sheaves of types is locally surjective iff it is epi
def
CategoryTheory.Presheaf.imageSieve
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (forget A).obj (G.obj (Opposite.op U)))
:
Sieve U
Given f : F ⟶ G, a morphism between presieves, and s : G.obj (op U), this is the sieve
of U consisting of the i : V ⟶ U such that s restricted along i is in the image of f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Presheaf.imageSieve_apply
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (forget A).obj (G.obj (Opposite.op U)))
(V : C)
(i : V ⟶ U)
:
(imageSieve f s).arrows i = ∃ (t : (forget A).obj (F.obj (Opposite.op V))), (f.app (Opposite.op V)) t = (G.map i.op) s
theorem
CategoryTheory.Presheaf.imageSieve_eq_sieveOfSection
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (forget A).obj (G.obj (Opposite.op U)))
:
imageSieve f s = (imagePresheaf (whiskerRight f (forget A))).sieveOfSection s
theorem
CategoryTheory.Presheaf.imageSieve_whisker_forget
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (forget A).obj (G.obj (Opposite.op U)))
:
imageSieve (whiskerRight f (forget A)) s = imageSieve f s
theorem
CategoryTheory.Presheaf.imageSieve_app
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (forget A).obj (F.obj (Opposite.op U)))
:
imageSieve f ((f.app (Opposite.op U)) s) = ⊤
noncomputable def
CategoryTheory.Presheaf.localPreimage
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : Cᵒᵖ}
(s : (forget A).obj (G.obj U))
{V : C}
(g : V ⟶ Opposite.unop U)
(hg : (imageSieve f s).arrows g)
:
(forget A).obj (F.obj (Opposite.op V))
If a morphism g : V ⟶ U.unop belongs to the sieve imageSieve f s g, then
this is choice of a preimage of G.map g.op s in F.obj (op V), see
app_localPreimage.
Equations
- CategoryTheory.Presheaf.localPreimage f s g hg = Exists.choose hg
Instances For
@[simp]
theorem
CategoryTheory.Presheaf.app_localPreimage
{C : Type u}
[Category.{v, u} C]
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : Cᵒᵖ}
(s : (forget A).obj (G.obj U))
{V : C}
(g : V ⟶ Opposite.unop U)
(hg : (imageSieve f s).arrows g)
:
(f.app (Opposite.op V)) (localPreimage f s g hg) = (G.map g.op) s
class
CategoryTheory.Presheaf.IsLocallySurjective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
:
A morphism of presheaves f : F ⟶ G is locally surjective with respect to a grothendieck
topology if every section of G is locally in the image of f.
Instances
theorem
CategoryTheory.Presheaf.imageSieve_mem
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
[IsLocallySurjective J f]
{U : Cᵒᵖ}
(s : (forget A).obj (G.obj U))
:
imageSieve f s ∈ J (Opposite.unop U)
instance
CategoryTheory.Presheaf.instIsLocallySurjectiveWhiskerRightOppositeForget
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
[IsLocallySurjective J f]
:
IsLocallySurjective J (whiskerRight f (forget A))
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
:
IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top'
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{F G : Functor Cᵒᵖ (Type w)}
(f : F ⟶ G)
:
IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf f) = ⊤
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
:
IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_surjective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
(H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U))
:
instance
CategoryTheory.Presheaf.isLocallySurjective_of_iso
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
[IsIso f]
:
instance
CategoryTheory.Presheaf.isLocallySurjective_comp
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallySurjective J f₁]
[IsLocallySurjective J f₂]
:
IsLocallySurjective J (CategoryStruct.comp f₁ f₂)
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallySurjective J (CategoryStruct.comp f₁ f₂)]
:
IsLocallySurjective J f₂
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_fac
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
{f₃ : F₁ ⟶ F₃}
(fac : CategoryStruct.comp f₁ f₂ = f₃)
[IsLocallySurjective J f₃]
:
IsLocallySurjective J f₂
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_of_fac
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
{f₃ : F₁ ⟶ F₃}
(fac : CategoryStruct.comp f₁ f₂ = f₃)
[IsLocallySurjective J f₁]
:
IsLocallySurjective J f₃ ↔ IsLocallySurjective J f₂
theorem
CategoryTheory.Presheaf.comp_isLocallySurjective_iff
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallySurjective J f₁]
:
IsLocallySurjective J (CategoryStruct.comp f₁ f₂) ↔ IsLocallySurjective J f₂
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_le
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{K : GrothendieckTopology C}
(hJK : J ≤ K)
{F G : Functor Cᵒᵖ A}
(f : F ⟶ G)
(h : IsLocallySurjective J f)
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallyInjective J (CategoryStruct.comp f₁ f₂)]
[IsLocallySurjective J f₁]
:
IsLocallyInjective J f₂
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
(f₃ : F₁ ⟶ F₃)
(fac : CategoryStruct.comp f₁ f₂ = f₃)
[IsLocallyInjective J f₃]
[IsLocallySurjective J f₁]
:
IsLocallyInjective J f₂
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallySurjective J (CategoryStruct.comp f₁ f₂)]
[IsLocallyInjective J f₂]
:
IsLocallySurjective J f₁
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
(f₃ : F₁ ⟶ F₃)
(fac : CategoryStruct.comp f₁ f₂ = f₃)
[IsLocallySurjective J f₃]
[IsLocallyInjective J f₂]
:
IsLocallySurjective J f₁
theorem
CategoryTheory.Presheaf.comp_isLocallyInjective_iff
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallyInjective J f₁]
[IsLocallySurjective J f₁]
:
IsLocallyInjective J (CategoryStruct.comp f₁ f₂) ↔ IsLocallyInjective J f₂
theorem
CategoryTheory.Presheaf.isLocallySurjective_comp_iff
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[IsLocallyInjective J f₂]
[IsLocallySurjective J f₂]
:
IsLocallySurjective J (CategoryStruct.comp f₁ f₂) ↔ IsLocallySurjective J f₁
instance
CategoryTheory.Presheaf.instIsLocallySurjectiveToImagePresheafSheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ (Type w)}
(f : F₁ ⟶ F₂)
:
noncomputable def
CategoryTheory.Presheaf.sheafificationIsoImagePresheaf
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(F : Functor Cᵒᵖ (Type (max u v)))
:
J.sheafify F ≅ (Subpresheaf.sheafify J (imagePresheaf (J.toSheafify F))).toPresheaf
The image of F in J.sheafify F is isomorphic to the sheafification.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Presheaf.isLocallySurjective_toPlus
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ (Type (max u v)))
:
IsLocallySurjective J (J.toPlus P)
instance
CategoryTheory.Presheaf.isLocallySurjective_toSheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ (Type (max u v)))
:
IsLocallySurjective J (J.toSheafify P)
instance
CategoryTheory.Presheaf.isLocallySurjective_toSheafify'
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type u_1}
[Category.{u_2, u_1} D]
[HasForget D]
(P : Functor Cᵒᵖ D)
[HasWeakSheafify J D]
[J.HasSheafCompose (forget D)]
[J.PreservesSheafification (forget D)]
:
IsLocallySurjective J (toSheafify J P)
@[reducible, inline]
abbrev
CategoryTheory.Sheaf.IsLocallySurjective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ : Sheaf J A}
(φ : F₁ ⟶ F₂)
:
If φ : F₁ ⟶ F₂ is a morphism of sheaves, this is an abbreviation for
Presheaf.IsLocallySurjective J φ.val.
Equations
Instances For
theorem
CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ : Sheaf J A}
(φ : F₁ ⟶ F₂)
:
Presheaf.IsLocallySurjective J ((sheafToPresheaf J A).map φ) ↔ IsLocallySurjective φ
instance
CategoryTheory.Sheaf.isLocallySurjective_comp
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ F₃ : Sheaf J A}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[IsLocallySurjective φ]
[IsLocallySurjective ψ]
:
instance
CategoryTheory.Sheaf.isLocallySurjective_of_iso
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ : Sheaf J A}
(φ : F₁ ⟶ F₂)
[IsIso φ]
:
instance
CategoryTheory.Sheaf.instIsLocallySurjectiveToImageSheaf
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{F G : Sheaf J (Type w)}
(f : F ⟶ G)
:
instance
CategoryTheory.Sheaf.instIsLocallySurjectiveMapTypeSheafComposeForget
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ : Sheaf J A}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (forget A)]
[IsLocallySurjective φ]
:
IsLocallySurjective ((sheafCompose J (forget A)).map φ)
theorem
CategoryTheory.Sheaf.isLocallySurjective_iff_isIso
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{F G : Sheaf J (Type w)}
(f : F ⟶ G)
:
IsLocallySurjective f ↔ IsIso (imageSheafι f)
instance
CategoryTheory.Sheaf.epi_of_isLocallySurjective'
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J (Type w)}
(φ : F₁ ⟶ F₂)
[IsLocallySurjective φ]
:
Epi φ
instance
CategoryTheory.Sheaf.epi_of_isLocallySurjective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
[HasForget A]
{F₁ F₂ : Sheaf J A}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (forget A)]
[IsLocallySurjective φ]
:
Epi φ
theorem
CategoryTheory.Sheaf.isLocallySurjective_iff_epi
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{F G : Sheaf J (Type w)}
(φ : F ⟶ G)
[HasSheafify J (Type w)]
:
IsLocallySurjective φ ↔ Epi φ
noncomputable def
CategoryTheory.Presieve.FamilyOfElements.localPreimage
{C : Type u}
[Category.{v, u} C]
{R R' : Functor Cᵒᵖ (Type w)}
(φ : R ⟶ R')
{X : Cᵒᵖ}
(r' : R'.obj X)
:
FamilyOfElements R (Presheaf.imageSieve φ r').arrows
Given a morphism φ : R ⟶ R' of presheaves of types and r' : R'.obj X,
this is the family of elements of R defined over the sieve Presheaf.imageSieve φ r'
which sends a map in this sieve to an arbitrary choice of a preimage of the
restriction of r'.
Equations
Instances For
theorem
CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage
{C : Type u}
[Category.{v, u} C]
{R R' : Functor Cᵒᵖ (Type w)}
(φ : R ⟶ R')
{X : Cᵒᵖ}
(r' : R'.obj X)
:
((localPreimage φ r').map φ).IsAmalgamation r'