Coercion for linear maps to submodules

Stream: mathlib4

[Oliver Butterley]

Informally in mathematics we often see a linear map into a Submodule as a linear map on the entire space. Would it make sense that this was an automatic coercion in mathlib?

import Mathlib
variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E}

variable (f : E →L[𝕜] K)
-- #check (f : E →L[𝕜] E) -- error
#check K.subtypeL.comp f -- `E →L[𝕜] E`

Particular motivation is when working with K.orthogonalProjection, the projector onto K.

[Kenny Lau]

I don't think you want that

[Oliver Butterley]

I can't myself see the problems it could cause. Very curious to know.

[Kenny Lau]

you can't deduce K from the resulting type so you'll need CoeOut, and then you'll also need some simp lemmas to make sure that everything transitions smoothly, and then beyond that I admit I don't really see an immediate problem so you can try it and see if you run into any problems later on

[Eric Wieser]

You won't need any simp lemmas because coercions are unfolded eagerly

[Eric Wieser]

So this would work:

instance {R M N} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {S : Submodule R N} :
    CoeOut (M →ₗ[R] S) (M →ₗ[R] N) where coe f := S.subtype.comp f

instance {R M N} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M]
    [TopologicalSpace N] [AddCommMonoid N] [Module R N] {S : Submodule R N} :
    CoeOut (M →L[R] S) (M →L[R] N) where coe f := S.subtypeL.comp f

and would have no harmful effect besides possibly confusing humans

[Jireh Loreaux]

Yeah, I would want to have a poll about this before we add it, because I think it could be rather confusing. I'm also not sure how convenient it would be in practice, but maybe I'm overlooking its utility.

[Oliver Butterley]

Thanks for the comments and clarifications. To be honest this functionality would only slightly improve the use case I had in mind, spelling out what I need is also fine and the situations which could be confusing weren't immediately apparent.

[Yoh Tanimoto]

I'm not sure if a coercion is the right choice, but I think we would like to have something like this:

import Mathlib

variable {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (p : E →L[𝕜] E)

def IsOrthogonalProjection (p : E →L[𝕜] E) : Prop := p = p ^ 2 ∧ p = p.adjoint

lemma IsOrthogonalProjection_iff (p : E →L[𝕜] E) : IsOrthogonalProjection p ↔ ∃ (K : Submodule 𝕜 E),
  ∃ (kH : K.HasOrthogonalProjection), p = K.subtypeL.comp (@K.orthogonalProjection _ _ _ _ _ kH) := by sorry
-- the subspace corresponding to the orthogonal projection
noncomputable def toSubmodule (p : E →L[𝕜] E) (hp : IsOrthogonalProjection p) :
  Submodule 𝕜 E := Classical.choose ((IsOrthogonalProjection_iff p).mp hp)
-- the projection as `orthogonalProjection`
noncomputable def toOrthogonalProjection (p : E →L[𝕜] E) (hp : IsOrthogonalProjection p) : E →L[𝕜] (toSubmodule p hp) :=
  (@(toSubmodule p hp).orthogonalProjection _ _ _ _ _ (Classical.choose (Classical.choose_spec ((IsOrthogonalProjection_iff p).mp hp))))

[Oliver Butterley]

With dot notation to make the last two defs more convenient in use.

[Yoh Tanimoto]

more generally, when there is a coercion from Y to Z, I wonder why there is no coercion from X → Y to X → Z (seeing Y-valued function as Z-valued function). probably the reason is that it is confusing humans?

[Jireh Loreaux]

@Yoh Tanimoto see docs#IsStarProjection and #25958

[Yoh Tanimoto]

ok so it's under review, nice!

[Oliver Butterley]

Jireh Loreaux said:

Yoh Tanimoto see docs#IsStarProjection and #25958

Great! I’m happy that reading that PR conversation I now understand how these things can be properly done. Also good that it is all in the pipeline!