Analog of LinearEquiv.submoduleMap for AffineIsometryEquiv?

Stream: Is there code for X?

[Jason Reed]

I'd like to show if $T : P_1 \to P_2$ is an affine isometry equivalence between two real inner product spaces, then

• (a) there exists a linear isometry equivalence $\mathtt{Submodule.map}$ between any subspace $Q$ and its image $T^{>}(Q)$ under $T$, and furthermore
• (b) the following diagram commutes:

image.png

where $\mathsf{proj}$ is orthogonal projection onto a subspace.

It looks like mathlib already has (b), at least elementwise, in LinearIsometry.map_orthogonalProjection'.

Does it have (a)? The closest I could find was LinearEquiv.submoduleMap which would give me the bottom horizontal arrow in the diagram but for (semi)linear equivalences instead of linear isometry equivalences

Is it possible to piece this together easily by composing things already in mathlib? Or is this something that ought to exist in mathlib and simply doesn't yet for whatever reason?

[Eric Wieser]

Usually the presence of a function for LinearEquiv is a good enough reason for it to exist for AffineEquiv and AffineIsometryEquiv and LinearIsometryEquiv

[Eric Wieser]

(or more rarely, an argument that it shouldn't exist for LinearEquiv after all)

[Jason Reed]

Great, makes sense, that's what I'd guessed was likely true.

[Jason Reed]

Maybe it's a good exercise to see if I can prove the lemma I want. Doesn't seem like it should be too difficult...

[Jason Reed]

Ok, great, that's actually quite trivial; at least the LinearIsometryEquiv case that motivated my question. I just need to slap on the fact that the norm is preserved, and that follows directly from norm preservation of the map on the ambient space. Functional record update is a terrific convenience. I'm able to prove

import Mathlib

def LinearIsometryEquiv.submoduleMap {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [RCLike R] [RCLike R₂]
    [NormedAddCommGroup M] [NormedAddCommGroup M₂]
    [InnerProductSpace R M] [InnerProductSpace R₂ M₂]
    {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
    {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
    (e : M ≃ₛₗᵢ[σ₁₂] M₂)
    (p : Submodule R M) : p ≃ₛₗᵢ[σ₁₂] (Submodule.map e p) :=
  { e.toLinearEquiv.submoduleMap p with norm_map' := fun x => e.norm_map' x }

I reckon I should try to cook up a tiny PR against mathlib? Probably filling in whatever other submoduleMap gaps that exist as well. Any obvious flaws in the code itself, from the point of view of mathlib conventions? I guess I'm thinking of more high-level conventions; I can go reread things like the standard documents on naming and code style for concrete syntax.

I'm especially wondering whether the collection of typeclasses is at the right level of generality, since I frequently find myself being uncertain about that. Although most likely if I hunted around for the right place to add it, the nearby variable clauses would probably guide me correctly.

[Eric Wieser]

I think the correct generality is

def LinearIsometryEquiv.submoduleMap {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [Ring R] [Ring R₂]
    [SeminormedAddCommGroup M] [SeminormedAddCommGroup M₂]
    [Module R M] [Module R₂ M₂]
    {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
    {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
    (e : M ≃ₛₗᵢ[σ₁₂] M₂)
    (p : Submodule R M) : p ≃ₛₗᵢ[σ₁₂] (Submodule.map e p) :=
  { e.toLinearEquiv.submoduleMap p with norm_map' := fun x => e.norm_map' x }

which is missing an instance that yo need!

[Jason Reed]

Ah, right, all the inner product space structure (which I think was the reason for RCLike) is necessary only for other stuff I was doing, not at all needed for this lemma

[Eric Wieser]

Edited above

[Jason Reed]

Gotcha; the full Ring-as-opposed-to-Semiring structure of R and R₂ seems right enough to me, yeah. And concretely I see how that's used to give the requisite SeminormedAddComGroup instance. I thought as merely a mathematician and as a sometime category theory enjoyer I was sufficiently obsessed (compared to, like, the general population) with squeezing the maximum generality from a statement, but mathlib library design is an impressive achievement in that field.

[Eric Wieser]

Semiring, not Subring :)

[Jason Reed]

Oops, yes, edited :) Have been spending all day so far typing Submodule that my fingers' autocomplete went there...

[Jason Reed]

I made #27357 and it looks like I'm still awaiting CI...

[Ruben Van de Velde]

CI seems to pass