Zulip Chat Archive

Stream: new members

Topic: inner product on subspaces


view this post on Zulip Busiso Chisala (Oct 06 2020 at 09:05):

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?

view this post on Zulip Kyle Miller (Oct 06 2020 at 09:09):

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 := ...

view this post on Zulip Kyle Miller (Oct 06 2020 at 09:11):

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

view this post on Zulip Busiso Chisala (Oct 06 2020 at 09:20):

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?

view this post on Zulip Eric Wieser (Oct 06 2020 at 09:58):

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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 13:50):

@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

view this post on Zulip Busiso Chisala (Oct 06 2020 at 14:10):

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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 14:13):

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!

view this post on Zulip Heather Macbeth (Oct 06 2020 at 14:18):

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.)

view this post on Zulip Busiso Chisala (Oct 06 2020 at 14:29):

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 :(

view this post on Zulip Heather Macbeth (Oct 06 2020 at 14:35):

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)

view this post on Zulip Busiso Chisala (Oct 06 2020 at 14:54):

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 ...?

view this post on Zulip Reid Barton (Oct 06 2020 at 14:58):

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.

view this post on Zulip Reid Barton (Oct 06 2020 at 14:59):

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

view this post on Zulip Heather Macbeth (Oct 06 2020 at 15:17):

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.

view this post on Zulip Busiso Chisala (Oct 06 2020 at 15:27):

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 ?

view this post on Zulip Kevin Buzzard (Oct 06 2020 at 16:07):

You learn the tricks as time goes on

view this post on Zulip Kevin Buzzard (Oct 06 2020 at 16:08):

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

view this post on Zulip Busiso Chisala (Oct 06 2020 at 16:43):

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)

view this post on Zulip Frédéric Dupuis (Oct 06 2020 at 19:41):

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.

view this post on Zulip Heather Macbeth (Oct 06 2020 at 23:37):

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)?

view this post on Zulip Heather Macbeth (Oct 06 2020 at 23:38):

Likewise for subgroups, submodules, ...

view this post on Zulip Yakov Pechersky (Oct 06 2020 at 23:46):

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

view this post on Zulip Heather Macbeth (Oct 07 2020 at 00:18):

@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.

view this post on Zulip Kyle Miller (Oct 07 2020 at 00:25):

docs#set.inclusion

view this post on Zulip Heather Macbeth (Oct 07 2020 at 00:26):

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

view this post on Zulip Heather Macbeth (Oct 07 2020 at 00:27):

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

view this post on Zulip Heather Macbeth (Oct 07 2020 at 00:28):

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

view this post on Zulip Kyle Miller (Oct 07 2020 at 00:31):

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.

view this post on Zulip Kyle Miller (Oct 07 2020 at 00:32):

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

view this post on Zulip Heather Macbeth (Oct 07 2020 at 00:41):

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)

view this post on Zulip Bhavik Mehta (Oct 07 2020 at 00:42):

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

view this post on Zulip Heather Macbeth (Oct 07 2020 at 00:45):

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.)

view this post on Zulip Busiso Chisala (Oct 07 2020 at 07:33):

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 :)

view this post on Zulip Busiso Chisala (Oct 07 2020 at 07:42):

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?

view this post on Zulip Patrick Massot (Oct 07 2020 at 07:46):

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

view this post on Zulip Patrick Massot (Oct 07 2020 at 07:51):

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.

view this post on Zulip Busiso Chisala (Oct 07 2020 at 09:53):

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?

view this post on Zulip Scott Morrison (Oct 07 2020 at 10:27):

leanproject upgrade-mathlib

view this post on Zulip Scott Morrison (Oct 07 2020 at 10:27):

(or just leanproject up for short)

view this post on Zulip Scott Morrison (Oct 07 2020 at 10:27):

This assumes that you followed the #install instructions.

view this post on Zulip Scott Morrison (Oct 07 2020 at 10:28):

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.

view this post on Zulip Scott Morrison (Oct 07 2020 at 10:31):

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

view this post on Zulip Busiso Chisala (Oct 07 2020 at 13:15):

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.

view this post on Zulip Heather Macbeth (Oct 07 2020 at 13:49):

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

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 13:55):

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

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 13:57):

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)

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 13:58):

Make sure your mathlib is up to date and your leanproject

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 13:59):

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

view this post on Zulip Busiso Chisala (Oct 07 2020 at 14:17):

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?

view this post on Zulip Busiso Chisala (Oct 07 2020 at 14:17):

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

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 15:07):

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

view this post on Zulip Busiso Chisala (Oct 07 2020 at 15:22):

Kevin Buzzard said:

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

Will do


Last updated: May 06 2021 at 23:11 UTC