mathlib documentation

category_theory.sites.subsheaf

Subsheaf of types #

We define the sub(pre)sheaf of a type valued presheaf.

Main results #

@[ext]

A subpresheaf of a presheaf consists of a subset of F.obj U for every U, compatible with the restriction maps F.map i.

Instances for category_theory.grothendieck_topology.subpresheaf

The subpresheaf as a presheaf.

Equations

The inclusion of a subpresheaf to a larger subpresheaf

Equations
Instances for category_theory.grothendieck_topology.subpresheaf.hom_of_le

If the image of a morphism falls in a subpresheaf, then the morphism factors through it.

Equations
@[simp]
theorem category_theory.grothendieck_topology.subpresheaf.lift_app_coe {C : Type u} [category_theory.category C] {F F' : Cᵒᵖ Type w} (G : category_theory.grothendieck_topology.subpresheaf F) (f : F' F) (hf : (U : Cᵒᵖ) (x : F'.obj U), f.app U x G.obj U) (U : Cᵒᵖ) (x : F'.obj U) :
((G.lift f hf).app U x) = f.app U x
@[simp]
@[simp]
theorem category_theory.grothendieck_topology.subpresheaf.lift_ι_assoc {C : Type u} [category_theory.category C] {F F' : Cᵒᵖ Type w} (G : category_theory.grothendieck_topology.subpresheaf F) (f : F' F) (hf : (U : Cᵒᵖ) (x : F'.obj U), f.app U x G.obj U) {X' : Cᵒᵖ Type w} (f' : F X') :
G.lift f hf G.ι f' = f f'

Given a subpresheaf G of F, an F-section s on U, we may define a sieve of U consisting of all f : V ⟶ U such that the restriction of s along f is in G.

Equations

Given a F-section s on U and a subpresheaf G, we may define a family of elements in G consisting of the restrictions of s

Equations

The sheafification of a subpresheaf as a subpresheaf. Note that this is a sheaf only when the whole presheaf is a sheaf.

Equations

The image presheaf of a morphism, whose components are the set-theoretic images.

Equations