Space with bilinear form

Stream: Is there code for X?

[Johan Commelin]

Do we have a typeclass (extending docs#Inner, or a mixin on top of it) that expresses that the inner product provided by Inner is bilinear?

[Eric Wieser]

No, it's currently all (docs#InnerProductSpace) or nothing

[Eric Wieser]

We have a fair bit of theory when passing around an arbitrary bilinear form, but nothing about when it is canonical

[Johan Commelin]

Here is a first draft

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.LinearAlgebra.SesquilinearForm

namespace WIP

variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
variable [Inner R M]

class InnerIsBilin : Prop where
  add_inner : ∀ (x y z : M), ⟪x + y, z⟫_R = ⟪x, z⟫_R + ⟪y, z⟫_R
  smul_inner : ∀ (r : R) (x y : M), ⟪r • x, y⟫_R = r * ⟪x, y⟫_R
  inner_add : ∀ (x y z : M), ⟪x, y + z⟫_R = ⟪x, y⟫_R + ⟪x, z⟫_R
  inner_smul : ∀ (r : R) (x y : M), ⟪x, r • y⟫_R = r * ⟪x, y⟫_R

export InnerIsBilin (add_inner smul_inner inner_add inner_smul)
attribute [simp] add_inner smul_inner inner_add inner_smul

@[simps!]
def innerₗ [InnerIsBilin R M] : M →ₗ[R] M →ₗ[R] R :=
  LinearMap.mk₂ R (⟪·, ·⟫_R) add_inner smul_inner inner_add inner_smul

class InnerIsSymmBilin : Prop where
  inner_symm : ∀ (x y : M), ⟪x, y⟫_R = ⟪y, x⟫_R
  add_inner : ∀ (x y z : M), ⟪x + y, z⟫_R = ⟪x, z⟫_R + ⟪y, z⟫_R
  smul_inner : ∀ (r : R) (x y : M), ⟪r • x, y⟫_R = r * ⟪x, y⟫_R

export InnerIsSymmBilin (inner_symm)

instance [InnerIsSymmBilin R M] : InnerIsBilin R M where
  __ := (inferInstance : InnerIsSymmBilin R M)
  inner_add x y z := by simp only [inner_symm x, InnerIsSymmBilin.add_inner]
  inner_smul r x y := by simp only [inner_symm x, InnerIsSymmBilin.smul_inner]

class InnerIsNondegenerate extends InnerIsSymmBilin R M : Prop where
  nondegenerate : (innerₗ R M).Nondegenerate

section nondegenerate

variable [InnerIsNondegenerate R M]

lemma innerₗ_nondegenerate : (innerₗ R M).Nondegenerate :=
  InnerIsNondegenerate.nondegenerate

variable {M} in
lemma inner_separatingLeft (x : M) (h : ∀ y, ⟪x, y⟫_R = 0) : x = 0 :=
  (innerₗ_nondegenerate R M).1 x h

variable {M} in
lemma inner_separatingRight (y : M) (h : ∀ x, ⟪x, y⟫_R = 0) : y = 0 :=
  (innerₗ_nondegenerate R M).2 y h

end nondegenerate

end WIP

[Johan Commelin]

I wrapped everything in the WIP namespace, since innerₗ is already taken for real inner products. But this would generalize that defn.

[Johan Commelin]

Maybe I should also factor sesquilinear forms into this setup.

[Johan Commelin]

Note that the classes I define above are all Prop-mixins on top of [Inner R M], instead of extending the data.

[Eric Wieser]

I think extending the data is fine here, InnerProductSpace already does it, and these classes fall between Inner and InnerProductSpace

[Johan Commelin]

Yes, but it means that you can throw several mixins together.

[Johan Commelin]

So we will need many more classes.

[Johan Commelin]

E.g. SymmNondegenerate is not needed in the current design, because you can just add both mixins.