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.
@[simp]
theorem
CategoryTheory.Presheaf.equalizerSieve_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{F : CategoryTheory.Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F.obj X))
(y : (CategoryTheory.forget D).obj (F.obj X))
:
∀ (x_1 : C) (f : x_1 ⟶ X.unop),
(CategoryTheory.Presheaf.equalizerSieve x y).arrows f = ((F.map f.op) x = (F.map f.op) y)
def
CategoryTheory.Presheaf.equalizerSieve
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{F : CategoryTheory.Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F.obj X))
(y : (CategoryTheory.forget D).obj (F.obj X))
:
CategoryTheory.Sieve X.unop
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
- CategoryTheory.Presheaf.equalizerSieve x y = { arrows := fun (x_1 : C) (f : x_1 ⟶ X.unop) => (F.map f.op) x = (F.map f.op) y, downward_closed := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Presheaf.equalizerSieve_self_eq_top
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{F : CategoryTheory.Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F.obj X))
:
@[simp]
theorem
CategoryTheory.Presheaf.equalizerSieve_eq_top_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{F : CategoryTheory.Functor Cᵒᵖ D}
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F.obj X))
(y : (CategoryTheory.forget D).obj (F.obj X))
:
CategoryTheory.Presheaf.equalizerSieve x y = ⊤ ↔ x = y
class
CategoryTheory.Presheaf.IsLocallyInjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.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 : (CategoryTheory.forget D).obj (F₁.obj X)), (φ.app X) x = (φ.app X) y → CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves X.unop
Instances
theorem
CategoryTheory.Presheaf.IsLocallyInjective.equalizerSieve_mem
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
{φ : F₁ ⟶ F₂}
[self : CategoryTheory.Presheaf.IsLocallyInjective J φ]
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F₁.obj X))
(y : (CategoryTheory.forget D).obj (F₁.obj X))
(h : (φ.app X) x = (φ.app X) y)
:
CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves X.unop
theorem
CategoryTheory.Presheaf.equalizerSieve_mem
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F₁.obj X))
(y : (CategoryTheory.forget D).obj (F₁.obj X))
(h : (φ.app X) x = (φ.app X) y)
:
CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves X.unop
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X))
:
instance
CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
[CategoryTheory.IsIso φ]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallyInjective_forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Presheaf.isLocallyInjective_forget_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
:
CategoryTheory.Presheaf.IsLocallyInjective J φ ↔ ∀ ⦃X : Cᵒᵖ⦄ (x y : (CategoryTheory.forget D).obj (F₁.obj X)),
CategoryTheory.Presheaf.equalizerSieve ((φ.app X) x) ((φ.app X) y) ∈ J.sieves X.unop →
CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves X.unop
theorem
CategoryTheory.Presheaf.equalizerSieve_mem_of_equalizerSieve_app_mem
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
{X : Cᵒᵖ}
(x : (CategoryTheory.forget D).obj (F₁.obj X))
(y : (CategoryTheory.forget D).obj (F₁.obj X))
(h : CategoryTheory.Presheaf.equalizerSieve ((φ.app X) x) ((φ.app X) y) ∈ J.sieves X.unop)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
:
CategoryTheory.Presheaf.equalizerSieve x y ∈ J.sieves X.unop
instance
CategoryTheory.Presheaf.isLocallyInjective_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
{F₃ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallyInjective J ψ]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
{F₃ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp φ ψ)]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
{F₃ : CategoryTheory.Functor Cᵒᵖ D}
{φ : F₁ ⟶ F₂}
{ψ : F₂ ⟶ F₃}
{φψ : F₁ ⟶ F₃}
(fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ)
[CategoryTheory.Presheaf.IsLocallyInjective J φψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_iff_of_fac
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
{F₃ : CategoryTheory.Functor Cᵒᵖ D}
{φ : F₁ ⟶ F₂}
{ψ : F₂ ⟶ F₃}
{φψ : F₁ ⟶ F₃}
(fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ)
[CategoryTheory.Presheaf.IsLocallyInjective J ψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_comp_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
{F₃ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(ψ : F₂ ⟶ F₃)
[CategoryTheory.Presheaf.IsLocallyInjective J ψ]
:
theorem
CategoryTheory.Presheaf.isLocallyInjective_iff_injective_of_separated
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
(J : CategoryTheory.GrothendieckTopology C)
{F₁ : CategoryTheory.Functor Cᵒᵖ D}
{F₂ : CategoryTheory.Functor Cᵒᵖ D}
(φ : F₁ ⟶ F₂)
(hsep : CategoryTheory.Presieve.IsSeparated J (F₁.comp (CategoryTheory.forget D)))
:
CategoryTheory.Presheaf.IsLocallyInjective J φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)
instance
CategoryTheory.Presheaf.instIsLocallyInjectiveι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor Cᵒᵖ (Type w))
(G : CategoryTheory.GrothendieckTopology.Subpresheaf F)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallyInjective_toPlus
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
:
CategoryTheory.Presheaf.IsLocallyInjective J (J.toPlus P)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallyInjective_toSheafify
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
:
CategoryTheory.Presheaf.IsLocallyInjective J (J.toSheafify P)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Presheaf.isLocallyInjective_toSheafify'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
(J : CategoryTheory.GrothendieckTopology C)
[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.IsLocallyInjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.Sheaf J D}
(φ : F₁ ⟶ F₂)
:
instance
CategoryTheory.Sheaf.isLocallyInjective_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.Sheaf J D}
(φ : F₁ ⟶ F₂)
[CategoryTheory.IsIso φ]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Sheaf.isLocallyInjective_forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.Sheaf J D}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (CategoryTheory.forget D)]
[CategoryTheory.Sheaf.IsLocallyInjective φ]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Sheaf.isLocallyInjective_iff_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.Sheaf J D}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (CategoryTheory.forget D)]
:
CategoryTheory.Sheaf.IsLocallyInjective φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X)
theorem
CategoryTheory.Sheaf.mono_of_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.Sheaf J D}
(φ : F₁ ⟶ F₂)
(hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X))
:
theorem
CategoryTheory.Sheaf.mono_of_isLocallyInjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.ConcreteCategory D]
{J : CategoryTheory.GrothendieckTopology C}
{F₁ : CategoryTheory.Sheaf J D}
{F₂ : CategoryTheory.Sheaf J D}
(φ : F₁ ⟶ F₂)
[J.HasSheafCompose (CategoryTheory.forget D)]
[CategoryTheory.Sheaf.IsLocallyInjective φ]
:
instance
CategoryTheory.Sheaf.instIsLocallyInjectiveImageSheafι
{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
- ⋯ = ⋯