Linear.IsSymm for sesquilinear maps

Stream: mathlib4

[Christopher Hoskin]

Currently mathlib has the definition LinearMap.IsSymm:

variable [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R}

/-- The proposition that a sesquilinear form is symmetric -/
def IsSymm (B : M →ₛₗ[I] M →ₗ[R] R) : Prop :=
  ∀ x y, I (B x y) = B y x

It's not clear to me how to generalise this to sesquilinear maps in mathlib. In the spirit of the current definition, I have opened the PR #18406 which uses:

variable [AddCommMonoid M₁] [AddCommMonoid M] [CommSemiring R] [Module R M₁] [Module R M]
  {I : R →+* R} {J : M →+ M} {B : M₁ →ₛₗ[I] M₁ →ₗ[R] M}

/-- The proposition that a sesquilinear form is conjugate symmetric -/
def IsConjSymm (B : M₁ →ₛₗ[I] M₁ →ₗ[R] M) (J : M →+ M) : Prop :=
  ∀ x y, J (B x y) = B y x

but this seems rather strange since it doesn't include the hypothesis:

J (r • a) = (I r) • (J a)

In particular, @Eric Wieser says:

I worry this is more generality than we really care about, and maybe we just want to allow I = J = star. Rather than changing anything here, it's probably best to discuss on Zulip.

An example of a conjugate symmetric (or Hermitian) sesquilinear map is the inner product on a Hilbert C*-module.

Thanks,

Christopher

[Christopher Hoskin]

Were there any further thoughts on this please? I'm bashing my head against not having a Map version of https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean#L120

[Eric Wieser]

I've been a little short of time recently; would you prefer I spend what I can find on this one or on the quadratic basis stuff first?

[Christopher Hoskin]

Eric Wieser said:

I've been a little short of time recently; would you prefer I spend what I can find on this one or on the quadratic basis stuff first?

@Eric Wieser thanks - I appreciate doing this must be a huge time sink for you. My thinking on the quadratic basis stuff is still coming together, and may possibly end up depending on this. Also this is more widely applicable and perhaps also a simpler problem, so perhaps best to focus on this first?

[Jireh Loreaux]

@Eric Wieser , @Frédéric Dupuis , and @Christopher Hoskin (also @Johan Commelin because you asked me to look at this; and @Antoine Chambert-Loir because you developed the API for equivariant maps): I'm not super keen on either #19809 or #18406. I don't like the former because it loses generality and requires us to add the starRingOfComm instance locally in many places. I don't like the latter because probably we only ever want I = J in practice. In fact, the stated use case is for I = J = star (which is why #19809 was proposed), and the only reason we can't do it with the existing set up is that docs#LinearMap requires a docs#RingHom, but star only satisfies that in the commutative case.

So, here's a question: Do we really need that for docs#LinearMap? Can we get away with anything weaker? Does it cause performance issues?

[Eric Wieser]

I think at the time I suggested we should take a raw function, because I didn't like declaring starRingHom the canonical spelling; but I think the compromise was to reconsider that later

[Eric Wieser]

Arguably the RingHom restriction is still fine for the noncommutative case, because you can write:

import Mathlib

def starLinearMap {R} [Semiring R] [StarRing R] :
    R →ₛₗ[(starRingEquiv (R := R)).toRingHom] R where
  __ := starAddEquiv
  map_smul' _ _ := by simp

[Eric Wieser]

(though generalizing this runs into issues with the definition of StarModule in the noncommutative case, which have threads elsewhere we should revive rather than repeating)

[Christopher Hoskin]

Jireh Loreaux said:

In fact, the stated use case is for I = J = star

Sorry, bad example now I think about it a bit more.

In fact what I was trying to achieve was to make a version of QuadraticForm.associated_tmul which works for quadratic maps (see the TODO). In that case the range of the map may be in a different module to the ring and therefore I and J are not the same thing.

Christopher

[Christopher Hoskin]

As a third suggestion, how about we leave LinearMap.IsSymm as it is (for now at least) and do something like #20177 instead?

[Christopher Hoskin]

Although this isn't a complete solution, as we also need LinearMap.IsSymm.tmul to work for maps, not just forms.

[Christopher Hoskin]

Christopher Hoskin said:

Although this isn't a complete solution, as we also need LinearMap.IsSymm.tmul to work for maps, not just forms

I've now updated #20177 to establish QuadraticMap.associated_tmul and derive QuadraticForm.associated_tmul from it resolving the TODO. I'm not sure this approach is entirely satisfactory either @Jireh Loreaux .