feat(CategoryTheory/MarkovCategory): Add Markov category (leanprover-community#29925)

This PR introduces Markov categories, extending copy-discard categories with natural discard to model categorical probability theory.

This PR builds on leanprover-community#29939 and leanprover-community#29919 and was split up from leanprover-community#29657.

## Main additions

### 1. Markov categories (`MarkovCategory`)

Extends `CopyDiscardCategory` where discard is natural: `f ≫ ε[Y] = ε[X]` for all morphisms `f : X → Y`. This forces a probabilistic interpretation where morphisms preserve normalization (probability measures sum to 1).

## Mathematical significance

Markov categories capture probability theory categorically:
- Morphisms: Stochastic processes/Markov kernels
- Copy: Perfect correlation (both outputs always equal)
- Discard: Marginalization (integrating out variables)
- Natural discard: Preservation of total probability

The same framework handles finite probability (stochastic matrices), measure-theoretic 
probability (Markov kernels), and quantum probability (completely positive maps).

## Design decisions

- Terminal unit follows from axioms. We prove `unit_terminal` and `unit_isTerminal` rather than assuming them

## Implementation notes

- Built on top of `CopyDiscardCategory` per suggestion [#mathlib4 > Markov categories PR @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Markov.20categories.20PR/near/539656225)
- Includes both computational (`unit_terminal`) and categorical (`unit_isTerminal`) characterizations of the terminal object

## References

Cho & Jacobs (2019) and Fritz (2020)

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

- [x] depends on: leanprover-community#29939

Author: jcreinhold

Mathlib.lean

@@ -2561,6 +2561,7 @@ import Mathlib.CategoryTheory.Localization.StructuredArrow
 import Mathlib.CategoryTheory.Localization.Triangulated
 import Mathlib.CategoryTheory.Localization.Trifunctor
 import Mathlib.CategoryTheory.LocallyDirected
+import Mathlib.CategoryTheory.MarkovCategory.Basic
 import Mathlib.CategoryTheory.Monad.Adjunction
 import Mathlib.CategoryTheory.Monad.Algebra
 import Mathlib.CategoryTheory.Monad.Basic

Mathlib/CategoryTheory/MarkovCategory/Basic.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2025 Jacob Reinhold. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacob Reinhold
+-/
+import Mathlib.CategoryTheory.CopyDiscardCategory.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
+
+/-!
+# Markov Categories
+
+Copy-discard categories where deletion is natural for all morphisms.
+
+## Main definitions
+
+* `MarkovCategory` - Copy-discard category with natural deletion
+
+## Main results
+
+* `eq_discard` - Any morphism to the unit equals discard
+* `isTerminalUnit` - The monoidal unit is terminal
+
+## Implementation notes
+
+Natural discard forces probabilistic interpretation: morphisms preserve normalization. The unit
+being terminal follows from naturality of discard.
+
+The key property `discard_natural : f ≫ ε[Y] = ε[X]` means discard "erases" any preceding
+morphism, a distinguishing feature of Markov categories in categorical probability.
+
+## References
+
+* [Cho and Jacobs, *Disintegration and Bayesian inversion via string diagrams*][cho_jacobs_2019]
+* [Fritz, *A synthetic approach to Markov kernels, conditional independence
+  and theorems on sufficient statistics*][fritz2020]
+
+## Tags
+
+Markov category, probability, categorical probability
+-/
+
+universe v u
+
+namespace CategoryTheory
+
+open MonoidalCategory CopyDiscardCategory ComonObj Limits
+
+variable {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C]
+
+/-- Copy-discard category where discard is natural. -/
+class MarkovCategory (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C]
+    extends CopyDiscardCategory C where
+  /-- Process then discard equals discard directly. -/
+  discard_natural {X Y : C} (f : X ⟶ Y) : f ≫ ε[Y] = ε[X]
+
+namespace MarkovCategory
+
+variable [MarkovCategory C]
+
+attribute [reassoc (attr := simp)] discard_natural
+
+/-- Any morphism to the unit equals discard. -/
+theorem eq_discard (X : C) (f : X ⟶ 𝟙_ C) : f = ε[X] := by
+  rw [← Category.comp_id f, ← discard_unit, discard_natural]
+
+/-- The monoidal unit is a terminal object. -/
+def isTerminalUnit : IsTerminal (𝟙_ C) :=
+  IsTerminal.ofUniqueHom _ eq_discard
+
+/-- There is a unique morphism to the unit (it is terminal). -/
+instance (X : C) : Subsingleton (X ⟶ 𝟙_ C) where
+  allEq := isTerminalUnit.hom_ext
+
+end MarkovCategory
+
+end CategoryTheory

MathlibTest/CategoryTheory/MarkovCategory.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2025 Jacob Reinhold. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacob Reinhold
+-/
+import Mathlib.CategoryTheory.MarkovCategory.Basic
+import Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian
+import Mathlib.CategoryTheory.Monoidal.Types.Basic
+
+/-!
+# Tests for Markov Categories
+
+Tests for the Markov category and copy-discard category implementation.
+
+## Tests included
+
+* Instance inference for cartesian and copy-discard structures
+* Comonoid laws: comultiplication and counit axioms
+* Markov category laws: naturality of discard and terminal unit
+* Simp automation for comonoid and discard naturality
+
+-/
+
+universe u
+
+open CategoryTheory MonoidalCategory CopyDiscardCategory ComonObj IsCommComonObj
+
+section BasicTests
+
+/-- CartesianMonoidalCategory instance exists for Type* -/
+example : CartesianMonoidalCategory (Type u) := inferInstance
+
+/-- CopyDiscardCategory instance for Type* via cartesian structure -/
+example : CopyDiscardCategory (Type u) := CartesianCopyDiscard.ofCartesianMonoidalCategory
+
+end BasicTests
+
+section ComonoidLaws
+
+variable {C : Type u} [Category.{u} C] [MonoidalCategory.{u} C] [CopyDiscardCategory C]
+
+/-- Comultiplication is commutative -/
+example (X : C) : Δ[X] ≫ (β_ X X).hom = Δ[X] := comul_comm X
+
+/-- Left counit law: copy then discard left component recovers object -/
+example (X : C) : Δ[X] ≫ (ε[X] ▷ X) = (λ_ X).inv := ComonObj.counit_comul X
+
+/-- Right counit law: copy then discard right component recovers object -/
+example (X : C) : Δ[X] ≫ (X ◁ ε[X]) = (ρ_ X).inv := ComonObj.comul_counit X
+
+/-- Comultiplication is coassociative -/
+example (X : C) :
+    Δ[X] ≫ (X ◁ Δ[X]) = Δ[X] ≫ (Δ[X] ▷ X) ≫ (α_ X X X).hom :=
+  ComonObj.comul_assoc X
+
+end ComonoidLaws
+
+section MarkovLaws
+
+variable {C : Type u} [Category.{u} C] [MonoidalCategory.{u} C] [MarkovCategory C]
+
+/-- Discard is natural -/
+example {X Y : C} (f : X ⟶ Y) : f ≫ ε[Y] = ε[X] := MarkovCategory.discard_natural f
+
+/-- Any morphism to the unit equals discard -/
+example (X : C) (f : X ⟶ 𝟙_ C) : f = ε[X] := MarkovCategory.eq_discard X f
+
+/-- The monoidal unit is terminal -/
+example : Limits.IsTerminal (𝟙_ C : C) := MarkovCategory.isTerminalUnit
+
+/-- Any two morphisms to the unit are equal (subsingleton instance) -/
+example (X : C) (f g : X ⟶ 𝟙_ C) : f = g := Subsingleton.elim f g
+
+end MarkovLaws
+
+section SimpLemmas
+
+variable {C : Type u} [Category.{u} C] [MonoidalCategory C] [CopyDiscardCategory C]
+
+/-- Simp automation for counit laws -/
+example (X : C) : Δ[X] ≫ (ε[X] ▷ X) = (λ_ X).inv := by simp
+
+/-- Simp automation for comultiplication commutativity -/
+example (X : C) : Δ[X] ≫ (β_ X X).hom = Δ[X] := by simp
+
+end SimpLemmas
+
+section MarkovSimpLemmas
+
+variable {C : Type u} [Category.{u} C] [MonoidalCategory.{u} C] [MarkovCategory C]
+
+/-- Simp automation for naturality of discard -/
+example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g ≫ ε[Z] = f ≫ ε[Y] := by simp
+
+end MarkovSimpLemmas