Qualification

Stream: general

[Neil Strickland]

The following situation is quite common. I have a family of types T α and maps supp : T α → set α, for example T α = list list α or T α = multiset α or T α = option α or T α = ℕ → α. In all these cases if supp x ⊆ s ⊆ α then in ordinary mathematical language I can "regard x as an element of T s". In Lean I have been calling this qualify x h : T s, where h is a proof that supp x ⊆ s. I then find that I need a long list of lemmas about this construction and its inverse.

Am I missing some kind of existing support for this? Is there a better/more standard name that qualify? Has anyone worked out a typeclass framework to treat all the different T's in parallel?

[Kevin Buzzard]

An example which @Chris Hughes had last week was a direct sum of modules over an index set α and an equality of two elements in this direct sum; for each element he had a subset of α where the support of the elements was known to lie, and s was the union of these two subsets. He then wanted equality of the restricted elements in the direct sum over s. I noted at the time that a mathematician would pass over this without any further comment.

[Jeremy Avigad]

Neil, as I described in my talk in Amsterdam, Mario, Simon, and I have been working on a method of defining data types as "quotients of polynomial functors": https://github.com/avigad/qpf. We were inspired by Isabelle's notion of a "bounded natural functor". Isabelle's BNFs come equipped with a natural transformation from T to set that has exactly the character you want. (I forget what they call it, but it is some cognate of set, IIRC.) We found that we can carry out the main constructions without supp, but it can be defined after the fact. For example, given x in T alpha, we can define supp x to be the union of the ranges of the "contents" parts of the representations of x. (We are grateful to Dmitry Traytel for this observation.)

We need to add another assumption to the definition of qpf for that supp to have all the right properties. For example, we can require that all the representations have the same range. Such an assumption will let us relate different ways of saying the same thing. For example, we can lift a predicate P on alpha to T alpha without supp, but if we have supp and the assumption above, saying that the lift of P holds of x will be the same as saying that P holds of every element in supp x.

We haven't worked out the details yet, and we do not have a general axiomatization of the properties that supp should satisfy. (Maybe the one I just mentioned is enough?) We also don't have a good list of properties to derive. So if you come up with a good list, please share it!

That said, you might want to take a look at the reference manual for the Isabelle datatype package. Whenever you define a BNF, their package outputs a list of constructions and theorems, and you can focus on the ones that mention their supp.

I am running off to teach now!

[Mario Carneiro]

@Neil Strickland

Am I missing some kind of existing support for this? Is there a better/more standard name that qualify? Has anyone worked out a typeclass framework to treat all the different T's in parallel?

There is no standard treatment of these functions, but there is a somewhat standardized name for when it comes up - cod_restrict. For example:

def linear_map.cod_restrict (p : submodule α β) (f : γ →ₗ[α] β) (H : ∀c, f c ∈ p) : γ →ₗ[α] p
def function.embedding.cod_restrict {α β} (p : set β) (f : α ↪ β) (H : ∀ a, f a ∈ p) : α ↪ p

The second assumption in each case is equivalent to supp f ⊆ p in your notation, but the details of how we want to say this vary from one pseudo-category to the next. list has a slight variation on cod_restrict called pmap which allows the function itself to be partial:

def list.pmap {p : α → Prop} (f : Π a, p a → β) : Π l : list α, (∀ a ∈ l, p a) → list β

[Neil Strickland]

Thanks. I will change the name to cod_restrict. I agree that that it is more convenient not to formulate things in terms of supp, although that might change if we tried to build a systematic framework covering all cases.