Name for a definition about Probability.Kernel

Stream: mathlib4

[Lorenzo Luccioli]

What should we name the following kernels, defined in #15466?

/-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for
 a given `b : β`. -/
 noncomputable def fst' (κ : Kernel (α × β) γ) (b : β) : Kernel α γ :=
   comap κ (fun a ↦ (a, b)) (measurable_id.prod_mk measurable_const)

/-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for
 a given `a : α`. -/
 noncomputable def snd' (κ : Kernel (α × β) γ) (a : α) : Kernel β γ :=
   comap κ (fun b ↦ (a, b)) (measurable_const.prod_mk measurable_id)

The names Kernel.fst and Kernel.snd are already used for the cases where the codomain is a product space, while here we have a product in the domain.

An idea from @Yury G. Kudryashov is to take inspiration from Function.Embedding.sectl or MonoidHom.inl.

Any other suggestions?

[Daniel Weber]

Perhaps left and right?

[Yaël Dillies]

sectl would rather be the name of docs#ProbabilityTheory.Kernel.fst, right?

[Yaël Dillies]

I think the current Kernel.fst and Kernel.snd are misnamed

[Lorenzo Luccioli]

Yaël Dillies ha scritto:

I think the current Kernel.fst and Kernel.snd are misnamed

I think the way those names are intended is that Kernel.fst and Kernel.snd correspond to taking the first and second marginals of the measures produced by the kernel.

[Lorenzo Luccioli]

Would mk_left and mk_right be suitable to this situation?

[Lorenzo Luccioli]

Yaël Dillies ha scritto:

sectl would rather be the name of docs#ProbabilityTheory.Kernel.fst, right?

To me sectl seems closer to fst' than to fst, because it needs an element of the second space to be fixed in order to only consider the variable from the first space, while fst does not need one.