feat(Category/Kernel): SFinKer morphisms are deterministic

[gaetanserre]

Add several Deterministic instances for SFinKer and Stoch associators, unitors, braiding, counit, and comul morphisms.

---

[github-actions]

PR summary b6c608e112

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Probability.Kernel.Category.SFinKer	1672	1673	+1 (+0.06%)
Mathlib.Probability.Kernel.Category.Stoch	1692	1693	+1 (+0.06%)

Import changes for all files

Files	Import difference
Mathlib.Probability.Kernel.Category.SFinKer Mathlib.Probability.Kernel.Category.Stoch	1

---

Declarations diff

+ deterministic_Deterministic
+ id_map_Deterministic
+ instance : Deterministic (λ_ X ).hom
+ instance : Deterministic (λ_ X).hom
+ instance : Deterministic (ρ_ X ).hom
+ instance : Deterministic (ρ_ X).hom
++ instance : Deterministic (Δ[X])
++ instance : Deterministic (α_ X Y Z).hom
++ instance : Deterministic (β_ X Y).hom
++ instance : Deterministic (ε[X])

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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[joelriou]

Are all isomorphisms deterministic? Or if e is an isomorphism, is it true that e.inv is deterministic if e.hom is? In any case, I would think we would like to know that not only (α_ X Y Z).hom is a deterministic, but also (α_ X Y Z).inv, and similarly for the unitors.

[gaetanserre]

Or if e is an isomorphism, is it true that e.inv is deterministic if e.hom is?

Indeed, thanks to instIsComonHomInvOfHom, the instances for .inv are automatically inferred.

[gaetanserre]

awaiting-author