Defining the subspace of a vector space

Stream: new members

[Luiz Kazuo Takei]

I am trying to define the subspace of a vector space in this way:

structure Subspace (V : Type) [AddCommGroup V] [Module ℝ V] where
  carrier : Set V
  closed_under_add : v₁ ∈ carrier → b ∈ carrier → v₁ + v₂ ∈ carrier
  closed_under_smul : ∀ a : ℝ, v ∈ carrier → a • v ∈ carrier

and this works just fine.

But originally my closed_under_smul was defined like this:

  closed_under_smul : a ∈ ℝ → v ∈ carrier → a • v ∈ carrier

and this did not work (Lean does not like the a ∈ ℝ bit).

Why is that?

[Kenny Lau]

@Luiz Kazuo Takei because you're doing type theory, not set theory. The key difference of type theory is that everything you say has to live in a type. In set theory, when you say "x ∈ ℝ", the "x" there can mean anything. For example, $3+4i \in \Bbb{R}$ is a valid mathematical statement (and it is false), and you can also state the statement $\Bbb{R} \in \Bbb{R}$ (which is also false)

but in Lean (and type theory), every object you mention has to have a type. That means, when you say x, you already have to tell Lean what its type is. So you're not even allowed to write "ℝ ∈ ℝ".

In other words, a : ℝ means "the symbol "a" has type "ℝ" in the following", and a ∈ ℝ means nothing

[Luiz Kazuo Takei]

Thanks a lot @Kenny Lau! It was very informative!

I am still getting used to type theory (as opposed to set theory). Do you know any good (and short) reference for a mathematician to learn about type theory?

Any (or all) of these would be appreciated:

1. Motivation of the theory
2. Brief history of type theory
3. Basics of type theory and how it interacts with math in general (and set theory in particular)

[Kenny Lau]

#tpil is usually recommended for beginners
the motivation would be Curry--Howard correspondence which equates computer programs with proofs
and the basic fact you would need to know is that every expression has a unique type, with a rough correspondence:

math                 | type theory
h is a proof of p    | h : p
x is an element of s | x : s

uniqueness means that 2 : ℕ and 2 : ℤ are considered to be different expressions, in contrast with mathematics where ℕ ⊆ ℤ ⊆ ℚ ⊆ ℝ ⊆ ℂ; instead in Lean you get "canonical functions" going from left to right

[Julian Berman]

https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ is also a nice read.

[Jireh Loreaux]

@Kenny Lau I don't think Lean has unique typing.

[Dexin Zhang]

But theorem 4.1 of #leantt does say Lean has unique typing

[Michael Rothgang]

Jireh Loreaux said:

Kenny Lau I don't think Lean has unique typing.

Why do you think so? Can you elaborate?

[Henrik Böving]

Dexin Zhang said:

But theorem 4.1 of #leantt does say Lean has unique typing

Theorem 4.1 of #leantt has since come to be doubted by Mario but is hopefully fixable was my last update.