Proving Quotient Structures

Stream: new members

[Gregory Wickham]

I'm trying to prove that an algebra, after I quotient out by a subspace, produces an inner product space with a particular inner product I've defined.

My questions are: How do I write proofs using quotient types? And, why is it asking me to prove norm_sq_eq_re_inner?

With respect to my first question, it seems I cannot dsimp or simp or aesop my way to a statement I can work with more easily. Is there some example I can look at to better understand how to work with quotient types?

With regard to my second question, why is it asking me to prove that the norm squared of an element is equal to its inner product with itself? Isn't that how the norm on an inner product space is defined? Shouldn't it be asking me to prove only that the function I've provided is, in fact, an inner product, so then the desired property follows by construction? But, assuming that this does make sense as something I need to prove, I am still left with my first question.

I've tried to construct a minimal example below. For the sake of brevity, I have replaced most of the proofs with sorrys, so the only sorrys I'm asking about are the last two, with the comment -- THIS ONE, next to them.

import Mathlib.Algebra.Order.Module.PositiveLinearMap
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.InnerProductSpace.Defs
import Mathlib.Analysis.Normed.Group.Quotient
import Mathlib.Data.Real.StarOrdered

open scoped ComplexOrder

variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
variable (f : A →ₚ[ℂ] ℂ)
variable (p : A) (q : A)

theorem aupetit_6_2_15ii (x y : A) :
  norm (f (x * star y)) ^ 2 ≤ f (x * star x) * f (y * star y) := by sorry

def N (f : A →ₚ[ℂ] ℂ) : Submodule ℂ A where
  carrier := {a : A | f (star a * a) = 0}
  add_mem' := sorry
  zero_mem' := by simp;
  smul_mem' := sorry
-- Begin code from Eric Wieser
noncomputable def mySesquilinear (f : A →ₚ[ℂ] ℂ) : A →ₗ⋆[ℂ] A →ₗ[ℂ] ℂ :=
  (LinearMap.mul ℂ A).comp (starLinearEquiv ℂ (A := A) : A →ₗ⋆[ℂ] A) |>.compr₂ₛₗ f

@[simp]
theorem mySesquilinear_apply (f : A →ₚ[ℂ] ℂ) (x y : A) :
  mySesquilinear f x y = f (star x * y) := rfl
-- End code from Eric Wieser

theorem helper (b : A) :  N f ≤ LinearMap.ker ((mySesquilinear f) b) := sorry

noncomputable def secondHalf := Submodule.liftQ (N f) ((mySesquilinear f) p) ((helper f) p)

noncomputable
def linearSecondHalf : LinearMap (starRingEnd ℂ) A (A ⧸ N f →ₗ[ℂ] ℂ) where
  toFun := (secondHalf f)
  map_add' := sorry
  map_smul' := sorry

theorem helper2 : N f ≤ LinearMap.ker (linearSecondHalf f) := sorry

noncomputable def myLiftedSesquiLinar := Submodule.liftQ (N f) (linearSecondHalf f) (helper2 f)

noncomputable instance myInnerProductSpace : InnerProductSpace ℂ (A ⧸ N f) where
  inner a b := (myLiftedSesquiLinar f) a b
  norm_sq_eq_re_inner := by
    intro a
    rw [RCLike.re_to_complex]
    sorry -- THIS ONE
  conj_inner_symm := by
    intro a b
    sorry -- THIS ONE
  add_left _ _ _ := LinearMap.map_add₂ _ _ _ _
  smul_left _ _ _ := LinearMap.map_smulₛₗ₂ _ _ _ _

Please let me know if there's any way I can make my question more specific. I just legitimately cannot see how to proceed on the last two sorrys. Also, I am aware that the way I have constructed myLiftedSesquiLinar is deeply questionable, so if a better construction would avoid the problems I'm having, that would be great.

[Matt Diamond]

Shouldn't it be asking me to prove only that the function I've provided is, in fact, an inner product, so then the desired property follows by construction?

Note that docs#Inner doesn't make any claims about how the inner product behaves. If it did, then you're correct that all you'd need to do is supply something of type Inner and the rest would follow. But the main purpose of the Inner class isn't to define a specific kind of mathematical object, but merely to enable the expected notation for the inner product (hence the description as a "syntactic" typeclass). Since it provides no guarantees on the behavior of the inner product, you need to supply those when constructing the inner product space.

Does that help clarify things?

[Matt Diamond]

re: your other question, I can't provide any in-depth guidance but I would recommend searching the Mathlib docs for lemmas related to Submodule.liftQ (since that's how you defined your inner product)

[Matt Diamond]

(deleted)

[Matt Diamond]

@loogle Submodule.liftQ

[loogle]

:search: Submodule.liftQ, Submodule.liftQ_mkQ, and 19 more

[Gregory Wickham]

Thank you for pointing out what was wrong w.r.t. my second question. I see now that I should be defining my inner product space like so:

noncomputable instance myInnerProductSpace : InnerProductSpace.Core ℂ (A ⧸ N f) where
  inner a b := (myLiftedSesquiLinar f) a b
  re_inner_nonneg := by
    intro a
    sorry
  definite := by
    intro a
    sorry
  conj_inner_symm := by
    intro a b
    sorry -- THIS ONE
  add_left _ _ _ := LinearMap.map_add₂ _ _ _ _
  smul_left _ _ _ := LinearMap.map_smulₛₗ₂ _ _ _ _

As for my second question, I did try browsing related docs, but I couldn't make anything work, so I asked here, hoping there would be someone who knows better how to work with these structures.

[Gregory Wickham]

I have made some progress:

noncomputable instance myInnerProductSpace : InnerProductSpace.Core ℂ (A ⧸ N f) where
  inner a b := mySesquilinear f (Quotient.out a) (Quotient.out b)
  re_inner_nonneg := by
    intro a
    rw [mySesquilinear_apply, RCLike.re_to_complex]
    have := star_mul_self_nonneg (Quotient.out a)
    have := PositiveLinearMap.map_nonneg f this
    have := re_le_re this
    exact this
  definite := by
    intro a h
    rw [mySesquilinear_apply] at h
    have := (Submodule.Quotient.mk_eq_zero (N f)).mpr h
    rwa [Submodule.Quotient.mk_out] at this
  conj_inner_symm := by
    intro a b
    rw [mySesquilinear_apply]
    rw [← (aupetit_6_2_15i _)]
    rw [star_mul, star_star, mySesquilinear_apply]
  add_left a b c := by
    repeat rw [mySesquilinear_apply]
    rw [← map_add]
    congr
    sorry
  smul_left _ _ _ := sorry

Now, it's just Quotient.out that's causing trouble, but I think I'll be able to figure it out eventually.

[Snir Broshi]

Gregory Wickham said:

Now, it's just Quotient.out that's causing trouble, but I think I'll be able to figure it out eventually.

AFAIK it's recommended to avoid Quotient.out, it chooses some representative and then you define things with it that aren't necessarily "well defined" (might depend on the choice).
The better path is to use some sort of induction on quotients, in this case Quotient.liftOn₂:

inner a b := Quotient.liftOn₂ a b (fun a b ↦ mySesquilinear f a b) fun a₁ b₁ a₂ b₂ ha hb ↦ by
  dsimp only
  sorry

This requires you to provide a proof that the function is well defined, and might be easier to work with than Quotient.out.

[Eric Wieser]

Gregory Wickham said:

With regard to my second question, why is it asking me to prove that the norm squared of an element is equal to its inner product with itself? Isn't that how the norm on an inner product space is defined?

No, you're in trouble here. The norm of a quotient is defined as the infimum of the norm of all elements in the congruence class. You can see that with:

noncomputable instance myInnerProductSpace : InnerProductSpace ℂ (A ⧸ N f) where
  inner a b := (myLiftedSesquiLinar f) a b
  norm_sq_eq_re_inner := by
    intro a
    rw [RCLike.re_to_complex]
    induction a using Submodule.Quotient.induction_on with | _ a
    have : ‖Submodule.Quotient.mk (p := N f) a‖ = Metric.infDist a (N f) := by
      erw [QuotientAddGroup.norm_mk]
      rfl
    rw [this]
    simp [myLiftedSesquiLinar, linearSecondHalf, secondHalf]
    -- goal is now `Metric.infDist a ↑(N f) ^ 2 = (f (star a * a)).re`
    -- which is surely not true in general
    sorry

[Eric Wieser]

Which is to say, mathlbi has already declared a canonical norm for A ⧸ N f, and it is almost certainly not equal to the norm that would be induced by your inner product space

[Eric Wieser]

As a result, to make this work you need to use a type synonym / one-field-structure, something like

structure MyQuotient (A N f) where
  val : A ⧸ N f

and then copy across the additive structure, but not the incompatible norm. Then your InnerProductSpace.Core approach will be safe.

[Gregory Wickham]

Eric Wieser said:

As a result, to make this work you need to use a type synonym / one-field-structure, something like

structure MyQuotient (A N f) where
  val : A ⧸ N f

and then copy across the additive structure, but not the incompatible norm. Then your InnerProductSpace.Core approach will be safe.

Is there a concise way to just copy the structures I want? Because, the one-liners that worked for a different type synonym, lines like this:
instance instAddCommGroup [AddCommGroup A] : AddCommGroup (WithFunctional A f) := ‹AddCommGroup A›
that I copied from, I think, the documentation on L^p spaces, doesn't seem to work in this situation.

[Gregory Wickham]

Having to prove an AddCommMonoid to then show that it's a module and everything, is a lot of extra work, which I can't really figure out how to do properly.

[Gregory Wickham]

Ideally, I could just prove def linEquiv : LinearEquiv (RingHom.id ℂ) (myQuot f) (A ⧸ N f) where sorry, but the statement itself won't even typecheck unless I prove AddCommMonoid (myQuot f) first.

[Matt Diamond]

are you looking for something like

instance : AddCommMonoid (myQuot f) := by unfold myQuot; infer_instance

[Aaron Liu]

but this time it's a structure

[Matt Diamond]

oh... well maybe define it as a def instead?

[Matt Diamond]

like def myQuot : Type u := A ⧸ N f

[Matt Diamond]

but if you have the answer for how to do it with structures, that works too

[Gregory Wickham]

Matt Diamond said:

are you looking for something like

instance : AddCommMonoid (myQuot f) := by unfold myQuot; infer_instance

Yes, that's exactly what I'm looking for! Thank you!

That lets me write

instance : AddCommGroup (myQuot f) := by unfold myQuot; infer_instance
instance : Module ℂ (myQuot f) := by unfold myQuot; infer_instance

noncomputable instance myInnerProductSpace : InnerProductSpace.Core ℂ (myQuot f) where
  inner a b := sorry
  conj_inner_symm := sorry
  re_inner_nonneg := sorry
  add_left := sorry
  smul_left := sorry
  definite := sorry

so now I only have to fill in these sorries. I've eliminate the default norm, so now I just have to figure out how to properly define and work with my inner product without Quotient.out.

[Gregory Wickham]

I now have this code:

import ThesisProjectRepo.AupetitTheorems
set_option linter.unusedSectionVars false -- remove later
open scoped ComplexOrder
variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
variable (f : A →ₚ[ℂ] ℂ)

def WithFunctional (_A : Type*) [CStarAlgebra _A] [PartialOrder _A] (_f : _A →ₚ[ℂ] ℂ) := _A

namespace WithFunctional

/-- The canonical inclusion of `A` into `WithFunctional A f`. -/
def toFunctional : A → WithFunctional A f := id

/-- The canonical inclusion of `WithFunctional A f` into `A`. -/
def ofFunctional : WithFunctional A f → A := id

instance instAddCommGroup [AddCommGroup A] : AddCommGroup (WithFunctional A f) := ‹AddCommGroup A›
instance instSemiring [Semiring A] : Semiring (WithFunctional A f) := ‹Semiring A›
instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring A] :
  NonUnitalNonAssocSemiring (WithFunctional A f) := ‹NonUnitalNonAssocSemiring A›
instance instModule [Semiring ℂ] [AddCommGroup A] [Module ℂ A] :
  Module ℂ (WithFunctional A f) := ‹Module ℂ (WithFunctional A f)›

instance ofFunctionalLinear : LinearMap (RingHom.id ℂ) (WithFunctional A f) A where
  toFun := ofFunctional f
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

/-- `WithFunctional.toFunctional` and `WithFunctional.toFunctional` as an equivalence. -/
@[simps]
protected def equiv : WithFunctional A f ≃ A where
  toFun := ofFunctional f
  invFun := toFunctional f
  left_inv _ := rfl
  right_inv _ := rfl

def myIdeal := N f

instance mySubModule (f : A →ₚ[ℂ] ℂ) : Submodule ℂ (WithFunctional A f) := sorry
-- Begin code from Eric Wieser
-- noncomputability should be fixed in by Eric Wieser's bug fix
noncomputable def mySesquilinear (f : A →ₚ[ℂ] ℂ) :
  (WithFunctional A f) →ₗ⋆[ℂ] (WithFunctional A f) →ₗ[ℂ] ℂ :=
  (LinearMap.mul ℂ (WithFunctional A f)).comp (starLinearEquiv ℂ (A := (WithFunctional A f)) :
    (WithFunctional A f) →ₗ⋆[ℂ] (WithFunctional A f)) |>.compr₂ₛₗ
    (f.comp (ofFunctionalLinear f))

@[simp]
theorem mySesquilinear_apply (f : A →ₚ[ℂ] ℂ) (x y : (WithFunctional A f)) :
  mySesquilinear f x y = f (star x * y) := rfl
-- End code from Eric Wieser
-- I believe this sucessfully erases the norm
def myQuot := (WithFunctional A f) ⧸ (mySubModule f)

def toQuot : (myQuot f) → (WithFunctional A f) ⧸ (mySubModule f) := id
def toMyQuot : (WithFunctional A f) ⧸ (mySubModule f) → (myQuot f) := id
def modOut := Submodule.Quotient.mk (M := (WithFunctional A f)) (p := (mySubModule f))

instance : AddCommGroup (myQuot f) := by unfold myQuot; infer_instance
instance : Module ℂ (myQuot f) := by unfold myQuot; infer_instance

noncomputable instance myInnerProductSpace : InnerProductSpace.Core ℂ (myQuot f) where
  inner a b := sorry
  conj_inner_symm := sorry
  re_inner_nonneg := sorry
  add_left := sorry
  smul_left := sorry
  definite := sorry

end WithFunctional

Does anyone know how I can define my inner product now? With a Submodule, I don't appear to have access to Quotient.Out or Quotient.lift, so I can't see any way to define the inner product as the f(a*b) by choosing coset representatives. Is there any way to do this? Or is there some way I can get access to the other quotient methods?

[Aaron Liu]

The canonical way to map out of a quotient module is to use docs#Submodule.liftQ

[Gregory Wickham]

Aaron Liu said:

The canonical way to map out of a quotient module is to use docs#Submodule.liftQ

Thank you! I'll try to make that work. I was looking for something like that in Mathlib.LinearAlgebra.Quotient.Defs, but I guess I should have noticed Mathlib.LinearAlgebra.Quotient.Basic was right there