[Merged by Bors] - feat(Kernel/Category): Stoch is a Markov category

[gaetanserre]

• Define SFinKer, the category of measurable spaces and s-finite kernels. Show that it is a copy-discard category.

• Define Stoch, the category of measurable spaces and Markov kernels as a WideSubcategory of SFinKer. Show that it is a Markov category. It uses new typeclasses for MorphismProperty that are stables under specific morphisms of the original category.

• Add some useful lemmas about parallel product of kernels.

---

[github-actions]

PR summary 6e77ee2fdb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.Widesubcategory (new file)	487
Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory (new file)	488
Mathlib.Probability.Kernel.Category.SFinKer (new file)	1673
Mathlib.Probability.Kernel.Category.Stoch (new file)	1693

---

Declarations diff

+ Hom
+ InducedWideCategory.Hom
+ IsMonoidalStable
+ IsStableUnderAssociator
+ IsStableUnderBraiding
+ IsStableUnderComonoid
+ IsStableUnderUnitor
+ SFinKer
+ Stoch
+ StochHom
+ WideSubcategory.hom_ext
+ hom_ext
+ id_parallelComp_comp_parallelComp_id
+ id_parallelComp_id
+ instance : CoeSort SFinKer Type*
+ instance : CopyDiscardCategory SFinKer.{u}
+ instance : LargeCategory SFinKer
+ instance : MarkovCategory Stoch.{u}
+ instance : MonoidalCategory SFinKer.{u}
+ instance : StochHom.IsStableUnderBraiding
+ instance : SymmetricCategory SFinKer.{u}
+ instance [BraidedCategory C] [P.IsStableUnderBraiding] (c : WideSubcategory P) [ComonObj c.obj]
+ instance [BraidedCategory C] [P.IsStableUnderBraiding] :
+ instance [CopyDiscardCategory C] [P.IsStableUnderBraiding] [∀ c, P.IsStableUnderComonoid c] :
+ instance [P.IsMonoidalStable] (c : WideSubcategory P) [ComonObj c.obj]
+ instance [P.IsMonoidalStable] : MonoidalCategory (WideSubcategory P)
+ instance [P.IsMonoidalStable] : MonoidalCategoryStruct (WideSubcategory P)
+ instance [SymmetricCategory C] [P.IsStableUnderBraiding] :
+ instance {X : SFinKer} : ComonObj X
+ instance {X Y : SFinKer} {κ : Hom X Y} : IsSFiniteKernel κ.hom := κ.property
+ instance {X Y : Stoch} (κ : X ⟶ Y) : IsMarkovKernel κ.hom.hom := κ.2
+ instance {X} : StochHom.IsStableUnderComonoid X
+ isoMk
+ tensorμ_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).

[joelriou]

This should also be reviewed by some expert in probability theory:

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joelriou.

---

issue_comment, wf_run

[RemyDegenne]

Thanks!
bors r+

[mathlib-bors]

Canceled.

[RemyDegenne]

bors d+

[mathlib-bors]

✌️ gaetanserre can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[gaetanserre]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step