Subsheaf of types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the sub(pre)sheaf of a type valued presheaf.
Main results #
category_theory.grothendieck_topology.subpresheaf: A subpresheaf of a presheaf of types.category_theory.grothendieck_topology.subpresheaf.sheafify: The sheafification of a subpresheaf as a subpresheaf. Note that this is a sheaf only when the whole sheaf is.category_theory.grothendieck_topology.subpresheaf.sheafify_is_sheaf: The sheafification is a sheafcategory_theory.grothendieck_topology.subpresheaf.sheafify_lift: The descent of a map into a sheaf to the sheafification.category_theory.grothendieck_topology.image_sheaf: The image sheaf of a morphism.category_theory.grothendieck_topology.image_factorization: The image sheaf as alimits.image_factorization.
theorem
category_theory.grothendieck_topology.subpresheaf.ext_iff
{C : Type u}
{_inst_1 : category_theory.category C}
{F : Cᵒᵖ ⥤ Type w}
(x y : category_theory.grothendieck_topology.subpresheaf F) :
@[ext]
structure
category_theory.grothendieck_topology.subpresheaf
{C : Type u}
[category_theory.category C]
(F : Cᵒᵖ ⥤ Type w) :
Type (max u w)
- obj : Π (U : Cᵒᵖ), set (F.obj U)
- map : ∀ {U V : Cᵒᵖ} (i : U ⟶ V), self.obj U ⊆ F.map i ⁻¹' self.obj V
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
- category_theory.grothendieck_topology.subpresheaf.has_sizeof_inst
- category_theory.grothendieck_topology.subpresheaf.partial_order
- category_theory.grothendieck_topology.subpresheaf.has_top
- category_theory.grothendieck_topology.subpresheaf.nonempty
theorem
category_theory.grothendieck_topology.subpresheaf.ext
{C : Type u}
{_inst_1 : category_theory.category C}
{F : Cᵒᵖ ⥤ Type w}
(x y : category_theory.grothendieck_topology.subpresheaf F)
(h : x.obj = y.obj) :
x = y
@[protected, instance]
def
category_theory.grothendieck_topology.subpresheaf.partial_order
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w} :
@[protected, instance]
def
category_theory.grothendieck_topology.subpresheaf.has_top
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w} :
@[protected, instance]
def
category_theory.grothendieck_topology.subpresheaf.nonempty
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w} :
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.to_presheaf_obj
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(U : Cᵒᵖ) :
G.to_presheaf.obj U = ↥(G.obj U)
def
category_theory.grothendieck_topology.subpresheaf.to_presheaf
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F) :
The subpresheaf as a presheaf.
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.to_presheaf_map_coe
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(U V : Cᵒᵖ)
(i : U ⟶ V)
(x : ↥(G.obj U)) :
@[protected, instance]
def
category_theory.grothendieck_topology.category_theory.functor.obj.has_coe
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
{U : Cᵒᵖ} :
has_coe (G.to_presheaf.obj U) (F.obj U)
def
category_theory.grothendieck_topology.subpresheaf.ι
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F) :
G.to_presheaf ⟶ F
The inclusion of a subpresheaf to the original presheaf.
Equations
- G.ι = {app := λ (U : Cᵒᵖ) (x : G.to_presheaf.obj U), ↑x, naturality' := _}
Instances for category_theory.grothendieck_topology.subpresheaf.ι
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.ι_app
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(U : Cᵒᵖ)
(x : G.to_presheaf.obj U) :
@[protected, instance]
def
category_theory.grothendieck_topology.subpresheaf.ι.category_theory.mono
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F) :
def
category_theory.grothendieck_topology.subpresheaf.hom_of_le
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
{G G' : category_theory.grothendieck_topology.subpresheaf F}
(h : G ≤ G') :
G.to_presheaf ⟶ G'.to_presheaf
The inclusion of a subpresheaf to a larger subpresheaf
Equations
- category_theory.grothendieck_topology.subpresheaf.hom_of_le h = {app := λ (U : Cᵒᵖ) (x : G.to_presheaf.obj U), ⟨↑x, _⟩, naturality' := _}
Instances for category_theory.grothendieck_topology.subpresheaf.hom_of_le
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.hom_of_le_app_coe
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
{G G' : category_theory.grothendieck_topology.subpresheaf F}
(h : G ≤ G')
(U : Cᵒᵖ)
(x : G.to_presheaf.obj U) :
@[protected, instance]
def
category_theory.grothendieck_topology.subpresheaf.hom_of_le.category_theory.mono
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
{G G' : category_theory.grothendieck_topology.subpresheaf F}
(h : G ≤ G') :
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.hom_of_le_ι_assoc
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
{G G' : category_theory.grothendieck_topology.subpresheaf F}
(h : G ≤ G')
{X' : Cᵒᵖ ⥤ Type w}
(f' : F ⟶ X') :
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.hom_of_le_ι
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
{G G' : category_theory.grothendieck_topology.subpresheaf F}
(h : G ≤ G') :
@[protected, instance]
def
category_theory.grothendieck_topology.subpresheaf.ι.category_theory.is_iso
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w} :
theorem
category_theory.grothendieck_topology.subpresheaf.eq_top_iff_is_iso
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F) :
G = ⊤ ↔ category_theory.is_iso G.ι
def
category_theory.grothendieck_topology.subpresheaf.lift
{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) :
F' ⟶ G.to_presheaf
If the image of a morphism falls in a subpresheaf, then the morphism factors through it.
@[simp]
@[simp]
theorem
category_theory.grothendieck_topology.subpresheaf.sieve_of_section_apply
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
{U : Cᵒᵖ}
(s : F.obj U)
(V : C)
(f : V ⟶ opposite.unop U) :
⇑(G.sieve_of_section s) f = (F.map f.op s ∈ G.obj (opposite.op V))
def
category_theory.grothendieck_topology.subpresheaf.sieve_of_section
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
{U : Cᵒᵖ}
(s : F.obj U) :
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
- G.sieve_of_section s = {arrows := λ (V : C) (f : V ⟶ opposite.unop U), F.map f.op s ∈ G.obj (opposite.op V), downward_closed' := _}
def
category_theory.grothendieck_topology.subpresheaf.family_of_elements_of_section
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
{U : Cᵒᵖ}
(s : F.obj U) :
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
- G.family_of_elements_of_section s = λ (V : C) (i : V ⟶ opposite.unop U) (hi : (G.sieve_of_section s).arrows i), ⟨F.map i.op s, hi⟩
theorem
category_theory.grothendieck_topology.subpresheaf.family_of_elements_compatible
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
{U : Cᵒᵖ}
(s : F.obj U) :
theorem
category_theory.grothendieck_topology.subpresheaf.nat_trans_naturality
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(f : F' ⟶ G.to_presheaf)
{U V : Cᵒᵖ}
(i : U ⟶ V)
(x : F'.obj U) :
def
category_theory.grothendieck_topology.subpresheaf.sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F) :
The sheafification of a subpresheaf as a subpresheaf. Note that this is a sheaf only when the whole presheaf is a sheaf.
Equations
- category_theory.grothendieck_topology.subpresheaf.sheafify J G = {obj := λ (U : Cᵒᵖ), {s : F.obj U | G.sieve_of_section s ∈ ⇑J (opposite.unop U)}, map := _}
theorem
category_theory.grothendieck_topology.subpresheaf.le_sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F) :
theorem
category_theory.grothendieck_topology.subpresheaf.eq_sheafify
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(h : category_theory.presieve.is_sheaf J F)
(hG : category_theory.presieve.is_sheaf J G.to_presheaf) :
theorem
category_theory.grothendieck_topology.subpresheaf.sheafify_is_sheaf
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(hF : category_theory.presieve.is_sheaf J F) :
theorem
category_theory.grothendieck_topology.subpresheaf.eq_sheafify_iff
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(h : category_theory.presieve.is_sheaf J F) :
theorem
category_theory.grothendieck_topology.subpresheaf.is_sheaf_iff
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(h : category_theory.presieve.is_sheaf J F) :
category_theory.presieve.is_sheaf J G.to_presheaf ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieve_of_section s ∈ ⇑J (opposite.unop U) → s ∈ G.obj U
theorem
category_theory.grothendieck_topology.subpresheaf.sheafify_sheafify
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(h : category_theory.presieve.is_sheaf J F) :
noncomputable
def
category_theory.grothendieck_topology.subpresheaf.sheafify_lift
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(f : G.to_presheaf ⟶ F')
(h : category_theory.presieve.is_sheaf J F') :
The lift of a presheaf morphism onto the sheafification subpresheaf.
Equations
- G.sheafify_lift f h = {app := λ (U : Cᵒᵖ) (s : (category_theory.grothendieck_topology.subpresheaf.sheafify J G).to_presheaf.obj U), _.amalgamate (category_theory.presieve.family_of_elements.comp_presheaf_map f (G.family_of_elements_of_section ↑s)) _, naturality' := _}
theorem
category_theory.grothendieck_topology.subpresheaf.to_sheafify_lift
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(f : G.to_presheaf ⟶ F')
(h : category_theory.presieve.is_sheaf J F') :
theorem
category_theory.grothendieck_topology.subpresheaf.to_sheafify_lift_unique
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : Cᵒᵖ ⥤ Type w}
(G : category_theory.grothendieck_topology.subpresheaf F)
(h : category_theory.presieve.is_sheaf J F')
(l₁ l₂ : (category_theory.grothendieck_topology.subpresheaf.sheafify J G).to_presheaf ⟶ F')
(e : category_theory.grothendieck_topology.subpresheaf.hom_of_le _ ≫ l₁ = category_theory.grothendieck_topology.subpresheaf.hom_of_le _ ≫ l₂) :
l₁ = l₂
theorem
category_theory.grothendieck_topology.subpresheaf.sheafify_le
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F : Cᵒᵖ ⥤ Type w}
(G G' : category_theory.grothendieck_topology.subpresheaf F)
(h : G ≤ G')
(hF : category_theory.presieve.is_sheaf J F)
(hG' : category_theory.presieve.is_sheaf J G'.to_presheaf) :
@[simp]
theorem
category_theory.grothendieck_topology.image_presheaf_obj
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F)
(U : Cᵒᵖ) :
def
category_theory.grothendieck_topology.image_presheaf
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F) :
The image presheaf of a morphism, whose components are the set-theoretic images.
@[simp]
theorem
category_theory.grothendieck_topology.image_presheaf_id
{C : Type u}
[category_theory.category C]
{F : Cᵒᵖ ⥤ Type w} :
@[simp]
theorem
category_theory.grothendieck_topology.to_image_presheaf_app_coe
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F)
(U : Cᵒᵖ)
(x : F'.obj U) :
↑((category_theory.grothendieck_topology.to_image_presheaf f).app U x) = f.app U x
def
category_theory.grothendieck_topology.to_image_presheaf
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F) :
A morphism factors through the image presheaf.
Equations
Instances for category_theory.grothendieck_topology.to_image_presheaf
@[simp]
theorem
category_theory.grothendieck_topology.to_image_presheaf_sheafify_app_coe
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F)
(X : Cᵒᵖ)
(ᾰ : F'.obj X) :
↑((J.to_image_presheaf_sheafify f).app X ᾰ) = f.app X ᾰ
def
category_theory.grothendieck_topology.to_image_presheaf_sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F) :
A morphism factors through the sheafification of the image presheaf.
@[simp]
theorem
category_theory.grothendieck_topology.to_image_presheaf_ι
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type w}
(f : F' ⟶ F) :
theorem
category_theory.grothendieck_topology.image_presheaf_comp_le
{C : Type u}
[category_theory.category C]
{F F' F'' : Cᵒᵖ ⥤ Type w}
(f₁ : F ⟶ F')
(f₂ : F' ⟶ F'') :
@[protected, instance]
def
category_theory.grothendieck_topology.to_image_presheaf.category_theory.is_iso
{C : Type u}
[category_theory.category C]
{F F' : Cᵒᵖ ⥤ Type (max v w)}
(f : F ⟶ F')
[hf : category_theory.mono f] :
def
category_theory.grothendieck_topology.image_sheaf
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
category_theory.Sheaf J (Type w)
The image sheaf of a morphism between sheaves, defined to be the sheafification of
image_presheaf.
@[simp]
theorem
category_theory.grothendieck_topology.image_sheaf_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
def
category_theory.grothendieck_topology.to_image_sheaf
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
A morphism factors through the image sheaf.
Equations
Instances for category_theory.grothendieck_topology.to_image_sheaf
@[simp]
theorem
category_theory.grothendieck_topology.to_image_sheaf_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
@[simp]
theorem
category_theory.grothendieck_topology.image_sheaf_ι_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
def
category_theory.grothendieck_topology.image_sheaf_ι
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
The inclusion of the image sheaf to the target.
Equations
Instances for category_theory.grothendieck_topology.image_sheaf_ι
@[simp]
theorem
category_theory.grothendieck_topology.to_image_sheaf_ι_assoc
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F')
{X' : category_theory.Sheaf J (Type w)}
(f' : F' ⟶ X') :
@[simp]
theorem
category_theory.grothendieck_topology.to_image_sheaf_ι
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
@[protected, instance]
def
category_theory.grothendieck_topology.image_sheaf_ι.category_theory.mono
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
@[protected, instance]
def
category_theory.grothendieck_topology.to_image_sheaf.category_theory.epi
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
def
category_theory.grothendieck_topology.image_mono_factorization
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type w)}
(f : F ⟶ F') :
The mono factorization given by image_sheaf for a morphism.
noncomputable
def
category_theory.grothendieck_topology.image_factorization
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{F F' : category_theory.Sheaf J (Type (max v u))}
(f : F ⟶ F') :
The mono factorization given by image_sheaf for a morphism is an image.
Equations
- category_theory.grothendieck_topology.image_factorization f = {F := category_theory.grothendieck_topology.image_mono_factorization f, is_image := {lift := λ (I : category_theory.limits.mono_factorisation f), {val := category_theory.grothendieck_topology.subpresheaf.hom_of_le _ ≫ category_theory.inv (category_theory.grothendieck_topology.to_image_presheaf I.m.val)}, lift_fac' := _}}
@[protected, instance]