Zulip Chat Archive

Stream: general

Topic: linear algebra library


Scott Morrison (May 28 2021 at 08:41):

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 (May 28 2021 at 08:44):

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 (May 28 2021 at 08:48):

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 (May 28 2021 at 08:55):

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 (May 28 2021 at 08:56):

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

Scott Morrison (May 28 2021 at 08:57):

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 (May 28 2021 at 08:58):

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 (May 28 2021 at 09:01):

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

Scott Morrison (May 28 2021 at 09:08):

#7735

Scott Morrison (May 28 2021 at 09:23):

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 (May 28 2021 at 09:33):

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 (May 28 2021 at 09:34):

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 (May 28 2021 at 09:37):

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

Riccardo Brasca (Jun 15 2021 at 10:57):

(deleted)

Riccardo Brasca (Jun 15 2021 at 10:57):

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 RMMR^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


Last updated: Dec 20 2023 at 11:08 UTC