Piling structures

Stream: lean4

[Sophie Morel]

When introducing a structure of type S that extends another structure of type S', if I already have a structure of type S', how do I tell Lean that I want to use it for the structure of type S ? Here is a toy example:

import Mathlib

universe U

structure test1 :=
(arbitrary : ∀ (𝕜 : Type U) [NontriviallyNormedField 𝕜], 𝕜)
(arbitrary_nonzero : ∀ (𝕜 : Type U) [NontriviallyNormedField 𝕜], arbitrary 𝕜 ≠ 0)

variable (t : test1)

lemma test2 (𝕜 : Type U) [Field 𝕜] (p : NontriviallyNormedField 𝕜) (q : NontriviallyNormedField 𝕜) :
(@test1.arbitrary t 𝕜 p) * (@test1.arbitrary t 𝕜 q) ≠ 0 := by
  simp only [ne_eq, mul_eq_zero]
  push_neg
  constructor
  . exact @test1.arbitrary_nonzero t 𝕜 p    -- type mismatch
  . sorry

Full error message:

type mismatch
  test1.arbitrary_nonzero t 𝕜
has type
  test1.arbitrary t 𝕜 ≠
    @OfNat.ofNat 𝕜 0
      (@Zero.toOfNat0 𝕜
        (@ExteriorAlgebra.instZero 𝕜
          (@NonUnitalNonAssocSemiring.toMulZeroClass 𝕜
            (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring 𝕜
              (@NonAssocRing.toNonUnitalNonAssocRing 𝕜
                (@Ring.toNonAssocRing 𝕜
                  (@NormedRing.toRing 𝕜
                    (@NormedCommRing.toNormedRing 𝕜
                      (@NormedField.toNormedCommRing 𝕜 (@NontriviallyNormedField.toNormedField 𝕜 p)))))))))) : Prop
but is expected to have type
  test1.arbitrary t 𝕜 ≠
    @OfNat.ofNat 𝕜 0
      (@Zero.toOfNat0 𝕜
        (@MulZeroClass.toZero 𝕜
          (@NonUnitalNonAssocSemiring.toMulZeroClass 𝕜
            (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring 𝕜
              (@NonAssocRing.toNonUnitalNonAssocRing 𝕜
                (@Ring.toNonAssocRing 𝕜
                  (@NormedRing.toRing 𝕜
                    (@NormedCommRing.toNormedRing 𝕜
                      (@NormedField.toNormedCommRing 𝕜 (@NontriviallyNormedField.toNormedField 𝕜 q)))))))))) : Prop

Here the variable t of type test1 is supposed to pick a nonzero element in every nontrivially normed field. (Auxiliary question: is putting instance arguments in the fields of a structure a Bad Idea ?)

Then I am playing around with a type 𝕜 that has two structures of nontrivially normed field called p and q, and I want to prove that the product of the nonzero elements is nonzero. Of course this should not work, because I have not told Lean that the two underlying field structures are the same, and my problem is that I don't know how to do that; I mean, I can probably tell Lean that p.toField = q.toField or something like that, but it seems like it would force me to do a huge amount of rewrites later; much better if p and q were just known to extend the same Field structure on 𝕜.
You can see how I tried by putting a Field instance on 𝕜 first, but it didn't work and Lean is using the field structure coming from q to in the simp step, if I am following well, and doesn't know that it has the same 0 as the other field structure. (Why there is an ExteriorAlgebra in the middle of all this, I am not sure.)

[Notification Bot]

Sophie Morel has marked this topic as resolved.

[Notification Bot]

Sophie Morel has marked this topic as unresolved.

[James Gallicchio]

I think having a hypothesis that they are equal might be the only reasonable approach here? but i'm not sure how that would interact with typeclass inference -- if you name the two instances and deconstruct them (to eliminate the field equality hypothesis) I don't know whether typeclass inference still knows that there's a NontriviallyNormedField there

[James Gallicchio]

is there a non-toy example where this is coming up? seems vaguely like abuse of typeclasses, but I don't know enough to say this is a bad idea >_<

[Patrick Massot]

Sophie, your issue is that in the statement it isn't clear what zero means since you have two completely unrelated field structures on $\mathbb k$.

[Patrick Massot]

Probably Lean picks one and then half of your goals become unprovable.

[Patrick Massot]

And see docs#mul_ne_zero

[James Gallicchio]

but the question is whether there is a clean way to say "i have two different NontriviallyNormedFields that are extensions of the same Field structure" (which might be an XY problem)

[Patrick Massot]

Oh, I actually didn't read Sophie's message at all. I saw she had a question, I copy-pasted the code and tried to guess the question...

[Patrick Massot]

I don't think there is any nice way to do that with those type class. You should probably try to use docs#IsAbsoluteValue.

[Yury G. Kudryashov]

I would consider two NontriviallyNormedFields with a RingEquiv between them. Answering wrong question too.

[Yury G. Kudryashov]

There is no way to say that you have 2 structures and their projections to a substructure agree. More precisely, you can create a new typeclass that extends both, then ask for it.

[Yury G. Kudryashov]

What do you actually want to do?

[Yaël Dillies]

This is a problem @María Inés de Frutos Fernández and I encountered. docs3#normed_ring is not quite the type of normed structures on a
ring since it includes the ring part, so instead we defined docs3#ring_norm

[Sophie Morel]

Thanks for all your answers. In the non-toy example, I want to talk about several semi-norms (and the associated topologies, which might be different) on a fixed vector space. I tried using the NormedSpace structure and ran into the problem that the vector space structures had no reason to be equal.

[Sophie Morel]

I might have to do something similar to what @Yaël Dillies mentioned, since I don't just want to have the semi-norms, I also need the induced topologies (probably uniform structures, actually) and all the stuff that comes with it. Yay...

[Sophie Morel]

(Another solution would be to have two NormedSpace structures with an isomorphism of vector fields between them. It might be easier in this case, I need to think about it.)

[Yury G. Kudryashov]

We have docs#Seminorm

[Sophie Morel]

Thanks! So this is another possibility. Does there also exist a way to make a space with a Seminorm into a NormedSpace ? (I am trying to use constructions that I can only find for NormedSpace.) If not, I guess I could write it myself, in case my other approach does not work well.

[Yury G. Kudryashov]

We have docs#AddGroupSeminorm.toSeminormedAddGroup
Not sure about a NormedSpace version.

[Sophie Morel]

Thanks! This is most of the way to NormedSpace already.

[Sophie Morel]

Well, I ended up writing a Seminorm.toNormedSpace definition, and I have to mix it with NormedSpace instances to make stuff work. Thanks again to everybody who helped!

Also, I needed a corollary of Hahn-Banach that was lightly more general than https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.html#exists_dual_vector, because my space only had a semi-norm, so I had a SeminormedAddCommGroup instance and that result requires a NormedAddCommGroup instance. More precisely, the result was this:

exists_dual_vector''_sn.{U} (𝕜 : Type U) [inst✝ : IsROrC 𝕜] {E : Type U} [inst✝¹ : SeminormedAddCommGroup E]
  [inst✝² : NormedSpace 𝕜 E] (x : E) : ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖

which I deduced from this:

exists_dual_vector_sn.{U} (𝕜 : Type U) [inst✝ : IsROrC 𝕜] {E : Type U} [inst✝¹ : SeminormedAddCommGroup E]
  [inst✝² : NormedSpace 𝕜 E] (x : E) (h : ‖x‖ ≠ 0) : ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖

I proved it by very slightly generalizing a bunch of results like ContinuousLinearEquiv.coord from NormedAddCommGroups to SeminormedAddCommGroups by replacing conditions like x ≠ 0 with ‖x‖ ≠ 0, which was not hard but a bit longuish. A more natural approach for a mathematician would be to go through the quotient of the space by the kernel of the semi-norm, but I don't know if that's in mathlib. So my question:

(1) Is the construction of a normed space (or module/group/etc) from a seminormed one by taking the quotient by the kernel of the seminorm in mathlib ?

(2) Would it be worth having the slightly more general Hahn-Banach corollary in mathlib ?

[Kevin Buzzard]

For (2) -- if you needed it, that's evidence that it should be in the library, and mathlib4 is now open for business!

[Sophie Morel]

@Kevin Buzzard But then I also need to answer (1), so I can decide what the "best" proof is. (I found Mathlib.Analysis.Normed.Group.Quotient so seminorms on quotients exist, but I did not find the norm on the separation yet.)