inner product on subspaces

Stream: new members

[Busiso Chisala]

I want to have 'inheritance' of the real inner product structure of my E , but run into a problem I cant figure out. Here is my context and the code for defining the inner product from .core:

import algebra.module
import linear_algebra.basic
import analysis.normed_space.real_inner_product
-- import data.complex.is_R_or_C
import tactic


noncomputable theory

open_locale big_operators classical

variables {ι  E : Type*} [inner_product_space E]


variable (K: submodule ℝ E)

instance : inner_product_space K :=
inner_product_space.of_core
{
  inner := λ v w, ⟪(v:E) ,(w:E) ⟫,
  comm := λ _ _, inner_comm _ _ ,
  nonneg := λ x, inner_self_nonneg,
  definite := by {intros x h, have := inner_self_eq_zero.mp h, simp at this, exact this,},
  add_left := λ _ _ _,inner_add_left,
  smul_left := λ _ _ _ , inner_smul_left,
}

I get the following error message in vscode, with the : after instance highlilghted as the offender:

failed to synthesize instance name, name should be provided explicitly

Is there an alternative, more straightforward way to have submodules recognized as inner product spaces?

[Kyle Miller]

According to that error message, all you have to do is provide an explicit name, like
instance submodule_inner_product_space : inner_product_space K := ...

[Kyle Miller]

instance is like a def that doesn't always need a name and that lets the typeclass resolution system know this definition exists.

[Busiso Chisala]

Kyle Miller said:

According to that error message, all you have to do is provide an explicit name, like
instance submodule_inner_product_space : inner_product_space K := ...

Thanks. I also realized that if enclosed in a namespace, it goes away!

But is this the way to ensure that in a lemma, every submodule used has the inherited inner product? what invocation is required?

[Eric Wieser]

It looks to me like the code you have already does that

[Heather Macbeth]

@Busiso Chisala Yes, once you have defined this instance, it should be picked up automatically for all submodules!

By the way, it would be nice to have this in mathlib, maybe you could contribute it! docs#submodule.normed_space does exist, but this one is missing, right? @Joseph Myers @Yury G. Kudryashov

[Busiso Chisala]

Heather Macbeth said:

Busiso Chisala Yes, once you have defined this instance, it should be picked up automatically for all submodules!

By the way, it would be nice to have this in mathlib, maybe you could contribute it! docs#submodule.normed_space does exist, but this one is missing, right? Joseph Myers Yury G. Kudryashov

Thanks for pointing out that @instance, which is the kind I wanted. But when I comment my code out, Lean gets upset. Are you suggesting a way around this, using that reference?

And while I have your attention: how do I 'lift' a map? I have this scenario: submodules F ≤ K, map w: fin (k + 1) → ↥F and e: ↥K. All I want is to get v: fin (k+2) → K by extending w with the value e (I guess best at the end). Why does this fail?:

  let v: fin (k+2) → K := λ i, if h:(i ≠ k+1) then (w  (fin.pred_above (k+1) i h )):K else e,

the returned error is

type mismatch at application
  dite (i ≠ ↑k + 1) (λ (h : i ≠ ↑k + 1), w ((↑k + 1).pred_above i h))
term
  λ (h : i ≠ ↑k + 1), w ((↑k + 1).pred_above i h)
has type
  i ≠ ↑k + 1 → ↥F
but is expected to have type
  i ≠ ↑k + 1 → ↥K

[Heather Macbeth]

Busiso Chisala said:

Thanks for pointing out that @instance, which is the kind I wanted. But when I comment my code out, Lean gets upset. Are you suggesting a way around this, using that reference?

No, I wasn't suggesting that the normed space instance could replace your code for the inner product space instance (since the normed space instance is strictly weaker). I was just checking what the closest existing thing was -- if docs#submodule.normed_space had not existed, I would have suggested you write that too and contribute them both!

[Heather Macbeth]

Busiso Chisala said:

And while I have your attention: how do I 'lift' a map? I have this scenario: submodules F ≤ K, map w: fin (k + 1) → ↥F and e: ↥K. All I want is to get v: fin (k+2) → K by extending w with the value e (I guess best at the end). Why does this fail?:

  let v: fin (k+2) → K := λ i, if h:(i ≠ k+1) then (w  (fin.pred_above (k+1) i h )):K else e,

the returned error is

type mismatch at application
  dite (i ≠ ↑k + 1) (λ (h : i ≠ ↑k + 1), w ((↑k + 1).pred_above i h))
term
  λ (h : i ≠ ↑k + 1), w ((↑k + 1).pred_above i h)
has type
  i ≠ ↑k + 1 → ↥F
but is expected to have type
  i ≠ ↑k + 1 → ↥K

Try this: You have a hypothesis somewhere that tells you e is in K, right? Let's call it he. Can you use else e, ⟨e, he⟩? (An element of K is an element of E together with a witness that that element is in K.)

[Busiso Chisala]

Heather Macbeth said:

Busiso Chisala said:

And while I have your attention: how do I 'lift' a map? I have this scenario: submodules F ≤ K, map w: fin (k + 1) → ↥F and e: ↥K. All I want is to get v: fin (k+2) → K by extending w with the value e (I guess best at the end). Why does this fail?:

  let v: fin (k+2) → K := λ i, if h:(i ≠ k+1) then (w  (fin.pred_above (k+1) i h )):K else e,

the returned error is

type mismatch at application
  dite (i ≠ ↑k + 1) (λ (h : i ≠ ↑k + 1), w ((↑k + 1).pred_above i h))
term
  λ (h : i ≠ ↑k + 1), w ((↑k + 1).pred_above i h)
has type
  i ≠ ↑k + 1 → ↥F
but is expected to have type
  i ≠ ↑k + 1 → ↥K

Try this: You have a hypothesis somewhere that tells you e is in K, right? Let's call it he. Can you use else e, ⟨e, he⟩? (An element of K is an element of E together with a witness that that element is in K.)

Not really, e came from an existential so appears as e:↥K. Witness enough? I do think the trouble is my failed 'coercion' into K, since w certainly maps into the subspace F ... no? It fails even with humble 0 (or (0:K)) . I 'checked' the rest of the syntax (I believe) by replacing K with F as target, and e with 0. That worked, but is not what I need :(

[Heather Macbeth]

For debugging at least, you can try to split e into its pieces. Some experiments to try:

let e' : E := e.1, -- or = e,
let he' : e \in K := e.2,
-- alternately,
obtain ⟨e', he'⟩ := e,

(these should be doing roughly the same thing, but I'm providing different variants in case one doesn't work)

[Busiso Chisala]

Heather Macbeth said:

For debugging at least, you can try to split e into its pieces. Some experiments to try:

let e' : E := e.1, -- or = e,
let he' : e \in K := e.2,
-- alternately,
obtain ⟨e', he'⟩ := e,

(these should be doing roughly the same thing, but I'm providing different variants in case one doesn't work)

Great. I have never seen obtain before. Very illuminating. It splits e indeed. And I don't think the trouble is there. obtain ⟨w0', hw0'⟩ := (w 0), reveals what I am failing to get over:

w0': E
hw0': w0' ∈ F

I thought that by simply writing (w 0):K [as in the code], I could coax the value of w into the containing K ... how do I do that? recombine each value of w ...?

[Reid Barton]

At a low level, you need to combine hw0': w0' ∈ F with your hypothesis that F is a submodule of K. It won't just be a coercion.

[Reid Barton]

At a higher level, there's likely to be some kind of submodule.incl or something that provides a map F -> K for you.

[Heather Macbeth]

Reid Barton said:

At a low level, you need to combine hw0': w0' ∈ F with your hypothesis that F is a submodule of K. It won't just be a coercion.

So just to do it the "low level" way for now: now that you have a hypothesis hw0': w0' ∈ F and a hypothesis that F is a submodule of K, you can probably get hw0'' : w0' ∈ Kby library_search.

[Busiso Chisala]

Heather Macbeth said:

Reid Barton said:

At a low level, you need to combine hw0': w0' ∈ F with your hypothesis that F is a submodule of K. It won't just be a coercion.

So just to do it the "low level" way for now: now that you have a hypothesis hw0': w0' ∈ F and a hypothesis that F is a submodule of K, you can probably get hw0'' : w0' ∈ Kby library_search.

Thank you so kindly ... I think I'm almost there. Surprisingly awkward, Isn't this an obvious thing ?

[Kevin Buzzard]

You learn the tricks as time goes on

[Kevin Buzzard]

Just keep doing projects and writing mathematics in lean and it doesn't take long to pick up the core tricks

[Busiso Chisala]

Kevin Buzzard said:

You learn the tricks as time goes on

like this? ...

let incl: F → K := λ x, ⟨x.1, f2k x.2⟩,
let v: fin (k+2) → K := λ i, if h:(i ≠ k+1) then incl (w  (fin.pred_above (k+1) i h )) else e,

I am dreading showing this has the desired properties :(
(where f2k: F ≤ K, of course)

[Frédéric Dupuis]

That looks like a statement we would definitely want in mathlib! If you're planning to PR it, I would suggest doing it for submodule 𝕜 E where 𝕜 is an [is_R_or_C 𝕜]; this way we get the statement for both the real and complex case at the same time.

[Heather Macbeth]

Reid Barton said:

At a higher level, there's likely to be some kind of submodule.incl or something that provides a map F -> K for you.

So does this exist? In the simplest possible context, given s t : set X, with a hypothesis that s is a subset of t, do we have the induced map s → t (when both have been promoted to types)?

[Heather Macbeth]

Likewise for subgroups, submodules, ...

[Yakov Pechersky]

Isn't that just the coe from subtype to parent type?

[Heather Macbeth]

@Yakov Pechersky What do you mean exactly? Coercion will turn an s object to an X object, not to a t object. See thread above.

[Kyle Miller]

docs#set.inclusion

[Heather Macbeth]

Ah good! I also find docs#subring.inclusion, docs#submonoid.inclusion

[Heather Macbeth]

@Busiso Chisala would need docs#submodule.inclusion, which doesn't currently exist.

[Heather Macbeth]

docs#subgroup.inclusion also missing, I'm not sure whether or not it is magically inherited from submonoids.

[Kyle Miller]

It looks like you'd have to use to_submonoid and then use some lemma to turn the coercion of to_submonoid of the subgroup into the coercion of the subgroup, since submonoid and subgroup are structures and not classes.

[Kyle Miller]

I think @Bhavik Mehta mentioned a couple weeks ago that there was a category of the lattice of subobjects that got added to mathlib. That would include all the induced maps from inclusion, I think

[Heather Macbeth]

Kyle Miller said:

It looks like you'd have to use to_submonoid and then use some lemma to turn the coercion of to_submonoid of the subgroup into the coercion of the subgroup, since submonoid and subgroup are structures and not classes.

Yes, it might be better to just construct subgroup.inclusion directly rather than trying to inherit something from monoids. Don't know if it's the correct analogy, but this is what's done for fields (no attempt to inherit from rings):

def inclusion {S T : subfield K} (h : S ≤ T) : S →+* T :=
S.subtype.cod_restrict_field _ (λ x, h x.2)

[Bhavik Mehta]

Kyle Miller said:

I think Bhavik Mehta mentioned a couple weeks ago that there was a category of the lattice of subobjects that got added to mathlib. That would include all the induced maps from inclusion, I think

It's not in yet, I've got it in a repo but not yet in mathlib, I can prioritise that if it'd help though. That said I think it wouldn't make this a lot easier, since you'd have to go through all the category theory machinery

[Heather Macbeth]

I would like to propose instead that @Busiso Chisala make a 4-line PR for subgroup.inclusion and submodule.inclusion :big_smile:

(If you have time! Here's how: https://leanprover-community.github.io/contribute/index.html , and anyone here will be happy to answer questions.)

[Busiso Chisala]

Heather Macbeth said:

Kyle Miller said:

It looks like you'd have to use to_submonoid and then use some lemma to turn the coercion of to_submonoid of the subgroup into the coercion of the subgroup, since submonoid and subgroup are structures and not classes.

Yes, it might be better to just construct subgroup.inclusion directly rather than trying to inherit something from monoids. Don't know if it's the correct analogy, but this is what's done for fields (no attempt to inherit from rings):

def inclusion {S T : subfield K} (h : S ≤ T) : S →+* T :=
S.subtype.cod_restrict_field _ (λ x, h x.2)

This is exactly what I need. Having defined my incl map, I realized that I actually need a monomorphism. I have yet to do that (easy enough) but thus far here is my ugly demonstration of injectivity:

 let incl: F → K := λ x, ⟨x.1, f2k x.2⟩,
  -- verify some properties
  have incl_inj: ∀ a b : F, incl a = incl b → a = b := by {
    intros a b cond,
    have one: ∀ x,(incl x).val = x.val:= by{ intro a,simp [incl],},
    have two : (incl a).val = (incl b).val := by { rw cond,},
    have onea:= one a,
    have oneb := one b,
    have : a.val = b.val := eq.trans (eq.trans onea.symm two) oneb,
    exact subtype.eq two,},

excuse the absence of lambdas :)

[Busiso Chisala]

Frédéric Dupuis said:

That looks like a statement we would definitely want in mathlib! If you're planning to PR it, I would suggest doing it for submodule 𝕜 E where 𝕜 is an [is_R_or_C 𝕜]; this way we get the statement for both the real and complex case at the same time.

This was my original plan, even though I'm only interested in the real field. But my headers simply wouldn't run! Here was where I started:

import algebra.module
import linear_algebra.basic
import data.complex.is_R_or_C
import analysis.normed_space.real_inner_product

noncomputable theory

-- open is_R_or_C real
open_locale big_operators classical

variables {𝕜 E : Type*} [is_R_or_C 𝕜]  [inner_product_space 𝕜 E]

And Lean complained about classes ..

failed to synthesize type class instance for
𝕜 : Type u_1,
E : Type u_2
⊢ nondiscrete_normed_field 𝕜

So I abandoned that route, once I saw that the old style was fussless. Where did I mess up?

[Patrick Massot]

This looks like an outdated mathlib. You shouldn't have analysis.normed_space.real_inner_product nowadays

[Patrick Massot]

I don't know what you want to do because I didn't follow this thread, but the lines you posted above compile just fine on an up to date mathlib as long as you replace import analysis.normed_space.real_inner_product by import analysis.normed_space.inner_product.

[Busiso Chisala]

Patrick Massot said:

I don't know what you want to do because I didn't follow this thread, but the lines you posted above compile just fine on an up to date mathlib as long as you replace import analysis.normed_space.real_inner_product by import analysis.normed_space.inner_product.

Thanks. This is the fix I wanted. I don't think my mathlib is dated - I only recently started.

I take that back. It wont compile, cant find the stuff. What do I do about my mathlib?

[Scott Morrison]

leanproject upgrade-mathlib

[Scott Morrison]

(or just leanproject up for short)

[Scott Morrison]

This assumes that you followed the #install instructions.

[Scott Morrison]

If you're working in a branch on mathlib, rather than in a project with mathlib as a dependency, then instead you need git merge master.

[Scott Morrison]

(mathlib changes about 20 times each day at the moment, so "out of date" is almost certain :-)

[Busiso Chisala]

Scott Morrison said:

This assumes that you followed the #install instructions.

I'm pretty sure that I did. I have upgraded mathlib and went back and did so a second time, because nothing changed except the substantial download. My project only recognizes import analysis.normed_space.real_inner_product as a normed space import. No idea.

[Heather Macbeth]

Can you directly open up the folder src/analysis/normed_space/... and see the names of the files listed there?

[Kevin Buzzard]

Older versions of leanproject can leave oleans behind, and imports work if the olean is still there

[Kevin Buzzard]

If I have weirdness like this going on I usually manually delete all the olean files and then put the correct ones back with leanproject get-cache (they will be backed up locally)

[Kevin Buzzard]

Make sure your mathlib is up to date and your leanproject

[Kevin Buzzard]

By the way, for more specific help you should clarify whether you are working with a clone of mathlib or with a project which has mathlib as a dependency

[Busiso Chisala]

Heather Macbeth said:

Can you directly open up the folder src/analysis/normed_space/... and see the names of the files listed there?

    -rw-r--r--    1 busiso   busiso     74232 Oct  7 13:17 inner_product.lean
    -rw-r--r--    1 busiso   busiso    487192 Oct  7 14:05 inner_product.olean
    -rw-r--r--    1 busiso   busiso      6213 Sep 20 10:53 mazur_ulam.lean

and then

 -rw-r--r--    1 busiso   busiso    312421 Oct  7 14:05 real_inner_product.olean

the offending olean?

[Busiso Chisala]

Kevin Buzzard said:

By the way, for more specific help you should clarify whether you are working with a clone of mathlib or with a project which has mathlib as a dependency

mathlib dependent project

[Kevin Buzzard]

I would recommend going into the project, deleting _target and then typing leanproject up.

[Busiso Chisala]

Kevin Buzzard said:

I would recommend going into the project, deleting _target and then typing leanproject up.

Will do