## Stream: new members

### Topic: inner product on subspaces

#### 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,},
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 (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 := ...

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

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

#### Eric Wieser (Oct 06 2020 at 09:58):

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

#### 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

#### 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


#### 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!

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

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

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

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

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

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

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

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

#### Kevin Buzzard (Oct 06 2020 at 16:07):

You learn the tricks as time goes on

#### 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

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

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

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

#### Heather Macbeth (Oct 06 2020 at 23:38):

Likewise for subgroups, submodules, ...

#### Yakov Pechersky (Oct 06 2020 at 23:46):

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

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

#### Kyle Miller (Oct 07 2020 at 00:25):

docs#set.inclusion

#### Heather Macbeth (Oct 07 2020 at 00:26):

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

#### Heather Macbeth (Oct 07 2020 at 00:27):

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

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

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

#### 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

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


#### 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

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

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

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

#### 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

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

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

#### Scott Morrison (Oct 07 2020 at 10:27):

leanproject upgrade-mathlib

#### Scott Morrison (Oct 07 2020 at 10:27):

(or just leanproject up for short)

#### Scott Morrison (Oct 07 2020 at 10:27):

This assumes that you followed the #install instructions.

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

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

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

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

#### 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

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

#### 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

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

#### 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

#### Kevin Buzzard (Oct 07 2020 at 15:07):

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

#### 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