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}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (CategoryTheory.forget A).obj (G.obj (Opposite.op 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}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U)))
(V : C)
(i : V ⟶ U)
:
(CategoryTheory.Presheaf.imageSieve f s).arrows i = ∃ (t : (CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U)))
:
CategoryTheory.Presheaf.imageSieve f s = (CategoryTheory.GrothendieckTopology.imagePresheaf
(CategoryTheory.whiskerRight f (CategoryTheory.forget A))).sieveOfSection
s
theorem
CategoryTheory.Presheaf.imageSieve_whisker_forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U)))
:
theorem
CategoryTheory.Presheaf.imageSieve_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : C}
(s : (CategoryTheory.forget A).obj (F.obj (Opposite.op U)))
:
CategoryTheory.Presheaf.imageSieve f ((f.app (Opposite.op U)) s) = ⊤
noncomputable def
CategoryTheory.Presheaf.localPreimage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : Cᵒᵖ}
(s : (CategoryTheory.forget A).obj (G.obj U))
{V : C}
(g : V ⟶ Opposite.unop U)
(hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g)
:
(CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
{U : Cᵒᵖ}
(s : (CategoryTheory.forget A).obj (G.obj U))
{V : C}
(g : V ⟶ Opposite.unop U)
(hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g)
:
(f.app (Opposite.op V)) (CategoryTheory.Presheaf.localPreimage f s g hg) = (G.map g.op) s
class
CategoryTheory.Presheaf.IsLocallySurjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.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.
- imageSieve_mem : ∀ {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))), CategoryTheory.Presheaf.imageSieve f s ∈ J U
Instances
theorem
CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
{inst_1 : CategoryTheory.Category.{v', u'} A} {inst_2 : CategoryTheory.ConcreteCategory A}
{F G : CategoryTheory.Functor Cᵒᵖ A} {f : F ⟶ G} [self : CategoryTheory.Presheaf.IsLocallySurjective J f] {U : C}
(s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))), CategoryTheory.Presheaf.imageSieve f s ∈ J U
theorem
CategoryTheory.Presheaf.imageSieve_mem
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
[CategoryTheory.Presheaf.IsLocallySurjective J f]
{U : Cᵒᵖ}
(s : (CategoryTheory.forget A).obj (G.obj U))
:
CategoryTheory.Presheaf.imageSieve f s ∈ J (Opposite.unop U)
instance
CategoryTheory.Presheaf.instIsLocallySurjectiveWhiskerRightOppositeForget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
[CategoryTheory.Presheaf.IsLocallySurjective J f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{F : CategoryTheory.Functor Cᵒᵖ (Type w)}
{G : CategoryTheory.Functor Cᵒᵖ (Type w)}
(f : F ⟶ G)
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_surjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
(H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U))
:
instance
CategoryTheory.Presheaf.isLocallySurjective_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
[CategoryTheory.IsIso f]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallySurjective_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallySurjective J f₁]
[CategoryTheory.Presheaf.IsLocallySurjective J f₂]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
{f₃ : F₁ ⟶ F₃}
(fac : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃)
[CategoryTheory.Presheaf.IsLocallySurjective J f₃]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_iff_of_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
{f₃ : F₁ ⟶ F₃}
(fac : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃)
[CategoryTheory.Presheaf.IsLocallySurjective J f₁]
:
theorem
CategoryTheory.Presheaf.comp_isLocallySurjective_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallySurjective J f₁]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_le
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{K : CategoryTheory.GrothendieckTopology C}
(hJK : J ≤ K)
{F : CategoryTheory.Functor Cᵒᵖ A}
{G : CategoryTheory.Functor Cᵒᵖ A}
(f : F ⟶ G)
(h : CategoryTheory.Presheaf.IsLocallySurjective J f)
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)]
[CategoryTheory.Presheaf.IsLocallySurjective J f₁]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
(f₃ : F₁ ⟶ F₃)
(fac : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃)
[CategoryTheory.Presheaf.IsLocallyInjective J f₃]
[CategoryTheory.Presheaf.IsLocallySurjective J f₁]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)]
[CategoryTheory.Presheaf.IsLocallyInjective J f₂]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
(f₃ : F₁ ⟶ F₃)
(fac : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃)
[CategoryTheory.Presheaf.IsLocallySurjective J f₃]
[CategoryTheory.Presheaf.IsLocallyInjective J f₂]
:
theorem
CategoryTheory.Presheaf.comp_isLocallyInjective_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallyInjective J f₁]
[CategoryTheory.Presheaf.IsLocallySurjective J f₁]
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_comp_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Functor Cᵒᵖ A}
{F₂ : CategoryTheory.Functor Cᵒᵖ A}
{F₃ : CategoryTheory.Functor Cᵒᵖ A}
(f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallyInjective J f₂]
[CategoryTheory.Presheaf.IsLocallySurjective J f₂]
:
instance
CategoryTheory.Presheaf.instIsLocallySurjectiveToImagePresheafSheafify
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ (Type w)}
{F₂ : CategoryTheory.Functor Cᵒᵖ (Type w)}
(f : F₁ ⟶ F₂)
:
CategoryTheory.Presheaf.IsLocallySurjective J (J.toImagePresheafSheafify f)
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Presheaf.sheafificationIsoImagePresheaf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
:
J.sheafify F ≅ (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J
(CategoryTheory.GrothendieckTopology.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}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
:
CategoryTheory.Presheaf.IsLocallySurjective J (J.toPlus P)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallySurjective_toSheafify
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
:
CategoryTheory.Presheaf.IsLocallySurjective J (J.toSheafify P)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallySurjective_toSheafify'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
[CategoryTheory.ConcreteCategory D]
(P : CategoryTheory.Functor Cᵒᵖ D)
[CategoryTheory.HasWeakSheafify J D]
[J.HasSheafCompose (CategoryTheory.forget D)]
[J.PreservesSheafification (CategoryTheory.forget D)]
:
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
CategoryTheory.Sheaf.IsLocallySurjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Sheaf J A}
{F₂ : CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Sheaf J A}
{F₂ : CategoryTheory.Sheaf J A}
(φ : F₁ ⟶ F₂)
:
instance
CategoryTheory.Sheaf.isLocallySurjective_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Sheaf J A}
{F₂ : CategoryTheory.Sheaf J A}
{F₃ : CategoryTheory.Sheaf J A}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[CategoryTheory.Sheaf.IsLocallySurjective φ]
[CategoryTheory.Sheaf.IsLocallySurjective ψ]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Sheaf.isLocallySurjective_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Sheaf J A}
{F₂ : CategoryTheory.Sheaf J A}
(φ : F₁ ⟶ F₂)
[CategoryTheory.IsIso φ]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Sheaf.instIsLocallySurjectiveToImageSheaf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{F : CategoryTheory.Sheaf J (Type w)}
{G : CategoryTheory.Sheaf J (Type w)}
(f : F ⟶ G)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Sheaf.instIsLocallySurjectiveMapTypeSheafComposeForget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Sheaf J A}
{F₂ : CategoryTheory.Sheaf J A}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (CategoryTheory.forget A)]
[CategoryTheory.Sheaf.IsLocallySurjective φ]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Sheaf.isLocallySurjective_iff_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{F : CategoryTheory.Sheaf J (Type w)}
{G : CategoryTheory.Sheaf J (Type w)}
(f : F ⟶ G)
:
instance
CategoryTheory.Sheaf.epi_of_isLocallySurjective'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J (Type w)}
{F₂ : CategoryTheory.Sheaf J (Type w)}
(φ : F₁ ⟶ F₂)
[CategoryTheory.Sheaf.IsLocallySurjective φ]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Sheaf.epi_of_isLocallySurjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{A : Type u'}
[CategoryTheory.Category.{v', u'} A]
[CategoryTheory.ConcreteCategory A]
{F₁ : CategoryTheory.Sheaf J A}
{F₂ : CategoryTheory.Sheaf J A}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (CategoryTheory.forget A)]
[CategoryTheory.Sheaf.IsLocallySurjective φ]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Sheaf.isLocallySurjective_iff_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{F : CategoryTheory.Sheaf J (Type w)}
{G : CategoryTheory.Sheaf J (Type w)}
(φ : F ⟶ G)
[CategoryTheory.HasSheafify J (Type w)]
:
noncomputable def
CategoryTheory.Presieve.FamilyOfElements.localPreimage
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{R : CategoryTheory.Functor Cᵒᵖ (Type w)}
{R' : CategoryTheory.Functor Cᵒᵖ (Type w)}
(φ : R ⟶ R')
{X : Cᵒᵖ}
(r' : R'.obj X)
:
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}
[CategoryTheory.Category.{v, u} C]
{R : CategoryTheory.Functor Cᵒᵖ (Type w)}
{R' : CategoryTheory.Functor Cᵒᵖ (Type w)}
(φ : R ⟶ R')
{X : Cᵒᵖ}
(r' : R'.obj X)
:
((CategoryTheory.Presieve.FamilyOfElements.localPreimage φ r').map φ).IsAmalgamation r'