feat(MarkovCategory/Positive): Define PositiveCategory

[gaetanserre]

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

For some additional context, please see #37851.

References

• Section 11 of A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics, Fritz, 2020
• Section 3 of A category-theoretic proof of the ergodic decomposition theorem, Moss and Perrone, 2023

---

[github-actions]

PR summary 896cc56a39

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.MarkovCategory.Positive (new file)	473

---

Declarations diff

+ PositiveCategory
+ instance {X Y : C} {e : X ≅ Y} : Deterministic e.hom
+ instance {e : X ≅ Y} : Deterministic (e.hom ≫ e.inv)
+ instance {e : X ≅ Y} : Deterministic (e.inv ≫ e.hom)

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).