StrictSeries !4#3858, !4#3852

Stream: PR reviews

[Scott Morrison]

@Jujian Zhang, now that you're proposing to add a lot of API to StrictSeries, I have some concerns.

1) I think defining it using StrictMono is unnecessarily burdensome: why isn't it just a list with elements that are pairwise <? Then StrictMono is just a theorem, not something you need to keep proving.
2) If we're adding this much API, perhaps it should be more general (not just < but an arbitrary relation or type). E.g. we have src#quiver.path already.

[Eric Wieser]

Note that docs#composition_series is a version with an different relation

[Eric Wieser]

Here monotonicity is proven by relating adjacent elements, which seems more useful

[Jujian Zhang]

This makes sense. I will temporarily mark these two PRs as draft and rework definitions of StrictSeries. Thanks

[Jujian Zhang]

The first attempt to define a RelSeries is at !4#3878

[Scott Morrison]

Two possible alternative designs, that might allow even more reuse:

import Std.Data.List.Basic

open List

structure RelSeries (r : α → α → Prop) where
  objects : List α
  not_nil : objects ≠ []
  chain : Chain' r objects

and

import Mathlib.Combinatorics.Quiver.Path

namespace Quiver

def of (_r : α → α → Sort _) : Type _ := α

instance : Quiver (of r) where
  Hom := r

end Quiver

open Quiver

/-- A series with specified endpoints. -/
def RelSeries' (r : α → α → Prop) (a b : α) := @Path (of r) _ a b

def RelSeries (r : α → α → Prop) := Σ a b, RelSeries' r a b

[Eric Wieser]

Fwiw, I think I prefer the fin spelling to the list spelling

[Jujian Zhang]

For the use case of Krull dimension, the most important bit about RelSeries is its length, so I think it make sense to make length explicit, otherwise a separate theorem about length needs to be proved for every construction related to RelSeries

[Scott Morrison]

I'm not sure why having it as a field is any more explicit!

[Scott Morrison]

The point of the two alternatives is that there is lots more shareable API!

[Jujian Zhang]

@Eric Wieser Why do you prefer the fin spelling?

[Jujian Zhang]

Scott Morrison said:

The point of the two alternatives is that there is lots more shareable API!

For example by using the path implementation, after constructing inserting an element operation, one has to prove the result has length exactly one bigger.

[Eric Wieser]

Jujian Zhang said:

Eric Wieser Why do you prefer the fin spelling?

I think mainly because I've worked with fin tuple a lot more than I have lists. I don't have a particularly objective argument to use.

Perhaps it's relevant that the recent cohomology stuff is also using fin tuples, though I don't know whether there's any overlap here.

[Scott Morrison]

Okay, thanks, I think I'm happy if you want to stick with Fin tuples.

[Jujian Zhang]

Can I pin on !4#3878 please.

[Jujian Zhang]

Can I pin on !4#3878 please.

[Scott Morrison]

Sorry this has been slow. The porting effort is holding up many things! :-)

Would you mind either adding the lemma(s) relating it to List.Chain' r (List.ofFn s.toFun), or at least a comment about Chain', so that users of this API are aware of the connection?

(If you really want to be thorough you could mention the Quiver.path connection too, but I think that is less important.)

[Jujian Zhang]

Sorry for the late reply, I have added a bijection between RelSeries and nonempty List satisfying chain condition.

[Jujian Zhang]

And also there is a very weird bug (I think this might be a bug), in RelSeries.lean, if I import Mathlib.Data.List.ofFn, then build will fail, but if I import something that imported Mathlib.Data.List.ofFn then it will build on github

[Jujian Zhang]

If I import Mathlib.Data.List.ofFn directly and run lake build, then this is the (important bit?) of the error message:

./././Mathlib/Order/KrullDimension.lean:7:0: error: import Mathlib.Data.List.OfFn failed, environment already contains '_private.Mathlib.Data.List.OfFn.0.List.replicate.match_1.splitter' from Mathlib.Data.List.ofFn

[Jujian Zhang]

one can see the failed run at here (this is where Mathlib.Data.List.ofFn is imported directly) and successful run at here, Mathlib.Data.List.Indexes is imported so thatofFn is only indirectly imported