## Stream: maths

### Topic: universe hell in linear algebra

#### Patrick Massot (Aug 07 2020 at 15:15):

Is there a user guide to universe hell fighting in linear algebra? For instance:

variables  {K : Type*}  [field K] {V : Type*} [add_comm_group V] [vector_space K V] [finite_dimensional K V]
{n : ℕ} {v : fin n → V}

lemma le_of_linear_independent (h : linear_independent K v) : n ≤ findim K V :=


#### Patrick Massot (Aug 07 2020 at 15:16):

It looks like docs#finite_dimensional.fintype_card_le_findim_of_linear_independent would help but it assumes the indexing type is in the same universe as the vector space.

what hell?

#### Mario Carneiro (Aug 07 2020 at 15:33):

I don't see anything troubling in this snippet

#### Patrick Massot (Aug 07 2020 at 15:33):

The trouble is in the proof.

#### Patrick Massot (Aug 07 2020 at 15:34):

Because fin n and V live in different universes, you cannot apply the lemma I linked to.

#### Floris van Doorn (Aug 07 2020 at 15:35):

The lemma has the note

-- Note here we've restricted the universe levels of ι and V to be the same, for convenience.


I think generalizing this lemma to arbitrary universe levels is a better use of time than writing a user guide to work around it.

#### Mario Carneiro (Aug 07 2020 at 15:36):

For whose convenience?

#### Floris van Doorn (Aug 07 2020 at 15:36):

The prover of the lemma, presumably.

#### Patrick Massot (Aug 07 2020 at 15:37):

My question is: how to prove a general version of such lemmas where it's convenient to assume universe equalities?

#### Floris van Doorn (Aug 07 2020 at 15:38):

after you have proven the lemma, apply it to ulift \i and ulift V, and then massage the statement along equivalences to get it for \i and V.

This assumes you have proven that every component of the (statement of the) lemma is invariant under equivalences.

#### Patrick Massot (Aug 07 2020 at 15:39):

Mario, what Floris wrote is what I called universe hell.

#### Mario Carneiro (Aug 07 2020 at 15:39):

Alternatively, just use the theorem that talks about lift (mk A) instead of mk A when using the cardinal library

#### Mario Carneiro (Aug 07 2020 at 15:39):

the proof is exactly as long, you just use different lemmas

#### Patrick Massot (Aug 07 2020 at 15:41):

This sounds promising.

#### Patrick Massot (Aug 07 2020 at 15:44):

Except I have no idea how to turn it into Lean code.

#### Mario Carneiro (Aug 07 2020 at 15:45):

I'm working on it

Thanks a lot!

#### Floris van Doorn (Aug 07 2020 at 15:45):

I think the fintype.card library is not as consistent as the cardinal library, but there is fintype.​card_ulift which requires one more step.

#### Floris van Doorn (Aug 07 2020 at 15:56):

import linear_algebra.finite_dimensional

variables  {K : Type*}  [field K] {V : Type*} [add_comm_group V] [vector_space K V] [finite_dimensional K V]
{n : ℕ} {v : fin n → V}

open finite_dimensional

lemma ulift.down.injective {α} : function.injective (ulift.down : ulift α → α) :=
by { rintro ⟨x⟩ ⟨y⟩ h, dsimp at h, rw h }

lemma le_of_linear_independent (h : linear_independent K v) : n ≤ findim K V :=
begin
have : linear_independent K (v ∘ ulift.down) :=
linear_independent.comp h _ ulift.down.injective,
convert finite_dimensional.fintype_card_le_findim_of_linear_independent this,
simp,
end


#3721

#### Mario Carneiro (Aug 07 2020 at 16:13):

Floris's suggestion is good for when you don't want to change the library, but it is better in this case to just already have the universe generalized versions of all the lemmas

#### Patrick Massot (Aug 07 2020 at 16:13):

Sure. Thank you very much to both of you anyway.

#### Kevin Buzzard (Aug 07 2020 at 16:36):

Patrick -- come back to Type! All your universe problems will melt away!

#### Utensil Song (Aug 08 2020 at 08:06):

I think in this topic I've learned something opposite to the other topic:

Even if we can put the universe issue aside at the beginning, one day we'll have to come back to give it a proper treatment.

This topic provides two methods to deal with the situation, both seem not costly, but both are hard to decipher, especially the changes in #3721 look totally random, I'm seeing the 's on u v w, Type*, lemma {m}, _s and maxs, and have no idea how the universes are arranged and by any chance u and u' (for example), m and others, * and others are related in the arrangement. There's so much magic in one page...

#### Utensil Song (Aug 08 2020 at 08:10):

Floris van Doorn said:

after you have proven the lemma, apply it to ulift \i and ulift V, and then massage the statement along equivalences to get it for \i and V.

This assumes you have proven that every component of the (statement of the) lemma is invariant under equivalences.

The massage seems to have a pattern, is turning this into a reusable tactic possible?

#### Patrick Massot (Aug 09 2020 at 15:00):

I have a variation on universe issues in linear algebras:

example {ι K V : Type*} [field K] [add_comm_group V] [vector_space K V]
[finite_dimensional K V] {v : ι → V} (hv : is_basis K v) :  fintype ι


the universe issue is hidden a bit, but not much since there are cardinals involved.

#### Patrick Massot (Aug 09 2020 at 18:42):

@Mario Carneiro do you have a magic trick here?

#### Mario Carneiro (Aug 09 2020 at 18:43):

what's the context?

#### Patrick Massot (Aug 09 2020 at 18:46):

import linear_algebra.finite_dimensional

example {ι K V : Type*} [field K] [add_comm_group V] [vector_space K V]
[finite_dimensional K V] {v : ι → V} (hv : is_basis K v) :  fintype ι :=
sorry


#### Patrick Massot (Aug 09 2020 at 18:47):

This is a combination of handling universes in cardinals and fighting fintype

#### Mario Carneiro (Aug 09 2020 at 19:16):

I didn't have any universe issues in the proof:

import linear_algebra.finite_dimensional

noncomputable example {ι K V : Type*} [field K] [add_comm_group V] [vector_space K V]
[finite_dimensional K V] {v : ι → V} (hv : is_basis K v) : fintype ι :=
begin
apply classical.choice,
rw [← cardinal.lt_omega_iff_fintype, ← finite_dimensional.findim_eq_card_basis' hv],
apply cardinal.nat_lt_omega,
end


#### Mario Carneiro (Aug 09 2020 at 19:17):

I'm not sure which finite_dimensional theorem you were intending to use

#### Patrick Massot (Aug 09 2020 at 21:40):

Thanks you very much Mario. I was stuck at:

  apply fintype.of_cardinal_lt,
have c1 := finite_dimensional.dim_lt_omega K V,
have c2 := hv.mk_eq_dim',


(with or without the last prime) which left me with a context having all I needed but all in wrong universes. Was it possible to salvage things from there? Is there any easy explanation of why this was the wrong road? Also I would have never guessed the first line would be this apply classical.choice but I guess this comes from the weirdness of fintype X not being in Prop.

#### Patrick Massot (Aug 09 2020 at 21:43):

Would you mind having

lemma fintype.of_cardinal_lt {α : Type*} (h : cardinal.mk α < cardinal.omega) : fintype α :=
classical.choice \$ cardinal.lt_omega_iff_fintype.mp h


PRed?

#### Patrick Massot (Aug 09 2020 at 21:44):

I makes your proof a lot less puzzling.

#### Patrick Massot (Aug 09 2020 at 22:50):

I have yet another example of "fintype is data" fun:

import data.fintype.card

open_locale big_operators

example  (n : ℕ) (ι : Type*)
[fintype ι]
--  [fintype (fin n ⊕ ι)]
(f : fin n ⊕ ι → ℤ)
: ∑ (i : fin n ⊕ ι), f i = 0 :=
begin
rw fintype.sum_sum_type,
end


Uncomment the commented line to see the rewrite failing. Something is really wrong in this whole fintype setup...

#### Mario Carneiro (Aug 09 2020 at 22:52):

why is that a reasonable thing to do? That's like having two group instances

#### Mario Carneiro (Aug 09 2020 at 22:52):

In this case the second fintype can clearly be inferred from the first

#### Patrick Massot (Aug 09 2020 at 22:53):

The sum does not depend on the fintype instance.

#### Patrick Massot (Aug 09 2020 at 22:53):

In my real example, the commented instance was used to build the uncommented one, not the other way around.

#### Patrick Massot (Aug 09 2020 at 22:54):

I'm not saying that fintype is useless, I can totally believe it can be useful for programming or constructive mathematics, but it's not the right class for defining sums.

#### Mario Carneiro (Aug 09 2020 at 22:56):

how about a sum that takes no finiteness argument and returns 0 when the input function is not finitely supported

#### Patrick Massot (Aug 09 2020 at 22:57):

I sometimes dreams about that, but I fear this will be very confusing where you think about converging series.

#### Mario Carneiro (Aug 09 2020 at 22:57):

We already have tsum for infinite series

#### Patrick Massot (Aug 09 2020 at 22:57):

Because such series would have a vanishing sum.

#### Mario Carneiro (Aug 09 2020 at 22:57):

Whatever this new sum is it has to work without a topology

#### Patrick Massot (Aug 09 2020 at 22:57):

But maybe this would still be better than the current situation.

#### Mario Carneiro (Aug 09 2020 at 22:58):

(or equivalently, the discrete topology, where convergence of the infinite sum means that it is finitely supported)

#### Mario Carneiro (Aug 09 2020 at 23:00):

we can't really get rid of the existing theory of finset sums, those are still true and applicable for their domain, but we can take the notation and apply it to a different constant

#### Mario Carneiro (Aug 09 2020 at 23:01):

of course, it's already a localized notation so it doesn't even have to conflict with the existing development

#### Mario Carneiro (Aug 09 2020 at 23:08):

Proposal:

import data.finsupp

open_locale classical

noncomputable def finsum {ι α} [add_comm_group α] (f : ι → α) : α :=
if h : ∃ f' : ι →₀ α, f = f' then (classical.some h).sum (λ _ a, a) else 0

noncomputable def finsum_in {ι α} [add_comm_group α] (s : set ι) (f : ι → α) : α :=
finsum (λ i, if i ∈ s then f i else 0)

localized "notation ∑ binders ,  r:(scoped:67 f, finsum f) := r" in finsum
localized "notation ∑ binders  in  s ,  r:(scoped:67 f, finsum_in s f) := r" in finsum


#### Patrick Massot (Aug 09 2020 at 23:11):

Yes, we should probably have something like that. But the next question is: can we avoid duplicating the whole API?

#### Mario Carneiro (Aug 09 2020 at 23:15):

that's sort of the cost of doing business. The theorems aren't the same, so it's mostly a question of which finset sum theorems we want to forego

#### Mario Carneiro (Aug 09 2020 at 23:16):

I imagine that most theorems that aren't in the big_operators file can just change to the new sum without being duplicated, but the old API itself still has to stay mostly intact

#### Mario Carneiro (Aug 09 2020 at 23:16):

one obvious reason being that the definition I just gave uses finsupp, which uses finset sums to define it

#### Mario Carneiro (Aug 09 2020 at 23:17):

so it's more like another API on top of the existing one than a replacement

#### Patrick Massot (Aug 09 2020 at 23:19):

All theorem will be there, but some of them will have finiteness assumptions. But sure, this is business.

#### Mario Carneiro (Aug 09 2020 at 23:20):

As consolation, I think most of the proofs will be one liners

#### Mario Carneiro (Aug 09 2020 at 23:20):

but people generally can never have enough API theorems

#### Kevin Buzzard (Aug 10 2020 at 12:24):

@Patrick Massot your theorem about fintype (fin n + iota) is provable with the weaker hypothesis nonempty (fintype iota) which I think is a more useful typeclass for people like you and me

#### Kevin Buzzard (Aug 10 2020 at 12:25):

And nonempty (fintype (X + Y)) implies nonempty (fintype X)

#### Kevin Buzzard (Aug 10 2020 at 12:29):

@Mario Carneiro you have done a brilliant job of making computable finiteness in Lean but we are missing API for a good noncomputable finiteness concept. I think Reid's idea of making set.finite the fundamental Prop-valued finiteness class and then bundling it with finset2 will produce a type which is easier for reasoning and which will have a noncomputable card which cant be #eval'ed but about which you can prove theorems like Sylow's theorems

#### Kevin Buzzard (Aug 10 2020 at 12:30):

I think there should be a typeclass which is propositional and equivalent to nonempty (fintype X)

#### Kevin Buzzard (Aug 10 2020 at 12:31):

I don't know whether this should be literally nonempty (fintype X) or whether its actual definition should be finite univ

#### Kevin Buzzard (Aug 10 2020 at 12:31):

Maybe it doesn't matter as long as it's proved equivalent to nonempty fintype X

#### Kevin Buzzard (Aug 10 2020 at 12:32):

Because Patrick is reasoning not computing, he should be using this Prop-valued concept of finiteness. He is in trouble because he's trying to do reasoning using the wrong typeclass

#### Patrick Massot (Aug 10 2020 at 18:30):

Clearly we should do something. The current setup just doesn't work for our purposes (we should probably keep it, maybe with a more specialized name since it corresponds to very specialized purposes).

#### Kevin Buzzard (Aug 10 2020 at 18:44):

I'm making an API for a class fintype2 X := nonempty (fintype X). This will at least fix the problem where I was working with finite groups and had a complicated expression involving card (bot : subgroup G) but I couldn't rw (card_bot : card (bot) = 1) because type class inference had managed to find two non-defeq proofs of fintype bot (one coming from the fact that G was finite and one indpendent of this).

#### Mario Carneiro (Aug 10 2020 at 19:25):

Kevin Buzzard said:

I think there should be a typeclass which is propositional and equivalent to nonempty (fintype X)

Why don't we just call it is_finite X?

#### Mario Carneiro (Aug 10 2020 at 19:29):

We could even eliminate set.finite in favor of is_finite (\u s)

#### Mario Carneiro (Aug 10 2020 at 19:30):

it's always been a bit weird that set.finite combines these two operations (going from type to prop and then using sets instead of types) and there is no term for the intermediate operation

#### Mario Carneiro (Aug 10 2020 at 19:31):

But I also think that for all these examples of noncomputable versions of functions like card you would be better served getting rid of the typeclass argument entirely rather than making it propositional

#### Kevin Buzzard (Aug 10 2020 at 19:59):

So for the definition of card we should dump the typeclass, but then when we're actually proving something which does need finiteness...the idea is that we put the is_finite typeclass into the theorem statement but still use the nat-valued card?

#### Kevin Buzzard (Aug 10 2020 at 19:59):

I wondered if finprop X was good name for it, but I think the type in fintype refers to X rather than the type of the output!

#### Scott Morrison (Aug 11 2020 at 00:36):

We could do something like rename fintype to finenum or fin_bij, or something that more clearly indicates it is carrying data? Not sure.

Last updated: May 06 2021 at 18:20 UTC