feat(MarkovCategory/Positive): Define PositiveCategory (leanprover-community#38212)

Define `PositiviveCategory`: a specific kind of Markov category deeply related to determinism of isomorphisms.

For some additional context, please see leanprover-community#37851.

### References
- Section 11 of [A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics, Fritz, 2020](https://arxiv.org/abs/1908.07021)
- Section 3 of [A category-theoretic proof of the ergodic decomposition theorem, Moss and Perrone, 2023](https://arxiv.org/abs/2207.07353)

Author: gaetanserre

Mathlib.lean

@@ -2974,6 +2974,7 @@ public import Mathlib.CategoryTheory.LocallyCartesianClosed.Over
 public import Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
 public import Mathlib.CategoryTheory.LocallyDirected
 public import Mathlib.CategoryTheory.MarkovCategory.Basic
+public import Mathlib.CategoryTheory.MarkovCategory.Positive
 public import Mathlib.CategoryTheory.Monad.Adjunction
 public import Mathlib.CategoryTheory.Monad.Algebra
 public import Mathlib.CategoryTheory.Monad.Basic

Mathlib/CategoryTheory/MarkovCategory/Positive.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import Mathlib.CategoryTheory.MarkovCategory.Basic
+public import Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
+
+/-!
+# Positive Categories
+
+Markov categories where deletion is natural for all morphisms.
+
+## Main definitions
+
+* `PositiveCategory`: Markov category where copy is natural given deterministic composition of
+  morphisms.
+
+## Main results
+
+* `copy_comp_natural` - Given morphisms `f : X ⟶ Y` and `g : Y ⟶ Z`, if their composition is
+  deterministic, then process `f`, copy and then process `g` equals copy and process `f` and `g`
+  independently.
+
+* All isomorphisms in a positive Markov category are deterministic.
+
+## Implementation notes
+
+The key property `copy_comp_natural : f ≫ Δ ≫ (g ⊗ₘ 𝟙 Y) = Δ ≫ (f ≫ g ⊗ₘ f)`, given
+`Deterministic (f ≫ g)`, means that after processing `f`, copying and then processing `g` is the
+same as copying and processing `f` and `g` independently. The probabilistic interpretation is that
+given a deterministic process that has a stochastic intermediate result, the same distribution over
+both results can be obtained by computing the intermediate result independently of the
+deterministic process.
+
+## References
+
+* [Fritz, *A synthetic approach to Markov kernels, conditional independence
+  and theorems on sufficient statistics*, Def. 11.22][fritz2020]
+* [Moss and Perrone, *A category-theoretic proof of the ergodic decomposition theorem*][moss2023]
+-/
+
+@[expose] public section
+
+universe v u
+
+namespace CategoryTheory
+
+open MonoidalCategory CopyDiscardCategory ComonObj
+
+/-- Markov category where copy is natural given deterministic composition of morphisms. -/
+class PositiveCategory (C : Type u) [Category.{v} C] [MonoidalCategory C] extends
+    MarkovCategory C where
+  /-- Given morphisms `f : X ⟶ Y` and `g : Y ⟶ Z`, if their composition is deterministic, then
+  process `f`, copy and then process `g` equals copy and process `f` and `g` independently. -/
+  copy_comp_natural {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : Deterministic (f ≫ g)] :
+      f ≫ Δ ≫ (g ⊗ₘ 𝟙 Y) = Δ ≫ (f ≫ g ⊗ₘ f)
+
+variable {C : Type u} [Category.{v} C] [MonoidalCategory C]
+
+namespace PositiveCategory
+
+variable [PositiveCategory C]
+
+instance {X Y : C} (f : X ⟶ Y) [IsIso f] : Deterministic f where
+  hom_comul := by
+    calc
+    _ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) := by
+      cat_disch
+    _ = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) := by
+      simp
+    _ = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) := by
+      rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
+      simp
+    _ = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y) := by
+      simp
+    _ = Δ ≫ ((𝟙 X ≫ f) ⊗ₘ (f ≫ 𝟙 Y)) := by
+      rw [MonoidalCategory.tensorHom_comp_tensorHom]
+    _ = Δ ≫ (f ⊗ₘ f) := by cat_disch
+
+end PositiveCategory
+
+end CategoryTheory

docs/references.bib

@@ -4073,6 +4073,18 @@ @Article{         moss-2020
   url           = {https://doi.org/10.1007/s40062-019-00247-y}
 }
 
+@Article{         moss2023,
+  title         = {A category-theoretic proof of the ergodic decomposition
+                  theorem},
+  author        = {Moss, Sean and Perrone, Paolo},
+  journal       = {Ergodic Theory and Dynamical Systems},
+  volume        = {43},
+  number        = {12},
+  pages         = {4166--4192},
+  year          = {2023},
+  publisher     = {Cambridge University Press}
+}
+
 @Article{         MR0236876,
   title         = {A new proof that metric spaces are paracompact},
   author        = {Mary Ellen Rudin},