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?