feat(CategoryTheory/Adhesive): slices of adhesive categories are adhesive (leanprover-community#36644)

contributions:
- Adhesive (Over B) instance — slices of adhesive categories are adhesive.

Found it as Proposition 8(ii) of Adhesive Categories, Lack & Sobociński (2004) while researching for a project. Needed the proof so perhaps others could rely on it too. The proof applies adhesive_of_preserves_and_reflects_isomorphism to Over.forget B, which creates all colimits and creates connected limits.

AI tools used. Claude Opus 4.6 + GitHub Copilot scaffolding

Co-authored-by: Denes Papai <denes.papai@gmail.com>

Author: gdies

Mathlib.lean

@@ -2389,6 +2389,7 @@ public import Mathlib.CategoryTheory.Action.Limits
 public import Mathlib.CategoryTheory.Action.Monoidal
 public import Mathlib.CategoryTheory.Adhesive
 public import Mathlib.CategoryTheory.Adhesive.Basic
+public import Mathlib.CategoryTheory.Adhesive.Over
 public import Mathlib.CategoryTheory.Adhesive.Subobject
 public import Mathlib.CategoryTheory.Adjunction.Additive
 public import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Mathlib/CategoryTheory/Adhesive/Over.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2026 Dénes Pápai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dénes Pápai
+-/
+module
+
+public import Mathlib.CategoryTheory.Adhesive.Basic
+public import Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
+
+/-! # Adhesive structure on slice categories
+
+The slice category `Over B` inherits the property of being adhesive from the
+base category.
+
+## TODO
+- The dual result for `Under B`.
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Limits
+
+variable {C : Type*} [Category* C]
+
+/-- Slices of adhesive categories are adhesive. See [adhesive2004], Proposition 8 (ii). -/
+instance adhesive_over [Adhesive C] [HasPullbacks C] [HasPushouts C] (B : C) :
+    Adhesive (Over B) :=
+  adhesive_of_preserves_and_reflects_isomorphism (Over.forget B)
+
+end CategoryTheory