linear algebra library

Stream: general

[Scott Morrison]

Is there some reason the linear algebra library has facts like:

theorem mem_span_iff_total {s : set α} {x : M} :
  x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, finsupp.total α M R v l = x := ...

but no iff statement about x ∈ span R w for w : set M?

span is defined in terms of set M, not in terms of indexed families, so there should be API in those terms, right?

Is this just historical accident, an oversight after many rounds of refactoring, or intentional? :-(

[Scott Morrison]

Should I just add this API? I don't think it's viable to rip out the current span and replace it with something in terms of familes rather than sets...

[Scott Morrison]

Gah, and how does our naming convention possibly support src#finsupp.total_range and src#finsupp.range_total? They are both talking about the range of the total function, just one has a surjective argument...

[Anne Baanen]

Scott Morrison said:

Is this just historical accident, an oversight after many rounds of refactoring, or intentional? :-(

Looks like this is mostly an oversight when switching some other definitions from sets to indexed families #943. I see no objection at all to having a lemma mem_span_iff_total about span R w and mem_span_image_iff_total about span R (v '' s).

[Kevin Buzzard]

I don't have anything to say, but I'm over here in England offering my moral support Scott :-)

[Scott Morrison]

finsupp.total_range is useless (how are you ever going to have a surjective function from an index set to a module?), and unused, so I'm just going to remove it rather than renaming it. #7734

[Scott Morrison]

Kevin Buzzard said:

I don't have anything to say, but I'm over here in England offering my moral support Scott :-)

I will stop complaining and go refactor. Sorry. :-)

[Anne Baanen]

Let's not feel too bad about complaining, since awareness is often the first step towards a solution :)

[Scott Morrison]

#7735

[Scott Morrison]

How would people feel about adding something like

def fintype.total (R : Type*) [semiring R] (M : Type*) [add_comm_monoid M] [module R M]
  (α : Type*) [fintype α] (f : α → M) : (α → R) →ₗ[R] M :=
(finsupp.total α M R f).comp (finsupp.linear_equiv_fun_on_fintype R R α).symm.to_linear_map

(needs a better name).

finsupp.total is great, and all, but in situations when you already know your types are finite, it is painful to have to migrate back and forth via finsupp.linear_equiv_fun_on_fintype all the time.

This proposal would involve repeating a fair bit of API for finsupp.total, however, so it is not cost-free (or maintaining-consistency-free).

[Anne Baanen]

Existing parts of the library have tended to use finset.sum (univ : finset α). Are there places where we need a bundled linear map?

[Scott Morrison]

I'm working out the consequences of having strong_rank_condition and rank_condition (and knowing that all noetherian rings and all commutative rings satisfy these), and hoping to generalize all our dimensions API to work with these (rather than requiring a field), and for this I'm working with bundled linear maps all the time.

[Anne Baanen]

OK, sounds like a good enough reason to do the extra work :+1:

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

Scott Morrison said:

Gah, and how does our naming convention possibly support src#finsupp.total_range and src#finsupp.range_total? They are both talking about the range of the total function, just one has a surjective argument...

I am proving that any module is a quotient of a free module, using the stupid surjection $R^M \to M$, so finsupp.total_range would be useful... should I bring it back to life or prove my lemma directly? I don't see any other reasonable applications