From 7d005ba0a03ec5fbdfc56d0259834d6ab8b58d53 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Thu, 25 Jun 2026 16:39:33 +0200
Subject: [PATCH 01/20] copy over file and fix: WIP

---
 Mathlib.lean                                |   1 +
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 201 ++++++++++++++++++++
 2 files changed, 202 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Sites/LocalSite.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 881db5f16663e8..62b085f9f3f114 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3370,6 +3370,7 @@ public import Mathlib.CategoryTheory.Sites.JointlySurjective
 public import Mathlib.CategoryTheory.Sites.LeftExact
 public import Mathlib.CategoryTheory.Sites.Limits
 public import Mathlib.CategoryTheory.Sites.LocalProperties
+public import Mathlib.CategoryTheory.Sites.LocalSite
 public import Mathlib.CategoryTheory.Sites.Localization
 public import Mathlib.CategoryTheory.Sites.LocallyBijective
 public import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
new file mode 100644
index 00000000000000..7acb01e65ea557
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2025 Ben Eltschig. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ben Eltschig
+-/
+import Mathlib.CategoryTheory.Adjunction.Triple
+import Mathlib.CategoryTheory.Sites.GlobalSections
+
+/-!
+# Local sites
+A site (C,J) is called local if it has a terminal object whose only covering sieve is trivial -
+this makes it possible to define coconstant sheaves on it, giving its sheaf topos the structure
+of a local topos. This makes them an important stepping stone to cohesive sites.
+
+See https://ncatlab.org/nlab/show/local+site.
+
+## Main definitions / results
+* `J.IsLocalSite`: typeclass stating that (C,J) is a local site.
+* `coconstantSheaf`: the coconstant sheaf functor `Type w ⥤ Sheaf J (Type max v w)` defined on any
+  local site.
+* `ΓCoconstantSheafAdj`: the adjunction between the global sections functor `Γ` and
+  `coconstantSheaf`.
+* `fullyFaithfulCoconstantSheaf`: `coconstantSheaf` is fully faithful.
+* `fullyFaithfulConstantSheaf`: on local sites, the constant sheaf functor is fully faithful.
+All together this shows that for local sites `Sheaf J (Type max u v w)` forms a local topos, but
+since we don't yet have local topoi this can't be stated yet.
+
+We also define a Grothendieck topology `localTopology C` on any category `C` with a terminal object,
+and show that it is the largest topology making `C` into a local site.
+
+TODO: generalise universe levels from `max u v` to `max u v w` again once that is possible.
+-/
+
+universe u v w
+
+open CategoryTheory Limits Sheaf Opposite GrothendieckTopology
+
+namespace CategoryTheory
+
+variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
+
+/-- A local site is a site that has a terminal object with only a single covering sieve. -/
+class GrothendieckTopology.IsLocalSite extends HasTerminal C where
+  /-- The only covering sieve of the terminal object is the trivial sieve. -/
+  eq_top_of_mem : ∀ S ∈ J (⊤_ C), S = ⊤
+
+/-- On a local site, every covering sieve contains every morphism from the terminal object. -/
+lemma LocalSite.from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
+    (hS : S ∈ J X) : S.arrows f :=
+  (S.mem_iff_pullback_eq_top f).2 <| IsLocalSite.eq_top_of_mem _ <| J.pullback_stable f hS
+
+/-- Every category with a terminal object becomes a local site with the trivial topology. -/
+instance {C : Type u} [Category.{v} C] [HasTerminal C] : (trivial C).IsLocalSite where
+  eq_top_of_mem _ := trivial_covering.1
+
+/-- The functor that sends any type `A` to the functor `Cᵒᵖ → Type _` that sends any `X : C`
+to the type of all functions `(⊤_ C ⟶ X) → A`. This can be defined on any site with a terminal
+object, but has values in sheaves in the case of local sites. -/
+@[simps!?]
+noncomputable def Presheaf.coconst {C : Type u} [Category.{v} C] [HasTerminal C] :
+    Type w ⥤ (Cᵒᵖ ⥤ Type max v w) :=
+  uliftFunctor ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj
+    (coyoneda.obj (op (⊤_ C)) ⋙ uliftFunctor).op
+
+set_option backward.isDefEq.respectTransparency false in
+/-- On local sites, `Presheaf.coconst` actually takes values in sheaves. -/
+lemma Presheaf.coconst_isSheaf [J.IsLocalSite] (X : Type w) : IsSheaf J (coconst.obj X) := by
+  refine (isSheaf_iff_isSheaf_of_type J _).2 fun Y S hS f hf ↦ ?_
+  refine ⟨TypeCat.ofHom fun g ↦ by
+    have := f g.down (LocalSite.from_terminal_mem_of_mem J g.down hS)
+    exact (TypeCat.Hom.hom this) ⟨𝟙 _⟩, ?_, ?_⟩
+  · intro Z g hg
+    exact funext fun (x : ULift (_ ⟶ _)) ↦
+      (congrFun (f.comp_of_compatible S hf hg x.down) _).trans (congrArg (f g hg) <| by simp)
+  · intro g hg
+    exact funext fun h : ULift (⊤_ C ⟶ Y) ↦ Eq.trans (by simp [Presheaf.coconst]) <|
+      congrFun (hg h.down ((LocalSite.from_terminal_mem_of_mem J h.down hS))) _
+
+/-- The right adjoint to the global sections functor that exists over any local site.
+Takes a type `X` to the sheaf that sends each `Y : C` to the type of functions `Y → X`. -/
+noncomputable def IsLocalSite.coconstantSheaf [J.IsLocalSite] :
+    Type w ⥤ Sheaf J (Type (max v w)) where
+  obj X := ⟨Presheaf.coconst.obj X, Presheaf.coconst_isSheaf J X⟩
+  map f := ⟨Presheaf.coconst.map f⟩
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+-- this is currently needed to obtain the instance `HasSheafify J (Type max u v)`.
+attribute [local instance] CategoryTheory.Types.instConcreteCategory
+attribute [local instance] CategoryTheory.Types.instFunLike
+
+/-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
+@[simps!]
+noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
+    Γ J (Type max u v) ⊣ coconstantSheaf J := by
+  refine Adjunction.ofNatIsoLeft ?_ (ΓNatIsoSheafSections J _ terminalIsTerminal).symm
+  exact {
+    unit := {
+      app X := ⟨{
+        app Y (x : X.obj.obj Y) y := ⟨X.obj.map (op y.down) x⟩
+        naturality Y Z f := by
+          ext (x : X.obj.obj Y); dsimp [coconstantSheaf, Presheaf.coconst]; ext z
+          exact (FunctorToTypes.map_comp_apply X.obj _ _ x).symm
+      }⟩
+      naturality X Y f := by
+        ext Z (x : X.obj.obj Z); dsimp [coconstantSheaf, Presheaf.coconst]; ext z
+        exact (NatTrans.naturality_apply f.hom _ x).symm
+    }
+    counit := { app X := fun f : ULift (_ ⟶ _) → _ ↦ (f default).down }
+    left_triangle_components X := by
+      ext (x : X.obj.obj _)
+      dsimp; convert congrFun (X.obj.map_id _) x; exact Subsingleton.elim _ _
+    right_triangle_components X := by
+      ext Y (f : _ → _); dsimp [coconstantSheaf, Presheaf.coconst]; ext y
+      dsimp; congr; convert Category.id_comp _; exact Subsingleton.elim _ _
+  }
+
+instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).IsRightAdjoint :=
+  ⟨Γ J _, ⟨IsLocalSite.ΓCoconstantSheafAdj J⟩⟩
+
+/-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type.-/
+noncomputable def coconstantSheafΓNatIsoId [J.IsLocalSite] :
+    IsLocalSite.coconstantSheaf J ⋙ Γ J _ ≅ 𝟭 (Type max u v) := by
+  refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
+  exact (NatIso.ofComponents (fun X ↦ {
+    hom x := fun _ ↦ ⟨x⟩
+    inv f := (f (default : ULift (⊤_ C ⟶ ⊤_ C))).down
+    inv_hom_id := by
+      dsimp [IsLocalSite.coconstantSheaf, Presheaf.coconst]; ext; dsimp
+      congr; exact Subsingleton.elim _ _
+  })).symm
+
+/-- `coconstantSheaf` is fully faithful. -/
+noncomputable def fullyFaithfulCoconstantSheaf [J.IsLocalSite] :
+    (IsLocalSite.coconstantSheaf.{u,v,max u v} J).FullyFaithful :=
+  (IsLocalSite.ΓCoconstantSheafAdj J).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId J)
+
+instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).Full :=
+  (fullyFaithfulCoconstantSheaf J).full
+
+instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).Faithful :=
+  (fullyFaithfulCoconstantSheaf J).faithful
+
+/-- On local sites, the constant sheaf functor is fully faithful. -/
+noncomputable def fullyFaithfulConstantSheaf [HasWeakSheafify J (Type max u v)] [J.IsLocalSite] :
+    (constantSheaf J (Type max u v)).FullyFaithful :=
+  (Adjunction.Triple.mk (constantSheafΓAdj J _)
+    (IsLocalSite.ΓCoconstantSheafAdj J)).fullyFaithfulEquiv.symm <| fullyFaithfulCoconstantSheaf J
+
+instance [HasWeakSheafify J (Type max u v)] [J.IsLocalSite] :
+    (constantSheaf J (Type max u v)).Full :=
+  (fullyFaithfulConstantSheaf J).full
+
+instance [HasWeakSheafify J (Type max u v)] [J.IsLocalSite] :
+    (constantSheaf J (Type max u v)).Faithful :=
+  (fullyFaithfulConstantSheaf J).faithful
+
+open List in
+/-- For any site with a terminal object, the following are equivalent:
+* the site is local, i.e. the only covering sieve of the terminal object is the trivial one
+* every covering sieve contains all morphisms from the terminal object
+* the coconstant presheaf on the empty type is a sheaf
+* every coconstant presheaf is a sheaf.
+
+I don't yet know how exactly `HasCoconstantSheaf J (Type max u v)` fits into this - every
+local site has a coconstant sheaf functor, and every *subcanonical* site with a coconstant sheaf
+functor is local, but it's not clear to me what can be said in the non-subcanonical case. Maybe
+having a fully faithful coconstant sheaf functor could be strong enough?
+TODO: figure this out -/
+protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
+    TFAE [J.IsLocalSite,
+      ∀ X : C, ∀ S ∈ J X, ∀ x : ⊤_ C ⟶ X, S x,
+      Presieve.IsSheaf J (Presheaf.coconst.{u,v,max u v}.obj PEmpty),
+      ∀ X : Type max u v, Presieve.IsSheaf J (Presheaf.coconst.obj X)] := by
+  tfae_have 2 → 1 := fun h ↦ ⟨fun S hS ↦ S.id_mem_iff_eq_top.1 <| h _ S hS _⟩
+  tfae_have 1 → 2 := fun h X S hS f ↦ by
+    simpa using Sieve.id_mem_iff_eq_top.2 <| h.eq_top_of_mem _ <| J.pullback_stable f HShiftRight
+  tfae_have 4 → 1 := fun h ↦ ⟨fun S hS ↦ by
+    replace h : IsEmpty (Presieve.FamilyOfElements
+        (Presheaf.coconst.{u,v,max u v}.obj PEmpty) S.arrows) := by
+      have : IsEmpty ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op (⊤_ C))) := by
+        dsimp [Presheaf.coconst]; exact isEmpty_fun.2 ⟨⟨⟨𝟙 _⟩⟩, inferInstance⟩
+      have {X : C} : Subsingleton ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) := by
+        dsimp [Presheaf.coconst]; exact Pi.instSubsingleton
+      refine not_nonempty_iff.1 fun ⟨x⟩ ↦ IsEmpty.false (h S hS x ?_).choose
+      exact fun _ _ _ _ _ _ _ _ _ _ ↦ Subsingleton.elim _ _
+    replace ⟨X, f, hf, h⟩ : ∃ X, ∃ f : X ⟶ ⊤_ C, S f ∧
+        IsEmpty ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) := by
+      by_contra! h'; exact h.false fun X f hf ↦ (h' X f hf).some
+    let ⟨⟨(g : _ ⟶ _)⟩⟩ := (isEmpty_fun.1 h).1
+    refine S.id_mem_iff_eq_top.1 ?_
+    convert S.downward_closed hf g
+    exact Subsingleton.elim _ _⟩
+  tfae_have 5 → 4 := fun h ↦ h _
+  tfae_have 1 → 5 := fun _ _ ↦ (isSheaf_iff_isSheaf_of_type _ _).1 <| Presheaf.coconst_isSheaf J _
+  tfae_finish
+
+instance [HasTerminal C] : (localTopology C).IsLocalSite :=
+  ((GrothendieckTopology.IsLocalSite.tfae _).out 0 2).2 le_rfl
+
+end CategoryTheory

From 6f7a338eb9ccc03a67a4cc48bb55e746fe5ce605 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Fri, 26 Jun 2026 16:37:47 +0200
Subject: [PATCH 02/20] WIP

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 64 +++++++++++----------
 1 file changed, 33 insertions(+), 31 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 7acb01e65ea557..4a450d284c95cc 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -25,9 +25,6 @@ See https://ncatlab.org/nlab/show/local+site.
 All together this shows that for local sites `Sheaf J (Type max u v w)` forms a local topos, but
 since we don't yet have local topoi this can't be stated yet.
 
-We also define a Grothendieck topology `localTopology C` on any category `C` with a terminal object,
-and show that it is the largest topology making `C` into a local site.
-
 TODO: generalise universe levels from `max u v` to `max u v w` again once that is possible.
 -/
 
@@ -56,25 +53,27 @@ instance {C : Type u} [Category.{v} C] [HasTerminal C] : (trivial C).IsLocalSite
 /-- The functor that sends any type `A` to the functor `Cᵒᵖ → Type _` that sends any `X : C`
 to the type of all functions `(⊤_ C ⟶ X) → A`. This can be defined on any site with a terminal
 object, but has values in sheaves in the case of local sites. -/
-@[simps!?]
+@[simps!]
 noncomputable def Presheaf.coconst {C : Type u} [Category.{v} C] [HasTerminal C] :
     Type w ⥤ (Cᵒᵖ ⥤ Type max v w) :=
   uliftFunctor ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj
     (coyoneda.obj (op (⊤_ C)) ⋙ uliftFunctor).op
 
+open ConcreteCategory in
 set_option backward.isDefEq.respectTransparency false in
 /-- On local sites, `Presheaf.coconst` actually takes values in sheaves. -/
 lemma Presheaf.coconst_isSheaf [J.IsLocalSite] (X : Type w) : IsSheaf J (coconst.obj X) := by
   refine (isSheaf_iff_isSheaf_of_type J _).2 fun Y S hS f hf ↦ ?_
-  refine ⟨TypeCat.ofHom fun g ↦ by
-    have := f g.down (LocalSite.from_terminal_mem_of_mem J g.down hS)
-    exact (TypeCat.Hom.hom this) ⟨𝟙 _⟩, ?_, ?_⟩
+  refine ⟨TypeCat.ofHom fun g ↦
+    (hom (f g.down (LocalSite.from_terminal_mem_of_mem J g.down hS))) ⟨𝟙 _⟩, ?_, ?_⟩
   · intro Z g hg
-    exact funext fun (x : ULift (_ ⟶ _)) ↦
-      (congrFun (f.comp_of_compatible S hf hg x.down) _).trans (congrArg (f g hg) <| by simp)
+    refine hom_ext _ _ fun (x : ULift (_ ⟶ _)) ↦ ?_
+    exact (congr_hom (f.comp_of_compatible S hf hg x.down) _).trans <|
+      congr_arg (f g hg) <| ULift.ext _ _ <| Category.id_comp _
   · intro g hg
-    exact funext fun h : ULift (⊤_ C ⟶ Y) ↦ Eq.trans (by simp [Presheaf.coconst]) <|
-      congrFun (hg h.down ((LocalSite.from_terminal_mem_of_mem J h.down hS))) _
+    refine hom_ext _ _ fun ⟨h⟩ ↦ ?_
+    exact Eq.trans (by simp [coconst, uliftFunctor, Functor.whiskeringLeft, Functor.comp]) <|
+      congr_hom (hg h ((LocalSite.from_terminal_mem_of_mem J h hS))) _
 
 /-- The right adjoint to the global sections functor that exists over any local site.
 Takes a type `X` to the sheaf that sends each `Y : C` to the type of functions `Y → X`. -/
@@ -85,10 +84,7 @@ noncomputable def IsLocalSite.coconstantSheaf [J.IsLocalSite] :
   map_id _ := rfl
   map_comp _ _ := rfl
 
--- this is currently needed to obtain the instance `HasSheafify J (Type max u v)`.
-attribute [local instance] CategoryTheory.Types.instConcreteCategory
-attribute [local instance] CategoryTheory.Types.instFunLike
-
+set_option backward.isDefEq.respectTransparency false in
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
 @[simps!]
 noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
@@ -97,16 +93,31 @@ noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
   exact {
     unit := {
       app X := ⟨{
-        app Y (x : X.obj.obj Y) y := ⟨X.obj.map (op y.down) x⟩
+        app Y := TypeCat.ofHom fun (x : X.obj.obj Y) ↦ TypeCat.ofHom fun y ↦
+          ⟨X.obj.map (op y.down) x⟩
         naturality Y Z f := by
-          ext (x : X.obj.obj Y); dsimp [coconstantSheaf, Presheaf.coconst]; ext z
-          exact (FunctorToTypes.map_comp_apply X.obj _ _ x).symm
+          ext (x : X.obj.obj Y)
+          dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp, Functor.whiskeringLeft,
+            uliftFunctor, yoneda, coyoneda]
+          ext z
+          exact (Functor.map_comp_apply X.obj _ _ x).symm
       }⟩
       naturality X Y f := by
-        ext Z (x : X.obj.obj Z); dsimp [coconstantSheaf, Presheaf.coconst]; ext z
+        ext Z (x : X.obj.obj Z)
+        dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp,
+          Functor.whiskeringLeft, uliftFunctor, yoneda, coyoneda]
+        ext z
         exact (NatTrans.naturality_apply f.hom _ x).symm
     }
-    counit := { app X := fun f : ULift (_ ⟶ _) → _ ↦ (f default).down }
+    counit := {
+      app X := by
+        refine TypeCat.ofHom fun f ↦ ?_
+
+        dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp, Functor.whiskeringLeft,
+          uliftFunctor, yoneda, coyoneda] at f
+        --exact (f.hom (𝟙 _)).down
+        --exact fun f : ULift (_ ⟶ _) → _ ↦ (f default).down
+        sorry }
     left_triangle_components X := by
       ext (x : X.obj.obj _)
       dsimp; convert congrFun (X.obj.map_id _) x; exact Subsingleton.elim _ _
@@ -160,13 +171,7 @@ open List in
 * the site is local, i.e. the only covering sieve of the terminal object is the trivial one
 * every covering sieve contains all morphisms from the terminal object
 * the coconstant presheaf on the empty type is a sheaf
-* every coconstant presheaf is a sheaf.
-
-I don't yet know how exactly `HasCoconstantSheaf J (Type max u v)` fits into this - every
-local site has a coconstant sheaf functor, and every *subcanonical* site with a coconstant sheaf
-functor is local, but it's not clear to me what can be said in the non-subcanonical case. Maybe
-having a fully faithful coconstant sheaf functor could be strong enough?
-TODO: figure this out -/
+* every coconstant presheaf is a sheaf. -/
 protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
     TFAE [J.IsLocalSite,
       ∀ X : C, ∀ S ∈ J X, ∀ x : ⊤_ C ⟶ X, S x,
@@ -174,7 +179,7 @@ protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
       ∀ X : Type max u v, Presieve.IsSheaf J (Presheaf.coconst.obj X)] := by
   tfae_have 2 → 1 := fun h ↦ ⟨fun S hS ↦ S.id_mem_iff_eq_top.1 <| h _ S hS _⟩
   tfae_have 1 → 2 := fun h X S hS f ↦ by
-    simpa using Sieve.id_mem_iff_eq_top.2 <| h.eq_top_of_mem _ <| J.pullback_stable f HShiftRight
+    simpa using Sieve.id_mem_iff_eq_top.2 <| h.eq_top_of_mem _ <| J.pullback_stable f hS
   tfae_have 4 → 1 := fun h ↦ ⟨fun S hS ↦ by
     replace h : IsEmpty (Presieve.FamilyOfElements
         (Presheaf.coconst.{u,v,max u v}.obj PEmpty) S.arrows) := by
@@ -195,7 +200,4 @@ protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
   tfae_have 1 → 5 := fun _ _ ↦ (isSheaf_iff_isSheaf_of_type _ _).1 <| Presheaf.coconst_isSheaf J _
   tfae_finish
 
-instance [HasTerminal C] : (localTopology C).IsLocalSite :=
-  ((GrothendieckTopology.IsLocalSite.tfae _).out 0 2).2 le_rfl
-
 end CategoryTheory

From ee19b79f4515279953eb73c5b298d677e3110edc Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Fri, 26 Jun 2026 17:22:30 +0200
Subject: [PATCH 03/20] switch approaches & finish fixing

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 80 +++++++++------------
 1 file changed, 35 insertions(+), 45 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 4a450d284c95cc..bc91a7671b4e2f 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -55,25 +55,22 @@ to the type of all functions `(⊤_ C ⟶ X) → A`. This can be defined on any
 object, but has values in sheaves in the case of local sites. -/
 @[simps!]
 noncomputable def Presheaf.coconst {C : Type u} [Category.{v} C] [HasTerminal C] :
-    Type w ⥤ (Cᵒᵖ ⥤ Type max v w) :=
-  uliftFunctor ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj
-    (coyoneda.obj (op (⊤_ C)) ⋙ uliftFunctor).op
+    Type w ⥤ (Cᵒᵖ ⥤ Type max v w) where
+  obj A := {
+    obj X := ((⊤_ C ⟶ X.unop) → A)
+    map f := TypeCat.ofHom fun g g' ↦ g (g' ≫ f.unop) }
+  map f := {
+    app X := TypeCat.ofHom fun g ↦ ConcreteCategory.hom f ∘ g }
 
-open ConcreteCategory in
 set_option backward.isDefEq.respectTransparency false in
-/-- On local sites, `Presheaf.coconst` actually takes values in sheaves. -/
+/-- On local sites, `Presheaf.coconst'` actually takes values in sheaves. -/
 lemma Presheaf.coconst_isSheaf [J.IsLocalSite] (X : Type w) : IsSheaf J (coconst.obj X) := by
   refine (isSheaf_iff_isSheaf_of_type J _).2 fun Y S hS f hf ↦ ?_
-  refine ⟨TypeCat.ofHom fun g ↦
-    (hom (f g.down (LocalSite.from_terminal_mem_of_mem J g.down hS))) ⟨𝟙 _⟩, ?_, ?_⟩
-  · intro Z g hg
-    refine hom_ext _ _ fun (x : ULift (_ ⟶ _)) ↦ ?_
-    exact (congr_hom (f.comp_of_compatible S hf hg x.down) _).trans <|
-      congr_arg (f g hg) <| ULift.ext _ _ <| Category.id_comp _
-  · intro g hg
-    refine hom_ext _ _ fun ⟨h⟩ ↦ ?_
-    exact Eq.trans (by simp [coconst, uliftFunctor, Functor.whiskeringLeft, Functor.comp]) <|
-      congr_hom (hg h ((LocalSite.from_terminal_mem_of_mem J h hS))) _
+  refine ⟨fun g ↦ f g (LocalSite.from_terminal_mem_of_mem J g hS) (𝟙 _), ?_, ?_⟩
+  · refine fun Z g hg ↦ funext fun x ↦ ?_
+    exact (congrFun (f.comp_of_compatible S hf hg x) _).trans (congrArg (f g hg) <| by simp)
+  · exact fun g hg ↦ funext fun h : (⊤_ C ⟶ Y) ↦ Eq.trans (by simp [Presheaf.coconst]) <|
+      congrFun (hg h ((LocalSite.from_terminal_mem_of_mem J h hS))) _
 
 /-- The right adjoint to the global sections functor that exists over any local site.
 Takes a type `X` to the sheaf that sends each `Y : C` to the type of functions `Y → X`. -/
@@ -93,52 +90,45 @@ noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
   exact {
     unit := {
       app X := ⟨{
-        app Y := TypeCat.ofHom fun (x : X.obj.obj Y) ↦ TypeCat.ofHom fun y ↦
-          ⟨X.obj.map (op y.down) x⟩
+        app Y := TypeCat.ofHom fun (x : X.obj.obj Y) y ↦ X.obj.map (op y) x
         naturality Y Z f := by
           ext (x : X.obj.obj Y)
-          dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp, Functor.whiskeringLeft,
-            uliftFunctor, yoneda, coyoneda]
+          dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp]
           ext z
           exact (Functor.map_comp_apply X.obj _ _ x).symm
       }⟩
       naturality X Y f := by
         ext Z (x : X.obj.obj Z)
-        dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp,
-          Functor.whiskeringLeft, uliftFunctor, yoneda, coyoneda]
+        dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp]
         ext z
         exact (NatTrans.naturality_apply f.hom _ x).symm
     }
-    counit := {
-      app X := by
-        refine TypeCat.ofHom fun f ↦ ?_
-
-        dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp, Functor.whiskeringLeft,
-          uliftFunctor, yoneda, coyoneda] at f
-        --exact (f.hom (𝟙 _)).down
-        --exact fun f : ULift (_ ⟶ _) → _ ↦ (f default).down
-        sorry }
+    counit := { app X := TypeCat.ofHom fun f ↦ f (𝟙 _) }
     left_triangle_components X := by
       ext (x : X.obj.obj _)
-      dsimp; convert congrFun (X.obj.map_id _) x; exact Subsingleton.elim _ _
+      exact ConcreteCategory.congr_hom (X.obj.map_id _) x
     right_triangle_components X := by
-      ext Y (f : _ → _); dsimp [coconstantSheaf, Presheaf.coconst]; ext y
-      dsimp; congr; convert Category.id_comp _; exact Subsingleton.elim _ _
+      ext Y (f : _ → _)
+      dsimp [coconstantSheaf, Presheaf.coconst]
+      ext y
+      simp
   }
 
 instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).IsRightAdjoint :=
   ⟨Γ J _, ⟨IsLocalSite.ΓCoconstantSheafAdj J⟩⟩
 
-/-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type.-/
+/-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
 noncomputable def coconstantSheafΓNatIsoId [J.IsLocalSite] :
     IsLocalSite.coconstantSheaf J ⋙ Γ J _ ≅ 𝟭 (Type max u v) := by
   refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
   exact (NatIso.ofComponents (fun X ↦ {
-    hom x := fun _ ↦ ⟨x⟩
-    inv f := (f (default : ULift (⊤_ C ⟶ ⊤_ C))).down
+    hom := TypeCat.ofHom fun x _ ↦ x
+    inv := TypeCat.ofHom fun f ↦ by exact f (𝟙 (⊤_ C))
     inv_hom_id := by
-      dsimp [IsLocalSite.coconstantSheaf, Presheaf.coconst]; ext; dsimp
-      congr; exact Subsingleton.elim _ _
+      dsimp [IsLocalSite.coconstantSheaf, Presheaf.coconst]
+      ext x
+      dsimp at ⊢
+      exact funext fun x ↦ congr_arg _ <| Subsingleton.elim _ _
   })).symm
 
 /-- `coconstantSheaf` is fully faithful. -/
@@ -180,24 +170,24 @@ protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
   tfae_have 2 → 1 := fun h ↦ ⟨fun S hS ↦ S.id_mem_iff_eq_top.1 <| h _ S hS _⟩
   tfae_have 1 → 2 := fun h X S hS f ↦ by
     simpa using Sieve.id_mem_iff_eq_top.2 <| h.eq_top_of_mem _ <| J.pullback_stable f hS
-  tfae_have 4 → 1 := fun h ↦ ⟨fun S hS ↦ by
+  tfae_have 3 → 1 := fun h ↦ ⟨fun S hS ↦ by
     replace h : IsEmpty (Presieve.FamilyOfElements
         (Presheaf.coconst.{u,v,max u v}.obj PEmpty) S.arrows) := by
       have : IsEmpty ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op (⊤_ C))) := by
-        dsimp [Presheaf.coconst]; exact isEmpty_fun.2 ⟨⟨⟨𝟙 _⟩⟩, inferInstance⟩
-      have {X : C} : Subsingleton ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) := by
-        dsimp [Presheaf.coconst]; exact Pi.instSubsingleton
+        dsimp [Presheaf.coconst]; exact isEmpty_fun.2 ⟨⟨𝟙 _⟩, inferInstance⟩
+      have {X : C} : Subsingleton ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) :=
+        Pi.instSubsingleton
       refine not_nonempty_iff.1 fun ⟨x⟩ ↦ IsEmpty.false (h S hS x ?_).choose
       exact fun _ _ _ _ _ _ _ _ _ _ ↦ Subsingleton.elim _ _
     replace ⟨X, f, hf, h⟩ : ∃ X, ∃ f : X ⟶ ⊤_ C, S f ∧
         IsEmpty ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) := by
       by_contra! h'; exact h.false fun X f hf ↦ (h' X f hf).some
-    let ⟨⟨(g : _ ⟶ _)⟩⟩ := (isEmpty_fun.1 h).1
+    let ⟨(g : _ ⟶ _)⟩ := (isEmpty_fun.1 h).1
     refine S.id_mem_iff_eq_top.1 ?_
     convert S.downward_closed hf g
     exact Subsingleton.elim _ _⟩
-  tfae_have 5 → 4 := fun h ↦ h _
-  tfae_have 1 → 5 := fun _ _ ↦ (isSheaf_iff_isSheaf_of_type _ _).1 <| Presheaf.coconst_isSheaf J _
+  tfae_have 4 → 3 := fun h ↦ h _
+  tfae_have 1 → 4 := fun _ _ ↦ (isSheaf_iff_isSheaf_of_type _ _).1 <| Presheaf.coconst_isSheaf J _
   tfae_finish
 
 end CategoryTheory

From cbfb7f70730b3f58559776036808b37f1004064f Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Fri, 26 Jun 2026 17:34:29 +0200
Subject: [PATCH 04/20] generalise universes

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 39 ++++++++++-----------
 1 file changed, 19 insertions(+), 20 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index bc91a7671b4e2f..2a7beccaa7ea68 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -22,13 +22,12 @@ See https://ncatlab.org/nlab/show/local+site.
   `coconstantSheaf`.
 * `fullyFaithfulCoconstantSheaf`: `coconstantSheaf` is fully faithful.
 * `fullyFaithfulConstantSheaf`: on local sites, the constant sheaf functor is fully faithful.
+
 All together this shows that for local sites `Sheaf J (Type max u v w)` forms a local topos, but
 since we don't yet have local topoi this can't be stated yet.
-
-TODO: generalise universe levels from `max u v` to `max u v w` again once that is possible.
 -/
 
-universe u v w
+universe w u v
 
 open CategoryTheory Limits Sheaf Opposite GrothendieckTopology
 
@@ -85,7 +84,7 @@ set_option backward.isDefEq.respectTransparency false in
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
 @[simps!]
 noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
-    Γ J (Type max u v) ⊣ coconstantSheaf J := by
+    Γ J (Type max u v w) ⊣ coconstantSheaf J := by
   refine Adjunction.ofNatIsoLeft ?_ (ΓNatIsoSheafSections J _ terminalIsTerminal).symm
   exact {
     unit := {
@@ -114,12 +113,12 @@ noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
       simp
   }
 
-instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).IsRightAdjoint :=
+instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v w} J).IsRightAdjoint :=
   ⟨Γ J _, ⟨IsLocalSite.ΓCoconstantSheafAdj J⟩⟩
 
 /-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
 noncomputable def coconstantSheafΓNatIsoId [J.IsLocalSite] :
-    IsLocalSite.coconstantSheaf J ⋙ Γ J _ ≅ 𝟭 (Type max u v) := by
+    IsLocalSite.coconstantSheaf J ⋙ Γ J _ ≅ 𝟭 (Type max u v w) := by
   refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
   exact (NatIso.ofComponents (fun X ↦ {
     hom := TypeCat.ofHom fun x _ ↦ x
@@ -133,27 +132,27 @@ noncomputable def coconstantSheafΓNatIsoId [J.IsLocalSite] :
 
 /-- `coconstantSheaf` is fully faithful. -/
 noncomputable def fullyFaithfulCoconstantSheaf [J.IsLocalSite] :
-    (IsLocalSite.coconstantSheaf.{u,v,max u v} J).FullyFaithful :=
+    (IsLocalSite.coconstantSheaf.{max u v w} J).FullyFaithful :=
   (IsLocalSite.ΓCoconstantSheafAdj J).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId J)
 
-instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).Full :=
+instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v} J).Full :=
   (fullyFaithfulCoconstantSheaf J).full
 
-instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{u,v,max u v} J).Faithful :=
+instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v} J).Faithful :=
   (fullyFaithfulCoconstantSheaf J).faithful
 
 /-- On local sites, the constant sheaf functor is fully faithful. -/
-noncomputable def fullyFaithfulConstantSheaf [HasWeakSheafify J (Type max u v)] [J.IsLocalSite] :
-    (constantSheaf J (Type max u v)).FullyFaithful :=
+noncomputable def fullyFaithfulConstantSheaf [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :
+    (constantSheaf J (Type max u v w)).FullyFaithful :=
   (Adjunction.Triple.mk (constantSheafΓAdj J _)
     (IsLocalSite.ΓCoconstantSheafAdj J)).fullyFaithfulEquiv.symm <| fullyFaithfulCoconstantSheaf J
 
-instance [HasWeakSheafify J (Type max u v)] [J.IsLocalSite] :
-    (constantSheaf J (Type max u v)).Full :=
+instance [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :
+    (constantSheaf J (Type max u v w)).Full :=
   (fullyFaithfulConstantSheaf J).full
 
-instance [HasWeakSheafify J (Type max u v)] [J.IsLocalSite] :
-    (constantSheaf J (Type max u v)).Faithful :=
+instance [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :
+    (constantSheaf J (Type max u v w)).Faithful :=
   (fullyFaithfulConstantSheaf J).faithful
 
 open List in
@@ -165,22 +164,22 @@ open List in
 protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
     TFAE [J.IsLocalSite,
       ∀ X : C, ∀ S ∈ J X, ∀ x : ⊤_ C ⟶ X, S x,
-      Presieve.IsSheaf J (Presheaf.coconst.{u,v,max u v}.obj PEmpty),
+      Presieve.IsSheaf J (Presheaf.coconst.{max u v}.obj PEmpty),
       ∀ X : Type max u v, Presieve.IsSheaf J (Presheaf.coconst.obj X)] := by
   tfae_have 2 → 1 := fun h ↦ ⟨fun S hS ↦ S.id_mem_iff_eq_top.1 <| h _ S hS _⟩
   tfae_have 1 → 2 := fun h X S hS f ↦ by
     simpa using Sieve.id_mem_iff_eq_top.2 <| h.eq_top_of_mem _ <| J.pullback_stable f hS
   tfae_have 3 → 1 := fun h ↦ ⟨fun S hS ↦ by
     replace h : IsEmpty (Presieve.FamilyOfElements
-        (Presheaf.coconst.{u,v,max u v}.obj PEmpty) S.arrows) := by
-      have : IsEmpty ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op (⊤_ C))) := by
+        (Presheaf.coconst.{max u v}.obj PEmpty) S.arrows) := by
+      have : IsEmpty ((Presheaf.coconst.{max u v}.obj PEmpty).obj (op (⊤_ C))) := by
         dsimp [Presheaf.coconst]; exact isEmpty_fun.2 ⟨⟨𝟙 _⟩, inferInstance⟩
-      have {X : C} : Subsingleton ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) :=
+      have {X : C} : Subsingleton ((Presheaf.coconst.{max u v}.obj PEmpty).obj (op X)) :=
         Pi.instSubsingleton
       refine not_nonempty_iff.1 fun ⟨x⟩ ↦ IsEmpty.false (h S hS x ?_).choose
       exact fun _ _ _ _ _ _ _ _ _ _ ↦ Subsingleton.elim _ _
     replace ⟨X, f, hf, h⟩ : ∃ X, ∃ f : X ⟶ ⊤_ C, S f ∧
-        IsEmpty ((Presheaf.coconst.{u,v,max u v}.obj PEmpty).obj (op X)) := by
+        IsEmpty ((Presheaf.coconst.{max u v}.obj PEmpty).obj (op X)) := by
       by_contra! h'; exact h.false fun X f hf ↦ (h' X f hf).some
     let ⟨(g : _ ⟶ _)⟩ := (isEmpty_fun.1 h).1
     refine S.id_mem_iff_eq_top.1 ?_

From 48772b84fa6c624c10af0ee72296f7ac67b0c60d Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Fri, 26 Jun 2026 18:38:13 +0200
Subject: [PATCH 05/20] fix

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 2a7beccaa7ea68..4d764f68d226c6 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Ben Eltschig. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ben Eltschig
 -/
-import Mathlib.CategoryTheory.Adjunction.Triple
-import Mathlib.CategoryTheory.Sites.GlobalSections
+module
+
+public import Mathlib.CategoryTheory.Adjunction.Triple
+public import Mathlib.CategoryTheory.Sites.GlobalSections
 
 /-!
 # Local sites
@@ -29,6 +31,8 @@ since we don't yet have local topoi this can't be stated yet.
 
 universe w u v
 
+@[expose] public section
+
 open CategoryTheory Limits Sheaf Opposite GrothendieckTopology
 
 namespace CategoryTheory

From 0b6c1fbc74c407510f71fc579301ef9309a9d8fc Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Sat, 27 Jun 2026 12:27:26 +0200
Subject: [PATCH 06/20] fix

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 4d764f68d226c6..47e49329be6c64 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -86,7 +86,6 @@ noncomputable def IsLocalSite.coconstantSheaf [J.IsLocalSite] :
 
 set_option backward.isDefEq.respectTransparency false in
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
-@[simps!]
 noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
     Γ J (Type max u v w) ⊣ coconstantSheaf J := by
   refine Adjunction.ofNatIsoLeft ?_ (ΓNatIsoSheafSections J _ terminalIsTerminal).symm
@@ -114,8 +113,7 @@ noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
       ext Y (f : _ → _)
       dsimp [coconstantSheaf, Presheaf.coconst]
       ext y
-      simp
-  }
+      simp }
 
 instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v w} J).IsRightAdjoint :=
   ⟨Γ J _, ⟨IsLocalSite.ΓCoconstantSheafAdj J⟩⟩

From 6419e846f4b8f9fc591a3eedec5393552ae4d774 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 29 Jun 2026 01:57:50 +0200
Subject: [PATCH 07/20] WIP: switch to approach using points

---
 Mathlib/CategoryTheory/ShrinkYoneda.lean    | 189 +++++++++++++
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 288 +++++++++++---------
 2 files changed, 348 insertions(+), 129 deletions(-)

diff --git a/Mathlib/CategoryTheory/ShrinkYoneda.lean b/Mathlib/CategoryTheory/ShrinkYoneda.lean
index 9de58282348005..6d83aab6128fb4 100644
--- a/Mathlib/CategoryTheory/ShrinkYoneda.lean
+++ b/Mathlib/CategoryTheory/ShrinkYoneda.lean
@@ -69,6 +69,8 @@ end FunctorToTypes
 
 variable [LocallySmall.{w} C]
 
+section Yoneda
+
 set_option backward.defeqAttrib.useBackward true in
 instance (X : C) : FunctorToTypes.Small.{w} (yoneda.obj X) :=
   fun _ ↦ by dsimp; infer_instance
@@ -249,4 +251,191 @@ def shrinkYonedaRepresentableBy (X : C) : (shrinkYoneda.{w}.obj X).Representable
 instance (X : C) : (shrinkYoneda.{w}.obj X).IsRepresentable :=
   (shrinkYonedaRepresentableBy X).isRepresentable
 
+end Yoneda
+
+section Coyoneda
+
+set_option backward.defeqAttrib.useBackward true in
+instance (X : Cᵒᵖ) : FunctorToTypes.Small.{w} (coyoneda.obj X) :=
+  fun _ ↦ by dsimp; infer_instance
+
+/-- The co-Yoneda embedding `Cᵒᵖ ⥤ C ⥤ Type w` for a locally `w`-small category `C`. -/
+@[simps -isSimp obj map, pp_with_univ]
+noncomputable def shrinkCoyoneda :
+    Cᵒᵖ ⥤ C ⥤ Type w where
+  obj X := FunctorToTypes.shrink (coyoneda.obj X)
+  map f := FunctorToTypes.shrinkMap (coyoneda.map f)
+
+/-- The type `(shrinkCoyoneda.obj X).obj Y` is equivalent to `X.unop ⟶ Y`. -/
+noncomputable def shrinkCoyonedaObjObjEquiv {X : Cᵒᵖ} {Y : C} :
+    ((shrinkCoyoneda.{w}.obj X).obj Y) ≃ (X.unop ⟶ Y) :=
+  (equivShrink _).symm
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm
+    {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : X.unop ⟶ Y) :
+    (shrinkCoyoneda.obj _).map g (shrinkCoyonedaObjObjEquiv.symm f) =
+      shrinkCoyonedaObjObjEquiv.symm (f ≫ g) := by
+  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+lemma shrinkCoyonedaObjObjEquiv_symm_comp {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) :
+    shrinkCoyonedaObjObjEquiv.symm (g ≫ f) =
+    (shrinkCoyoneda.obj _).map f (shrinkCoyonedaObjObjEquiv.symm g) :=
+  (shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm f g).symm
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm
+    {X X' : Cᵒᵖ} {Y : C} (f : X.unop ⟶ Y) (g : X ⟶ X') :
+    (shrinkCoyoneda.map g).app _ (shrinkCoyonedaObjObjEquiv.symm f) =
+      shrinkCoyonedaObjObjEquiv.symm (g.unop ≫ f) := by
+  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc]
+lemma shrinkCoyonedaObjObjEquiv_map_app
+    {X X' : Cᵒᵖ} {Y : C} (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') :
+    shrinkCoyonedaObjObjEquiv ((shrinkCoyoneda.map g).app Y f) =
+      g.unop ≫ shrinkCoyonedaObjObjEquiv f := by
+  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc]
+lemma shrinkCoyonedaObjObjEquiv_obj_map {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y')
+    (f : (shrinkCoyoneda.{w}.obj X).obj Y) :
+    shrinkCoyonedaObjObjEquiv ((shrinkCoyoneda.{w}.obj X).map g f) =
+      shrinkCoyonedaObjObjEquiv f ≫ g := by
+  simp [shrinkCoyonedaObjObjEquiv, shrinkCoyoneda]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The type of natural transformations `shrinkCoyoneda.{w}.obj X ⟶ P`
+with `X : Cᵒᵖ` and `P : C ⥤ Type w` is equivalent to `P.obj (op X)`. -/
+noncomputable def shrinkCoyonedaEquiv {X : Cᵒᵖ} {P : C ⥤ Type w} :
+    (shrinkCoyoneda.{w}.obj X ⟶ P) ≃ P.obj X.unop where
+  toFun τ := τ.app _ (equivShrink.{w} _ (𝟙 X.unop))
+  invFun x :=
+    { app Y := ↾fun f ↦ P.map ((equivShrink.{w} _).symm f) x
+      naturality Y Z g := by ext; simp [shrinkCoyoneda] }
+  left_inv τ := by
+    ext Y f
+    obtain ⟨f, rfl⟩ := (equivShrink _).surjective f
+    simpa [shrinkCoyoneda] using ((τ.naturality_apply f) (equivShrink _ (𝟙 X.unop))).symm
+  right_inv x := by simp
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma map_shrinkCoyonedaEquiv {X Y : Cᵒᵖ} {P : C ⥤ Type w} (f : shrinkCoyoneda.obj X ⟶ P)
+    (g : Y ⟶ X) : P.map g.unop (shrinkCoyonedaEquiv f) =
+      f.app Y.unop (shrinkCoyonedaObjObjEquiv.symm g.unop) := by
+  simp [shrinkCoyonedaObjObjEquiv, shrinkCoyonedaEquiv, shrinkCoyoneda,
+    ← comp_apply, ← NatTrans.naturality]
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyonedaEquiv_shrinkCoyoneda_map {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    shrinkCoyonedaEquiv (shrinkCoyoneda.{w}.map f) = shrinkCoyonedaObjObjEquiv.symm f.unop := by
+  simp [shrinkCoyonedaEquiv, shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+lemma shrinkCoyonedaEquiv_comp {X : Cᵒᵖ} {P Q : C ⥤ Type w} (α : shrinkCoyoneda.obj X ⟶ P)
+    (β : P ⟶ Q) :
+    shrinkCoyonedaEquiv (α ≫ β) = β.app _ (shrinkCoyonedaEquiv α) := by
+  simp [shrinkCoyonedaEquiv]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyonedaEquiv_naturality {X Y : Cᵒᵖ} {P : C ⥤ Type w}
+    (f : shrinkCoyoneda.obj X ⟶ P) (g : Y ⟶ X) :
+    P.map g.unop (shrinkCoyonedaEquiv f) = shrinkCoyonedaEquiv (shrinkCoyoneda.map g ≫ f) := by
+  simpa [shrinkCoyonedaEquiv, shrinkCoyoneda]
+    using (f.naturality_apply g.unop ((equivShrink _) (𝟙 _))).symm
+
+@[reassoc]
+lemma shrinkCoyonedaEquiv_symm_map {X Y : C} (f : X ⟶ Y) {P : C ⥤ Type w} (t : P.obj X) :
+    shrinkCoyonedaEquiv.symm (P.map f t) =
+      shrinkCoyoneda.map f.op ≫ shrinkCoyonedaEquiv.symm t :=
+  shrinkCoyonedaEquiv.injective (by
+    obtain ⟨t, rfl⟩ := shrinkCoyonedaEquiv.surjective t
+    rw [← shrinkCoyonedaEquiv_naturality]
+    simp)
+
+lemma shrinkCoyonedaEquiv_symm_app_shrinkCoyonedaObjObjEquiv_symm {X : Cᵒᵖ} {P : C ⥤ Type w}
+    (s : P.obj X.unop) {Y : Cᵒᵖ} (f : Y ⟶ X) :
+    (shrinkCoyonedaEquiv.symm s).app Y.unop (shrinkCoyonedaObjObjEquiv.symm f.unop) =
+      P.map f.unop s := by
+  obtain ⟨g, rfl⟩ := shrinkCoyonedaEquiv.surjective s
+  simp [map_shrinkCoyonedaEquiv]
+
+variable (C) in
+/-- The functor `shrinkCoyoneda : Cᵒᵖ ⥤ C ⥤ Type w` for a locally `w`-small category `C`
+is fully faithful. -/
+noncomputable def fullyFaithfulShrinkCoyoneda :
+    (shrinkCoyoneda.{w} (C := C)).FullyFaithful where
+  preimage f := (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv f)).op
+  map_preimage f := by
+    obtain ⟨f, rfl⟩ := shrinkCoyonedaEquiv.symm.surjective f
+    cat_disch
+  preimage_map f := by simp [shrinkCoyonedaEquiv_shrinkCoyoneda_map]
+
+instance : (shrinkCoyoneda.{w} (C := C)).Faithful := (fullyFaithfulShrinkCoyoneda C).faithful
+
+instance : (shrinkCoyoneda.{w} (C := C)).Full := (fullyFaithfulShrinkCoyoneda C).full
+
+set_option backward.defeqAttrib.useBackward true in
+/-- `shrinkCoyoneda` at the morphism universe level is `coyoneda`. -/
+@[simps! hom_app inv_app]
+noncomputable
+def shrinkCoyonedaIsoCoyoneda : shrinkCoyoneda.{v} ≅ coyoneda (C := C) :=
+  NatIso.ofComponents
+    (fun X ↦ NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso)
+      (by intros; ext; simp [shrinkCoyonedaObjObjEquiv_obj_map]))
+    (by intros; ext; simp [shrinkCoyonedaObjObjEquiv_map_app])
+
+set_option backward.defeqAttrib.useBackward true in
+/-- `shrinkCoyoneda` is compatible with `uliftFunctor`. -/
+noncomputable
+def shrinkCoyonedaUliftFunctorIso [LocallySmall.{max w w'} C] :
+    shrinkCoyoneda.{w} ⋙ (Functor.whiskeringRight Cᵒᵖ _ _).obj uliftFunctor.{w', w} ≅
+      shrinkCoyoneda :=
+  NatIso.ofComponents
+    (fun X ↦ FunctorToTypes.shrinkCompUliftFunctorIso.{w, v} (coyoneda.obj X))
+    fun _ ↦ by ext; simp [shrinkCoyoneda]
+
+/-- `uliftYoneda` identifies to `shrinkCoyoneda`. -/
+noncomputable def uliftYonedaIsoShrinkCoyoneda :
+    uliftCoyoneda.{w'} (C := C) ≅ shrinkCoyoneda.{max w' v} :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
+    (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) (fun f ↦ by
+      ext
+      exact (shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm _ _).symm)) (fun g ↦ by
+      ext
+      exact (shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm _ _).symm)
+
+set_option backward.defeqAttrib.useBackward true in
+/-- The functor `shrinkCoyoneda.{w}` followed by the evaluation
+at `Y : C` and `uliftFunctor.{v}` identifies to `yoneda.obj Y` followed
+by `uliftFunctor.{w}`. -/
+noncomputable def shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctor (Y : C) :
+    shrinkCoyoneda.{w} ⋙ (evaluation C _).obj Y ⋙ uliftFunctor.{v} ≅
+      yoneda.obj Y ⋙ uliftFunctor.{w} :=
+  NatIso.ofComponents (fun X ↦ (Equiv.ulift.trans
+    (shrinkCoyonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso) (fun f ↦ by
+      ext ⟨g⟩
+      obtain ⟨g, rfl⟩ := shrinkCoyonedaObjObjEquiv.symm.surjective g
+      simp [shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm])
+
+/-- `shrinkCoyoneda.obj X` is corepresented by `X`. -/
+@[simps]
+noncomputable
+def shrinkCoyonedaRepresentableBy (X : Cᵒᵖ) :
+    (shrinkCoyoneda.{w}.obj X).CorepresentableBy X.unop where
+  homEquiv := shrinkCoyonedaObjObjEquiv.symm
+  homEquiv_comp f g := shrinkCoyonedaObjObjEquiv_symm_comp g f
+
+instance (X : Cᵒᵖ) : (shrinkCoyoneda.{w}.obj X).IsCorepresentable :=
+  (shrinkCoyonedaRepresentableBy X).isCorepresentable
+
+end Coyoneda
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 47e49329be6c64..3f63b674df05cf 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -6,7 +6,9 @@ Authors: Ben Eltschig
 module
 
 public import Mathlib.CategoryTheory.Adjunction.Triple
+public import Mathlib.CategoryTheory.Limits.Elements
 public import Mathlib.CategoryTheory.Sites.GlobalSections
+public import Mathlib.CategoryTheory.Sites.Point.Skyscraper
 
 /-!
 # Local sites
@@ -18,10 +20,14 @@ See https://ncatlab.org/nlab/show/local+site.
 
 ## Main definitions / results
 * `J.IsLocalSite`: typeclass stating that (C,J) is a local site.
-* `coconstantSheaf`: the coconstant sheaf functor `Type w ⥤ Sheaf J (Type max v w)` defined on any
-  local site.
-* `ΓCoconstantSheafAdj`: the adjunction between the global sections functor `Γ` and
-  `coconstantSheaf`.
+* `IsLocalSite.point J`: the canonical point of any local site, whose fibre functor is given by
+  the coyoneda embedding of the terminal object and extends to the global sections functors on
+  presheaves and sheaves.
+* `coconstantSheaf J A`: the coconstant sheaf functor `A ⥤ Sheaf J A` for any local site (C,J) and
+  sufficiently nice target category `A`, defined as the skyscraper sheaf functor of the canonical
+  point.
+* `ΓCoconstantSheafAdj J A`: the adjunction between the global sections functor `Γ J A` and
+  `coconstantSheaf J A`.
 * `fullyFaithfulCoconstantSheaf`: `coconstantSheaf` is fully faithful.
 * `fullyFaithfulConstantSheaf`: on local sites, the constant sheaf functor is fully faithful.
 
@@ -29,7 +35,7 @@ All together this shows that for local sites `Sheaf J (Type max u v w)` forms a
 since we don't yet have local topoi this can't be stated yet.
 -/
 
-universe w u v
+universe w u v u' v'
 
 @[expose] public section
 
@@ -45,7 +51,7 @@ class GrothendieckTopology.IsLocalSite extends HasTerminal C where
   eq_top_of_mem : ∀ S ∈ J (⊤_ C), S = ⊤
 
 /-- On a local site, every covering sieve contains every morphism from the terminal object. -/
-lemma LocalSite.from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
+lemma IsLocalSite.from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
     (hS : S ∈ J X) : S.arrows f :=
   (S.mem_iff_pullback_eq_top f).2 <| IsLocalSite.eq_top_of_mem _ <| J.pullback_stable f hS
 
@@ -53,142 +59,166 @@ lemma LocalSite.from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶
 instance {C : Type u} [Category.{v} C] [HasTerminal C] : (trivial C).IsLocalSite where
   eq_top_of_mem _ := trivial_covering.1
 
-/-- The functor that sends any type `A` to the functor `Cᵒᵖ → Type _` that sends any `X : C`
-to the type of all functions `(⊤_ C ⟶ X) → A`. This can be defined on any site with a terminal
-object, but has values in sheaves in the case of local sites. -/
-@[simps!]
-noncomputable def Presheaf.coconst {C : Type u} [Category.{v} C] [HasTerminal C] :
-    Type w ⥤ (Cᵒᵖ ⥤ Type max v w) where
-  obj A := {
-    obj X := ((⊤_ C ⟶ X.unop) → A)
-    map f := TypeCat.ofHom fun g g' ↦ g (g' ≫ f.unop) }
-  map f := {
-    app X := TypeCat.ofHom fun g ↦ ConcreteCategory.hom f ∘ g }
+/-- Every local site has a canonical point, given as a fibre functor by the coyoneda embedding of
+the terminal object `⊤_ C`. -/
+noncomputable def IsLocalSite.point [LocallySmall.{w} C] [J.IsLocalSite] : Point.{w} J where
+  fiber := shrinkCoyoneda.obj (op (⊤_ C))
+  jointly_surjective := fun R hR x ↦
+    ⟨(⊤_ C), shrinkCoyonedaObjObjEquiv x,
+      (IsLocalSite.from_terminal_mem_of_mem J (shrinkCoyonedaObjObjEquiv x) hR),
+          shrinkCoyonedaObjObjEquiv.symm (𝟙 _), by
+        rw [shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm]
+        simp⟩
+
+lemma shrinkCoyoneda_obj_map [LocallySmall.{w} C]
+    {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (shrinkCoyoneda.obj X).obj Y) :
+    (shrinkCoyoneda.obj _).map g f =
+      shrinkCoyonedaObjObjEquiv.symm (shrinkCoyonedaObjObjEquiv f ≫ g) :=
+  rfl
+
+/-- The canonical initial object of `(shrinkCoyoneda.{w}.obj (op X)).Elements`, given
+by `𝟙 X : X ⟶ X`. -/
+noncomputable def shrinkCoyonedaElementsInitial [LocallySmall.{w} C] (X : C) :
+  (shrinkCoyoneda.{w}.obj (op X)).Elements :=
+    ⟨X, shrinkCoyonedaObjObjEquiv.symm (𝟙 X)⟩
 
 set_option backward.isDefEq.respectTransparency false in
-/-- On local sites, `Presheaf.coconst'` actually takes values in sheaves. -/
-lemma Presheaf.coconst_isSheaf [J.IsLocalSite] (X : Type w) : IsSheaf J (coconst.obj X) := by
-  refine (isSheaf_iff_isSheaf_of_type J _).2 fun Y S hS f hf ↦ ?_
-  refine ⟨fun g ↦ f g (LocalSite.from_terminal_mem_of_mem J g hS) (𝟙 _), ?_, ?_⟩
-  · refine fun Z g hg ↦ funext fun x ↦ ?_
-    exact (congrFun (f.comp_of_compatible S hf hg x) _).trans (congrArg (f g hg) <| by simp)
-  · exact fun g hg ↦ funext fun h : (⊤_ C ⟶ Y) ↦ Eq.trans (by simp [Presheaf.coconst]) <|
-      congrFun (hg h ((LocalSite.from_terminal_mem_of_mem J h hS))) _
-
-/-- The right adjoint to the global sections functor that exists over any local site.
-Takes a type `X` to the sheaf that sends each `Y : C` to the type of functions `Y → X`. -/
-noncomputable def IsLocalSite.coconstantSheaf [J.IsLocalSite] :
-    Type w ⥤ Sheaf J (Type (max v w)) where
-  obj X := ⟨Presheaf.coconst.obj X, Presheaf.coconst_isSheaf J X⟩
-  map f := ⟨Presheaf.coconst.map f⟩
-  map_id _ := rfl
-  map_comp _ _ := rfl
+/-- `shrinkCoyonedaElementsInitial X` is indeed initial. -/
+noncomputable def shrinkCoyonedaElementsInitialIsInitial [LocallySmall.{w} C] (X : C) :
+    IsInitial (shrinkCoyonedaElementsInitial X) where
+  desc s := ⟨shrinkCoyonedaObjObjEquiv s.pt.snd, by
+    simp only [asEmptyCocone, shrinkCoyonedaElementsInitial]
+    rw [← shrinkCoyonedaObjObjEquiv_symm_comp]
+    simp⟩
+  uniq := by
+    intro s ⟨(f : X ⟶ _), hf⟩ _
+    ext1
+    simp only [shrinkCoyoneda_obj_map, asEmptyCocone, shrinkCoyonedaElementsInitial,
+      Equiv.apply_symm_apply, Category.id_comp] at hf
+    exact (Equiv.symm_apply_eq _).1 hf
 
 set_option backward.isDefEq.respectTransparency false in
+/-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `IsLocalSite.point J` is just `P` evaluated at
+the terminal object. -/
+noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
+    {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : Cᵒᵖ ⥤ A) :
+    (IsLocalSite.point J).presheafFiber.obj P ≅ P.obj (op (⊤_ C)) :=
+  (colimit.isColimit _).coconePointUniqueUpToIso
+    (colimitOfDiagramTerminal (shrinkCoyonedaElementsInitialIsInitial (⊤_ C)).op _)
+
+set_option backward.isDefEq.respectTransparency false in
+lemma IsColimit.map_comp_coconePointUniqueUpToIso {J : Type*} [Category* J] {F G : J ⥤ C}
+    {s : Cocone F} {t t' : Cocone G} (hs : IsColimit s) (ht : IsColimit t)
+    (ht' : IsColimit t') (α : F ⟶ G) :
+    hs.map t α ≫ (ht.coconePointUniqueUpToIso ht').hom = hs.map t' α :=
+  hs.uniq (((Cocone.precompose α).obj t')) _ fun i ↦ by simp
+
+set_option backward.isDefEq.respectTransparency false in
+lemma IsColimit.coconePointUniqueUpToIso_comp_map {J : Type*} [Category* J] {F G : J ⥤ C}
+    {s' s : Cocone F} (hs' : IsColimit s') (hs : IsColimit s) (t : Cocone G) (α : F ⟶ G) :
+    (hs'.coconePointUniqueUpToIso hs).hom ≫ hs.map t α = hs'.map t α :=
+  hs'.uniq (((Cocone.precompose α).obj t)) _ fun i ↦ by simp
+
+lemma IsColimit.coconePointUniqueUpToIso_naturality {J : Type*} [Category* J] {F G : J ⥤ C}
+    {s s' : Cocone F} {t t' : Cocone G} (hs : IsColimit s) (hs' : IsColimit s') (ht : IsColimit t)
+    (ht' : IsColimit t') (α : F ⟶ G) :
+    hs.map t α ≫ (ht.coconePointUniqueUpToIso ht').hom =
+      (hs.coconePointUniqueUpToIso hs').hom ≫ hs'.map t' α := by
+  rw [map_comp_coconePointUniqueUpToIso, coconePointUniqueUpToIso_comp_map]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
+    {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
+    (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
+      (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C)) := by
+  refine (IsColimit.coconePointUniqueUpToIso_naturality _
+    (colimitOfDiagramTerminal (shrinkCoyonedaElementsInitialIsInitial (⊤_ C)).op _) _ _
+      (((CategoryOfElements.π (shrinkCoyoneda.{w}.obj (op (⊤_ C)))).op.whiskerLeft F))).trans ?_
+  congr
+  simp only [IsColimit.map, colimitOfDiagramTerminal, Cocone.precompose_obj_ι, NatTrans.comp_app,
+    Functor.whiskerLeft_app, coconeOfDiagramTerminal_ι_app, IsTerminal.from_self, Functor.map_id]
+  exact Category.comp_id _
+
+/-- The presheaf fibre functor of `IsLocalSite.point J` is given by evaluation at the terminal
+object. -/
+noncomputable def IsLocalSite.pointPresheafFiberNatIso [LocallySmall.{w} C] [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] :
+    ((IsLocalSite.point J).presheafFiber : _ ⥤ A) ≅ (evaluation _ _).obj (op (⊤_ C)) :=
+  NatIso.ofComponents (pointPresheafFiberIso J) fun F ↦ pointPresheafFiberIso_naturality J F
+
+/-- The sheaf fibre functor of `IsLocalSite.point J` is the global sections functor. -/
+noncomputable def IsLocalSite.pointSheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    [HasWeakSheafify J A] : (IsLocalSite.point J).sheafFiber ≅ Γ J A :=
+  ((sheafToPresheaf J A).isoWhiskerLeft (pointPresheafFiberNatIso J A)).trans
+    (ΓNatIsoSheafSections J A terminalIsTerminal).symm
+
+/-- The right adjoint to the global sections functor that exists over any local site. This is
+implemented as the skyscraper functor associated to `IsLocalSite.point.{w} J`, but can be thought of
+as taking any object `X : A` to the sheaf that sends each `Y : C` to the product over copies of `A`
+indexed by the points `⊤_ C ⟶ Y` of `Y`. -/
+noncomputable def IsLocalSite.coconstantSheaf [LocallySmall.{w} C] [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    [HasProducts.{w} A] : A ⥤ Sheaf J A :=
+  (point.{w} J).skyscraperSheafFunctor
+
+noncomputable example [J.IsLocalSite] : Type max v w ⥤ Sheaf J (Type (max v w)) :=
+  IsLocalSite.coconstantSheaf.{max v w} J (Type max v w)
+
+variable [LocallySmall.{w} C] [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    [HasProducts.{w} A] [HasWeakSheafify J A]
+
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
-noncomputable def IsLocalSite.ΓCoconstantSheafAdj [J.IsLocalSite] :
-    Γ J (Type max u v w) ⊣ coconstantSheaf J := by
-  refine Adjunction.ofNatIsoLeft ?_ (ΓNatIsoSheafSections J _ terminalIsTerminal).symm
-  exact {
-    unit := {
-      app X := ⟨{
-        app Y := TypeCat.ofHom fun (x : X.obj.obj Y) y ↦ X.obj.map (op y) x
-        naturality Y Z f := by
-          ext (x : X.obj.obj Y)
-          dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp]
-          ext z
-          exact (Functor.map_comp_apply X.obj _ _ x).symm
-      }⟩
-      naturality X Y f := by
-        ext Z (x : X.obj.obj Z)
-        dsimp [coconstantSheaf, Presheaf.coconst, Functor.comp]
-        ext z
-        exact (NatTrans.naturality_apply f.hom _ x).symm
-    }
-    counit := { app X := TypeCat.ofHom fun f ↦ f (𝟙 _) }
-    left_triangle_components X := by
-      ext (x : X.obj.obj _)
-      exact ConcreteCategory.congr_hom (X.obj.map_id _) x
-    right_triangle_components X := by
-      ext Y (f : _ → _)
-      dsimp [coconstantSheaf, Presheaf.coconst]
-      ext y
-      simp }
-
-instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v w} J).IsRightAdjoint :=
-  ⟨Γ J _, ⟨IsLocalSite.ΓCoconstantSheafAdj J⟩⟩
+noncomputable def IsLocalSite.ΓCoconstantSheafAdj' : Γ J A ⊣ coconstantSheaf J A :=
+  (point.{w} J).skyscraperSheafAdjunction.ofNatIsoLeft (pointSheafFiberIso J A)
+
+instance : (Γ J A).IsLeftAdjoint :=
+  ⟨IsLocalSite.coconstantSheaf.{w} J A, ⟨IsLocalSite.ΓCoconstantSheafAdj' J A⟩⟩
+
+instance : (IsLocalSite.coconstantSheaf.{w} J A).IsRightAdjoint :=
+  ⟨Γ J A, ⟨IsLocalSite.ΓCoconstantSheafAdj' J A⟩⟩
 
 /-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
-noncomputable def coconstantSheafΓNatIsoId [J.IsLocalSite] :
-    IsLocalSite.coconstantSheaf J ⋙ Γ J _ ≅ 𝟭 (Type max u v w) := by
+noncomputable def coconstantSheafΓNatIsoId' :
+    IsLocalSite.coconstantSheaf J A ⋙ Γ J A ≅ 𝟭 A := by
   refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
-  exact (NatIso.ofComponents (fun X ↦ {
-    hom := TypeCat.ofHom fun x _ ↦ x
-    inv := TypeCat.ofHom fun f ↦ by exact f (𝟙 (⊤_ C))
-    inv_hom_id := by
-      dsimp [IsLocalSite.coconstantSheaf, Presheaf.coconst]
-      ext x
-      dsimp at ⊢
-      exact funext fun x ↦ congr_arg _ <| Subsingleton.elim _ _
-  })).symm
+  refine NatIso.ofComponents (fun X ↦ @productUniqueIso
+    (((IsLocalSite.point J).fiber.obj (⊤_ C))) _ _ (equivShrink (⊤_ C ⟶ ⊤_ C)).symm.unique _) ?_
+  intro X Y f
+  simp only [IsLocalSite.coconstantSheaf, Point.skyscraperSheafFunctor,
+    Point.skyscraperPresheafFunctor, Functor.comp, Functor.id_obj, Functor.flip_obj_map,
+    ObjectProperty.ι_obj, ObjectProperty.ι_map, Functor.flip_map_app, piFunctor_map_app,
+    productUniqueIso_hom, Functor.id_map]
+  exact Pi.map_π _ _
 
 /-- `coconstantSheaf` is fully faithful. -/
-noncomputable def fullyFaithfulCoconstantSheaf [J.IsLocalSite] :
-    (IsLocalSite.coconstantSheaf.{max u v w} J).FullyFaithful :=
-  (IsLocalSite.ΓCoconstantSheafAdj J).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId J)
+noncomputable def fullyFaithfulCoconstantSheaf :
+    (IsLocalSite.coconstantSheaf.{w} J A).FullyFaithful :=
+  (IsLocalSite.ΓCoconstantSheafAdj' J A).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId' J A)
 
-instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v} J).Full :=
-  (fullyFaithfulCoconstantSheaf J).full
+instance : (IsLocalSite.coconstantSheaf.{w} J A).Full :=
+  (fullyFaithfulCoconstantSheaf J A).full
 
-instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v} J).Faithful :=
-  (fullyFaithfulCoconstantSheaf J).faithful
+instance : (IsLocalSite.coconstantSheaf.{w} J A).Faithful :=
+  (fullyFaithfulCoconstantSheaf J A).faithful
+
+/-- The adjoint triple `constantSheaf J A ⊣ Γ J A ⊣ coconstantSheaf J A` on any local site. -/
+noncomputable abbrev IsLocalSite.constantΓCoconstantTriple :
+    Adjunction.Triple (constantSheaf J A) (Γ J A) (coconstantSheaf.{w} J A) where
+  adj₁ := constantSheafΓAdj J A
+  adj₂ := ΓCoconstantSheafAdj' J A
 
 /-- On local sites, the constant sheaf functor is fully faithful. -/
-noncomputable def fullyFaithfulConstantSheaf [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :
-    (constantSheaf J (Type max u v w)).FullyFaithful :=
-  (Adjunction.Triple.mk (constantSheafΓAdj J _)
-    (IsLocalSite.ΓCoconstantSheafAdj J)).fullyFaithfulEquiv.symm <| fullyFaithfulCoconstantSheaf J
-
-instance [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :
-    (constantSheaf J (Type max u v w)).Full :=
-  (fullyFaithfulConstantSheaf J).full
-
-instance [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :
-    (constantSheaf J (Type max u v w)).Faithful :=
-  (fullyFaithfulConstantSheaf J).faithful
-
-open List in
-/-- For any site with a terminal object, the following are equivalent:
-* the site is local, i.e. the only covering sieve of the terminal object is the trivial one
-* every covering sieve contains all morphisms from the terminal object
-* the coconstant presheaf on the empty type is a sheaf
-* every coconstant presheaf is a sheaf. -/
-protected theorem GrothendieckTopology.IsLocalSite.tfae [HasTerminal C] :
-    TFAE [J.IsLocalSite,
-      ∀ X : C, ∀ S ∈ J X, ∀ x : ⊤_ C ⟶ X, S x,
-      Presieve.IsSheaf J (Presheaf.coconst.{max u v}.obj PEmpty),
-      ∀ X : Type max u v, Presieve.IsSheaf J (Presheaf.coconst.obj X)] := by
-  tfae_have 2 → 1 := fun h ↦ ⟨fun S hS ↦ S.id_mem_iff_eq_top.1 <| h _ S hS _⟩
-  tfae_have 1 → 2 := fun h X S hS f ↦ by
-    simpa using Sieve.id_mem_iff_eq_top.2 <| h.eq_top_of_mem _ <| J.pullback_stable f hS
-  tfae_have 3 → 1 := fun h ↦ ⟨fun S hS ↦ by
-    replace h : IsEmpty (Presieve.FamilyOfElements
-        (Presheaf.coconst.{max u v}.obj PEmpty) S.arrows) := by
-      have : IsEmpty ((Presheaf.coconst.{max u v}.obj PEmpty).obj (op (⊤_ C))) := by
-        dsimp [Presheaf.coconst]; exact isEmpty_fun.2 ⟨⟨𝟙 _⟩, inferInstance⟩
-      have {X : C} : Subsingleton ((Presheaf.coconst.{max u v}.obj PEmpty).obj (op X)) :=
-        Pi.instSubsingleton
-      refine not_nonempty_iff.1 fun ⟨x⟩ ↦ IsEmpty.false (h S hS x ?_).choose
-      exact fun _ _ _ _ _ _ _ _ _ _ ↦ Subsingleton.elim _ _
-    replace ⟨X, f, hf, h⟩ : ∃ X, ∃ f : X ⟶ ⊤_ C, S f ∧
-        IsEmpty ((Presheaf.coconst.{max u v}.obj PEmpty).obj (op X)) := by
-      by_contra! h'; exact h.false fun X f hf ↦ (h' X f hf).some
-    let ⟨(g : _ ⟶ _)⟩ := (isEmpty_fun.1 h).1
-    refine S.id_mem_iff_eq_top.1 ?_
-    convert S.downward_closed hf g
-    exact Subsingleton.elim _ _⟩
-  tfae_have 4 → 3 := fun h ↦ h _
-  tfae_have 1 → 4 := fun _ _ ↦ (isSheaf_iff_isSheaf_of_type _ _).1 <| Presheaf.coconst_isSheaf J _
-  tfae_finish
+noncomputable def fullyFaithfulConstantSheaf : (constantSheaf J A).FullyFaithful :=
+  (IsLocalSite.constantΓCoconstantTriple J A).fullyFaithfulEquiv.symm <|
+    fullyFaithfulCoconstantSheaf.{w} J A
+
+instance : (constantSheaf J A).Full :=
+  (fullyFaithfulConstantSheaf.{w} J A).full
+
+instance : (constantSheaf J A).Faithful :=
+  (fullyFaithfulConstantSheaf.{w} J A).faithful
 
 end CategoryTheory

From 28066540774bebb06f4bd51e5157dea5e1ab0483 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 29 Jun 2026 13:48:39 +0200
Subject: [PATCH 08/20] apply suggestions

---
 Mathlib/CategoryTheory/ShrinkYoneda.lean    |   6 +-
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 106 +++++++++++++-------
 2 files changed, 71 insertions(+), 41 deletions(-)

diff --git a/Mathlib/CategoryTheory/ShrinkYoneda.lean b/Mathlib/CategoryTheory/ShrinkYoneda.lean
index 6d83aab6128fb4..a8a8f73f64c307 100644
--- a/Mathlib/CategoryTheory/ShrinkYoneda.lean
+++ b/Mathlib/CategoryTheory/ShrinkYoneda.lean
@@ -402,7 +402,7 @@ def shrinkCoyonedaUliftFunctorIso [LocallySmall.{max w w'} C] :
     (fun X ↦ FunctorToTypes.shrinkCompUliftFunctorIso.{w, v} (coyoneda.obj X))
     fun _ ↦ by ext; simp [shrinkCoyoneda]
 
-/-- `uliftYoneda` identifies to `shrinkCoyoneda`. -/
+/-- `uliftCoyoneda` identifies to `shrinkCoyoneda`. -/
 noncomputable def uliftYonedaIsoShrinkCoyoneda :
     uliftCoyoneda.{w'} (C := C) ≅ shrinkCoyoneda.{max w' v} :=
   NatIso.ofComponents (fun X ↦ NatIso.ofComponents
@@ -428,13 +428,13 @@ noncomputable def shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctor (Y
 /-- `shrinkCoyoneda.obj X` is corepresented by `X`. -/
 @[simps]
 noncomputable
-def shrinkCoyonedaRepresentableBy (X : Cᵒᵖ) :
+def shrinkCoyonedaCorepresentableBy (X : Cᵒᵖ) :
     (shrinkCoyoneda.{w}.obj X).CorepresentableBy X.unop where
   homEquiv := shrinkCoyonedaObjObjEquiv.symm
   homEquiv_comp f g := shrinkCoyonedaObjObjEquiv_symm_comp g f
 
 instance (X : Cᵒᵖ) : (shrinkCoyoneda.{w}.obj X).IsCorepresentable :=
-  (shrinkCoyonedaRepresentableBy X).isCorepresentable
+  (shrinkCoyonedaCorepresentableBy X).isCorepresentable
 
 end Coyoneda
 
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 3f63b674df05cf..87f2277d379380 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -18,6 +18,10 @@ of a local topos. This makes them an important stepping stone to cohesive sites.
 
 See https://ncatlab.org/nlab/show/local+site.
 
+Sheaves of types on any local site form a local topos (i.e. a topos whose global sections functor
+has a fully faithful right adjoint), and a subcanonical site is local if and only if its topos of
+sheaves of types is.
+
 ## Main definitions / results
 * `J.IsLocalSite`: typeclass stating that (C,J) is a local site.
 * `IsLocalSite.point J`: the canonical point of any local site, whose fibre functor is given by
@@ -76,27 +80,6 @@ lemma shrinkCoyoneda_obj_map [LocallySmall.{w} C]
       shrinkCoyonedaObjObjEquiv.symm (shrinkCoyonedaObjObjEquiv f ≫ g) :=
   rfl
 
-/-- The canonical initial object of `(shrinkCoyoneda.{w}.obj (op X)).Elements`, given
-by `𝟙 X : X ⟶ X`. -/
-noncomputable def shrinkCoyonedaElementsInitial [LocallySmall.{w} C] (X : C) :
-  (shrinkCoyoneda.{w}.obj (op X)).Elements :=
-    ⟨X, shrinkCoyonedaObjObjEquiv.symm (𝟙 X)⟩
-
-set_option backward.isDefEq.respectTransparency false in
-/-- `shrinkCoyonedaElementsInitial X` is indeed initial. -/
-noncomputable def shrinkCoyonedaElementsInitialIsInitial [LocallySmall.{w} C] (X : C) :
-    IsInitial (shrinkCoyonedaElementsInitial X) where
-  desc s := ⟨shrinkCoyonedaObjObjEquiv s.pt.snd, by
-    simp only [asEmptyCocone, shrinkCoyonedaElementsInitial]
-    rw [← shrinkCoyonedaObjObjEquiv_symm_comp]
-    simp⟩
-  uniq := by
-    intro s ⟨(f : X ⟶ _), hf⟩ _
-    ext1
-    simp only [shrinkCoyoneda_obj_map, asEmptyCocone, shrinkCoyonedaElementsInitial,
-      Equiv.apply_symm_apply, Category.id_comp] at hf
-    exact (Equiv.symm_apply_eq _).1 hf
-
 set_option backward.isDefEq.respectTransparency false in
 /-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `IsLocalSite.point J` is just `P` evaluated at
 the terminal object. -/
@@ -104,7 +87,8 @@ noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLo
     {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : Cᵒᵖ ⥤ A) :
     (IsLocalSite.point J).presheafFiber.obj P ≅ P.obj (op (⊤_ C)) :=
   (colimit.isColimit _).coconePointUniqueUpToIso
-    (colimitOfDiagramTerminal (shrinkCoyonedaElementsInitialIsInitial (⊤_ C)).op _)
+    (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
+      <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _)
 
 set_option backward.isDefEq.respectTransparency false in
 lemma IsColimit.map_comp_coconePointUniqueUpToIso {J : Type*} [Category* J] {F G : J ⥤ C}
@@ -126,19 +110,24 @@ lemma IsColimit.coconePointUniqueUpToIso_naturality {J : Type*} [Category* J] {F
       (hs.coconePointUniqueUpToIso hs').hom ≫ hs'.map t' α := by
   rw [map_comp_coconePointUniqueUpToIso, coconePointUniqueUpToIso_comp_map]
 
-set_option backward.isDefEq.respectTransparency false in
+lemma IsColimit.colimitOfDiagramTerminal_map {J : Type*} [Category* J] {F G : J ⥤ C}
+    {X : J} (hX : IsTerminal X) (α : F ⟶ G) :
+    (colimitOfDiagramTerminal hX F).map (coconeOfDiagramTerminal hX G) α = α.app X := by
+  simp only [IsColimit.map, colimitOfDiagramTerminal, Cocone.precompose_obj_ι, NatTrans.comp_app,
+    coconeOfDiagramTerminal_ι_app, IsTerminal.from_self, Functor.map_id]
+  exact Category.comp_id _
+
 lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
     {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
     {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
     (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
       (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C)) := by
   refine (IsColimit.coconePointUniqueUpToIso_naturality _
-    (colimitOfDiagramTerminal (shrinkCoyonedaElementsInitialIsInitial (⊤_ C)).op _) _ _
+    (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
+      <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _) _ _
       (((CategoryOfElements.π (shrinkCoyoneda.{w}.obj (op (⊤_ C)))).op.whiskerLeft F))).trans ?_
   congr
-  simp only [IsColimit.map, colimitOfDiagramTerminal, Cocone.precompose_obj_ι, NatTrans.comp_app,
-    Functor.whiskerLeft_app, coconeOfDiagramTerminal_ι_app, IsTerminal.from_self, Functor.map_id]
-  exact Category.comp_id _
+  exact IsColimit.colimitOfDiagramTerminal_map _ _
 
 /-- The presheaf fibre functor of `IsLocalSite.point J` is given by evaluation at the terminal
 object. -/
@@ -157,12 +146,17 @@ noncomputable def IsLocalSite.pointSheafFiberIso [LocallySmall.{w} C] [J.IsLocal
 /-- The right adjoint to the global sections functor that exists over any local site. This is
 implemented as the skyscraper functor associated to `IsLocalSite.point.{w} J`, but can be thought of
 as taking any object `X : A` to the sheaf that sends each `Y : C` to the product over copies of `A`
-indexed by the points `⊤_ C ⟶ Y` of `Y`. -/
+indexed by the points `⊤_ C ⟶ Y` of `Y`.
+
+Note this takes in an extra universe parameter `w` that does not appear in the output type
+`A ⥤ Sheaf J A` but is required for the construction; it should always be given explicitly when
+referring to this functor, as in e.g. `coconstantSheaf.{w} J A`. -/
 noncomputable def IsLocalSite.coconstantSheaf [LocallySmall.{w} C] [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
     [HasProducts.{w} A] : A ⥤ Sheaf J A :=
   (point.{w} J).skyscraperSheafFunctor
 
+/-- In particular, this construction works for sheaves of types. -/
 noncomputable example [J.IsLocalSite] : Type max v w ⥤ Sheaf J (Type (max v w)) :=
   IsLocalSite.coconstantSheaf.{max v w} J (Type max v w)
 
@@ -171,18 +165,30 @@ variable [LocallySmall.{w} C] [J.IsLocalSite]
     [HasProducts.{w} A] [HasWeakSheafify J A]
 
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
-noncomputable def IsLocalSite.ΓCoconstantSheafAdj' : Γ J A ⊣ coconstantSheaf J A :=
+noncomputable def IsLocalSite.ΓCoconstantSheafAdj : Γ J A ⊣ coconstantSheaf.{w} J A :=
   (point.{w} J).skyscraperSheafAdjunction.ofNatIsoLeft (pointSheafFiberIso J A)
 
-instance : (Γ J A).IsLeftAdjoint :=
-  ⟨IsLocalSite.coconstantSheaf.{w} J A, ⟨IsLocalSite.ΓCoconstantSheafAdj' J A⟩⟩
+/-- On any locally `w`-small local site, the global sections functor to any category with colimits
+and products of size `w` is a left adulljoint. A variant of this without the universe parameter `w`
+is registered as an instance. -/
+lemma IsLocalSite.Γ_isLeftAdjoint : (Γ J A).IsLeftAdjoint :=
+  ⟨IsLocalSite.coconstantSheaf.{w} J A, ⟨IsLocalSite.ΓCoconstantSheafAdj J A⟩⟩
+
+/-- On any local site with morphism types in `Type v`, the global sections functor to any category
+with colimits and products of size `v` is a left adjoint. See `IsLocalSite.ΓIsLeftAdjoint` for a
+version for `w`-locally small sites that can't be registered as an instance because of the extra
+universe parameter `w`. -/
+instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A]
+    [HasProducts.{v} A] [HasWeakSheafify J A] : (Γ J A).IsLeftAdjoint :=
+  IsLocalSite.Γ_isLeftAdjoint.{v} J A
 
 instance : (IsLocalSite.coconstantSheaf.{w} J A).IsRightAdjoint :=
-  ⟨Γ J A, ⟨IsLocalSite.ΓCoconstantSheafAdj' J A⟩⟩
+  ⟨Γ J A, ⟨IsLocalSite.ΓCoconstantSheafAdj J A⟩⟩
 
 /-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
-noncomputable def coconstantSheafΓNatIsoId' :
-    IsLocalSite.coconstantSheaf J A ⋙ Γ J A ≅ 𝟭 A := by
+noncomputable def coconstantSheafΓNatIsoId :
+    IsLocalSite.coconstantSheaf.{w} J A ⋙ Γ J A ≅ 𝟭 A := by
   refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
   refine NatIso.ofComponents (fun X ↦ @productUniqueIso
     (((IsLocalSite.point J).fiber.obj (⊤_ C))) _ _ (equivShrink (⊤_ C ⟶ ⊤_ C)).symm.unique _) ?_
@@ -196,7 +202,7 @@ noncomputable def coconstantSheafΓNatIsoId' :
 /-- `coconstantSheaf` is fully faithful. -/
 noncomputable def fullyFaithfulCoconstantSheaf :
     (IsLocalSite.coconstantSheaf.{w} J A).FullyFaithful :=
-  (IsLocalSite.ΓCoconstantSheafAdj' J A).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId' J A)
+  (IsLocalSite.ΓCoconstantSheafAdj J A).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId J A)
 
 instance : (IsLocalSite.coconstantSheaf.{w} J A).Full :=
   (fullyFaithfulCoconstantSheaf J A).full
@@ -208,17 +214,41 @@ instance : (IsLocalSite.coconstantSheaf.{w} J A).Faithful :=
 noncomputable abbrev IsLocalSite.constantΓCoconstantTriple :
     Adjunction.Triple (constantSheaf J A) (Γ J A) (coconstantSheaf.{w} J A) where
   adj₁ := constantSheafΓAdj J A
-  adj₂ := ΓCoconstantSheafAdj' J A
+  adj₂ := ΓCoconstantSheafAdj J A
 
 /-- On local sites, the constant sheaf functor is fully faithful. -/
 noncomputable def fullyFaithfulConstantSheaf : (constantSheaf J A).FullyFaithful :=
   (IsLocalSite.constantΓCoconstantTriple J A).fullyFaithfulEquiv.symm <|
     fullyFaithfulCoconstantSheaf.{w} J A
 
-instance : (constantSheaf J A).Full :=
+/-- On any locally `w`-small local site, the constant sheaf functor from any category with colimits
+and products of size `w` is full. A variant of this without the universe parameter `w`
+is registered as an instance. -/
+lemma IsLocalSite.constantSheaf_full : (constantSheaf J A).Full :=
   (fullyFaithfulConstantSheaf.{w} J A).full
 
-instance : (constantSheaf J A).Faithful :=
+/-- On any locally `w`-small local site, the constant sheaf functor from any category with colimits
+and products of size `w` is faithful. A variant of this without the universe parameter `w`
+is registered as an instance. -/
+lemma IsLocalSite.constantSheaf_faithful : (constantSheaf J A).Faithful :=
   (fullyFaithfulConstantSheaf.{w} J A).faithful
 
+/-- On any local site with morphism types in `Type v`, the constant sheaf functor from any category
+with colimits and products of size `v` is full. See `IsLocalSite.constantSheaf_full` for a
+version for `w`-locally small sites that can't be registered as an instance because of the extra
+universe parameter `w`. -/
+instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A]
+    [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Full :=
+  IsLocalSite.constantSheaf_full.{v} J A
+
+/-- On any local site with morphism types in `Type v`, the constant sheaf functor from any category
+with colimits and products of size `v` is faithful. See `IsLocalSite.constantSheaf_faithful` for a
+version for `w`-locally small sites that can't be registered as an instance because of the extra
+universe parameter `w`. -/
+instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
+    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A]
+    [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Faithful :=
+  IsLocalSite.constantSheaf_faithful.{v} J A
+
 end CategoryTheory

From ffffc9eee61194ce514c55de6723a1005d185113 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 29 Jun 2026 13:52:47 +0200
Subject: [PATCH 09/20] add `shrinkCoyoneda`

---
 Mathlib/CategoryTheory/ShrinkYoneda.lean | 189 +++++++++++++++++++++++
 1 file changed, 189 insertions(+)

diff --git a/Mathlib/CategoryTheory/ShrinkYoneda.lean b/Mathlib/CategoryTheory/ShrinkYoneda.lean
index 9de58282348005..a8a8f73f64c307 100644
--- a/Mathlib/CategoryTheory/ShrinkYoneda.lean
+++ b/Mathlib/CategoryTheory/ShrinkYoneda.lean
@@ -69,6 +69,8 @@ end FunctorToTypes
 
 variable [LocallySmall.{w} C]
 
+section Yoneda
+
 set_option backward.defeqAttrib.useBackward true in
 instance (X : C) : FunctorToTypes.Small.{w} (yoneda.obj X) :=
   fun _ ↦ by dsimp; infer_instance
@@ -249,4 +251,191 @@ def shrinkYonedaRepresentableBy (X : C) : (shrinkYoneda.{w}.obj X).Representable
 instance (X : C) : (shrinkYoneda.{w}.obj X).IsRepresentable :=
   (shrinkYonedaRepresentableBy X).isRepresentable
 
+end Yoneda
+
+section Coyoneda
+
+set_option backward.defeqAttrib.useBackward true in
+instance (X : Cᵒᵖ) : FunctorToTypes.Small.{w} (coyoneda.obj X) :=
+  fun _ ↦ by dsimp; infer_instance
+
+/-- The co-Yoneda embedding `Cᵒᵖ ⥤ C ⥤ Type w` for a locally `w`-small category `C`. -/
+@[simps -isSimp obj map, pp_with_univ]
+noncomputable def shrinkCoyoneda :
+    Cᵒᵖ ⥤ C ⥤ Type w where
+  obj X := FunctorToTypes.shrink (coyoneda.obj X)
+  map f := FunctorToTypes.shrinkMap (coyoneda.map f)
+
+/-- The type `(shrinkCoyoneda.obj X).obj Y` is equivalent to `X.unop ⟶ Y`. -/
+noncomputable def shrinkCoyonedaObjObjEquiv {X : Cᵒᵖ} {Y : C} :
+    ((shrinkCoyoneda.{w}.obj X).obj Y) ≃ (X.unop ⟶ Y) :=
+  (equivShrink _).symm
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm
+    {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : X.unop ⟶ Y) :
+    (shrinkCoyoneda.obj _).map g (shrinkCoyonedaObjObjEquiv.symm f) =
+      shrinkCoyonedaObjObjEquiv.symm (f ≫ g) := by
+  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+lemma shrinkCoyonedaObjObjEquiv_symm_comp {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) :
+    shrinkCoyonedaObjObjEquiv.symm (g ≫ f) =
+    (shrinkCoyoneda.obj _).map f (shrinkCoyonedaObjObjEquiv.symm g) :=
+  (shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm f g).symm
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm
+    {X X' : Cᵒᵖ} {Y : C} (f : X.unop ⟶ Y) (g : X ⟶ X') :
+    (shrinkCoyoneda.map g).app _ (shrinkCoyonedaObjObjEquiv.symm f) =
+      shrinkCoyonedaObjObjEquiv.symm (g.unop ≫ f) := by
+  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc]
+lemma shrinkCoyonedaObjObjEquiv_map_app
+    {X X' : Cᵒᵖ} {Y : C} (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') :
+    shrinkCoyonedaObjObjEquiv ((shrinkCoyoneda.map g).app Y f) =
+      g.unop ≫ shrinkCoyonedaObjObjEquiv f := by
+  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc]
+lemma shrinkCoyonedaObjObjEquiv_obj_map {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y')
+    (f : (shrinkCoyoneda.{w}.obj X).obj Y) :
+    shrinkCoyonedaObjObjEquiv ((shrinkCoyoneda.{w}.obj X).map g f) =
+      shrinkCoyonedaObjObjEquiv f ≫ g := by
+  simp [shrinkCoyonedaObjObjEquiv, shrinkCoyoneda]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The type of natural transformations `shrinkCoyoneda.{w}.obj X ⟶ P`
+with `X : Cᵒᵖ` and `P : C ⥤ Type w` is equivalent to `P.obj (op X)`. -/
+noncomputable def shrinkCoyonedaEquiv {X : Cᵒᵖ} {P : C ⥤ Type w} :
+    (shrinkCoyoneda.{w}.obj X ⟶ P) ≃ P.obj X.unop where
+  toFun τ := τ.app _ (equivShrink.{w} _ (𝟙 X.unop))
+  invFun x :=
+    { app Y := ↾fun f ↦ P.map ((equivShrink.{w} _).symm f) x
+      naturality Y Z g := by ext; simp [shrinkCoyoneda] }
+  left_inv τ := by
+    ext Y f
+    obtain ⟨f, rfl⟩ := (equivShrink _).surjective f
+    simpa [shrinkCoyoneda] using ((τ.naturality_apply f) (equivShrink _ (𝟙 X.unop))).symm
+  right_inv x := by simp
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma map_shrinkCoyonedaEquiv {X Y : Cᵒᵖ} {P : C ⥤ Type w} (f : shrinkCoyoneda.obj X ⟶ P)
+    (g : Y ⟶ X) : P.map g.unop (shrinkCoyonedaEquiv f) =
+      f.app Y.unop (shrinkCoyonedaObjObjEquiv.symm g.unop) := by
+  simp [shrinkCoyonedaObjObjEquiv, shrinkCoyonedaEquiv, shrinkCoyoneda,
+    ← comp_apply, ← NatTrans.naturality]
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyonedaEquiv_shrinkCoyoneda_map {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    shrinkCoyonedaEquiv (shrinkCoyoneda.{w}.map f) = shrinkCoyonedaObjObjEquiv.symm f.unop := by
+  simp [shrinkCoyonedaEquiv, shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+
+lemma shrinkCoyonedaEquiv_comp {X : Cᵒᵖ} {P Q : C ⥤ Type w} (α : shrinkCoyoneda.obj X ⟶ P)
+    (β : P ⟶ Q) :
+    shrinkCoyonedaEquiv (α ≫ β) = β.app _ (shrinkCoyonedaEquiv α) := by
+  simp [shrinkCoyonedaEquiv]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyonedaEquiv_naturality {X Y : Cᵒᵖ} {P : C ⥤ Type w}
+    (f : shrinkCoyoneda.obj X ⟶ P) (g : Y ⟶ X) :
+    P.map g.unop (shrinkCoyonedaEquiv f) = shrinkCoyonedaEquiv (shrinkCoyoneda.map g ≫ f) := by
+  simpa [shrinkCoyonedaEquiv, shrinkCoyoneda]
+    using (f.naturality_apply g.unop ((equivShrink _) (𝟙 _))).symm
+
+@[reassoc]
+lemma shrinkCoyonedaEquiv_symm_map {X Y : C} (f : X ⟶ Y) {P : C ⥤ Type w} (t : P.obj X) :
+    shrinkCoyonedaEquiv.symm (P.map f t) =
+      shrinkCoyoneda.map f.op ≫ shrinkCoyonedaEquiv.symm t :=
+  shrinkCoyonedaEquiv.injective (by
+    obtain ⟨t, rfl⟩ := shrinkCoyonedaEquiv.surjective t
+    rw [← shrinkCoyonedaEquiv_naturality]
+    simp)
+
+lemma shrinkCoyonedaEquiv_symm_app_shrinkCoyonedaObjObjEquiv_symm {X : Cᵒᵖ} {P : C ⥤ Type w}
+    (s : P.obj X.unop) {Y : Cᵒᵖ} (f : Y ⟶ X) :
+    (shrinkCoyonedaEquiv.symm s).app Y.unop (shrinkCoyonedaObjObjEquiv.symm f.unop) =
+      P.map f.unop s := by
+  obtain ⟨g, rfl⟩ := shrinkCoyonedaEquiv.surjective s
+  simp [map_shrinkCoyonedaEquiv]
+
+variable (C) in
+/-- The functor `shrinkCoyoneda : Cᵒᵖ ⥤ C ⥤ Type w` for a locally `w`-small category `C`
+is fully faithful. -/
+noncomputable def fullyFaithfulShrinkCoyoneda :
+    (shrinkCoyoneda.{w} (C := C)).FullyFaithful where
+  preimage f := (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv f)).op
+  map_preimage f := by
+    obtain ⟨f, rfl⟩ := shrinkCoyonedaEquiv.symm.surjective f
+    cat_disch
+  preimage_map f := by simp [shrinkCoyonedaEquiv_shrinkCoyoneda_map]
+
+instance : (shrinkCoyoneda.{w} (C := C)).Faithful := (fullyFaithfulShrinkCoyoneda C).faithful
+
+instance : (shrinkCoyoneda.{w} (C := C)).Full := (fullyFaithfulShrinkCoyoneda C).full
+
+set_option backward.defeqAttrib.useBackward true in
+/-- `shrinkCoyoneda` at the morphism universe level is `coyoneda`. -/
+@[simps! hom_app inv_app]
+noncomputable
+def shrinkCoyonedaIsoCoyoneda : shrinkCoyoneda.{v} ≅ coyoneda (C := C) :=
+  NatIso.ofComponents
+    (fun X ↦ NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso)
+      (by intros; ext; simp [shrinkCoyonedaObjObjEquiv_obj_map]))
+    (by intros; ext; simp [shrinkCoyonedaObjObjEquiv_map_app])
+
+set_option backward.defeqAttrib.useBackward true in
+/-- `shrinkCoyoneda` is compatible with `uliftFunctor`. -/
+noncomputable
+def shrinkCoyonedaUliftFunctorIso [LocallySmall.{max w w'} C] :
+    shrinkCoyoneda.{w} ⋙ (Functor.whiskeringRight Cᵒᵖ _ _).obj uliftFunctor.{w', w} ≅
+      shrinkCoyoneda :=
+  NatIso.ofComponents
+    (fun X ↦ FunctorToTypes.shrinkCompUliftFunctorIso.{w, v} (coyoneda.obj X))
+    fun _ ↦ by ext; simp [shrinkCoyoneda]
+
+/-- `uliftCoyoneda` identifies to `shrinkCoyoneda`. -/
+noncomputable def uliftYonedaIsoShrinkCoyoneda :
+    uliftCoyoneda.{w'} (C := C) ≅ shrinkCoyoneda.{max w' v} :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
+    (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) (fun f ↦ by
+      ext
+      exact (shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm _ _).symm)) (fun g ↦ by
+      ext
+      exact (shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm _ _).symm)
+
+set_option backward.defeqAttrib.useBackward true in
+/-- The functor `shrinkCoyoneda.{w}` followed by the evaluation
+at `Y : C` and `uliftFunctor.{v}` identifies to `yoneda.obj Y` followed
+by `uliftFunctor.{w}`. -/
+noncomputable def shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctor (Y : C) :
+    shrinkCoyoneda.{w} ⋙ (evaluation C _).obj Y ⋙ uliftFunctor.{v} ≅
+      yoneda.obj Y ⋙ uliftFunctor.{w} :=
+  NatIso.ofComponents (fun X ↦ (Equiv.ulift.trans
+    (shrinkCoyonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso) (fun f ↦ by
+      ext ⟨g⟩
+      obtain ⟨g, rfl⟩ := shrinkCoyonedaObjObjEquiv.symm.surjective g
+      simp [shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm])
+
+/-- `shrinkCoyoneda.obj X` is corepresented by `X`. -/
+@[simps]
+noncomputable
+def shrinkCoyonedaCorepresentableBy (X : Cᵒᵖ) :
+    (shrinkCoyoneda.{w}.obj X).CorepresentableBy X.unop where
+  homEquiv := shrinkCoyonedaObjObjEquiv.symm
+  homEquiv_comp f g := shrinkCoyonedaObjObjEquiv_symm_comp g f
+
+instance (X : Cᵒᵖ) : (shrinkCoyoneda.{w}.obj X).IsCorepresentable :=
+  (shrinkCoyonedaCorepresentableBy X).isCorepresentable
+
+end Coyoneda
+
 end CategoryTheory

From 2337494961e57381b1d7fb6dc50986bd97651ff6 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 29 Jun 2026 14:04:49 +0200
Subject: [PATCH 10/20] clean up `shrinkCoyoneda`-lemma

---
 Mathlib/CategoryTheory/ShrinkYoneda.lean    | 18 ++++++++++++------
 Mathlib/CategoryTheory/Sites/LocalSite.lean |  7 -------
 2 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/Mathlib/CategoryTheory/ShrinkYoneda.lean b/Mathlib/CategoryTheory/ShrinkYoneda.lean
index a8a8f73f64c307..ebb5c0d9d34f21 100644
--- a/Mathlib/CategoryTheory/ShrinkYoneda.lean
+++ b/Mathlib/CategoryTheory/ShrinkYoneda.lean
@@ -87,13 +87,16 @@ noncomputable def shrinkYonedaObjObjEquiv {X : C} {Y : Cᵒᵖ} :
     ((shrinkYoneda.{w}.obj X).obj Y) ≃ (Y.unop ⟶ X) :=
   (equivShrink _).symm
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
+lemma shrinkYoneda_obj_map {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : (shrinkYoneda.obj X).obj Y) :
+    (shrinkYoneda.obj _).map g f =
+      shrinkYonedaObjObjEquiv.symm (g.unop ≫ shrinkYonedaObjObjEquiv f) :=
+  rfl
+
 lemma shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm
     {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Y.unop ⟶ X) :
     (shrinkYoneda.obj _).map g (shrinkYonedaObjObjEquiv.symm f) =
       shrinkYonedaObjObjEquiv.symm (g.unop ≫ f) := by
-  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]
+  simp [shrinkYoneda_obj_map]
 
 lemma shrinkYonedaObjObjEquiv_symm_comp {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) :
     shrinkYonedaObjObjEquiv.symm (g ≫ f) =
@@ -271,13 +274,16 @@ noncomputable def shrinkCoyonedaObjObjEquiv {X : Cᵒᵖ} {Y : C} :
     ((shrinkCoyoneda.{w}.obj X).obj Y) ≃ (X.unop ⟶ Y) :=
   (equivShrink _).symm
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
+lemma shrinkCoyoneda_obj_map {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (shrinkCoyoneda.obj X).obj Y) :
+    (shrinkCoyoneda.obj _).map g f =
+      shrinkCoyonedaObjObjEquiv.symm (shrinkCoyonedaObjObjEquiv f ≫ g) :=
+  rfl
+
 lemma shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm
     {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : X.unop ⟶ Y) :
     (shrinkCoyoneda.obj _).map g (shrinkCoyonedaObjObjEquiv.symm f) =
       shrinkCoyonedaObjObjEquiv.symm (f ≫ g) := by
-  simp [shrinkCoyoneda, shrinkCoyonedaObjObjEquiv]
+  simp [shrinkCoyoneda_obj_map]
 
 lemma shrinkCoyonedaObjObjEquiv_symm_comp {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) :
     shrinkCoyonedaObjObjEquiv.symm (g ≫ f) =
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 87f2277d379380..88f4768d8ab6d4 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -74,13 +74,6 @@ noncomputable def IsLocalSite.point [LocallySmall.{w} C] [J.IsLocalSite] : Point
         rw [shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm]
         simp⟩
 
-lemma shrinkCoyoneda_obj_map [LocallySmall.{w} C]
-    {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (shrinkCoyoneda.obj X).obj Y) :
-    (shrinkCoyoneda.obj _).map g f =
-      shrinkCoyonedaObjObjEquiv.symm (shrinkCoyonedaObjObjEquiv f ≫ g) :=
-  rfl
-
-set_option backward.isDefEq.respectTransparency false in
 /-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `IsLocalSite.point J` is just `P` evaluated at
 the terminal object. -/
 noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]

From 5826a02749df2c6705aa541c32011bc9cb307e03 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Mon, 29 Jun 2026 16:32:45 +0200
Subject: [PATCH 11/20] clean up `IsColimit`-lemmas

---
 Mathlib/CategoryTheory/Limits/IsLimit.lean    | 44 +++++++++++++++++++
 .../Limits/Shapes/IsTerminal.lean             | 12 +++++
 Mathlib/CategoryTheory/Sites/LocalSite.lean   | 31 +------------
 3 files changed, 58 insertions(+), 29 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
index 57c4bedb521de0..5dcc66be7ed013 100644
--- a/Mathlib/CategoryTheory/Limits/IsLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean
@@ -183,6 +183,50 @@ theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q
     Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r :=
   P.uniq _ _ (by simp)
 
+set_option backward.isDefEq.respectTransparency false in
+@[to_dual (attr := reassoc (attr := simp)) coconePointUniqueUpToIso_inv_comp_map]
+lemma map_comp_conePointUniqueUpToIso {F G : J ⥤ C} (s : Cone F) {t t' : Cone G}
+    (ht : IsLimit t) (ht' : IsLimit t') (α : F ⟶ G) :
+    ht.map s α ≫ (ht.conePointUniqueUpToIso ht').hom = ht'.map s α := by
+  simp [map]
+
+set_option backward.isDefEq.respectTransparency false in
+@[to_dual map_comp_coconePointUniqueUpToIso_inv, reassoc (attr := simp)]
+lemma conePointUniqueUpToIso_comp_map {F G : J ⥤ C} {s' s : Cone F} {t : Cone G}
+    (hs' : IsLimit s') (hs : IsLimit s) (ht : IsLimit t) (α : F ⟶ G) :
+    (hs'.conePointUniqueUpToIso hs).hom ≫ ht.map s α = ht.map s' α :=
+  ht.uniq (((Cone.postcompose α).obj s')) _ fun i ↦ by simp
+
+@[to_dual coconePointUniqueUpToIso_inv_naturality, reassoc]
+lemma conePointUniqueUpToIso_naturality {F G : J ⥤ C}
+    {s s' : Cone F} {t t' : Cone G} (hs : IsLimit s) (hs' : IsLimit s') (ht : IsLimit t)
+    (ht' : IsLimit t') (α : F ⟶ G) :
+    ht.map s α ≫ (ht.conePointUniqueUpToIso ht').hom =
+      (hs.conePointUniqueUpToIso hs').hom ≫ ht'.map s' α := by
+  rw [map_comp_conePointUniqueUpToIso, conePointUniqueUpToIso_comp_map]
+
+set_option backward.isDefEq.respectTransparency false in
+@[to_dual (attr := reassoc (attr := simp)) coconePointUniqueUpToIso_comp_map]
+lemma map_comp_conePointUniqueUpToIso_inv {F G : J ⥤ C} (s : Cone F) {t t' : Cone G}
+    (ht : IsLimit t) (ht' : IsLimit t') (α : F ⟶ G) :
+    ht.map s α ≫ (ht'.conePointUniqueUpToIso ht).inv = ht'.map s α := by
+  simp [map]
+
+set_option backward.isDefEq.respectTransparency false in
+@[to_dual map_comp_coconePointUniqueUpToIso, reassoc (attr := simp)]
+lemma conePointUniqueUpToIso_inv_comp_map {F G : J ⥤ C} {s' s : Cone F} {t : Cone G}
+    (hs' : IsLimit s') (hs : IsLimit s) (ht : IsLimit t) (α : F ⟶ G) :
+    (hs.conePointUniqueUpToIso hs').inv ≫ ht.map s α = ht.map s' α :=
+  ht.uniq (((Cone.postcompose α).obj s')) _ fun i ↦ by simp
+
+@[to_dual coconePointUniqueUpToIso_naturality, reassoc]
+lemma conePointUniqueUpToIso_inv_naturality {F G : J ⥤ C}
+    {s s' : Cone F} {t t' : Cone G} (hs : IsLimit s) (hs' : IsLimit s') (ht : IsLimit t)
+    (ht' : IsLimit t') (α : F ⟶ G) :
+    (hs'.conePointUniqueUpToIso hs).inv ≫ ht'.map s' α =
+      ht.map s α ≫ (ht'.conePointUniqueUpToIso ht).inv := by
+  rw [map_comp_conePointUniqueUpToIso_inv, conePointUniqueUpToIso_inv_comp_map]
+
 /-- Transport evidence that a cone is a limit cone across an isomorphism of cones. -/
 @[to_dual
 /-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones. -/]
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
index f68d561c9176f3..eae91a19408828 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
@@ -359,6 +359,12 @@ def limitOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) :
     simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
     simp
 
+lemma IsLimit.limitOfDiagramInitial_map {F G : J ⥤ C} {X : J} (hX : IsInitial X) (α : F ⟶ G) :
+    (limitOfDiagramInitial hX G).map (coneOfDiagramInitial hX F) α = α.app X := by
+  simp only [IsLimit.map, limitOfDiagramInitial, Cone.postcompose_obj_π, NatTrans.comp_app,
+    coneOfDiagramInitial_π_app, IsInitial.to_self, Functor.map_id]
+  exact Category.id_comp _
+
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cone for `J`,
@@ -403,6 +409,12 @@ def colimitOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) :
   desc s := s.ι.app X
   uniq s m w := by simp [← w X]
 
+lemma IsColimit.colimitOfDiagramTerminal_map {F G : J ⥤ C} {X : J} (hX : IsTerminal X) (α : F ⟶ G) :
+    (colimitOfDiagramTerminal hX F).map (coconeOfDiagramTerminal hX G) α = α.app X := by
+  simp only [IsColimit.map, colimitOfDiagramTerminal, Cocone.precompose_obj_ι, NatTrans.comp_app,
+    coconeOfDiagramTerminal_ι_app, IsTerminal.from_self, Functor.map_id]
+  exact Category.comp_id _
+
 lemma IsColimit.isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c)
     (X : J) (hX : IsTerminal X) :
     IsIso (c.ι.app X) := by
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 88f4768d8ab6d4..ea846c715c792c 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -83,41 +83,14 @@ noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLo
     (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
       <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _)
 
-set_option backward.isDefEq.respectTransparency false in
-lemma IsColimit.map_comp_coconePointUniqueUpToIso {J : Type*} [Category* J] {F G : J ⥤ C}
-    {s : Cocone F} {t t' : Cocone G} (hs : IsColimit s) (ht : IsColimit t)
-    (ht' : IsColimit t') (α : F ⟶ G) :
-    hs.map t α ≫ (ht.coconePointUniqueUpToIso ht').hom = hs.map t' α :=
-  hs.uniq (((Cocone.precompose α).obj t')) _ fun i ↦ by simp
-
-set_option backward.isDefEq.respectTransparency false in
-lemma IsColimit.coconePointUniqueUpToIso_comp_map {J : Type*} [Category* J] {F G : J ⥤ C}
-    {s' s : Cocone F} (hs' : IsColimit s') (hs : IsColimit s) (t : Cocone G) (α : F ⟶ G) :
-    (hs'.coconePointUniqueUpToIso hs).hom ≫ hs.map t α = hs'.map t α :=
-  hs'.uniq (((Cocone.precompose α).obj t)) _ fun i ↦ by simp
-
-lemma IsColimit.coconePointUniqueUpToIso_naturality {J : Type*} [Category* J] {F G : J ⥤ C}
-    {s s' : Cocone F} {t t' : Cocone G} (hs : IsColimit s) (hs' : IsColimit s') (ht : IsColimit t)
-    (ht' : IsColimit t') (α : F ⟶ G) :
-    hs.map t α ≫ (ht.coconePointUniqueUpToIso ht').hom =
-      (hs.coconePointUniqueUpToIso hs').hom ≫ hs'.map t' α := by
-  rw [map_comp_coconePointUniqueUpToIso, coconePointUniqueUpToIso_comp_map]
-
-lemma IsColimit.colimitOfDiagramTerminal_map {J : Type*} [Category* J] {F G : J ⥤ C}
-    {X : J} (hX : IsTerminal X) (α : F ⟶ G) :
-    (colimitOfDiagramTerminal hX F).map (coconeOfDiagramTerminal hX G) α = α.app X := by
-  simp only [IsColimit.map, colimitOfDiagramTerminal, Cocone.precompose_obj_ι, NatTrans.comp_app,
-    coconeOfDiagramTerminal_ι_app, IsTerminal.from_self, Functor.map_id]
-  exact Category.comp_id _
-
 lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
     {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
     {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
     (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
       (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C)) := by
-  refine (IsColimit.coconePointUniqueUpToIso_naturality _
+  refine (IsColimit.coconePointUniqueUpToIso_naturality _ _
     (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
-      <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _) _ _
+      <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _) _
       (((CategoryOfElements.π (shrinkCoyoneda.{w}.obj (op (⊤_ C)))).op.whiskerLeft F))).trans ?_
   congr
   exact IsColimit.colimitOfDiagramTerminal_map _ _

From 03223a4b911c67bf596606553f1844d0e14953bd Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 14:27:21 +0200
Subject: [PATCH 12/20] fix

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index ea846c715c792c..cf512d3e42150c 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -77,14 +77,14 @@ noncomputable def IsLocalSite.point [LocallySmall.{w} C] [J.IsLocalSite] : Point
 /-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `IsLocalSite.point J` is just `P` evaluated at
 the terminal object. -/
 noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
-    {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : Cᵒᵖ ⥤ A) :
+    {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A] (P : Cᵒᵖ ⥤ A) :
     (IsLocalSite.point J).presheafFiber.obj P ≅ P.obj (op (⊤_ C)) :=
   (colimit.isColimit _).coconePointUniqueUpToIso
     (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
       <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _)
 
 lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
-    {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
     (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
       (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C)) := by
@@ -98,13 +98,13 @@ lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLoc
 /-- The presheaf fibre functor of `IsLocalSite.point J` is given by evaluation at the terminal
 object. -/
 noncomputable def IsLocalSite.pointPresheafFiberNatIso [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] :
+    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A] :
     ((IsLocalSite.point J).presheafFiber : _ ⥤ A) ≅ (evaluation _ _).obj (op (⊤_ C)) :=
   NatIso.ofComponents (pointPresheafFiberIso J) fun F ↦ pointPresheafFiberIso_naturality J F
 
 /-- The sheaf fibre functor of `IsLocalSite.point J` is the global sections functor. -/
 noncomputable def IsLocalSite.pointSheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     [HasWeakSheafify J A] : (IsLocalSite.point J).sheafFiber ≅ Γ J A :=
   ((sheafToPresheaf J A).isoWhiskerLeft (pointPresheafFiberNatIso J A)).trans
     (ΓNatIsoSheafSections J A terminalIsTerminal).symm
@@ -118,8 +118,7 @@ Note this takes in an extra universe parameter `w` that does not appear in the o
 `A ⥤ Sheaf J A` but is required for the construction; it should always be given explicitly when
 referring to this functor, as in e.g. `coconstantSheaf.{w} J A`. -/
 noncomputable def IsLocalSite.coconstantSheaf [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
-    [HasProducts.{w} A] : A ⥤ Sheaf J A :=
+    (A : Type u') [Category.{v', u'} A] [HasProducts.{w} A] : A ⥤ Sheaf J A :=
   (point.{w} J).skyscraperSheafFunctor
 
 /-- In particular, this construction works for sheaves of types. -/
@@ -127,7 +126,7 @@ noncomputable example [J.IsLocalSite] : Type max v w ⥤ Sheaf J (Type (max v w)
   IsLocalSite.coconstantSheaf.{max v w} J (Type max v w)
 
 variable [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A]
+    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     [HasProducts.{w} A] [HasWeakSheafify J A]
 
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
@@ -145,7 +144,7 @@ with colimits and products of size `v` is a left adjoint. See `IsLocalSite.ΓIsL
 version for `w`-locally small sites that can't be registered as an instance because of the extra
 universe parameter `w`. -/
 instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A]
+    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
     [HasProducts.{v} A] [HasWeakSheafify J A] : (Γ J A).IsLeftAdjoint :=
   IsLocalSite.Γ_isLeftAdjoint.{v} J A
 
@@ -204,7 +203,7 @@ with colimits and products of size `v` is full. See `IsLocalSite.constantSheaf_f
 version for `w`-locally small sites that can't be registered as an instance because of the extra
 universe parameter `w`. -/
 instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A]
+    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
     [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Full :=
   IsLocalSite.constantSheaf_full.{v} J A
 
@@ -213,7 +212,7 @@ with colimits and products of size `v` is faithful. See `IsLocalSite.constantShe
 version for `w`-locally small sites that can't be registered as an instance because of the extra
 universe parameter `w`. -/
 instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [Limits.HasColimitsOfSize.{v, v, v', u'} A]
+    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
     [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Faithful :=
   IsLocalSite.constantSheaf_faithful.{v} J A
 

From a63b660865d1a73d5411edbbbfa16abdfffbc34d Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 30 Jun 2026 15:15:51 +0200
Subject: [PATCH 13/20] some suggestions during in person review

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index cf512d3e42150c..1f09f57ea84732 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -83,17 +83,24 @@ noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLo
     (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
       <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _)
 
+set_option backward.isDefEq.respectTransparency false in
+set_option backward.defeqAttrib.useBackward true in
+@[reassoc (attr := simp)]
+lemma IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom [LocallySmall.{w} C] [J.IsLocalSite]
+    {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
+    {P : Cᵒᵖ ⥤ A} (X : C) (x : (point J).fiber.obj X) :
+    (Point.toPresheafFiber (point J) _ x _) ≫ (pointPresheafFiberIso J P).hom =
+      P.map (.op <| shrinkCoyonedaObjObjEquiv x) := by
+  simp [Point.toPresheafFiber, pointPresheafFiberIso]
+  rfl
+
+@[reassoc (attr := simp)]
 lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
     {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
     (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
       (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C)) := by
-  refine (IsColimit.coconePointUniqueUpToIso_naturality _ _
-    (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
-      <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _) _
-      (((CategoryOfElements.π (shrinkCoyoneda.{w}.obj (op (⊤_ C)))).op.whiskerLeft F))).trans ?_
-  congr
-  exact IsColimit.colimitOfDiagramTerminal_map _ _
+  cat_disch
 
 /-- The presheaf fibre functor of `IsLocalSite.point J` is given by evaluation at the terminal
 object. -/

From 64cd55339fe99112cbc7dc872321514e1784df77 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 15:19:12 +0200
Subject: [PATCH 14/20] update module docstring

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 1f09f57ea84732..1c1d94425fce0c 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -12,7 +12,8 @@ public import Mathlib.CategoryTheory.Sites.Point.Skyscraper
 
 /-!
 # Local sites
-A site (C,J) is called local if it has a terminal object whose only covering sieve is trivial -
+
+A site is called local if it has a terminal object whose only covering sieve is trivial -
 this makes it possible to define coconstant sheaves on it, giving its sheaf topos the structure
 of a local topos. This makes them an important stepping stone to cohesive sites.
 
@@ -23,11 +24,12 @@ has a fully faithful right adjoint), and a subcanonical site is local if and onl
 sheaves of types is.
 
 ## Main definitions / results
-* `J.IsLocalSite`: typeclass stating that (C,J) is a local site.
+
+* `J.IsLocalSite`: typeclass stating that `J` makes the category it is defined on into a local site.
 * `IsLocalSite.point J`: the canonical point of any local site, whose fibre functor is given by
   the coyoneda embedding of the terminal object and extends to the global sections functors on
   presheaves and sheaves.
-* `coconstantSheaf J A`: the coconstant sheaf functor `A ⥤ Sheaf J A` for any local site (C,J) and
+* `coconstantSheaf J A`: the coconstant sheaf functor `A ⥤ Sheaf J A` for any local site and
   sufficiently nice target category `A`, defined as the skyscraper sheaf functor of the canonical
   point.
 * `ΓCoconstantSheafAdj J A`: the adjunction between the global sections functor `Γ J A` and
@@ -35,8 +37,11 @@ sheaves of types is.
 * `fullyFaithfulCoconstantSheaf`: `coconstantSheaf` is fully faithful.
 * `fullyFaithfulConstantSheaf`: on local sites, the constant sheaf functor is fully faithful.
 
-All together this shows that for local sites `Sheaf J (Type max u v w)` forms a local topos, but
-since we don't yet have local topoi this can't be stated yet.
+## TODO
+
+* Define local topoi and prove that sheaves on any local site form a local topos
+* Show that a subcanonical site is local if and only if its global sections functor has a fully
+  faithful right adjoint
 -/
 
 universe w u v u' v'

From 91c4382232c65c4fe0f3c6402c270fd4938647c2 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 15:21:53 +0200
Subject: [PATCH 15/20] namespace everything

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 34 ++++++++++++---------
 1 file changed, 19 insertions(+), 15 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 1c1d94425fce0c..42ff6c5d699d3e 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -59,8 +59,10 @@ class GrothendieckTopology.IsLocalSite extends HasTerminal C where
   /-- The only covering sieve of the terminal object is the trivial sieve. -/
   eq_top_of_mem : ∀ S ∈ J (⊤_ C), S = ⊤
 
+namespace GrothendieckTopology.IsLocalSite
+
 /-- On a local site, every covering sieve contains every morphism from the terminal object. -/
-lemma IsLocalSite.from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
+lemma from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
     (hS : S ∈ J X) : S.arrows f :=
   (S.mem_iff_pullback_eq_top f).2 <| IsLocalSite.eq_top_of_mem _ <| J.pullback_stable f hS
 
@@ -70,7 +72,7 @@ instance {C : Type u} [Category.{v} C] [HasTerminal C] : (trivial C).IsLocalSite
 
 /-- Every local site has a canonical point, given as a fibre functor by the coyoneda embedding of
 the terminal object `⊤_ C`. -/
-noncomputable def IsLocalSite.point [LocallySmall.{w} C] [J.IsLocalSite] : Point.{w} J where
+noncomputable def point [LocallySmall.{w} C] [J.IsLocalSite] : Point.{w} J where
   fiber := shrinkCoyoneda.obj (op (⊤_ C))
   jointly_surjective := fun R hR x ↦
     ⟨(⊤_ C), shrinkCoyonedaObjObjEquiv x,
@@ -81,7 +83,7 @@ noncomputable def IsLocalSite.point [LocallySmall.{w} C] [J.IsLocalSite] : Point
 
 /-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `IsLocalSite.point J` is just `P` evaluated at
 the terminal object. -/
-noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
+noncomputable def pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
     {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A] (P : Cᵒᵖ ⥤ A) :
     (IsLocalSite.point J).presheafFiber.obj P ≅ P.obj (op (⊤_ C)) :=
   (colimit.isColimit _).coconePointUniqueUpToIso
@@ -91,7 +93,7 @@ noncomputable def IsLocalSite.pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLo
 set_option backward.isDefEq.respectTransparency false in
 set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
-lemma IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom [LocallySmall.{w} C] [J.IsLocalSite]
+lemma toPresheafFiber_pointPresheafFiberIso_hom [LocallySmall.{w} C] [J.IsLocalSite]
     {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     {P : Cᵒᵖ ⥤ A} (X : C) (x : (point J).fiber.obj X) :
     (Point.toPresheafFiber (point J) _ x _) ≫ (pointPresheafFiberIso J P).hom =
@@ -100,7 +102,7 @@ lemma IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom [LocallySmall.{w} C]
   rfl
 
 @[reassoc (attr := simp)]
-lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
+lemma pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
     {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
     (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
@@ -109,13 +111,13 @@ lemma IsLocalSite.pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLoc
 
 /-- The presheaf fibre functor of `IsLocalSite.point J` is given by evaluation at the terminal
 object. -/
-noncomputable def IsLocalSite.pointPresheafFiberNatIso [LocallySmall.{w} C] [J.IsLocalSite]
+noncomputable def pointPresheafFiberNatIso [LocallySmall.{w} C] [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A] :
     ((IsLocalSite.point J).presheafFiber : _ ⥤ A) ≅ (evaluation _ _).obj (op (⊤_ C)) :=
   NatIso.ofComponents (pointPresheafFiberIso J) fun F ↦ pointPresheafFiberIso_naturality J F
 
 /-- The sheaf fibre functor of `IsLocalSite.point J` is the global sections functor. -/
-noncomputable def IsLocalSite.pointSheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
+noncomputable def pointSheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     [HasWeakSheafify J A] : (IsLocalSite.point J).sheafFiber ≅ Γ J A :=
   ((sheafToPresheaf J A).isoWhiskerLeft (pointPresheafFiberNatIso J A)).trans
@@ -129,26 +131,26 @@ indexed by the points `⊤_ C ⟶ Y` of `Y`.
 Note this takes in an extra universe parameter `w` that does not appear in the output type
 `A ⥤ Sheaf J A` but is required for the construction; it should always be given explicitly when
 referring to this functor, as in e.g. `coconstantSheaf.{w} J A`. -/
-noncomputable def IsLocalSite.coconstantSheaf [LocallySmall.{w} C] [J.IsLocalSite]
+noncomputable def coconstantSheaf [LocallySmall.{w} C] [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [HasProducts.{w} A] : A ⥤ Sheaf J A :=
   (point.{w} J).skyscraperSheafFunctor
 
 /-- In particular, this construction works for sheaves of types. -/
 noncomputable example [J.IsLocalSite] : Type max v w ⥤ Sheaf J (Type (max v w)) :=
-  IsLocalSite.coconstantSheaf.{max v w} J (Type max v w)
+  coconstantSheaf.{max v w} J (Type max v w)
 
 variable [LocallySmall.{w} C] [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
     [HasProducts.{w} A] [HasWeakSheafify J A]
 
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
-noncomputable def IsLocalSite.ΓCoconstantSheafAdj : Γ J A ⊣ coconstantSheaf.{w} J A :=
+noncomputable def ΓCoconstantSheafAdj : Γ J A ⊣ coconstantSheaf.{w} J A :=
   (point.{w} J).skyscraperSheafAdjunction.ofNatIsoLeft (pointSheafFiberIso J A)
 
 /-- On any locally `w`-small local site, the global sections functor to any category with colimits
 and products of size `w` is a left adulljoint. A variant of this without the universe parameter `w`
 is registered as an instance. -/
-lemma IsLocalSite.Γ_isLeftAdjoint : (Γ J A).IsLeftAdjoint :=
+lemma Γ_isLeftAdjoint : (Γ J A).IsLeftAdjoint :=
   ⟨IsLocalSite.coconstantSheaf.{w} J A, ⟨IsLocalSite.ΓCoconstantSheafAdj J A⟩⟩
 
 /-- On any local site with morphism types in `Type v`, the global sections functor to any category
@@ -188,26 +190,26 @@ instance : (IsLocalSite.coconstantSheaf.{w} J A).Faithful :=
   (fullyFaithfulCoconstantSheaf J A).faithful
 
 /-- The adjoint triple `constantSheaf J A ⊣ Γ J A ⊣ coconstantSheaf J A` on any local site. -/
-noncomputable abbrev IsLocalSite.constantΓCoconstantTriple :
+noncomputable abbrev constantΓCoconstantTriple :
     Adjunction.Triple (constantSheaf J A) (Γ J A) (coconstantSheaf.{w} J A) where
   adj₁ := constantSheafΓAdj J A
   adj₂ := ΓCoconstantSheafAdj J A
 
 /-- On local sites, the constant sheaf functor is fully faithful. -/
 noncomputable def fullyFaithfulConstantSheaf : (constantSheaf J A).FullyFaithful :=
-  (IsLocalSite.constantΓCoconstantTriple J A).fullyFaithfulEquiv.symm <|
+  (constantΓCoconstantTriple J A).fullyFaithfulEquiv.symm <|
     fullyFaithfulCoconstantSheaf.{w} J A
 
 /-- On any locally `w`-small local site, the constant sheaf functor from any category with colimits
 and products of size `w` is full. A variant of this without the universe parameter `w`
 is registered as an instance. -/
-lemma IsLocalSite.constantSheaf_full : (constantSheaf J A).Full :=
+lemma constantSheaf_full : (constantSheaf J A).Full :=
   (fullyFaithfulConstantSheaf.{w} J A).full
 
 /-- On any locally `w`-small local site, the constant sheaf functor from any category with colimits
 and products of size `w` is faithful. A variant of this without the universe parameter `w`
 is registered as an instance. -/
-lemma IsLocalSite.constantSheaf_faithful : (constantSheaf J A).Faithful :=
+lemma constantSheaf_faithful : (constantSheaf J A).Faithful :=
   (fullyFaithfulConstantSheaf.{w} J A).faithful
 
 /-- On any local site with morphism types in `Type v`, the constant sheaf functor from any category
@@ -228,4 +230,6 @@ instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSi
     [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Faithful :=
   IsLocalSite.constantSheaf_faithful.{v} J A
 
+end GrothendieckTopology.IsLocalSite
+
 end CategoryTheory

From 7a325355b674d4c430d13581580143e42ce079f1 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 16:09:27 +0200
Subject: [PATCH 16/20] more changes

---
 .../Limits/Shapes/Products.lean               |  28 +++-
 Mathlib/CategoryTheory/Sites/LocalSite.lean   | 129 ++++++++----------
 2 files changed, 80 insertions(+), 77 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
index 3bb17a7c11f5f5..142ea4c3b30a84 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -826,10 +826,21 @@ instance (priority := 100) hasProduct_unique [Nonempty β] [Subsingleton β] (f
   let ⟨_⟩ := nonempty_unique β; HasLimit.mk (limitConeOfUnique f)
 
 /-- A product over an index type with exactly one term is just the object over that term. -/
-@[simps!]
 def productUniqueIso [Unique β] (f : β → C) : ∏ᶜ f ≅ f default :=
   IsLimit.conePointUniqueUpToIso (limit.isLimit _) (limitConeOfUnique f).isLimit
 
+@[simp]
+lemma productUniqueIso_hom [Unique β] (f : β → C) : (productUniqueIso f).hom = Pi.π f default :=
+  rfl
+
+@[simp]
+lemma productUniqueIso_inv_π [Unique β] (f : β → C) (b : β) :
+    (productUniqueIso f).inv ≫ Pi.π f b = eqToHom (congrArg _ <| Subsingleton.allEq _ _) := by
+  obtain rfl := Subsingleton.allEq b default
+  simp [Iso.inv_comp_eq]
+
+@[deprecated (since := "2026-06-30")] alias productUniqueIso_inv := productUniqueIso_inv_π
+
 set_option backward.defeqAttrib.useBackward true in
 /-- Any isomorphism is the projection from a single object product. -/
 def Fan.isLimitMkOfUnique {X Y : C} (e : X ≅ Y) (J : Type*) [Unique J] :
@@ -863,10 +874,23 @@ instance (priority := 100) hasCoproduct_unique [Nonempty β] [Subsingleton β] (
   let ⟨_⟩ := nonempty_unique β; HasColimit.mk (colimitCoconeOfUnique f)
 
 /-- A coproduct over an index type with exactly one term is just the object over that term. -/
-@[simps!]
 def coproductUniqueIso [Unique β] (f : β → C) : ∐ f ≅ f default :=
   IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (colimitCoconeOfUnique f).isColimit
 
+@[simp]
+lemma coproductUniqueIso_inv [Unique β] (f : β → C) :
+    (coproductUniqueIso f).inv = Sigma.ι f default :=
+  rfl
+
+@[simp]
+lemma ι_coproductUniqueIso_hom [Unique β] (f : β → C) (b : β) :
+    Sigma.ι f b ≫ (coproductUniqueIso f).hom = eqToHom (congrArg _ <| Subsingleton.allEq _ _) := by
+  obtain rfl := Subsingleton.allEq b default
+  symm
+  simp [← Iso.comp_inv_eq]
+
+@[deprecated (since := "2026-06-30")] alias coproductUniqueIso_hom := ι_coproductUniqueIso_hom
+
 set_option backward.defeqAttrib.useBackward true in
 /-- Any isomorphism is the projection from a single object product. -/
 def Cofan.isColimitMkOfUnique {X Y : C} (e : X ≅ Y) (J : Type*) [Unique J] :
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 42ff6c5d699d3e..86a05cfb14b878 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -64,84 +64,77 @@ namespace GrothendieckTopology.IsLocalSite
 /-- On a local site, every covering sieve contains every morphism from the terminal object. -/
 lemma from_terminal_mem_of_mem [J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : Sieve X}
     (hS : S ∈ J X) : S.arrows f :=
-  (S.mem_iff_pullback_eq_top f).2 <| IsLocalSite.eq_top_of_mem _ <| J.pullback_stable f hS
+  (S.mem_iff_pullback_eq_top f).mpr <| eq_top_of_mem _ <| J.pullback_stable f hS
 
 /-- Every category with a terminal object becomes a local site with the trivial topology. -/
 instance {C : Type u} [Category.{v} C] [HasTerminal C] : (trivial C).IsLocalSite where
-  eq_top_of_mem _ := trivial_covering.1
+  eq_top_of_mem _ := trivial_covering.mp
 
 /-- Every local site has a canonical point, given as a fibre functor by the coyoneda embedding of
 the terminal object `⊤_ C`. -/
 noncomputable def point [LocallySmall.{w} C] [J.IsLocalSite] : Point.{w} J where
   fiber := shrinkCoyoneda.obj (op (⊤_ C))
-  jointly_surjective := fun R hR x ↦
+  jointly_surjective R hR x :=
     ⟨(⊤_ C), shrinkCoyonedaObjObjEquiv x,
-      (IsLocalSite.from_terminal_mem_of_mem J (shrinkCoyonedaObjObjEquiv x) hR),
+      (from_terminal_mem_of_mem J (shrinkCoyonedaObjObjEquiv x) hR),
           shrinkCoyonedaObjObjEquiv.symm (𝟙 _), by
         rw [shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm]
         simp⟩
 
-/-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `IsLocalSite.point J` is just `P` evaluated at
+variable [LocallySmall.{w} C] [J.IsLocalSite] (A : Type u') [Category.{v', u'} A]
+
+/-- The right adjoint to the global sections functor that exists over any local site. This is
+implemented as the skyscraper functor associated to `point.{w} J`, but can be thought of
+as taking any object `X : A` to the sheaf that sends each `Y : C` to the product over copies of `A`
+indexed by the points `⊤_ C ⟶ Y` of `Y`.
+
+Note this takes in an extra universe parameter `w` that does not appear in the output type
+`A ⥤ Sheaf J A` but is required for the construction; it should always be given explicitly when
+referring to this functor, as in e.g. `coconstantSheaf.{w} J A`. -/
+noncomputable def coconstantSheaf [HasProducts.{w} A] : A ⥤ Sheaf J A :=
+  (point.{w} J).skyscraperSheafFunctor
+
+variable [HasColimitsOfSize.{w, w, v', u'} A]
+
+variable {A} in
+/-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `point J` is just `P` evaluated at
 the terminal object. -/
-noncomputable def pointPresheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
-    {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A] (P : Cᵒᵖ ⥤ A) :
-    (IsLocalSite.point J).presheafFiber.obj P ≅ P.obj (op (⊤_ C)) :=
+noncomputable def pointPresheafFiberIso (P : Cᵒᵖ ⥤ A) :
+    (point J).presheafFiber.obj P ≅ P.obj (op (⊤_ C)) :=
   (colimit.isColimit _).coconePointUniqueUpToIso
     (colimitOfDiagramTerminal (Functor.Elements.isInitialOfCorepresentableBy
       <| shrinkCoyonedaCorepresentableBy <| op (⊤_ C)).op _)
 
+variable {A} in
 set_option backward.isDefEq.respectTransparency false in
 set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
-lemma toPresheafFiber_pointPresheafFiberIso_hom [LocallySmall.{w} C] [J.IsLocalSite]
-    {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
-    {P : Cᵒᵖ ⥤ A} (X : C) (x : (point J).fiber.obj X) :
-    (Point.toPresheafFiber (point J) _ x _) ≫ (pointPresheafFiberIso J P).hom =
+lemma toPresheafFiber_pointPresheafFiberIso_hom {P : Cᵒᵖ ⥤ A} (X : C) (x : (point J).fiber.obj X) :
+    (point J).toPresheafFiber  _ x _ ≫ (pointPresheafFiberIso J P).hom =
       P.map (.op <| shrinkCoyonedaObjObjEquiv x) := by
   simp [Point.toPresheafFiber, pointPresheafFiberIso]
   rfl
 
+variable {A} in
 @[reassoc (attr := simp)]
-lemma pointPresheafFiberIso_naturality [LocallySmall.{w} C] [J.IsLocalSite]
-    {A : Type u'} [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
-    {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
+lemma pointPresheafFiberIso_naturality {P P' : Cᵒᵖ ⥤ A} (F : P ⟶ P') :
     (point J).presheafFiber.map F ≫ (pointPresheafFiberIso J P').hom =
       (pointPresheafFiberIso J P).hom ≫ F.app (op (⊤_ C)) := by
   cat_disch
 
-/-- The presheaf fibre functor of `IsLocalSite.point J` is given by evaluation at the terminal
+/-- The presheaf fibre functor of `point J` is given by evaluation at the terminal
 object. -/
-noncomputable def pointPresheafFiberNatIso [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A] :
-    ((IsLocalSite.point J).presheafFiber : _ ⥤ A) ≅ (evaluation _ _).obj (op (⊤_ C)) :=
+noncomputable def pointPresheafFiberNatIso :
+    ((point J).presheafFiber : _ ⥤ A) ≅ (evaluation _ _).obj (op (⊤_ C)) :=
   NatIso.ofComponents (pointPresheafFiberIso J) fun F ↦ pointPresheafFiberIso_naturality J F
 
-/-- The sheaf fibre functor of `IsLocalSite.point J` is the global sections functor. -/
-noncomputable def pointSheafFiberIso [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
-    [HasWeakSheafify J A] : (IsLocalSite.point J).sheafFiber ≅ Γ J A :=
+/-- The sheaf fibre functor of `point J` is the global sections functor. -/
+noncomputable def pointSheafFiberIso
+    [HasWeakSheafify J A] : (point J).sheafFiber ≅ Γ J A :=
   ((sheafToPresheaf J A).isoWhiskerLeft (pointPresheafFiberNatIso J A)).trans
     (ΓNatIsoSheafSections J A terminalIsTerminal).symm
 
-/-- The right adjoint to the global sections functor that exists over any local site. This is
-implemented as the skyscraper functor associated to `IsLocalSite.point.{w} J`, but can be thought of
-as taking any object `X : A` to the sheaf that sends each `Y : C` to the product over copies of `A`
-indexed by the points `⊤_ C ⟶ Y` of `Y`.
-
-Note this takes in an extra universe parameter `w` that does not appear in the output type
-`A ⥤ Sheaf J A` but is required for the construction; it should always be given explicitly when
-referring to this functor, as in e.g. `coconstantSheaf.{w} J A`. -/
-noncomputable def coconstantSheaf [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [HasProducts.{w} A] : A ⥤ Sheaf J A :=
-  (point.{w} J).skyscraperSheafFunctor
-
-/-- In particular, this construction works for sheaves of types. -/
-noncomputable example [J.IsLocalSite] : Type max v w ⥤ Sheaf J (Type (max v w)) :=
-  coconstantSheaf.{max v w} J (Type max v w)
-
-variable [LocallySmall.{w} C] [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{w, w, v', u'} A]
-    [HasProducts.{w} A] [HasWeakSheafify J A]
+variable [HasProducts.{w} A] [HasWeakSheafify J A]
 
 /-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor. -/
 noncomputable def ΓCoconstantSheafAdj : Γ J A ⊣ coconstantSheaf.{w} J A :=
@@ -151,28 +144,26 @@ noncomputable def ΓCoconstantSheafAdj : Γ J A ⊣ coconstantSheaf.{w} J A :=
 and products of size `w` is a left adulljoint. A variant of this without the universe parameter `w`
 is registered as an instance. -/
 lemma Γ_isLeftAdjoint : (Γ J A).IsLeftAdjoint :=
-  ⟨IsLocalSite.coconstantSheaf.{w} J A, ⟨IsLocalSite.ΓCoconstantSheafAdj J A⟩⟩
+  ⟨coconstantSheaf.{w} J A, ⟨ΓCoconstantSheafAdj J A⟩⟩
 
 /-- On any local site with morphism types in `Type v`, the global sections functor to any category
-with colimits and products of size `v` is a left adjoint. See `IsLocalSite.ΓIsLeftAdjoint` for a
+with colimits and products of size `v` is a left adjoint. See `ΓIsLeftAdjoint` for a
 version for `w`-locally small sites that can't be registered as an instance because of the extra
 universe parameter `w`. -/
-instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
-    (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
+instance (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
     [HasProducts.{v} A] [HasWeakSheafify J A] : (Γ J A).IsLeftAdjoint :=
-  IsLocalSite.Γ_isLeftAdjoint.{v} J A
+  Γ_isLeftAdjoint.{v} J A
 
-instance : (IsLocalSite.coconstantSheaf.{w} J A).IsRightAdjoint :=
-  ⟨Γ J A, ⟨IsLocalSite.ΓCoconstantSheafAdj J A⟩⟩
+instance : (coconstantSheaf.{w} J A).IsRightAdjoint :=
+  ⟨Γ J A, ⟨ΓCoconstantSheafAdj J A⟩⟩
 
 /-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
-noncomputable def coconstantSheafΓNatIsoId :
-    IsLocalSite.coconstantSheaf.{w} J A ⋙ Γ J A ≅ 𝟭 A := by
+noncomputable def coconstantSheafΓNatIsoId : coconstantSheaf.{w} J A ⋙ Γ J A ≅ 𝟭 A := by
   refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
   refine NatIso.ofComponents (fun X ↦ @productUniqueIso
-    (((IsLocalSite.point J).fiber.obj (⊤_ C))) _ _ (equivShrink (⊤_ C ⟶ ⊤_ C)).symm.unique _) ?_
+    (((point J).fiber.obj (⊤_ C))) _ _ (equivShrink.{w} (⊤_ C ⟶ ⊤_ C)).symm.unique _) ?_
   intro X Y f
-  simp only [IsLocalSite.coconstantSheaf, Point.skyscraperSheafFunctor,
+  simp only [coconstantSheaf, Point.skyscraperSheafFunctor,
     Point.skyscraperPresheafFunctor, Functor.comp, Functor.id_obj, Functor.flip_obj_map,
     ObjectProperty.ι_obj, ObjectProperty.ι_map, Functor.flip_map_app, piFunctor_map_app,
     productUniqueIso_hom, Functor.id_map]
@@ -180,13 +171,13 @@ noncomputable def coconstantSheafΓNatIsoId :
 
 /-- `coconstantSheaf` is fully faithful. -/
 noncomputable def fullyFaithfulCoconstantSheaf :
-    (IsLocalSite.coconstantSheaf.{w} J A).FullyFaithful :=
-  (IsLocalSite.ΓCoconstantSheafAdj J A).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId J A)
+    (coconstantSheaf.{w} J A).FullyFaithful :=
+  (ΓCoconstantSheafAdj J A).fullyFaithfulROfCompIsoId (coconstantSheafΓNatIsoId J A)
 
-instance : (IsLocalSite.coconstantSheaf.{w} J A).Full :=
+instance : (coconstantSheaf.{w} J A).Full :=
   (fullyFaithfulCoconstantSheaf J A).full
 
-instance : (IsLocalSite.coconstantSheaf.{w} J A).Faithful :=
+instance : (coconstantSheaf.{w} J A).Faithful :=
   (fullyFaithfulCoconstantSheaf J A).faithful
 
 /-- The adjoint triple `constantSheaf J A ⊣ Γ J A ⊣ coconstantSheaf J A` on any local site. -/
@@ -200,35 +191,23 @@ noncomputable def fullyFaithfulConstantSheaf : (constantSheaf J A).FullyFaithful
   (constantΓCoconstantTriple J A).fullyFaithfulEquiv.symm <|
     fullyFaithfulCoconstantSheaf.{w} J A
 
-/-- On any locally `w`-small local site, the constant sheaf functor from any category with colimits
-and products of size `w` is full. A variant of this without the universe parameter `w`
-is registered as an instance. -/
-lemma constantSheaf_full : (constantSheaf J A).Full :=
+lemma full_constantSheaf : (constantSheaf J A).Full :=
   (fullyFaithfulConstantSheaf.{w} J A).full
 
-/-- On any locally `w`-small local site, the constant sheaf functor from any category with colimits
-and products of size `w` is faithful. A variant of this without the universe parameter `w`
-is registered as an instance. -/
-lemma constantSheaf_faithful : (constantSheaf J A).Faithful :=
+lemma faithful_constantSheaf : (constantSheaf J A).Faithful :=
   (fullyFaithfulConstantSheaf.{w} J A).faithful
 
-/-- On any local site with morphism types in `Type v`, the constant sheaf functor from any category
-with colimits and products of size `v` is full. See `IsLocalSite.constantSheaf_full` for a
-version for `w`-locally small sites that can't be registered as an instance because of the extra
-universe parameter `w`. -/
+/-- See `IsLocalSite.full_constantSheaf` for a version for `w`-locally small sites. -/
 instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
     [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Full :=
-  IsLocalSite.constantSheaf_full.{v} J A
+  full_constantSheaf.{v} J A
 
-/-- On any local site with morphism types in `Type v`, the constant sheaf functor from any category
-with colimits and products of size `v` is faithful. See `IsLocalSite.constantSheaf_faithful` for a
-version for `w`-locally small sites that can't be registered as an instance because of the extra
-universe parameter `w`. -/
+/-- See `IsLocalSite.faithful_constantSheaf` for a version for `w`-locally small sites. -/
 instance {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) [J.IsLocalSite]
     (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A]
     [HasProducts.{v} A] [HasWeakSheafify J A] : (constantSheaf J A).Faithful :=
-  IsLocalSite.constantSheaf_faithful.{v} J A
+  faithful_constantSheaf.{v} J A
 
 end GrothendieckTopology.IsLocalSite
 

From ff64def562f1012acebd034391ac116f2757f6cc Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 16:27:18 +0200
Subject: [PATCH 17/20] =?UTF-8?q?clean=20up=20`coconstantSheaf=CE=93NatIso?=
 =?UTF-8?q?Id`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 86a05cfb14b878..77de07a0a7ca6d 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -157,17 +157,14 @@ instance (A : Type u') [Category.{v', u'} A] [HasColimitsOfSize.{v, v, v', u'} A
 instance : (coconstantSheaf.{w} J A).IsRightAdjoint :=
   ⟨Γ J A, ⟨ΓCoconstantSheafAdj J A⟩⟩
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
-noncomputable def coconstantSheafΓNatIsoId : coconstantSheaf.{w} J A ⋙ Γ J A ≅ 𝟭 A := by
-  refine (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)).trans ?_
-  refine NatIso.ofComponents (fun X ↦ @productUniqueIso
-    (((point J).fiber.obj (⊤_ C))) _ _ (equivShrink.{w} (⊤_ C ⟶ ⊤_ C)).symm.unique _) ?_
-  intro X Y f
-  simp only [coconstantSheaf, Point.skyscraperSheafFunctor,
-    Point.skyscraperPresheafFunctor, Functor.comp, Functor.id_obj, Functor.flip_obj_map,
-    ObjectProperty.ι_obj, ObjectProperty.ι_map, Functor.flip_map_app, piFunctor_map_app,
-    productUniqueIso_hom, Functor.id_map]
-  exact Pi.map_π _ _
+noncomputable def coconstantSheafΓNatIsoId :
+    IsLocalSite.coconstantSheaf.{w} J A ⋙ Γ J A ≅ 𝟭 A :=
+  letI : Unique (unop ((IsLocalSite.point J).fiber.op.obj (op (⊤_ C)))) :=
+    (equivShrink (⊤_ C ⟶ ⊤_ C)).symm.unique
+  (Functor.isoWhiskerLeft _ (ΓNatIsoSheafSections J _ terminalIsTerminal)) ≪≫
+    NatIso.ofComponents (fun X ↦ productUniqueIso _) (by simp [IsLocalSite.coconstantSheaf])
 
 /-- `coconstantSheaf` is fully faithful. -/
 noncomputable def fullyFaithfulCoconstantSheaf :

From fd28bce42f090c7bb25eebe39a705fc6703d5cab Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 16:34:53 +0200
Subject: [PATCH 18/20] clean up old lemmas

---
 Mathlib/CategoryTheory/Limits/IsLimit.lean    | 44 -------------------
 .../Limits/Shapes/IsTerminal.lean             | 12 -----
 2 files changed, 56 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
index 5dcc66be7ed013..57c4bedb521de0 100644
--- a/Mathlib/CategoryTheory/Limits/IsLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean
@@ -183,50 +183,6 @@ theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q
     Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r :=
   P.uniq _ _ (by simp)
 
-set_option backward.isDefEq.respectTransparency false in
-@[to_dual (attr := reassoc (attr := simp)) coconePointUniqueUpToIso_inv_comp_map]
-lemma map_comp_conePointUniqueUpToIso {F G : J ⥤ C} (s : Cone F) {t t' : Cone G}
-    (ht : IsLimit t) (ht' : IsLimit t') (α : F ⟶ G) :
-    ht.map s α ≫ (ht.conePointUniqueUpToIso ht').hom = ht'.map s α := by
-  simp [map]
-
-set_option backward.isDefEq.respectTransparency false in
-@[to_dual map_comp_coconePointUniqueUpToIso_inv, reassoc (attr := simp)]
-lemma conePointUniqueUpToIso_comp_map {F G : J ⥤ C} {s' s : Cone F} {t : Cone G}
-    (hs' : IsLimit s') (hs : IsLimit s) (ht : IsLimit t) (α : F ⟶ G) :
-    (hs'.conePointUniqueUpToIso hs).hom ≫ ht.map s α = ht.map s' α :=
-  ht.uniq (((Cone.postcompose α).obj s')) _ fun i ↦ by simp
-
-@[to_dual coconePointUniqueUpToIso_inv_naturality, reassoc]
-lemma conePointUniqueUpToIso_naturality {F G : J ⥤ C}
-    {s s' : Cone F} {t t' : Cone G} (hs : IsLimit s) (hs' : IsLimit s') (ht : IsLimit t)
-    (ht' : IsLimit t') (α : F ⟶ G) :
-    ht.map s α ≫ (ht.conePointUniqueUpToIso ht').hom =
-      (hs.conePointUniqueUpToIso hs').hom ≫ ht'.map s' α := by
-  rw [map_comp_conePointUniqueUpToIso, conePointUniqueUpToIso_comp_map]
-
-set_option backward.isDefEq.respectTransparency false in
-@[to_dual (attr := reassoc (attr := simp)) coconePointUniqueUpToIso_comp_map]
-lemma map_comp_conePointUniqueUpToIso_inv {F G : J ⥤ C} (s : Cone F) {t t' : Cone G}
-    (ht : IsLimit t) (ht' : IsLimit t') (α : F ⟶ G) :
-    ht.map s α ≫ (ht'.conePointUniqueUpToIso ht).inv = ht'.map s α := by
-  simp [map]
-
-set_option backward.isDefEq.respectTransparency false in
-@[to_dual map_comp_coconePointUniqueUpToIso, reassoc (attr := simp)]
-lemma conePointUniqueUpToIso_inv_comp_map {F G : J ⥤ C} {s' s : Cone F} {t : Cone G}
-    (hs' : IsLimit s') (hs : IsLimit s) (ht : IsLimit t) (α : F ⟶ G) :
-    (hs.conePointUniqueUpToIso hs').inv ≫ ht.map s α = ht.map s' α :=
-  ht.uniq (((Cone.postcompose α).obj s')) _ fun i ↦ by simp
-
-@[to_dual coconePointUniqueUpToIso_naturality, reassoc]
-lemma conePointUniqueUpToIso_inv_naturality {F G : J ⥤ C}
-    {s s' : Cone F} {t t' : Cone G} (hs : IsLimit s) (hs' : IsLimit s') (ht : IsLimit t)
-    (ht' : IsLimit t') (α : F ⟶ G) :
-    (hs'.conePointUniqueUpToIso hs).inv ≫ ht'.map s' α =
-      ht.map s α ≫ (ht'.conePointUniqueUpToIso ht).inv := by
-  rw [map_comp_conePointUniqueUpToIso_inv, conePointUniqueUpToIso_inv_comp_map]
-
 /-- Transport evidence that a cone is a limit cone across an isomorphism of cones. -/
 @[to_dual
 /-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones. -/]
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
index eae91a19408828..f68d561c9176f3 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
@@ -359,12 +359,6 @@ def limitOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) :
     simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
     simp
 
-lemma IsLimit.limitOfDiagramInitial_map {F G : J ⥤ C} {X : J} (hX : IsInitial X) (α : F ⟶ G) :
-    (limitOfDiagramInitial hX G).map (coneOfDiagramInitial hX F) α = α.app X := by
-  simp only [IsLimit.map, limitOfDiagramInitial, Cone.postcompose_obj_π, NatTrans.comp_app,
-    coneOfDiagramInitial_π_app, IsInitial.to_self, Functor.map_id]
-  exact Category.id_comp _
-
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cone for `J`,
@@ -409,12 +403,6 @@ def colimitOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) :
   desc s := s.ι.app X
   uniq s m w := by simp [← w X]
 
-lemma IsColimit.colimitOfDiagramTerminal_map {F G : J ⥤ C} {X : J} (hX : IsTerminal X) (α : F ⟶ G) :
-    (colimitOfDiagramTerminal hX F).map (coconeOfDiagramTerminal hX G) α = α.app X := by
-  simp only [IsColimit.map, colimitOfDiagramTerminal, Cocone.precompose_obj_ι, NatTrans.comp_app,
-    coconeOfDiagramTerminal_ι_app, IsTerminal.from_self, Functor.map_id]
-  exact Category.comp_id _
-
 lemma IsColimit.isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c)
     (X : J) (hX : IsTerminal X) :
     IsIso (c.ι.app X) := by

From 3266c2f17da23a1ee745b3080dabde998d070753 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <b.eltschig@protonmail.com>
Date: Tue, 30 Jun 2026 16:37:14 +0200
Subject: [PATCH 19/20] update module docstring

---
 Mathlib/CategoryTheory/Sites/LocalSite.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 77de07a0a7ca6d..4b937df0ef1b55 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -15,9 +15,7 @@ public import Mathlib.CategoryTheory.Sites.Point.Skyscraper
 
 A site is called local if it has a terminal object whose only covering sieve is trivial -
 this makes it possible to define coconstant sheaves on it, giving its sheaf topos the structure
-of a local topos. This makes them an important stepping stone to cohesive sites.
-
-See https://ncatlab.org/nlab/show/local+site.
+of a local topos. This is one of the conditions of cohesive sites.
 
 Sheaves of types on any local site form a local topos (i.e. a topos whose global sections functor
 has a fully faithful right adjoint), and a subcanonical site is local if and only if its topos of
@@ -37,6 +35,10 @@ sheaves of types is.
 * `fullyFaithfulCoconstantSheaf`: `coconstantSheaf` is fully faithful.
 * `fullyFaithfulConstantSheaf`: on local sites, the constant sheaf functor is fully faithful.
 
+## References
+
+* https://ncatlab.org/nlab/show/local+site
+
 ## TODO
 
 * Define local topoi and prove that sheaves on any local site form a local topos

From 335f3bdcb4d4a3dfb61b5bf8f67cdbf53dbaea98 Mon Sep 17 00:00:00 2001
From: Ben Eltschig <43812953+peabrainiac@users.noreply.github.com>
Date: Tue, 30 Jun 2026 16:40:14 +0200
Subject: [PATCH 20/20] Apply suggestions from code review

Co-authored-by: Christian Merten <christian@merten.dev>
---
 Mathlib/CategoryTheory/Limits/Shapes/Products.lean | 4 ++--
 Mathlib/CategoryTheory/Sites/LocalSite.lean        | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
index 142ea4c3b30a84..e7c71c245c1e4f 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -833,7 +833,7 @@ def productUniqueIso [Unique β] (f : β → C) : ∏ᶜ f ≅ f default :=
 lemma productUniqueIso_hom [Unique β] (f : β → C) : (productUniqueIso f).hom = Pi.π f default :=
   rfl
 
-@[simp]
+@[reassoc (attr := simp)]
 lemma productUniqueIso_inv_π [Unique β] (f : β → C) (b : β) :
     (productUniqueIso f).inv ≫ Pi.π f b = eqToHom (congrArg _ <| Subsingleton.allEq _ _) := by
   obtain rfl := Subsingleton.allEq b default
@@ -882,7 +882,7 @@ lemma coproductUniqueIso_inv [Unique β] (f : β → C) :
     (coproductUniqueIso f).inv = Sigma.ι f default :=
   rfl
 
-@[simp]
+@[reassoc (attr := simp)]
 lemma ι_coproductUniqueIso_hom [Unique β] (f : β → C) (b : β) :
     Sigma.ι f b ≫ (coproductUniqueIso f).hom = eqToHom (congrArg _ <| Subsingleton.allEq _ _) := by
   obtain rfl := Subsingleton.allEq b default
diff --git a/Mathlib/CategoryTheory/Sites/LocalSite.lean b/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 4b937df0ef1b55..bf2e55fe591272 100644
--- a/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -19,7 +19,7 @@ of a local topos. This is one of the conditions of cohesive sites.
 
 Sheaves of types on any local site form a local topos (i.e. a topos whose global sections functor
 has a fully faithful right adjoint), and a subcanonical site is local if and only if its topos of
-sheaves of types is.
+sheaves of types is (see TODOs).
 
 ## Main definitions / results