(non-positive) GNS representation

Stream: mathlib4

[Yoh Tanimoto]

I wanted to write a variation of GNS representation where one takes the ideal of isotropic elements, instead of those with zero norm. This works even if the linear functional is not positive-definite.

It's easy to show that this is indeed a left ideal, so I can take the quotient. If I want show that the quotient is also a module for the scalar, I got a problem
(actually I don't need it anymore because there is Quotient.module' and I now understood that the definition was bad, but I would like to know the solution).

import Mathlib

open Submodule Quotient

variable {R : Type*} {A : Type*} [CommRing R] [StarRing R] [Ring A] [StarRing A]
  [Algebra R A] [StarModule R A]

def nullIdeal (ψ : A →ₗ[R] R) : Ideal A where
  carrier := {x : A | ∀ y, ψ (star y * x) = 0}
  add_mem' {x y} hx hy := by
    simp only [Set.mem_setOf_eq]
    intro z
    rw [mul_add, map_add, hx, hy]
    exact zero_add 0
  zero_mem' := by simp
  smul_mem' := by
    intro x y hy
    simp only [smul_eq_mul, Set.mem_setOf_eq]
    intro z
    rw [← mul_assoc, ← star_star_mul, hy]

noncomputable instance (ψ : A →ₗ[R] R) : Module R (A ⧸ (nullIdeal ψ)) where
  smul c x := Submodule.Quotient.mk (c • (Classical.choose (Submodule.Quotient.mk_surjective _ x)))
  one_smul y := by
    simp only [one_mul] -- fails, although in the definition it is there
--    nth_rw 2 [← Classical.choose_spec (Submodule.Quotient.mk_surjective _ y)]
  mul_smul := sorry
  smul_zero := sorry
  smul_add := sorry
  add_smul := sorry
  zero_smul := sorry

To show the remaining properties, I need to unfold the definition of smul. How can I do it?

[Kenny Lau]

don't use Classical.choose

[Kenny Lau]

the whole point of quotient is to use the quotient API

[Kenny Lau]

but you shouldn't need that here anyway?

[Kenny Lau]

import Mathlib

open Submodule Quotient

variable {R : Type*} {A : Type*} [CommRing R] [StarRing R] [Ring A] [StarRing A]
  [Algebra R A] [StarModule R A]

def nullIdeal (ψ : A →ₗ[R] R) : Ideal A where
  carrier := {x : A | ∀ y, ψ (star y * x) = 0}
  add_mem' {x y} hx hy := by
    simp only [Set.mem_setOf_eq]
    intro z
    rw [mul_add, map_add, hx, hy]
    exact zero_add 0
  zero_mem' := by simp
  smul_mem' := by
    intro x y hy
    simp only [smul_eq_mul, Set.mem_setOf_eq]
    intro z
    rw [← mul_assoc, ← star_star_mul, hy]

instance (ψ : A →ₗ[R] R) : Module R (A ⧸ (nullIdeal ψ)) := inferInstance

[Kenny Lau]

Lean already knows that it's a module

[Yoh Tanimoto]

yes, I know that Quotient.module' uses Submodule.Quotient.mk_smul, so I don't need this, but I would like to know how to unfold the definition

[Kenny Lau]

you write custom simp lemmas which you prove by rfl

[Kenny Lau]

btw I read the source code to try to show the point of not using choose, but I was horrified by the source code, can someone explain to me what a fast_instance is

[Kenny Lau]

For a demonstration of how Quotient is supposed to work, see https://github.com/leanprover-community/mathlib4/blob/5e4c8bc4c9bfa67ed137e675329e373d90ad6554/Mathlib/Algebra/Group/Conj.lean#L158

[Yoh Tanimoto]

well, the smul is just defined there, so I cannot add simp lemmas in the instance declaration, or do you mean something else?

[Eric Wieser]

You can pretend fast_instance% doesn't exist, it is peformance only

[Anatole Dedecker]

What is the version of the GNS theorem you're trying to prove ? I'm asking because there shouldn't be a need to explicitly write down the ideal for the usual GNS, the Hausdorff-Completion procedure should take care of it.

[Kenny Lau]

Yoh Tanimoto said:

well, the smul is just defined there, so I cannot add simp lemmas in the instance declaration, or do you mean something else?

You write a simp lemma after that

[Eric Wieser]

You define the SMul instance before the Module instance

[Yoh Tanimoto]

I would like to know the way to unfold the definition of smul to prove other properties of the instance

[Eric Wieser]

Then you have somewhere in between to write lemmas

[Yoh Tanimoto]

ah I see, thanks!

[Kenny Lau]

instance (ψ : A →ₗ[R] R) : Module R (A ⧸ (nullIdeal ψ)) := inferInstance

omit [StarRing R] [StarModule R A] in
@[simp] lemma smul_mk (ψ : A →ₗ[R] R) (c : R) (x : A) :
    c • Submodule.mkQ (nullIdeal ψ) x = Submodule.mkQ (nullIdeal ψ) (c • x) := rfl

[Kenny Lau]

this is the simp lemma you need

[Yoh Tanimoto]

Anatole Dedecker said:

What is the version of the GNS theorem you're trying to prove ? I'm asking because there shouldn't be a need to explicitly write down the ideal for the usual GNS, the Hausdorff-Completion procedure should take care of it.

It's a kind of variation where you take the quotient by the isotropic elements (y such that ψ (star x * y) = 0 for all x. This should work (to some extent, just giving a Module) even if ψ is not positive definite.

[Kenny Lau]

(but you don't really need to write this because Lean already knows it)

[Kenny Lau]

Eric Wieser said:

You define the SMul instance before the Module instance

This is for the original code; but in this case you don't need the Module instance because Lean already knows it, and you also don't need the simp lemma because Lean also already knows it!

[Yoh Tanimoto]

(my question was how to unfold/rewrite/simp the definition and not how to get an instance. sorry if it was not clear)

[Kenny Lau]

which I answered you above, look at the @[simp] lemma I wrote

[Kenny Lau]

I am also telling you the extra information that you don't need to write it separately

[Kenny Lau]

I think I see the missing piece now

[Kenny Lau]

@Yoh Tanimoto Here are the full instructions. If you want to "unfold the definition of smul", you need to:

1. Use Submodule.Quotient.induction_on to convert the element to something of the form Submodule.Quotient.mk x.
2. Then use rw [← Submodule.Quotient.mk_smul].

[Yoh Tanimoto]

I'm not sure if I got it

noncomputable instance (ψ : A →ₗ[R] R) : Module R (A ⧸ (nullIdeal ψ)) where
  smul c x := Submodule.Quotient.mk (c • (Classical.choose (Submodule.Quotient.mk_surjective _ x)))
  one_smul y := by
    nth_rw 2 [← Classical.choose_spec (Submodule.Quotient.mk_surjective _ y)]
    nth_rw 1 [← Classical.choose_spec (Submodule.Quotient.mk_surjective _ y)]
    rw [← Submodule.Quotient.mk_smul] -- fails

  mul_smul := sorry
  smul_zero := sorry
  smul_add := sorry
  add_smul := sorry
  zero_smul := sorry

[Kenny Lau]

well, as I've explained above, you're shooting yourself on the foot by using Classical.choose

[Aaron Liu]

You should use quotient lift instead

[Kenny Lau]

my explanation is for the case when you've fixed that definition

[Kenny Lau]

and also as I explained above, you also don't need to even provide the module instance yourself

[Aaron Liu]

interesting, I don't see a submodule quotient lift function anywhere

[Eric Wieser]

docs#AddCon.lift

[Aaron Liu]

quotient needs a redesign

[Kenny Lau]

Please PR :melt:

[Yoh Tanimoto]

(I knew that there was an instance, I wrote it in the original post)

[Eric Wieser]

Kenny Lau said:

Please PR :melt:

Design work probably belongs in a zulip thread, not in a PR

[Kenny Lau]

Yoh Tanimoto said:

(I knew that there was an instance, I wrote it in the original post)

ok, sorry, in that case you should still use whatever lift function there is

[Kenny Lau]

the problem with Classical.choose is that it cannot be unfolded

[Eric Wieser]

Aaron Liu said:

interesting, I don't see a submodule quotient lift function anywhere

Eric Wieser said:

docs#AddCon.lift

Actually, it's docs#Submodule.liftQ

[Eric Wieser]

Even so, it's still almost always best to write the SMul instance separately and characterize it with rfl, rather than trying to unfold a lift.

[Yoh Tanimoto]

Kenny Lau said:

the problem with Classical.choose is that it cannot be unfolded

really? I just wanted to unfold the definition of smul, not Classical.choose