Skip to content

Commit c93dd21

Browse files
joelrioujoelriou
committed
feat(CategoryTheory/Sites): categories of sheaves have a separator (#19979)
In this file, we show that if `J : GrothendieckTopology C` and `A` is a preadditive category which has a separator (and suitable coproducts), then `Sheaf J A` has a separator. General results about generators are moved to a directory `CategoryTheory.Generator`. Together with #19914, we shall be able to deduce that categories of abelian sheaves are Grothendieck abelian categories (cf. #19986).
1 parent 3874e58 commit c93dd21

File tree

9 files changed

+208
-7
lines changed

9 files changed

+208
-7
lines changed

‎Mathlib.lean‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1587,7 +1587,6 @@ import Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
15871587
import Mathlib.CategoryTheory.Abelian.Exact
15881588
import Mathlib.CategoryTheory.Abelian.Ext
15891589
import Mathlib.CategoryTheory.Abelian.FunctorCategory
1590-
import Mathlib.CategoryTheory.Abelian.Generator
15911590
import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
15921591
import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
15931592
import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
@@ -1782,7 +1781,12 @@ import Mathlib.CategoryTheory.Galois.GaloisObjects
17821781
import Mathlib.CategoryTheory.Galois.IsFundamentalgroup
17831782
import Mathlib.CategoryTheory.Galois.Prorepresentability
17841783
import Mathlib.CategoryTheory.Galois.Topology
1785-
import Mathlib.CategoryTheory.Generator
1784+
import Mathlib.CategoryTheory.Generator.Abelian
1785+
import Mathlib.CategoryTheory.Generator.Basic
1786+
import Mathlib.CategoryTheory.Generator.Coproduct
1787+
import Mathlib.CategoryTheory.Generator.Preadditive
1788+
import Mathlib.CategoryTheory.Generator.Presheaf
1789+
import Mathlib.CategoryTheory.Generator.Sheaf
17861790
import Mathlib.CategoryTheory.GlueData
17871791
import Mathlib.CategoryTheory.GradedObject
17881792
import Mathlib.CategoryTheory.GradedObject.Associator
@@ -2060,7 +2064,6 @@ import Mathlib.CategoryTheory.Preadditive.Biproducts
20602064
import Mathlib.CategoryTheory.Preadditive.EilenbergMoore
20612065
import Mathlib.CategoryTheory.Preadditive.EndoFunctor
20622066
import Mathlib.CategoryTheory.Preadditive.FunctorCategory
2063-
import Mathlib.CategoryTheory.Preadditive.Generator
20642067
import Mathlib.CategoryTheory.Preadditive.HomOrthogonal
20652068
import Mathlib.CategoryTheory.Preadditive.Injective
20662069
import Mathlib.CategoryTheory.Preadditive.InjectiveResolution

‎Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
88
import Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
99
import Mathlib.Algebra.Homology.ShortComplex.Exact
1010
import Mathlib.CategoryTheory.Elements
11-
import Mathlib.CategoryTheory.Generator
11+
import Mathlib.CategoryTheory.Generator.Basic
1212

1313
/-!
1414
# Generators for the category of presheaves of modules

‎Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Bhavik Mehta
55
-/
66
import Mathlib.CategoryTheory.Comma.StructuredArrow.Small
7-
import Mathlib.CategoryTheory.Generator
7+
import Mathlib.CategoryTheory.Generator.Basic
88
import Mathlib.CategoryTheory.Limits.ConeCategory
99
import Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
1010
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

‎Mathlib/CategoryTheory/Abelian/Generator.lean‎ renamed to ‎Mathlib/CategoryTheory/Generator/Abelian.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Markus Himmel
66
import Mathlib.CategoryTheory.Abelian.Subobject
77
import Mathlib.CategoryTheory.Limits.EssentiallySmall
88
import Mathlib.CategoryTheory.Preadditive.Injective
9-
import Mathlib.CategoryTheory.Preadditive.Generator
9+
import Mathlib.CategoryTheory.Generator.Preadditive
1010
import Mathlib.CategoryTheory.Abelian.Opposite
1111

1212
/-!

‎Mathlib/CategoryTheory/Generator.lean‎ renamed to ‎Mathlib/CategoryTheory/Generator/Basic.lean‎

File renamed without changes.

‎Mathlib/CategoryTheory/Generator/Coproduct.lean‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
7+
import Mathlib.CategoryTheory.Generator.Basic
8+
import Mathlib.CategoryTheory.Limits.Shapes.Products
9+
10+
/-!
11+
# The coproduct of a separating family of objects is separating
12+
13+
If a family of objects `S : ι → C` in a category with zero morphisms
14+
is separating, then the coproduct of `S` is a separator in `C`.
15+
16+
-/
17+
18+
universe w v u
19+
20+
namespace CategoryTheory.IsSeparating
21+
22+
open Limits
23+
24+
variable {C : Type u} [Category.{v} C] [HasZeroMorphisms C]
25+
{ι : Type w} {S : ι → C}
26+
27+
open Classical in
28+
lemma isSeparator_of_isColimit_cofan
29+
(hS : IsSeparating (Set.range S)) {c : Cofan S} (hc : IsColimit c) :
30+
IsSeparator c.pt := by
31+
intro X Y f g h
32+
apply hS
33+
rintro _ ⟨i, rfl⟩ α
34+
let β : c.pt ⟶ X := Cofan.IsColimit.desc hc
35+
(fun j ↦ if hij : i = j then eqToHom (by rw [hij]) ≫ α else 0)
36+
have hβ : c.inj i ≫ β = α := by simp [β]
37+
simp only [← hβ, Category.assoc, h c.pt (by simp) β]
38+
39+
lemma isSeparator_coproduct (hS : IsSeparating (Set.range S)) [HasCoproduct S] :
40+
IsSeparator (∐ S) :=
41+
isSeparator_of_isColimit_cofan hS (colimit.isColimit _)
42+
43+
end CategoryTheory.IsSeparating

‎Mathlib/CategoryTheory/Preadditive/Generator.lean‎ renamed to ‎Mathlib/CategoryTheory/Generator/Preadditive.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Markus Himmel. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Markus Himmel
55
-/
6-
import Mathlib.CategoryTheory.Generator
6+
import Mathlib.CategoryTheory.Generator.Basic
77
import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
88

99
/-!

‎Mathlib/CategoryTheory/Generator/Presheaf.lean‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
7+
import Mathlib.CategoryTheory.Generator.Coproduct
8+
import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
9+
10+
/-!
11+
# Generators in the category of presheaves
12+
13+
In this file, we show that if `A` is a category with zero morphisms that
14+
has a separator (and suitable coproducts), then the category of
15+
presheaves `Cᵒᵖ ⥤ A` also has a separator.
16+
17+
-/
18+
19+
universe w v' v u' u
20+
21+
namespace CategoryTheory
22+
23+
open Limits Opposite
24+
25+
namespace Presheaf
26+
27+
variable {C : Type u} [Category.{v} C] {A : Type u'} [Category.{v'} A]
28+
[HasCoproducts.{v} A]
29+
30+
/-- Given `X : C` and `M : A`, this is the presheaf `Cᵒᵖ ⥤ A` which sends
31+
`Y : Cᵒᵖ` to the coproduct of copies of `M` indexed by `Y.unop ⟶ X`. -/
32+
@[simps]
33+
noncomputable def freeYoneda (X : C) (M : A) : Cᵒᵖ ⥤ A where
34+
obj Y := ∐ (fun (i : (yoneda.obj X).obj Y) ↦ M)
35+
map f := Sigma.map' ((yoneda.obj X).map f) (fun _ ↦ 𝟙 M)
36+
37+
/-- The bijection `(Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X))`. -/
38+
noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Cᵒᵖ ⥤ A} :
39+
(freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X)) where
40+
toFun f := Sigma.ι (fun (i : (yoneda.obj X).obj _) ↦ M) (𝟙 _) ≫ f.app (op X)
41+
invFun g :=
42+
{ app Y := Sigma.desc (fun φ ↦ g ≫ F.map φ.op)
43+
naturality _ _ _ := Sigma.hom_ext _ _ (by simp)}
44+
left_inv f := by
45+
ext Y
46+
refine Sigma.hom_ext _ _ (fun φ ↦ ?_)
47+
simpa using (Sigma.ι _ (𝟙 _) ≫= f.naturality φ.op).symm
48+
right_inv g := by simp
49+
50+
@[reassoc]
51+
lemma freeYonedaHomEquiv_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A}
52+
(α : freeYoneda X M ⟶ F) (f : F ⟶ G) :
53+
freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X) := by
54+
simp [freeYonedaHomEquiv]
55+
56+
@[reassoc]
57+
lemma freeYonedaHomEquiv_symm_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : M ⟶ F.obj (op X))
58+
(f : F ⟶ G) :
59+
freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X)) := by
60+
obtain ⟨β, rfl⟩ := freeYonedaHomEquiv.surjective α
61+
apply freeYonedaHomEquiv.injective
62+
simp only [Equiv.symm_apply_apply, freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]
63+
64+
variable (C)
65+
66+
lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
67+
IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) := by
68+
intro F G f g h
69+
ext ⟨X⟩
70+
refine hS _ _ ?_
71+
rintro _ ⟨i, rfl⟩ α
72+
apply freeYonedaHomEquiv.symm.injective
73+
simpa only [freeYonedaHomEquiv_symm_comp] using
74+
h _ ⟨⟨X, i⟩, rfl⟩ (freeYonedaHomEquiv.symm α)
75+
76+
lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
77+
[HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))]
78+
[HasZeroMorphisms A] :
79+
IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) :=
80+
(isSeparating C hS).isSeparator_coproduct
81+
82+
variable (A) in
83+
instance hasSeparator [HasSeparator A] [HasZeroMorphisms A] [HasCoproducts.{u} A] :
84+
HasSeparator (Cᵒᵖ ⥤ A) where
85+
hasSeparator := ⟨_, isSeparator C (S := fun (_ : Unit) ↦ separator A)
86+
(by simpa using isSeparator_separator A)⟩
87+
88+
end Presheaf
89+
90+
end CategoryTheory

‎Mathlib/CategoryTheory/Generator/Sheaf.lean‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
7+
import Mathlib.CategoryTheory.Generator.Presheaf
8+
import Mathlib.CategoryTheory.Sites.Sheafification
9+
import Mathlib.CategoryTheory.Sites.Limits
10+
11+
/-!
12+
# Generators in the category of sheaves
13+
14+
In this file, we show that if `J : GrothendieckTopology C` and `A` is a preadditive
15+
category which has a separator (and suitable coproducts), then `Sheaf J A` has a separator.
16+
17+
-/
18+
19+
universe w v' v u' u
20+
21+
namespace CategoryTheory
22+
23+
open Limits Opposite
24+
25+
namespace Sheaf
26+
27+
variable {C : Type u} [Category.{v} C]
28+
(J : GrothendieckTopology C) {A : Type u'} [Category.{v'} A]
29+
[HasCoproducts.{v} A] [HasWeakSheafify J A]
30+
31+
/-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
32+
sheaf to the presheaf `Presheaf.freeYoneda X M`. -/
33+
noncomputable def freeYoneda (X : C) (M : A) : Sheaf J A :=
34+
(presheafToSheaf J A).obj (Presheaf.freeYoneda X M)
35+
36+
variable {J} in
37+
/-- The bijection `(Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X))`
38+
when `F : Sheaf J A`, `X : C` and `M : A`. -/
39+
noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
40+
(freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) :=
41+
((sheafificationAdjunction J A).homEquiv _ _).trans Presheaf.freeYonedaHomEquiv
42+
43+
lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
44+
IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by
45+
intro F G f g hfg
46+
refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)
47+
rintro _ ⟨⟨X, i⟩, rfl⟩ a
48+
apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
49+
simpa only [← Adjunction.homEquiv_naturality_right_symm] using
50+
hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
51+
52+
lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
53+
[HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))] [Preadditive A] :
54+
IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) :=
55+
(isSeparating J hS).isSeparator_coproduct
56+
57+
variable (A) in
58+
instance hasSeparator [HasSeparator A] [Preadditive A] [HasCoproducts.{u} A] :
59+
HasSeparator (Sheaf J A) where
60+
hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A)
61+
(by simpa using isSeparator_separator A)⟩
62+
63+
end Sheaf
64+
65+
end CategoryTheory

0 commit comments

Comments
 (0)