(re)defining vector spaces while allowing for subspaces

Stream: new members

[Nilay Patel]

Hi everyone, I'm Nilay, a CS PhD student working on a project with Lean. Wow, it's tough! I'm still brand new, so please forgive any grievous mistakes.

Problem introduction

Part of the project involves redefining things a bit more explicitly. I've been working on redefining a vector space, and here's what I've got so far:

class vector_space_over_reals (V : Type*) [has_smul ℝ V] [has_add V] [has_zero V] :=
  (smul : ℝ → V → V  := has_smul.smul)
  (add : V → V → V := has_add.add)
  (add_comm : ∀ (v w: V), v + w = w + v)
  (add_smul : ∀ (a b : ℝ) (v: V), (a + b) • v = (a • v) + (b • v))
  (has_one : ∀ (v : V), (1 : ℝ) • v = v)
  (has_inv : ∀ (v : V), ∃ (w : V), v + w = (0 : V))

(I'm not worrying about generalizing it to any field yet, just sticking to ℝ is good enough.)

Here's an example instantiation for ℝ × ℝ given that it's a module:

-- (ℝ × ℝ) is an ℝ-module
instance prod.module [module ℝ ℝ] : module ℝ (ℝ × ℝ) :=
  { add_smul := λ a b v, prod.mk.inj_iff.mpr ⟨add_smul a b v.fst, add_smul a b v.snd⟩
  , zero_smul := λ ⟨x, y⟩, prod.mk.inj_iff.mpr ⟨module.zero_smul x, module.zero_smul y⟩}

-- (ℝ × ℝ) is an ℝ-vector space
instance prod.is_vector_space [field ℝ] [module ℝ (ℝ × ℝ)] : vector_space_over_reals (ℝ × ℝ) :=
  { smul := default
  , add := default
  , add_comm := prod.add_comm_monoid.add_comm
  , add_smul := begin intros, rw prod.module.add_smul, end
  , has_one := begin simp end
  , has_inv := begin intros, existsi -v, simp, end
}

I could be way off with these, but I hope they're at least reasonable.

Problem with subspaces

The problem happens when I try to define a subspace. This definition is based on how subsemigroups are defined in mathlib:

class subspace (V : Type*) [add_comm_monoid V] [has_smul ℝ V] [module ℝ V] [vector_space_over_reals V] :=
  (carrier : set V)
  (add_mem : (∀ {v w : V}, v ∈ carrier → w ∈ carrier → v + w ∈ carrier))
  (smul_mem : (∀ {r : ℝ}, ∀ (v : V), v ∈ carrier → r • v ∈ carrier))

However, I have no idea how to prove that a subspace is a vector space. This instance looks totally wrong...

instance subspace_is_vector_space
  {V : Type*} [add_comm_monoid V] [has_smul ℝ V] [module ℝ V] [vector_space_over_reals V]
  (carrier : set V)
  [add_comm_monoid carrier] [has_smul ℝ carrier] [module ℝ carrier] [vector_space_over_reals carrier]
  : subspace V :=
  { carrier := carrier
  , add_mem := sorry
  , smul_mem := sorry}

Reversing the definition

It would be way more helpful for me if I could define it the other way around:

• definition: a subset U of a vector space V is a subspace if U is also a vector space
• theorem: if a subset U of a vector space V is closed under addition and scalar multiplication, it's a subspace

I tried doing this but got nowhere, fast. My attempt was basically trying to define a subtype:

def U : Sort* := {x : V // x ∈ carrier}

and try to build the definition of subspace from that. Unfortunately I don't have the attempt saved anymore, but could something like this work? I feel like subtypes are the right thing to use in a type-theory-based language, but my brain is hard-wired for sets still.

Summary:

• Is my definition for vector_space_over_reals a good one? Is there anything I can do to improve it?
• Is my definition for subspace correct? If it is, how do I even begin proving add_mem and smul_mem? I tried for a bit and got nowhere.
• Is it possible to reverse the definitions for subspace? That is, start with "a subspace is a vector space", and then show if a subset is closed under add/smul then it's a vector space?
• Can I define a subspace as a vector space over a subtype, where the subtype is just restricted to a particular set?

Any and all help is very much appreciated, thanks in advance!

[Yaël Dillies]

Your translation of "a subspace is a vector space" is wrong. Currently, it rather reads "A vector space structure over a random set of a vector space gives a vector subspace", which is most definitely wrong (the two vector space structures can be completely unrelated).

[Yaël Dillies]

Also note that [has_smul ℝ V] [module ℝ V] gives two (possibly different) meanings to r • v.

[Yaël Dillies]

What you rather want is

variables {V : Type*} [add_comm_monoid V] [has_smul ℝ V]
  [vector_space_over_reals V] (S : subspace V)

instance subspace.add_comm_monoid : add_comm_monoid S.carrier := sorry

instance subspace.has_smul : has_smul ℝ S.carrier := sorry

instance subspace.vector_space_over_reals : vector_space_over_reals S.carrier := sorry

[Nilay Patel]

Currently, it rather reads "A vector space structure over a random set of a vector space gives a vector subspace", which is most definitely wrong (the two vector space structures can be completely unrelated).

Right, that makes sense. I've copied your fix, but one thing is a bit unclear:

instance subspace.vector_space_over_reals : vector_space_over_reals S.carrier := sorry

Since S.carrier is a particular set of the type set V, is vector_space_over_reals S.carrier constructing a vector space structure over the set S.carrier? And if so, is Lean automatically converting the set S.carrier into a type? Can I then use it like let x : S.carrier or something?

Thanks again Yaël.

[Junyan Xu]

Yes, a set can be automatically treated as a type via docs#set.has_coe_to_sort

[Nilay Patel]

Thank you Junyan!

[Kevin Buzzard]

In prod.module the assumption [module \R \R] means "let the reals be given a totally random vector space structure over the reals" (so eg 2 \bub 1 could be 37), which is probably not what you want.

[Eric Wieser]

Also, smul := default does not use your default from earlier, it sets a • b = default = 0 everywhere

[Nilay Patel]

Kevin Buzzard said:

In prod.module the assumption [module \R \R] means "let the reals be given a totally random vector space structure over the reals" (so eg 2 \bub 1 could be 37), which is probably not what you want.

So instead, I should be instantiating a specific module structure for module \R \R and then removing the assumption?

instance real.is_module : module ℝ ℝ := sorry
instance prod.is_module : module ℝ (ℝ × ℝ) := sorry

[Nilay Patel]

Eric Wieser said:

Also, smul := default does not use your default from earlier, it sets a • b = default = 0 everywhere

Fascinating...not sure I totally understand. Where is the default coming from then? Is that from a different typeclass?

[Kyle Miller]

default is from docs#inhabited, which the real numbers implement.

[Kyle Miller]

right here: https://github.com/leanprover-community/mathlib/blob/83871f6cff322a1eafaa382ef70e9515fe240abd/src/data/real/basic.lean#L152

[Nilay Patel]

Ah I see. Thanks!

[Nilay Patel]

So going back to one of my initial questions:

It would be way more helpful for me if I could define it the other way around:

• definition: a subset U of a vector space V is a subspace if U is also a vector space
• theorem: if a subset U of a vector space V is closed under addition and scalar multiplication, it's a subspace

I've been working on this a little, and this is what I came up with so far:

class subspace' (V : Type*)
  -- given a vector space structure on V
  [add_comm_monoid V] [module ℝ V] [parent_space : real_vector_space V] :=
  -- a subspace is a subset that also has a vector space structure
  (carrier : set V)
  [is_monoid : add_comm_monoid carrier]
  [is_module : module ℝ carrier]
  [is_vector_space : real_vector_space carrier]
  -- ... and has the same smul/add operations as V
  (same_smul := ∀ (r : ℝ) (v : carrier), ((is_vector_space.smul r v) : V) = parent_space.smul r (v : V))
  (same_add := ∀ (w v : carrier), (w + v : V) = (v : V) + (w : V))

I'm interpreting this definition as: "Given a vector space on V, a subspace is a subset carrier which itself has a vector space structure whose smul and add operations are the same as V's smul and add.

Is this right, or am I misinterpreting?

I tried just doing (same_smul : is_vector_space.smul = parent_space.smul) but of course the types don't exactly line up. Maybe there's something more concise along those lines...

Thanks yet again, you've all been very helpful.

[Eric Wieser]

you might need a same_zero field too unless you can prove that from the other fields. That approach looks like it ought to work, but it's a rather strange design still.

[Eric Wieser]

Can you show the latest version of real_vector_space too?

[Reid Barton]

The :=s in the fields should be :s.