Teaching functions

Stream: maths

[Gihan Marasingha]

For those using Lean for teaching mathematics, how do you treat the notion of function?

Until this year, I've taught my beginning undergraduates that a function is a triple $(A, B, C)$ of sets where $C \subseteq A \times B$ with the properties:

1. $\forall a \in A, \exists b \in B, (a,b) \in C$ and

2. $\forall a \in A, \forall b_1 b_2 \in B, (a,b_1) \in C \land (a,b_2) \in C \to b_1 = b_2$.

The type-theoretic notion of a function as a named lambda abstraction does away with the distinction between functions that have the same 'map' but different domains or codomains. I see that data.set.function provides, for example, inj_on to define what it means for a (type-theoretic) function to be injective on a set. But this moves the notion of domain of a function to the definition of injectivity, rather than treating it as part of the definition of the function. That's fine, but it isn't the same notion of function as that given above.

My question to those teaching undergraduate maths with Lean is: do you just work with the type-theoretic definition? If not, do you use inj_on to define injectivity, or do you do something else entirely?

[Yury G. Kudryashov]

In Lean each function knows its domain: f : α → β has domain α.

[Yury G. Kudryashov]

If we want to study this function on a subset of its domain, then we introduce an auxiliary s : set α and define docs#set.inj_on etc

[Yury G. Kudryashov]

docs#function.injective does not use any sets

[Gihan Marasingha]

OK, so is the best solution not to worry about the distinction between sets and types?

When we use inj_on to look at a function on a subset of its domain, then the new domain is not part of the function, but has been moved into the position of being an argument of inj_on. To me, this is a different definition of function than that which I'm used to, but I accept that it's the most natural definition as far as Lean is concerned.

My view would be that α and β aren't domains and codomains in the traditional sense, as they aren't sets. Rather, to reconcile with the set-theoretic notion of function, a function would consist of a triple A : set α, B : set β, C : set α × β with the above properties, but this seems overly complicated and hard to work with in Lean.

[Reid Barton]

For most (math) purposes the correct mapping is "set" = Type, "subset" = set

[Floris van Doorn]

When I explain functions, I like to explain that a function is a mathematical procedure that takes a certain class of inputs to an output. A function "knows" what its inputs can be (its domain), and what its potential outputs can be (its codomain).

The definition you gave is an encoding of that idea in set theory. I don't think what you wrote has to be the definition, it just the most convenient encoding of the mathematical idea of a function in set theory. In type theory there is a different encoding (which is hardly an encoding, since functions are a primitive notion in type theory).

The idea that functions have the same 'map' but different domains and codomains looks a little different in type theory than in set theory, but you can find analogues of everything in one theory in the other theory. In type theory, two maps cannot be "the same" without having the same domain and codomain, but I don't think that is an essential feature of function.
If you have A → B and C ⊆ A you can still restrict your function to C in both set theory and type theory. In set theory, the "map" of your new function will be a subset, in type theory it will use subtype.rec, if we encode C as a subtype of A.

[Reid Barton]

e.g. "A group is a set $G$ equipped with a binary operation $m : G \times G \to G$ and ..." -> (G : Type) (m : G -> G -> G)
"A subgroup $H$ of a group $G$ is a subset $H \subset G$ such that ..." -> (H : set G) ...

[Reid Barton]

(This works better with a "structural" idea of what a set is, e.g., "an object of the category of sets", rather than a "material" one as in a set theory like ZFC)

[Gihan Marasingha]

Thanks everyone. That makes sense and will save a lot of faffing about. I suspect students will find the type-theoretic notion to be more natural that the set-theoretic one anyway.

[Patrick Massot]

@Gihan Marasingha did you have a look at the tutorials project? It's almost only a translation into English of the Lean files I use with first year undergrads (double major in math and computer science). The only differences are a couple of efficiency optimizations (saving a couple of lines of Lean code using rintros instead of intros followed by cases, things like that). The question you asked here simply do not arise. Functions in (dependent) type theory is just way closer to actual mathematical intuition that the set theory bullshit we sometimes have to pretend to believe when teaching.

[Yury G. Kudryashov]

E.g., the type-theoretic notion corresponds to function types in programming languages:

double sqr (double x) { return x * x; }

corresponds to

def sqr : double → double := λ x, x * x

[Kevin Buzzard]

Floris said

When I explain functions, I like to explain that a function is a mathematical procedure that takes a certain class of inputs to an output. A function "knows" what its inputs can be (its domain), and what its potential outputs can be (its codomain).

I shy away from saying exactly what kind of procedure it is -- if I prove that for all f :R -> R, if f is differentiable then it is continuous, the f in that argument is not something defined by a mathematical procedure

[Kevin Buzzard]

But just to add to the chorus Gihan -- the A and B you have in your definition are definitely types in Lean. All the intuition goes through.

[Gihan Marasingha]

@Patrick Massot yes, I really enjoyed the tutorial project! I learned much about Lean (including rintros) from it. Fortunately, my high-school French was sufficient to understand the only text that remained untranslated: "Ce n'est pas cela. Essayez encore".

@Kevin Buzzard: according to Liebeck, 'A function from $S$ to $T$ is a rule that assigns to each $s \in S$ a single element of $T$'. Is 'rule' different from 'procedure' or has M1F changed since the 1990s? ;)

All: I like the type-theoretic approach and I agree that it's more natural in many ways (the definition of function being a case in point) than the set-theoretic approach. I'm lucky to have the freedom to try this, but not all of my colleagues are sold on teaching mathematics formally (one said 'Buzzard can do this at Imperial, but...'). That's one of the reasons for raising the set / type issue as it relates to functions.

I hope others will come round eventually. This is reminiscent of the Bourbaki-influenced changes in teaching last century.

[Johan Commelin]

People are still bashing Bourbaki, right?

[Patrick Massot]

Gihan Marasingha said:

yes, I really enjoyed the tutorial project! I learned much about Lean (including rintros) from it. Fortunately, my high-school French was sufficient to understand the only text that remained untranslated: "Ce n'est pas cela. Essayez encore".

Good catch! I just translated it. But really, the message is that good (but not elite) first year students can handle those exercises.

[Patrick Massot]

Gihan Marasingha said:

I'm lucky to have the freedom to try this, but not all of my colleagues are sold on teaching mathematics formally (one said 'Buzzard can do this at Imperial, but...').

You can tell them "Massot can do that at Orsay too".

[Patrick Massot]

Actually I use Lean for teaching much more than Kevin since I have 50 students each year which have a mandatory mathematics course using Lean.

[Patrick Massot]

Johan Commelin said:

People are still bashing Bourbaki, right?

Some people like to do that, but they will never undo the effect that Bourbaki had on mathematics.