Linear independence over semirings

Stream: maths

[Eric Wieser]

I started attempting this in #18426; unfortunately a lot of downstream theory relies on many LinearIndependent theorems holding for semirings, presumably bringing with it analogous nonsense

[Notification Bot]

2 messages were moved here from #Is there code for X? > ✔ E/L/F and K/L'/F isomorphic => [E:L]=[K:L'] by Eric Wieser.

[Eric Wieser]

Now merged, I guess now the question is whether Module.rank S S = 1 holds for some class of semirings

[Junyan Xu]

What do you have in mind? It's unknown whether it always fails for rings failing StrongRankCondition.

[Junyan Xu]

Probably a fun exercise: for a nontrivial semiring R and an infinite type ι, let A := Module.End R (ι →₀ R). Construct A ≃ₗ[A] ι →₀ A and deduce that #ι ≤ Module.rank A A. (I'm not sure when the equality holds.)

[Eric Wieser]

Mainly just something that works for Nat, NNRat, and NNReal

[Eric Wieser]

Hopefully those all satisfy docs#StrongRankCondition, but I don't think mathlib knows that

[Junyan Xu]

Yes, I think you can consider localizations of their additive monoids, endow them with ring structures, which will be isomorphic to Int, Rat, and Real respectively. (Will also need this to put ring structure on $K_0$.) The LocalizationMap will be injective if the additive monoid is cancellative. These are commutative rings so they satisfy StrongRankCondition. There is docs#AddSubmonoid.LocalizationMap.map_injective_of_injective but we need a more general statement and we need to show the map is linear.

[Jz Pan]

Junyan Xu said:

can consider localizations of their additive monoids

docs#AddOreLocalization ? Will they always have a ring structure?

[Junyan Xu]

Yeah I'm claiming AddLocalization (⊤ : AddSubmonoid R) is a ring if R is a semiring.

[Junyan Xu]

We probably need to come up with a proper IsAddLocalization predicate, as Int isn't defeq to AddLocalizaiton of Nat, etc.

[Jz Pan]

Junyan Xu said:

We probably need to come up with a proper IsAddLocalization predicate, as Int isn't defeq to AddLocalizaiton of Nat, etc.

Does @[to_additive] works for IsLocalization -> IsAddLocalization?

[Junyan Xu]

There is already docs#AddSubmonoid.LocalizationMap, but we at least want to assume it's a multiplicative homomorphism as well. Looks like no additional constraints are necessary.

[Junyan Xu]

Junyan Xu said:

Yeah I'm claiming AddLocalization (⊤ : AddSubmonoid R) is a ring if R is a semiring.

I realized that ℤ ⊗[ℕ] R is a readily available construction soon after I wrote this comment. Maybe we should introduce an Algebra version of IsTensorProduct?

[Johan Commelin]

Yes, I think an algebra version is a good idea.

[Christian Merten]

Isn't docs#Algebra.IsPushout this Algebra version?

[Junyan Xu]

Good find! There's a drawback of formulating everything in terms of Algebra though, which is that you must assume S and R' are commutative. In our setting R is N, S is Z but R' can be an arbitrary semiring.

Even for commutative semirings I think we might still need the AddLocalization construction, just like we access some properties of the tensor product with a localized ring by the explicit construction of localized modules, e.g. that's how we prove flatness of localization.

Anyway, this is something hopefully true and one might try to prove:

import Mathlib.RingTheory.IsTensorProduct
variable {R S} [CommSemiring R] [CommRing S] [Algebra R S]
example : Algebra.IsPushout ℕ ℤ R S ↔
    ∃ f : (⊤ : AddSubmonoid R).LocalizationMap S, f.toFun = algebraMap R S :=
  sorry

[Junyan Xu]

As a follow-up to #18426, I opened #20480 to generalize the file LinearIndependent.

[Eric Wieser]

Eek, I had an open PR already, #18503

[Eric Wieser]

It looks like you put in more work than I did though, so probably yours is the one to ultimately merge

[Junyan Xu]

It looks like our work are mostly disjoint; I have included the generalizations from #18503 in my PR. The first commit of #20480 took me about 6 hours.

[Junyan Xu]

I just opened #20497 for more generalizations in some other files. Feel free to push more generalizations!

[Johan Commelin]

Note that github will close #20497 once it's target branch is closed by bors.

[Kevin Buzzard]

Indeed it was just closed

[Eric Wieser]

I'm a little concerned that bors says it deleted the master branch

[Johan Commelin]

Yeah, that's weird!

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/tree/master still works

[Junyan Xu]

It's probably GitHub's bug; the branch name under the PR title is also crossed out, and Refined GitHub no longer creates a "merge master" button at the bottom so I have to create a PR for that.
image.png

Note that github will close #20497 once it's target branch is closed by bors.

It seems that a bot now automatically change the target branch to master? But it doesn't automatically reopen the PR. I had to manually change the base branch 2 weeks ago (and before doing that I needed to temporarily restore the merged/deleted branch).

[Junyan Xu]

#20534 generalizes all generalizable results (without changing statements) about Noetherian and Artinian. Partially enabled by the generalization of linear independence; the PR also generalizes two lemmas missed by #20480.

[Junyan Xu]

#20774 generalizes results about ranks.

[Junyan Xu]

Somehow #20497 got no review yet, while 20534 (which was opened later) has already been merged thanks to Johan.

[Junyan Xu]

I'd also appreciate a review on #19115 (flatness over semirings).

[Riccardo Brasca]

#19115 has a merge conflict, so it is not on the queue

[Junyan Xu]

Thanks, fixed! The PR has been WIP for some time and only ready for review ~ 3 weeks ago.

[Junyan Xu]

Explanation of the declarations diff: #PR reviews > #19115 Generalize flatness to semirings @ 💬

[Junyan Xu]

#20774 makes mathlib slightly faster, though the speedups in CardinalEmb and RelRank are due to AddCommMonoid instance reminders within proofs.

[Junyan Xu]

It turns out the "flatness" in #19115 is called "mono-flatness" in the literature. The difference is that tensoring with a mono-flat module preserves monomorphisms, while tensoring with a flat module preserves all finite limits. (Modules over semirings are called "semimodules" in the literature.)

[Junyan Xu]

It turns out a professor (Markus Banagl) in my university (Heidelberg) publishes about semimodules, and it's used in TQFT ...
The paper says the semimodule tensor product (same as in mathlib) was constructed by Y. Katsov in 1997. Should we add a reference to that paper?

[Junyan Xu]

#23742 is a case where an attempt to generalize to semirings led me to discover a proof that golfed 100 lines away from Mathlib. The mathematical lesson is posted in this comment on Stacks Project.

[Antoine Chambert-Loir]

Isn't it the same proof? Just avoiding localization and quotient by talking of the ideals themselves?

[Junyan Xu]

Junyan Xu said:

import Mathlib.RingTheory.IsTensorProduct
variable {R S} [CommSemiring R] [CommRing S] [Algebra R S]
example : Algebra.IsPushout ℕ ℤ R S ↔
    ∃ f : (⊤ : AddSubmonoid R).LocalizationMap S, f.toFun = algebraMap R S :=
  sorry

I now have this in #28468 stated using an extracted IsLocalizationMap predicate.

[Junyan Xu]

I found that there are at least two notions of linear independence in use over semirings, and even and expert in the subject matter can get confused. Golan's classic reference Semirings and their Applications (1999) agrees with the current mathlib definition, and in Example (17.7) (only two pages after the definition), Golan claims that B is a linearly-independent subset of M having more than three elements, ostensibly violating the strong rank condition. However if you look into the reference Guo et al., 1988 (Example 2), you see that they use a different notion of linearly independence (each element is not contained in the span of the other elements). This notion is equivalent to the span of individual elements being docs#iSupIndep, and could be named LinearIrredundant to avoid the terminology clash.

Golan: Definition of linear independence
Golan: Example (17.7)
Alternative definition

A 2016 paper I found yesterday uses the same definition of linear independence, and mathlib's docs#LinearIndependent is called "free" there. (Mathlib's docs#Basis is called "free basis", and docs#Submodule.spanRank is called "rank".) With this dictionary in mind, Theorem 3.2 of the paper implies that nontrivial commutative semirings satisfy the strong rank condition, answering a MO question of mine. It looks like the proof depends on 14 pages of the paper plus an 2013 paper by the same author and a 2004 paper (update: all that are needed in this paper seem to be included in @Thomas Browning's work in #19581), so it will be a nontrivial effort to formalize the result.

2016 paper: Definitions
2016 paper: Theorem 3.2

[Ruben Van de Velde]

You were looking for a project, right? :innocent:

[Junyan Xu]

I'm not ... Aristotle and Gauss likely are!

[Eric Wieser]

Junyan Xu said:

This notion is equivalent to the span of individual elements being docs#iSupIndep, and could be named LinearIrredundant to avoid the terminology clash.

I think this came up when trying to define docs#DirectSum.IsInternal, where the original definition used lattices but then we switched to injectivity.

[Junyan Xu]

Yeah you don't get isomorphism with direct sum assuming only iSupIndep/irredundancy, though if working with rings/groups we have docs#linearIndepOn_iff_notMem_span showing the equivalence.

[Junyan Xu]

Sorry, the iSupIndep idea doesn't quite work: even if one element isn't contained in the span of the other elements, a multiple of it may be. For example {2, 3} ⊆ ℕ is linearly independent by that definition; in comparison the example in $\mathbb{I}^3$ seems unnecessarily complicated.