Showing a subset that's a vector space contains zero

Stream: new members

[Martin C. Martin]

I have a definition of vector_space F V that extends has_zero V. I want to show that any subset of the vector space, where the subset itself is a vector space, contains zero. But I think I'm struggling with the syntax.

I'm using set_like so I can treat my subset as a type:

structure subset_of_vector_space (F : Type*) (V : Type*)
  [field F] [vector_space F V]:=
(carrier : set V)

namespace subset_of_vector_space

variables (F : Type*) {V : Type*} [field F] [vector_space F V]
variable {v : V}


instance : set_like (subset_of_vector_space F V) V :=
⟨ subset_of_vector_space.carrier, λ p q h, by cases p; cases q; congr'⟩

@[simp] lemma mem_carrier {p : subset_of_vector_space F V} : v ∈ p.carrier ↔ v ∈ (p : set V) := iff.rfl

@[ext] theorem ext {p q : subset_of_vector_space F V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q := set_like.ext h

theorem contains_zero {p : subset_of_vector_space F V} [h : vector_space F p] : (0 : V) ∈ p :=
begin
  sorry
end

end subset_of_vector_space

Neither rw has_zero V nor use h.zero work. Should I be stating the theorem differently? Am I missing a ↥ somewhere? How can I prove this?

[Riccardo Brasca]

The problem is that you're providing a new vector space structure to p, completely unrelated to V

[Riccardo Brasca]

If you want a predicate saying that a subset is a subspace you have to define it by hand I think (meaning it's not in mathlib, not even in deprecated)

[Eric Wieser]

vector_space F V that extends has_zero V

This is a "dangerous instance", and won't actually work

[Eric Wieser]

See https://arxiv.org/abs/2202.01629 for a short explanation

[Martin C. Martin]

Eric Wieser said:

vector_space F V that extends has_zero V

This is a "dangerous instance", and won't actually work

Isn't this what mathlib does with groups? For example: https://github.com/leanprover-community/mathlib/blob/36938f775671ff28bea1c0310f1608e4afbb22e0/src/algebra/group/defs.lean#L312

[Yaël Dillies]

Yes, but that's not comparable. A group involves a single type. A vector space involves two: the additive group and the field of scalars. Your instance applies to the additive group for any (understand "unknown to Lean") field of scalars.

[Jireh Loreaux]

Martin, to understand the problem, imagine it from Lean's perspective. The user gives you some type V and then later uses 0 : V. In order for this to make sense, you (i.e., Lean) need to find a has_zero V instance. If you have one on hand, great, but what if you need to go hunting? You look around at what you have available, and you see that if you can find a vector_space F V instance on V, that will entail a has_zero V instance. But you weren't given F when the user specified 0 : V. So which F should you pick? Well, you're Lean, so you go hunting forever trying to see whether V is a vector space over any possible choice of F, which is generally doomed to failure (or at least an unimaginably long search). You may even give up and say, "I have no idea how in the world to choose F". This is the essence of the dangerous instance issue.

[Jireh Loreaux]

Note how the instance add_group V → has_zero V does not exhibit the same problem (as Yaël mentioned) because there are no unspecified parameters.

[Martin C. Martin]

Ah got it, thanks!

[Martin C. Martin]

The fact that module F V doesn't directly specify the group structure on V, but kind of expects the user to provide that separately, means you don't have the problem there?

[Martin C. Martin]

I see that module doesn't extends add_comm_monoid, but rather has it in square brackets [add_comm_monoid M]. Interesting, thanks.

[Martin C. Martin]

Jireh Loreaux said:

Martin, to understand the problem,

Thanks, it was very help to read this explanation, rather than skimming an 18 page short explanation.

[Martin C. Martin]

So I'm updating my vector_space definition to pull out has_add, has_zero and has_neg. However, now any theorem about vector spaces, e.g. that the additive identity is unique, no longer has just [vector_space F V], but rather [has_add V] [has_zero V] [has_neg V] [vs : vector_space F V]. Is there a way to encapsulate all those into a single definition, so I don't need to repeat all 4 on every theorem? Is this what abbreviation does?

[Kevin Buzzard]

In mathlib3 you would just do [add_comm_group V] [vector_space F V]. In mathlib4 you can use the variable! command to avoid even [add_comm_group V].

[Martin C. Martin]

Thanks Kevin. Not wanting to bring in abstract algebra concepts, I defined my own class that extends those three, with nothing else. However, now when I try to use a lemma, something fails:

import algebra.field.basic


@[ext]
class add_zero_neg (V : Type*) extends has_add V, has_zero V, has_neg V

@[ext]
class vector_space (F : Type*) (V : Type*) [field F] [add_zero_neg V]
  extends has_smul F V :=
(add_comm : ∀ u v : V, u + v = v + u)
(add_assoc : ∀ u v w : V, (u + v) + w = u + (v + w))
(add_zero : ∀ v : V, v + 0 = v)
(add_right_inv : ∀ v : V, v + -v = 0)
-- Deleted all unused vector space axioms, to make a minimal example.

variables {F : Type*} [field F]


namespace vector_space

lemma zero_add {V : Type*} [field F] [add_zero_neg V] [vs: vector_space F V] {v : V} : 0 + v = v :=
sorry

theorem unique_add_inv {V : Type*} [add_zero_neg V] [vs : vector_space F V] (v w : V):
  v + w = 0 → w = -v :=
begin
  intro h,
  calc w = w + 0 : by rw vs.add_zero
  ...    = w + (v + -v) : by rw ← vs.add_right_inv
  ...    = (w + v) + -v : by rw vs.add_assoc
  ...    = (v + w) + -v : by rw vs.add_comm w v
  ...    = 0 + -v : by rw h
  ...    = -v : by rw zero_add -- "failed to synthesize type class instance for field ?m_1"
end

end vector_space

If I make the field an explicit argument to zero_add, I get "there are unsolved goals, vector_space F V". How can I proceed?

[Kevin Buzzard]

The problem is that you are proving zero_add for vector spaces when it's a theorem about add_comm_groups, so Lean is having to find a field and it doesn't know where to look. If you insist on not developing the theory of add_comm_groups then you will have to make F an explicit input to zero_add (like it is to vector_space) and then zero_add will become usable.

[Kevin Buzzard]

The easiest solution is just to add zero_add and add_left_inv as axioms for vector_space. By omitting them you are saying "I will develop some of the theory of add_comm_group myself" but you seem to be resistant to this.

[Martin C. Martin]

Thanks. Making the field explicit didn't work, but making the vector_space explicit did work. I guess I still think of V as the vector space, as we tend to do in math, and forget that the vector_space is a separate object in Lean.

I'm trying to formalize Linear Algebra Done Right, and want to stick as close as I can to its pedagogy. It doesn't bring in the concept of group, presumably considering it an extra complication, so I'd like to keep thing simple in the same way, if possible.

Note that there must be something else going on here than just "can't find the vector_space", since if I get rid of my add_zero_neg class and explicitly list [has_add V] [has_zero V] [has_neg V] everywhere, everything works. So it's something about collecting those three into their own class that's confusing it.

[Eric Wieser]

It doesn't bring in the concept of group, presumably considering it an extra complication, so I'd like to keep thing simple in the same way, if possible.

In that case I'd recommend two typeclasses, vector_space_aux V and [field K] [vector_space_aux V] : vector_space K V. You don't need to worry about the mathematical meaning of the second, but Lean is going to be annoying if you write lemmas about vector_space K V which have nothing to do with K.

[Eric Wieser]

Note that there must be something else going on here

Without a #mwe with your changes it's hard to help you diagnose

[Martin C. Martin]

Thanks Eric. My code above is an #mwe, does it not work in Lean 3 for you?

[Eric Wieser]

Martin, my point is that you say in your message above that you tried a bunch of things that did and didn't work, but you didn't show the code for them; I think making K explicit would work, so my assumption is that you're not actually doing what I'm thinking of.

[Eric Wieser]

Your earlier post is a great #mwe, but it doesn't help once you start having problems with a modified version!

[Eric Wieser]

This is wrong:

variables {F : Type*} [field F]

namespace vector_space

lemma zero_add {V : Type*} [field F] [add_zero_neg V] [vs: vector_space F V] {v : V} : 0 + v = v :=

You wrote [field F] twice, so this means "let F have two unrelated field structures; two different 0s, two different +s, etc"

[Martin C. Martin]

Ah, thanks. Let me see if I can recreate things, and give all variants as #mwe s.

[Eric Wieser]

Here's the answer to your problem anyway; to make it work you need rw zero_add F (_ : V) instead of rw zero_add (after making F and v explicit)

[Yakov Pechersky]

Martin C. Martin said:

I'm trying to formalize Linear Algebra Done Right, and want to stick as close as I can to its pedagogy.

I think Axler is great for giving motivating theory and building good intuition on the topic. But following a pedagogical style might not be easy because it might clash with the requirements of formalization. For example, consider the difficulty in formalizing the concept of dimension and existence of maximally linearly independent sets. I don't think, for Axler, diving into Zorn and AC is that critical.

Another example is something that is very familiar from elementary school arithmetic - decimal notation for numbers. We write 1/3 = 0.666... or 0.66 bar, and that 0.99 bar is 1, but actually formalizing that decimal expansions represent the same real or rational, don't add anything to an understanding of addition.

[Jireh Loreaux]

Martin, the main problem I see with your approach of eschewing mathlib is that you will end up developing an entire linear algebra library on your own, and if the mathlib community has spent years developing this library with lots of contributors, that means such a task is a lot of work. Moreover, if people learn from the library you build, their knowledge (of the formalized version in Lean) won't transfer that well to mathlib.

[Martin C. Martin]

Jireh, thanks for the insight. The project is to cast the book Linear Algebra Done Right into Lean. The goal is for those who are familiar with linear algebra from their undergraduate education, but not familiar with Lean, to see how something familiar to them would be cast in Lean. Like a Rosetta stone. A second goal is to discover any missing parts of mathlib that are needed to prove all the theorems in LADR.

As such, the plan is to "build it and throw away." So once we've defined vector_space as a way to show how to build structures in mathlib, and prove some basic theorems such as the uniqueness of the inverse, we throw it away and use the built in mathlib module. This is the technique followed in e.g. Theorem Proving In Lean and The Complex Numbers Game.

I guess a third goal is for me to learn how all this stuff works, so I can contribute to mathlib some day. :)

[Martin C. Martin]

So it seems the best tradeoff is to split vector_space into to classes and create an add_comm_group class, and put all the relevant vector_space axioms in there, leaving just the ones involving scalar multiplication in vector_space. Like mathlib but unlike Axler. The alternative is to make the vector_space argument to various theorems explicit, but that seems worse.

[Jireh Loreaux]

There is pedagogical advantage to doing the split the mathlib way also: it forces students to confront the fact that a bunch of these axioms are only about +, 0, -! This is something I try to emphasize whenever I teach linear algebra, but they don't seem to strongly grasp; most of the time they just think of the axioms as a big list all lumped together and they have trouble remembering them.

[Eric Wieser]

Like mathlib but unlike Axler.

I would guess that Axler says nothing about class; so

class vector_space.aux (V : Type*) extends has_add V, has_neg V, has_zero V :=
(add_comm : _) -- etc
class vector_space (K V : Type*) [field K] [vector_space.aux V] extends has_smul K V :=
-- etc

is not really any less accurate a translation than the one that uses class just once.

Of course, it's mathematically more useful to call that add_comm_group rather than vector_space.aux, but if you really wanted to you could stick with the aux name and insist on not using mathematical words that are avoided by Axler.

[Martin C. Martin]

Thank you to everyone in this thread, the feedback has been very helpful. Here's the latest rendering of vector_space, as defined in section 1.B of LADR. Any other feedback, insights or improvements?

[Scott Morrison]

Another approach would be to write a document that states all the theorems from Axler (more generally, your favourite elementary textbook), giving as proofs the appropriate invocations of mathlib lemmas, or short proofs in terms of mathlib lemmas if a single lemma isn't available. Presumably you'll find the occasional statement where you really need to work, and then those can be contributed back to mathlib.

At the end you get a document that:

• is perhaps accessible to someone who knows that book but not mathlib
• perhaps is helpful to learning what is in mathlib and how to make use of it
• demonstrates that mathlib has sufficient coverage to formalise the book

This approach, however, relies on a certain amount of pedagogical flexibility, because it will only really work if you use mathlib's definitions, and don't make any attempt to replace them with hand-rolled versions.

[Scott Morrison]

I made some attempt at following this approach in the mathlib file docs/tutorial/representation_theory/etingof.lean (formalising Etingof's excellent book on representation theory), although didn't get nearly as far as I'd hoped.

(Partly because this was more advanced material, that mathlib doesn't have yet, so I was formalising as I went along, and partly because other priorities got in the way.)

[Eric Wieser]

That's also what I've been doing with https://github.com/eric-wieser/lean-matrix-cookbook; but if your goal is to demonstrate how to prove things, and not just that mathlib already knows the proof, it might not be as pedagogically useful