feat(CategoryTheory/Sites): the category structure on the points of a site (#31711)

Author: joelriou

Mathlib.lean

@@ -3038,6 +3038,7 @@ public import Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
 public import Mathlib.CategoryTheory.Sites.Over
 public import Mathlib.CategoryTheory.Sites.Plus
 public import Mathlib.CategoryTheory.Sites.Point.Basic
+public import Mathlib.CategoryTheory.Sites.Point.Category
 public import Mathlib.CategoryTheory.Sites.Precoverage
 public import Mathlib.CategoryTheory.Sites.Preserves
 public import Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Mathlib/CategoryTheory/Sites/Point/Basic.lean

@@ -97,6 +97,13 @@ noncomputable def toPresheafFiber (X : C) (x : Φ.fiber.obj X) (P : Cᵒᵖ ⥤
     P.obj (op X) ⟶ Φ.presheafFiber.obj P :=
   colimit.ι ((CategoryOfElements.π Φ.fiber).op ⋙ P) (op ⟨X, x⟩)
 
+@[ext]
+lemma presheafFiber_hom_ext
+    {P : Cᵒᵖ ⥤ A} {T : A} {f g : Φ.presheafFiber.obj P ⟶ T}
+    (h : ∀ (X : C) (x : Φ.fiber.obj X), Φ.toPresheafFiber X x P ≫ f =
+      Φ.toPresheafFiber X x P ≫ g) : f = g :=
+  colimit.hom_ext (by rintro ⟨⟨X, x⟩⟩; exact h X x)
+
 /-- Given a point `Φ` of a site `(C, J)`, `X : C` and `x : Φ.fiber.obj X`,
 this is the map `P.obj (op X) ⟶ Φ.presheafFiber.obj P` for any `P : Cᵒᵖ ⥤ A`
 as a natural transformation. -/
@@ -106,20 +113,38 @@ noncomputable def toPresheafFiberNatTrans (X : C) (x : Φ.fiber.obj X) :
   app := Φ.toPresheafFiber X x
   naturality _ _ f := by simp [presheafFiber, toPresheafFiber]
 
-@[elementwise (attr := simp)]
+@[reassoc (attr := simp), elementwise (attr := simp)]
 lemma toPresheafFiber_w {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X) (P : Cᵒᵖ ⥤ A) :
     P.map f.op ≫ Φ.toPresheafFiber X x P =
       Φ.toPresheafFiber Y (Φ.fiber.map f x) P :=
   colimit.w ((CategoryOfElements.π Φ.fiber).op ⋙ P)
       (CategoryOfElements.homMk ⟨X, x⟩ ⟨Y, Φ.fiber.map f x⟩ f rfl).op
 
-@[reassoc (attr := elementwise)]
+@[reassoc (attr := simp), elementwise (attr := simp)]
 lemma toPresheafFiber_naturality {P Q : Cᵒᵖ ⥤ A} (g : P ⟶ Q) (X : C) (x : Φ.fiber.obj X) :
     Φ.toPresheafFiber X x P ≫ Φ.presheafFiber.map g =
       g.app (op X) ≫ Φ.toPresheafFiber X x Q :=
   ((Φ.toPresheafFiberNatTrans X x).naturality g).symm
 
-attribute [simp] toPresheafFiber_naturality_apply
+section
+
+variable {P : Cᵒᵖ ⥤ A} {T : A}
+  (φ : ∀ (X : C) (_ : Φ.fiber.obj X), P.obj (op X) ⟶ T)
+  (hφ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
+    P.map f.op ≫ φ X x = φ Y (Φ.fiber.map f x) := by cat_disch)
+
+/-- Constructor for morphisms from the fiber of a presheaf. -/
+noncomputable def presheafFiberDesc :
+    Φ.presheafFiber.obj P ⟶ T :=
+  colimit.desc _ (Cocone.mk _ { app x := φ x.unop.1 x.unop.2 })
+
+@[reassoc (attr := simp)]
+lemma toPresheafFiber_presheafFiberDesc (X : C) (x : Φ.fiber.obj X) :
+    Φ.toPresheafFiber X x P ≫ Φ.presheafFiberDesc φ hφ = φ X x :=
+  colimit.ι_desc _ _
+
+end
+
 variable {FC : A → A → Type*} {CC : A → Type w'}
   [∀ (X Y : A), FunLike (FC X Y) (CC X) (CC Y)]
   [ConcreteCategory.{w'} A FC]

Mathlib/CategoryTheory/Sites/Point/Category.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.CategoryTheory.Sites.Point.Basic
+
+/-!
+# The category of points of a site
+
+We define the category structure on the points of a site `(C, J)`:
+a morphism between `Φ₁ ⟶ Φ₂` between two points consists of a
+morphism `Φ₂.fiber ⟶ Φ₁.fiber` (SGA 4 IV 3.2).
+
+## References
+* [Alexander Grothendieck and Jean-Louis Verdier, *Exposé IV : Topos*,
+  SGA 4 IV 3.2][sga-4-tome-1]
+
+-/
+
+@[expose] public section
+
+universe w v v' u u'
+
+namespace CategoryTheory
+
+open Limits Opposite
+
+variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
+
+namespace GrothendieckTopology.Point
+
+/-- A morphism between points of a site consists of a morphism
+between the functors `Point.fiber`, in the opposite direction. -/
+@[ext]
+structure Hom (Φ₁ Φ₂ : Point.{w} J) where
+  /-- a natural transformation, in the opposite direction -/
+  hom : Φ₂.fiber ⟶ Φ₁.fiber
+
+instance : Category (Point.{w} J) where
+  Hom := Hom
+  id _ := ⟨𝟙 _⟩
+  comp f g := ⟨g.hom ≫ f.hom⟩
+
+@[ext]
+lemma hom_ext {Φ₁ Φ₂ : Point.{w} J} {f g : Φ₁ ⟶ Φ₂} (h : f.hom = g.hom) : f = g :=
+  Hom.ext h
+
+@[simp]
+lemma id_hom (Φ : Point.{w} J) : Hom.hom (𝟙 Φ) = 𝟙 _ := rfl
+
+@[simp, reassoc]
+lemma comp_hom {Φ₁ Φ₂ Φ₃ : Point.{w} J} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) :
+    (f ≫ g).hom = g.hom ≫ f.hom := rfl
+
+variable {A : Type u'} [Category.{v'} A]
+  [HasColimitsOfSize.{w, w} A]
+
+namespace Hom
+
+variable {Φ₁ Φ₂ Φ₃ : Point.{w} J} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃)
+
+attribute [local simp] FunctorToTypes.naturality in
+/-- The natural transformation on fibers of presheaves that is induced
+by a morphism of points of a site. -/
+@[simps]
+noncomputable def presheafFiber :
+    Φ₂.presheafFiber (A := A) ⟶ Φ₁.presheafFiber where
+  app P := Φ₂.presheafFiberDesc (fun X x ↦ Φ₁.toPresheafFiber X (f.hom.app X x) P)
+
+@[simp]
+lemma presheafFiber_id (Φ : Point.{w} J) :
+    presheafFiber (𝟙 Φ) (A := A) = 𝟙 _ := by
+  cat_disch
+
+@[reassoc, simp]
+lemma presheafFiber_comp :
+    (f ≫ g).presheafFiber (A := A) = g.presheafFiber ≫ f.presheafFiber := by
+  cat_disch
+
+/-- The natural transformation on fibers of sheaves that is induced
+by a morphism of points of a site. -/
+noncomputable abbrev sheafFiber :
+    Φ₂.sheafFiber (A := A) ⟶ Φ₁.sheafFiber :=
+  Functor.whiskerLeft _ f.presheafFiber
+
+@[simp]
+lemma sheafFiber_id (Φ : Point.{w} J) :
+    sheafFiber (𝟙 Φ) (A := A) = 𝟙 _ := by
+  cat_disch
+
+@[reassoc, simp]
+lemma sheafFiber_comp :
+    (f ≫ g).sheafFiber (A := A) = g.sheafFiber ≫ f.sheafFiber := by
+  cat_disch
+
+end Hom
+
+end GrothendieckTopology.Point
+
+end CategoryTheory

docs/references.bib

@@ -4580,6 +4580,31 @@ @Book{            serre1968
   mrnumber      = {354618}
 }
 
+@Book{            sga-4-tome-1,
+  editor        = {Artin, Michael and Grothendieck, Alexander and Verdier, J.
+                  L. and Bourbaki, N. and Deligne, P. and Saint-Donat,
+                  Bernard},
+  title         = {S{\'e}minaire de g{\'e}om{\'e}trie alg{\'e}brique du
+                  {Bois}-{Marie} 1963--1964. {Th{\'e}orie} des topos et
+                  cohomologie {\'e}tale des sch{\'e}mas. ({SGA} 4). {Un}
+                  s{\'e}minaire dirig{\'e} par {M}. {Artin}, {A}.
+                  {Grothendieck}, {J}. {L}. {Verdier}. {Avec} la
+                  collaboration de {N}. {Bourbaki}, {P}. {Deligne}, {B}.
+                  {Saint}-{Donat}. {Tome} 1: {Th{\'e}orie} des topos.
+                  {Expos{\'e}s} {I} {\`a} {IV}. 2e {\'e}d.},
+  fseries       = {Lecture Notes in Mathematics},
+  series        = {Lect. Notes Math.},
+  issn          = {0075-8434},
+  volume        = {269},
+  year          = {1972},
+  publisher     = {Springer, Cham},
+  language      = {French},
+  doi           = {10.1007/BFb0081551},
+  keywords      = {00B15,14-06},
+  zbmath        = {3370272},
+  zbl           = {0234.00007}
+}
+
 @Book{            silverman2009,
   author        = {Silverman, Joseph},
   publisher     = {Springer New York, NY},