feat (Probability.Kernel): Add definitions and API for Kernel.fst' and snd'

[LorenzoLuccioli]

Define a Kernel α γ and a Kernel β γ from a Kernel (α × β) γ by taking the comap of fun a ↦ (a, b) and fun b ↦ (a, b) respectively.

• Add definitions of Kernel.fst' and Kernel.snd'.
• Add some API lemmas: fst'_apply, fst'_zero, comap_fst', fst'_prodMkLeft, fst'_prodMkRight and the equivalent lemmas for snd'.
• Add instances for IsMarkovKernel, IsFiniteKernel, IsSFiniteKernel and NeZero.
• Add fst'_swapRight and snd'_swapRight.
• Add compProd_apply_eq_compProd_snd'.

---

[github-actions]

PR summary 61c817e548

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_snd'
+ comap_fst'
+ comap_snd'
+ fst'
+ fst'_apply
+ fst'_prodMkLeft
+ fst'_prodMkRight
+ fst'_swapRight
+ fst'_zero
+ instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (fst' κ b)] :
+ instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (snd' κ b)] :
+ instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((fst' κ b) a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((snd' κ a) b) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (snd' κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (snd' κ a) := by
+ instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (snd' κ a) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (fst' κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (fst' κ b) := by
+ instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (fst' κ b) := by
+ snd'
+ snd'_apply
+ snd'_prodMkLeft
+ snd'_prodMkRight
+ snd'_swapRight
+ snd'_zero

You can run this locally as follows

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

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

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

[LorenzoLuccioli]

The names are Kernel.fst' and Kernel.snd', since Kernel.fst and Kernel.snd are already taken for the case where the codomain is a product space. Suggestions for a better name are welcome.

[urkud]

About names: there are Function.Embedding.sectl and MonoidHom.inl. Probably, the former is closer to this case. Also, please ask on Zulip for other suggestions.

[YaelDillies]

Could you rename that to

Suggested change

	noncomputable def fst' (κ : Kernel (α × β) γ) (b : β) : Kernel α γ :=
	noncomputable def domFst (κ : Kernel (α × β) γ) (b : β) : Kernel α γ :=

? Then Kernel.fst can be renamed to Kernel.codFst