Locally injective morphisms of (pre)sheaves #
Let C be a category equipped with a Grothendieck topology J,
and let D be a concrete category. In this file, we introduce the typeclass
Presheaf.IsLocallyInjective J φ for a morphism φ : F₁ ⟶ F₂ in the category
Cᵒᵖ ⥤ D. This means that φ is locally injective. More precisely,
if x and y are two elements of some F₁.obj U such
the images of x and y in F₂.obj U coincide, then
the equality x = y must hold locally, i.e. after restriction
by the maps of a covering sieve.
def
CategoryTheory.Presheaf.equalizerSieve
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{F : Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x y : ToType (F.obj X))
:
Sieve (Opposite.unop X)
If F : Cᵒᵖ ⥤ D is a presheaf with values in a concrete category, if x and y are
elements in F.obj X, this is the sieve of X.unop consisting of morphisms f
such that F.map f.op x = F.map f.op y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Presheaf.equalizerSieve_apply
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{F : Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x y : ToType (F.obj X))
(x✝ : C)
(f : x✝ ⟶ Opposite.unop X)
:
(equalizerSieve x y).arrows f = ((ConcreteCategory.hom (F.map f.op)) x = (ConcreteCategory.hom (F.map f.op)) y)
@[simp]
theorem
CategoryTheory.Presheaf.equalizerSieve_self_eq_top
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{F : Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x : ToType (F.obj X))
:
@[simp]
theorem
CategoryTheory.Presheaf.equalizerSieve_eq_top_iff
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{F : Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x y : ToType (F.obj X))
:
class
CategoryTheory.Presheaf.IsLocallyInjective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
:
A morphism φ : F₁ ⟶ F₂ of presheaves Cᵒᵖ ⥤ D (with D a concrete category)
is locally injective for a Grothendieck topology J on C if
whenever two sections of F₁ are sent to the same section of F₂, then these two
sections coincide locally.
- equalizerSieve_mem {X : Cᵒᵖ} (x y : ToType (F₁.obj X)) (h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y) : equalizerSieve x y ∈ J (Opposite.unop X)
Instances
theorem
CategoryTheory.Presheaf.equalizerSieve_mem
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
[IsLocallyInjective J φ]
{X : Cᵒᵖ}
(x y : ToType (F₁.obj X))
(h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y)
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_injective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X)))
:
instance
CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
[IsIso φ]
:
instance
CategoryTheory.Presheaf.isLocallyInjective_forget
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
[IsLocallyInjective J φ]
:
IsLocallyInjective J (whiskerRight φ (forget D))
theorem
CategoryTheory.Presheaf.isLocallyInjective_forget_iff
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
:
IsLocallyInjective J φ ↔ ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType (F₁.obj X)),
equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (Opposite.unop X) →
equalizerSieve x y ∈ J (Opposite.unop X)
theorem
CategoryTheory.Presheaf.equalizerSieve_mem_of_equalizerSieve_app_mem
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
{X : Cᵒᵖ}
(x y : ToType (F₁.obj X))
(h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (Opposite.unop X))
[IsLocallyInjective J φ]
:
instance
CategoryTheory.Presheaf.isLocallyInjective_comp
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ F₃ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[IsLocallyInjective J φ]
[IsLocallyInjective J ψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ F₃ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[IsLocallyInjective J (CategoryStruct.comp φ ψ)]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ F₃ : Functor Cᵒᵖ D}
{φ : F₁ ⟶ F₂}
{ψ : F₂ ⟶ F₃}
{φψ : F₁ ⟶ F₃}
(fac : CategoryStruct.comp φ ψ = φψ)
[IsLocallyInjective J φψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_iff_of_fac
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ F₃ : Functor Cᵒᵖ D}
{φ : F₁ ⟶ F₂}
{ψ : F₂ ⟶ F₃}
{φψ : F₁ ⟶ F₃}
(fac : CategoryStruct.comp φ ψ = φψ)
[IsLocallyInjective J ψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_comp_iff
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ F₃ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[IsLocallyInjective J ψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_iff_injective_of_separated
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(J : GrothendieckTopology C)
{F₁ F₂ : Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(hsep : Presieve.IsSeparated J (F₁.comp (forget D)))
:
instance
CategoryTheory.Presheaf.instIsLocallyInjectiveHomObjForgetTypeι
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(F : Functor Cᵒᵖ (Type w))
(G : Subpresheaf F)
:
IsLocallyInjective J G.ι
instance
CategoryTheory.Presheaf.isLocallyInjective_toPlus
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ (Type (max u v)))
:
IsLocallyInjective J (J.toPlus P)
instance
CategoryTheory.Presheaf.isLocallyInjective_toSheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ (Type (max u v)))
:
IsLocallyInjective J (J.toSheafify P)
instance
CategoryTheory.Presheaf.isLocallyInjective_toSheafify'
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
(J : GrothendieckTopology C)
{CD : D → Type (max u v)}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
(P : Functor Cᵒᵖ D)
[HasWeakSheafify J D]
[J.HasSheafCompose (forget D)]
[J.PreservesSheafification (forget D)]
:
IsLocallyInjective J (toSheafify J P)
@[reducible, inline]
abbrev
CategoryTheory.Sheaf.IsLocallyInjective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
:
If φ : F₁ ⟶ F₂ is a morphism of sheaves, this is an abbreviation for
Presheaf.IsLocallyInjective J φ.val. Under suitable assumptions, it
is equivalent to the injectivity of all maps φ.val.app X,
see isLocallyInjective_iff_injective.
Equations
Instances For
theorem
CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
:
instance
CategoryTheory.Sheaf.isLocallyInjective_of_iso
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
[IsIso φ]
:
theorem
CategoryTheory.Sheaf.mono_of_injective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
(hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.val.app X)))
:
Mono φ
instance
CategoryTheory.Sheaf.isLocallyInjective_forget
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (forget D)]
[IsLocallyInjective φ]
:
IsLocallyInjective ((sheafCompose J (forget D)).map φ)
theorem
CategoryTheory.Sheaf.isLocallyInjective_iff_injective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (forget D)]
:
theorem
CategoryTheory.Sheaf.mono_of_isLocallyInjective
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
{FD : D → D → Type u_1}
{CD : D → Type w}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
{J : GrothendieckTopology C}
{F₁ F₂ : Sheaf J D}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (forget D)]
[IsLocallyInjective φ]
:
Mono φ
instance
CategoryTheory.Sheaf.instIsLocallyInjectiveHomObjForgetTypeImageι
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{F G : Sheaf J (Type w)}
(f : F ⟶ G)
: