Theory of sieves #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- For an object
Xof a categoryC, asieve Xis a set of morphisms toXwhich is closed under left-composition. - The complete lattice structure on sieves is given, as well as the Galois insertion given by downward-closing.
- A
sieve X(functorially) induces a presheaf onCtogether with a monomorphism to the yoneda embedding ofX.
Tags #
sieve, pullback
A set of arrows all with codomain X.
Equations
- category_theory.presieve X = Π ⦃Y : C⦄, set (Y ⟶ X)
Instances for category_theory.presieve
@[protected, instance]
@[protected, instance]
Equations
@[reducible]
def
category_theory.presieve.diagram
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.presieve X) :
category_theory.full_subcategory (λ (f : category_theory.over X), S f.hom) ⥤ C
Given a sieve S on X : C, its associated diagram S.diagram is defined to be
the natural functor from the full subcategory of the over category C/X consisting
of arrows in S to C.
@[reducible]
def
category_theory.presieve.cocone
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.presieve X) :
Given a sieve S on X : C, its associated cocone S.cocone is defined to be
the natural cocone over the diagram defined above with cocone point X.
def
category_theory.presieve.bind
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.presieve X)
(R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → category_theory.presieve Y) :
Given a set of arrows S all with codomain X, and a set of arrows with codomain Y for each
f : Y ⟶ X in S, produce a set of arrows with codomain X:
{ g ≫ f | (f : Y ⟶ X) ∈ S, (g : Z ⟶ Y) ∈ R f }.
@[simp]
theorem
category_theory.presieve.bind_comp
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : Y ⟶ X)
{S : category_theory.presieve X}
{R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → category_theory.presieve Y}
{g : Z ⟶ Y}
(h₁ : S f)
(h₂ : R h₁ g) :
inductive
category_theory.presieve.singleton
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
- mk : ∀ {C : Type u₁} [_inst_1 : category_theory.category C] {X Y : C} {f : Y ⟶ X}, category_theory.presieve.singleton f f
The singleton presieve.
@[simp]
theorem
category_theory.presieve.singleton_eq_iff_domain
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f g : Y ⟶ X) :
category_theory.presieve.singleton f g ↔ f = g
theorem
category_theory.presieve.singleton_self
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
inductive
category_theory.presieve.pullback_arrows
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
[category_theory.limits.has_pullbacks C]
(R : category_theory.presieve X) :
- mk : ∀ {C : Type u₁} [_inst_1 : category_theory.category C] {X Y : C} {f : Y ⟶ X} [_inst_3 : category_theory.limits.has_pullbacks C] {R : category_theory.presieve X} (Z : C) (h : Z ⟶ X), R h → category_theory.presieve.pullback_arrows f R category_theory.limits.pullback.snd
Pullback a set of arrows with given codomain along a fixed map, by taking the pullback in the
category.
This is not the same as the arrow set of sieve.pullback, but there is a relation between them
in pullback_arrows_comm.
theorem
category_theory.presieve.pullback_singleton
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : Y ⟶ X)
[category_theory.limits.has_pullbacks C]
(g : Z ⟶ X) :
inductive
category_theory.presieve.of_arrows
{C : Type u₁}
[category_theory.category C]
{X : C}
{ι : Type u_1}
(Y : ι → C)
(f : Π (i : ι), Y i ⟶ X) :
- mk : ∀ {C : Type u₁} [_inst_1 : category_theory.category C] {X : C} {ι : Type u_1} {Y : ι → C} {f : Π (i : ι), Y i ⟶ X} (i : ι), category_theory.presieve.of_arrows Y f (f i)
Construct the presieve given by the family of arrows indexed by ι.
theorem
category_theory.presieve.of_arrows_punit
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
category_theory.presieve.of_arrows (λ (_x : punit), Y) (λ (_x : punit), f) = category_theory.presieve.singleton f
theorem
category_theory.presieve.of_arrows_pullback
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
[category_theory.limits.has_pullbacks C]
{ι : Type u_1}
(Z : ι → C)
(g : Π (i : ι), Z i ⟶ X) :
category_theory.presieve.of_arrows (λ (i : ι), category_theory.limits.pullback (g i) f) (λ (i : ι), category_theory.limits.pullback.snd) = category_theory.presieve.pullback_arrows f (category_theory.presieve.of_arrows Z g)
theorem
category_theory.presieve.of_arrows_bind
{C : Type u₁}
[category_theory.category C]
{X : C}
{ι : Type u_1}
(Z : ι → C)
(g : Π (i : ι), Z i ⟶ X)
(j : Π ⦃Y : C⦄ (f : Y ⟶ X), category_theory.presieve.of_arrows Z g f → Type u_2)
(W : Π ⦃Y : C⦄ (f : Y ⟶ X) (H : category_theory.presieve.of_arrows Z g f), j f H → C)
(k : Π ⦃Y : C⦄ (f : Y ⟶ X) (H : category_theory.presieve.of_arrows Z g f) (i : j f H), W f H i ⟶ Y) :
(category_theory.presieve.of_arrows Z g).bind (λ (Y : C) (f : Y ⟶ X) (H : category_theory.presieve.of_arrows Z g f), category_theory.presieve.of_arrows (W f H) (k f H)) = category_theory.presieve.of_arrows (λ (i : Σ (i : ι), j (g i) _), W (g i.fst) _ i.snd) (λ (ij : Σ (i : ι), j (g i) _), k (g ij.fst) _ ij.snd ≫ g ij.fst)
def
category_theory.presieve.functor_pullback
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.presieve (F.obj X)) :
Given a presieve on F(X), we can define a presieve on X by taking the preimage via F.
Equations
- category_theory.presieve.functor_pullback F R = λ (_x : C) (f : _x ⟶ X), R (F.map f)
@[simp]
theorem
category_theory.presieve.functor_pullback_mem
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.presieve (F.obj X))
{Y : C}
(f : Y ⟶ X) :
category_theory.presieve.functor_pullback F R f ↔ R (F.map f)
@[simp]
theorem
category_theory.presieve.functor_pullback_id
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.presieve X) :
def
category_theory.presieve.functor_pushforward
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(S : category_theory.presieve X) :
category_theory.presieve (F.obj X)
Given a presieve on X, we can define a presieve on F(X) (which is actually a sieve)
by taking the sieve generated by the image via F.
@[nolint]
structure
category_theory.presieve.functor_pushforward_structure
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(S : category_theory.presieve X)
{Y : D}
(f : Y ⟶ F.obj X) :
Type (max u₁ v₁ v₂)
- preobj : C
- premap : self.preobj ⟶ X
- lift : Y ⟶ F.obj self.preobj
- cover : S self.premap
- fac : f = self.lift ≫ F.map self.premap
An auxillary definition in order to fix the choice of the preimages between various definitions.
Instances for category_theory.presieve.functor_pushforward_structure
- category_theory.presieve.functor_pushforward_structure.has_sizeof_inst
noncomputable
def
category_theory.presieve.get_functor_pushforward_structure
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X : C}
{F : C ⥤ D}
{S : category_theory.presieve X}
{Y : D}
{f : Y ⟶ F.obj X}
(h : category_theory.presieve.functor_pushforward F S f) :
The fixed choice of a preimage.
Equations
- category_theory.presieve.get_functor_pushforward_structure h = (λ (_x : ∃ (g : classical.some h ⟶ X) (h_1 : Y ⟶ F.obj (classical.some h)), S g ∧ f = h_1 ≫ F.map g), (λ (_x_1 : ∃ (h_1 : Y ⟶ F.obj (classical.some h)), S (classical.some _x) ∧ f = h_1 ≫ F.map (classical.some _x)), (λ (_x_2 : S (classical.some _x) ∧ f = classical.some _x_1 ≫ F.map (classical.some _x)), {preobj := classical.some h, premap := classical.some _x, lift := classical.some _x_1, cover := _, fac := _}) _) _) _
theorem
category_theory.presieve.functor_pushforward_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E)
(R : category_theory.presieve X) :
theorem
category_theory.presieve.image_mem_functor_pushforward
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(R : category_theory.presieve X)
{f : Y ⟶ X}
(h : R f) :
structure
category_theory.sieve
{C : Type u₁}
[category_theory.category C]
(X : C) :
Type (max u₁ v₁)
- arrows : category_theory.presieve X
- downward_closed' : ∀ {Y Z : C} {f : Y ⟶ X}, self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (g ≫ f)
For an object X of a category C, a sieve X is a set of morphisms to X which is closed under
left-composition.
Instances for category_theory.sieve
@[protected, instance]
def
category_theory.sieve.has_coe_to_fun
{C : Type u₁}
[category_theory.category C]
{X : C} :
has_coe_to_fun (category_theory.sieve X) (λ (_x : category_theory.sieve X), category_theory.presieve X)
Equations
@[simp]
theorem
category_theory.sieve.downward_closed
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(S : category_theory.sieve X)
{f : Y ⟶ X}
(hf : ⇑S f)
(g : Z ⟶ Y) :
theorem
category_theory.sieve.arrows_ext
{C : Type u₁}
[category_theory.category C]
{X : C}
{R S : category_theory.sieve X} :
@[protected, ext]
theorem
category_theory.sieve.ext
{C : Type u₁}
[category_theory.category C]
{X : C}
{R S : category_theory.sieve X}
(h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), ⇑R f ↔ ⇑S f) :
R = S
@[protected]
theorem
category_theory.sieve.ext_iff
{C : Type u₁}
[category_theory.category C]
{X : C}
{R S : category_theory.sieve X} :
@[protected]
def
category_theory.sieve.Sup
{C : Type u₁}
[category_theory.category C]
{X : C}
(𝒮 : set (category_theory.sieve X)) :
The supremum of a collection of sieves: the union of them all.
Equations
- category_theory.sieve.Sup 𝒮 = {arrows := λ (Y : C), {f : Y ⟶ X | ∃ (S : category_theory.sieve X) (H : S ∈ 𝒮), S.arrows f}, downward_closed' := _}
@[protected]
def
category_theory.sieve.Inf
{C : Type u₁}
[category_theory.category C]
{X : C}
(𝒮 : set (category_theory.sieve X)) :
The infimum of a collection of sieves: the intersection of them all.
Equations
- category_theory.sieve.Inf 𝒮 = {arrows := λ (Y : C), {f : Y ⟶ X | ∀ (S : category_theory.sieve X), S ∈ 𝒮 → S.arrows f}, downward_closed' := _}
@[protected]
def
category_theory.sieve.union
{C : Type u₁}
[category_theory.category C]
{X : C}
(S R : category_theory.sieve X) :
The union of two sieves is a sieve.
@[protected]
def
category_theory.sieve.inter
{C : Type u₁}
[category_theory.category C]
{X : C}
(S R : category_theory.sieve X) :
The intersection of two sieves is a sieve.
@[protected, instance]
Sieves on an object X form a complete lattice.
We generate this directly rather than using the galois insertion for nicer definitional properties.
Equations
- category_theory.sieve.complete_lattice = {sup := category_theory.sieve.union X, le := λ (S R : category_theory.sieve X), ∀ ⦃Y : C⦄ (f : Y ⟶ X), ⇑S f → ⇑R f, lt := lattice.lt._default (λ (S R : category_theory.sieve X), ∀ ⦃Y : C⦄ (f : Y ⟶ X), ⇑S f → ⇑R f), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := category_theory.sieve.inter X, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := category_theory.sieve.Sup X, le_Sup := _, Sup_le := _, Inf := category_theory.sieve.Inf X, Inf_le := _, le_Inf := _, top := {arrows := λ (_x : C), set.univ, downward_closed' := _}, bot := {arrows := λ (_x : C), ∅, downward_closed' := _}, le_top := _, bot_le := _}
@[protected, instance]
The maximal sieve always exists.
Equations
@[simp]
theorem
category_theory.sieve.Inf_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
{Ss : set (category_theory.sieve X)}
{Y : C}
(f : Y ⟶ X) :
⇑(has_Inf.Inf Ss) f ↔ ∀ (S : category_theory.sieve X), S ∈ Ss → ⇑S f
@[simp]
theorem
category_theory.sieve.Sup_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
{Ss : set (category_theory.sieve X)}
{Y : C}
(f : Y ⟶ X) :
⇑(has_Sup.Sup Ss) f ↔ ∃ (S : category_theory.sieve X) (H : S ∈ Ss), ⇑S f
@[simp]
theorem
category_theory.sieve.inter_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
{R S : category_theory.sieve X}
{Y : C}
(f : Y ⟶ X) :
@[simp]
theorem
category_theory.sieve.union_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
{R S : category_theory.sieve X}
{Y : C}
(f : Y ⟶ X) :
@[simp]
theorem
category_theory.sieve.top_apply
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
def
category_theory.sieve.generate
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.presieve X) :
Generate the smallest sieve containing the given set of arrows.
@[simp]
theorem
category_theory.sieve.generate_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.presieve X)
(Z : C)
(f : Z ⟶ X) :
@[simp]
theorem
category_theory.sieve.bind_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.presieve X)
(R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → category_theory.sieve Y) :
def
category_theory.sieve.bind
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.presieve X)
(R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → category_theory.sieve Y) :
Given a presieve on X, and a sieve on each domain of an arrow in the presieve, we can bind to
produce a sieve on X.
Equations
- category_theory.sieve.bind S R = {arrows := S.bind (λ (Y : C) (f : Y ⟶ X) (h : S f), ⇑(R h)), downward_closed' := _}
theorem
category_theory.sieve.sets_iff_generate
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.presieve X)
(S : category_theory.sieve X) :
category_theory.sieve.generate R ≤ S ↔ R ≤ ⇑S
Show that there is a galois insertion (generate, set_over).
Equations
- category_theory.sieve.gi_generate = {choice := λ (𝒢 : category_theory.presieve X) (_x : (category_theory.sieve.generate 𝒢).arrows ≤ 𝒢), category_theory.sieve.generate 𝒢, gc := _, le_l_u := _, choice_eq := _}
theorem
category_theory.sieve.le_generate
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.presieve X) :
@[simp]
theorem
category_theory.sieve.generate_sieve
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.sieve X) :
theorem
category_theory.sieve.id_mem_iff_eq_top
{C : Type u₁}
[category_theory.category C]
{X : C}
{S : category_theory.sieve X} :
If the identity arrow is in a sieve, the sieve is maximal.
theorem
category_theory.sieve.generate_of_contains_is_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{R : category_theory.presieve X}
(f : Y ⟶ X)
[category_theory.is_split_epi f]
(hf : R f) :
If an arrow set contains a split epi, it generates the maximal sieve.
@[simp]
theorem
category_theory.sieve.generate_of_singleton_is_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
[category_theory.is_split_epi f] :
@[simp]
def
category_theory.sieve.pullback
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(h : Y ⟶ X)
(S : category_theory.sieve X) :
Given a morphism h : Y ⟶ X, send a sieve S on X to a sieve on Y
as the inverse image of S with _ ≫ h.
That is, sieve.pullback S h := (≫ h) '⁻¹ S.
Equations
- category_theory.sieve.pullback h S = {arrows := λ (Y_1 : C) (sl : Y_1 ⟶ Y), ⇑S (sl ≫ h), downward_closed' := _}
@[simp]
theorem
category_theory.sieve.pullback_apply
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(h : Y ⟶ X)
(S : category_theory.sieve X)
(Y_1 : C)
(sl : Y_1 ⟶ Y) :
⇑(category_theory.sieve.pullback h S) sl = ⇑S (sl ≫ h)
@[simp]
theorem
category_theory.sieve.pullback_id
{C : Type u₁}
[category_theory.category C]
{X : C}
{S : category_theory.sieve X} :
category_theory.sieve.pullback (𝟙 X) S = S
@[simp]
theorem
category_theory.sieve.pullback_top
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : Y ⟶ X} :
theorem
category_theory.sieve.pullback_comp
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : Y ⟶ X}
{g : Z ⟶ Y}
(S : category_theory.sieve X) :
@[simp]
theorem
category_theory.sieve.pullback_inter
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : Y ⟶ X}
(S R : category_theory.sieve X) :
theorem
category_theory.sieve.pullback_eq_top_iff_mem
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{S : category_theory.sieve X}
(f : Y ⟶ X) :
⇑S f ↔ category_theory.sieve.pullback f S = ⊤
theorem
category_theory.sieve.pullback_eq_top_of_mem
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(S : category_theory.sieve X)
{f : Y ⟶ X} :
⇑S f → category_theory.sieve.pullback f S = ⊤
def
category_theory.sieve.pushforward
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
(R : category_theory.sieve Y) :
Push a sieve R on Y forward along an arrow f : Y ⟶ X: gf : Z ⟶ X is in the sieve if gf
factors through some g : Z ⟶ Y which is in R.
@[simp]
theorem
category_theory.sieve.pushforward_apply
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
(R : category_theory.sieve Y)
(Z : C)
(gf : Z ⟶ X) :
theorem
category_theory.sieve.pushforward_apply_comp
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{R : category_theory.sieve Y}
{Z : C}
{g : Z ⟶ Y}
(hg : ⇑R g)
(f : Y ⟶ X) :
⇑(category_theory.sieve.pushforward f R) (g ≫ f)
theorem
category_theory.sieve.pushforward_comp
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : Y ⟶ X}
{g : Z ⟶ Y}
(R : category_theory.sieve Z) :
theorem
category_theory.sieve.galois_connection
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
theorem
category_theory.sieve.pullback_monotone
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
theorem
category_theory.sieve.pushforward_monotone
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X) :
theorem
category_theory.sieve.le_pushforward_pullback
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
(R : category_theory.sieve Y) :
theorem
category_theory.sieve.pullback_pushforward_le
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
(R : category_theory.sieve X) :
theorem
category_theory.sieve.pushforward_union
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{f : Y ⟶ X}
(S R : category_theory.sieve Y) :
theorem
category_theory.sieve.pushforward_le_bind_of_mem
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(S : category_theory.presieve X)
(R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → category_theory.sieve Y)
(f : Y ⟶ X)
(h : S f) :
theorem
category_theory.sieve.le_pullback_bind
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(S : category_theory.presieve X)
(R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → category_theory.sieve Y)
(f : Y ⟶ X)
(h : S f) :
def
category_theory.sieve.galois_coinsertion_of_mono
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
[category_theory.mono f] :
If f is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.
Equations
def
category_theory.sieve.galois_insertion_of_is_split_epi
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : Y ⟶ X)
[category_theory.is_split_epi f] :
If f is a split epi, the pushforward-pullback adjunction on sieves is reflective.
theorem
category_theory.sieve.pullback_arrows_comm
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{X Y : C}
(f : Y ⟶ X)
(R : category_theory.presieve X) :
def
category_theory.sieve.functor_pullback
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve (F.obj X)) :
If R is a sieve, then the category_theory.presieve.functor_pullback of R is actually a sieve.
Equations
@[simp]
theorem
category_theory.sieve.functor_pullback_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve (F.obj X)) :
@[simp]
theorem
category_theory.sieve.functor_pullback_arrows
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve (F.obj X)) :
@[simp]
theorem
category_theory.sieve.functor_pullback_id
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.sieve X) :
category_theory.sieve.functor_pullback (𝟭 C) R = R
theorem
category_theory.sieve.functor_pullback_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E)
(R : category_theory.sieve ((F ⋙ G).obj X)) :
theorem
category_theory.sieve.functor_pushforward_extend_eq
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
{R : category_theory.presieve X} :
@[simp]
theorem
category_theory.sieve.functor_pushforward_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve X) :
def
category_theory.sieve.functor_pushforward
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve X) :
category_theory.sieve (F.obj X)
The sieve generated by the image of R under F.
Equations
@[simp]
theorem
category_theory.sieve.functor_pushforward_id
{C : Type u₁}
[category_theory.category C]
{X : C}
(R : category_theory.sieve X) :
theorem
category_theory.sieve.functor_pushforward_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E)
(R : category_theory.sieve X) :
theorem
category_theory.sieve.functor_galois_connection
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
theorem
category_theory.sieve.functor_pullback_monotone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
theorem
category_theory.sieve.functor_pushforward_monotone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
theorem
category_theory.sieve.le_functor_pushforward_pullback
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve X) :
theorem
category_theory.sieve.functor_pullback_pushforward_le
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve (F.obj X)) :
theorem
category_theory.sieve.functor_pushforward_union
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(S R : category_theory.sieve X) :
theorem
category_theory.sieve.functor_pullback_union
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(S R : category_theory.sieve (F.obj X)) :
theorem
category_theory.sieve.functor_pullback_inter
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(S R : category_theory.sieve (F.obj X)) :
@[simp]
theorem
category_theory.sieve.functor_pushforward_bot
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
@[simp]
theorem
category_theory.sieve.functor_pushforward_top
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
@[simp]
theorem
category_theory.sieve.functor_pullback_bot
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
@[simp]
theorem
category_theory.sieve.functor_pullback_top
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
theorem
category_theory.sieve.image_mem_functor_pushforward
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
(R : category_theory.sieve X)
{V : C}
{f : V ⟶ X}
(h : ⇑R f) :
⇑(category_theory.sieve.functor_pushforward F R) (F.map f)
def
category_theory.sieve.ess_surj_full_functor_galois_insertion
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.ess_surj F]
[category_theory.full F]
(X : C) :
When F is essentially surjective and full, the galois connection is a galois insertion.
Equations
def
category_theory.sieve.fully_faithful_functor_galois_coinsertion
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F]
(X : C) :
When F is fully faithful, the galois connection is a galois coinsertion.
def
category_theory.sieve.functor
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.sieve X) :
A sieve induces a presheaf.
@[simp]
theorem
category_theory.sieve.functor_obj
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.sieve X)
(Y : Cᵒᵖ) :
@[simp]
theorem
category_theory.sieve.functor_map_coe
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.sieve X)
(Y Z : Cᵒᵖ)
(f : Y ⟶ Z)
(g : {g // ⇑S g}) :
@[simp]
theorem
category_theory.sieve.nat_trans_of_le_app_coe
{C : Type u₁}
[category_theory.category C]
{X : C}
{S T : category_theory.sieve X}
(h : S ≤ T)
(Y : Cᵒᵖ)
(f : S.functor.obj Y) :
↑((category_theory.sieve.nat_trans_of_le h).app Y f) = f.val
def
category_theory.sieve.nat_trans_of_le
{C : Type u₁}
[category_theory.category C]
{X : C}
{S T : category_theory.sieve X}
(h : S ≤ T) :
If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.
Equations
- category_theory.sieve.nat_trans_of_le h = {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), ⟨f.val, _⟩, naturality' := _}
@[simp]
theorem
category_theory.sieve.functor_inclusion_app
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.sieve X)
(Y : Cᵒᵖ)
(f : S.functor.obj Y) :
S.functor_inclusion.app Y f = f.val
def
category_theory.sieve.functor_inclusion
{C : Type u₁}
[category_theory.category C]
{X : C}
(S : category_theory.sieve X) :
The natural inclusion from the functor induced by a sieve to the yoneda embedding.
Equations
- S.functor_inclusion = {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), f.val, naturality' := _}
Instances for category_theory.sieve.functor_inclusion
theorem
category_theory.sieve.nat_trans_of_le_comm
{C : Type u₁}
[category_theory.category C]
{X : C}
{S T : category_theory.sieve X}
(h : S ≤ T) :
@[protected, instance]
def
category_theory.sieve.functor_inclusion_is_mono
{C : Type u₁}
[category_theory.category C]
{X : C}
{S : category_theory.sieve X} :
The presheaf induced by a sieve is a subobject of the yoneda embedding.
def
category_theory.sieve.sieve_of_subfunctor
{C : Type u₁}
[category_theory.category C]
{X : C}
{R : Cᵒᵖ ⥤ Type v₁}
(f : R ⟶ category_theory.yoneda.obj X) :
A natural transformation to a representable functor induces a sieve. This is the left inverse of
functor_inclusion, shown in sieve_of_functor_inclusion.
Equations
- category_theory.sieve.sieve_of_subfunctor f = {arrows := λ (Y : C) (g : Y ⟶ X), ∃ (t : R.obj (opposite.op Y)), f.app (opposite.op Y) t = g, downward_closed' := _}
@[simp]
theorem
category_theory.sieve.sieve_of_subfunctor_apply
{C : Type u₁}
[category_theory.category C]
{X : C}
{R : Cᵒᵖ ⥤ Type v₁}
(f : R ⟶ category_theory.yoneda.obj X)
(Y : C)
(g : Y ⟶ X) :
⇑(category_theory.sieve.sieve_of_subfunctor f) g = ∃ (t : R.obj (opposite.op Y)), f.app (opposite.op Y) t = g
theorem
category_theory.sieve.sieve_of_subfunctor_functor_inclusion
{C : Type u₁}
[category_theory.category C]
{X : C}
{S : category_theory.sieve X} :
@[protected, instance]
def
category_theory.sieve.functor_inclusion_top_is_iso
{C : Type u₁}
[category_theory.category C]
{X : C} :