Inner product is bijective in both components

Stream: Is there code for X?

[Yaël Dillies]

I am trying to show that the inner product is a continuous perfect pairing (docs#LinearMap.IsContPerfPair). I could show that it is continuous in both arguments and bijective in the first, but I cannot seem to find the bijectivity in the second argument:

import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Topology.Algebra.Module.PerfectPairing

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

instance : (innerₗ E).IsContPerfPair where
  continuous_uncurry := continuous_inner
  bijective_left := (InnerProductSpace.toDual ℝ E).bijective
  bijective_right := sorry

[Yaël Dillies]

Is it possible somehow to reuse docs#InnerProductSpace.toDual for bijectivity in the second argument, by defining InnerOp E := E and ⟪x, y⟫ := ⟪y.ofInnerOp, x.ofInnerOp⟫ when x y : InnerOp E?

[Yaël Dillies]

As in, it is obviously possibly to do so for E a real inner product space, but I am not sure how the story goes for a complex inner product. Does ⟪x, y⟫ := conj ⟪y.ofInnerOp, x.ofInnerOp⟫ Just Work?

[Kenny Lau]

Yaël Dillies said:

As in, it is obviously possibly to do so for E a real inner product space, but I am not sure how the story goes for a complex inner product. Does ⟪x, y⟫ := conj ⟪y.ofInnerOp, x.ofInnerOp⟫ Just Work?

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Basic.html#inner_conj_symm

(starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y

[Yaël Dillies]

Sure, yes, I guess there isn't much point to the type synonym

[Kenny Lau]

Why do you need the type synonym?

[Yaël Dillies]

Sorry, I went off for lunch without posting what I did. Here's what I came up with:

instance (innerₗ E).IsContPerfPair where
  continuous_uncurry := continuous_inner
  bijective_left := (InnerProductSpace.toDual ℝ E).bijective
  bijective_right := by
    convert (InnerProductSpace.toDual ℝ E).bijective
    ext y
    simp

[Yaël Dillies]

I still think the type synonym could be useful to dualise results about inner products. But I don't really need it here

[Yaël Dillies]

Here's the full code I wrote before throwing it away:

/-
Copyright (c) 2025 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Analysis.InnerProductSpace.Basic

/-!
# Inner opposite of an inner product space

For an inner product space `E`, this file defines ``
-/

variable {𝕜 E : Type*}

set_option linter.unusedVariables false in
/-- Type synonym for swapping the argument the arguments to the inner product of an inner product
space. -/
def InnerOp (𝕜 E : Type*) := E

section Defs
variable [SeminormedAddCommGroup E]

instance : SeminormedAddCommGroup (InnerOp 𝕜 E) := ‹_›

variable [RCLike 𝕜] [NormedSpace 𝕜 E]

instance : NormedSpace 𝕜 (InnerOp 𝕜 E) := ‹_›

variable (𝕜) in
/-- The linear isometry equivalence from `E` to `InnerOp 𝕜 E`. -/
def toInnerOp : E ≃ₗᵢ[𝕜] InnerOp 𝕜 E := .refl _ _

/-- The linear isometry equivalence from `InnerOp 𝕜 E` to `E`. -/
def ofInnerOp : InnerOp 𝕜 E ≃ₗᵢ[𝕜] E := .refl _ _

@[simp] lemma symm_toDual : (@toInnerOp 𝕜 E).symm = ofInnerOp := rfl
@[simp] lemma symm_ofInnerOp : (@ofInnerOp 𝕜 E).symm = toInnerOp 𝕜 := rfl
@[simp] lemma toInnerOp_ofInnerOp (x : InnerOp 𝕜 E) : toInnerOp 𝕜 (ofInnerOp x) = x := rfl
@[simp] lemma ofInnerOp_toInnerOp (x : E) : ofInnerOp (toInnerOp 𝕜 x) = x := rfl

lemma toInnerOp_inj {x y : E} : toInnerOp 𝕜 x = toInnerOp 𝕜 y ↔ x = y := .rfl
lemma ofInnerOp_inj {x y : InnerOp 𝕜 E} : ofInnerOp x = ofInnerOp y ↔ x = y := .rfl

lemma InnerOp.forall {P : InnerOp 𝕜 E → Prop} : (∀ x, P x) ↔ ∀ x, P (toInnerOp 𝕜 x) := .rfl

end Defs

instance [NormedAddCommGroup E] : NormedAddCommGroup (InnerOp 𝕜 E) := ‹_›

variable [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]

instance : InnerProductSpace 𝕜 (InnerOp 𝕜 E) where
  inner x y := star <| inner 𝕜 (ofInnerOp y) (ofInnerOp x)
  norm_sq_eq_re_inner := by simp [← norm_sq_eq_re_inner]
  conj_inner_symm := by simp
  add_left := by simp [inner_add_right]
  smul_left := by simp [inner_smul_right]

[Kenny Lau]

but where's the bijective stuff?

[Yaël Dillies]

Sorry, wdym? Isn't it the proof of bijective_right above?

[Kenny Lau]

I meant that it's not in your full code

[Yaël Dillies]

Ah sure, I threw it away before using it