data.set.finite

Stream: mathlib4

[Patrick Massot]

I think an interesting graph to took at in order to measure how far we are from porting anything interesting is the import graph of data.set.finite:
data_set_finite.pdf

[Patrick Massot]

This is rather depressing but I suspect that a lot of this comes from the fact that data.finite.basic both defines finiteness and tries to provide all possible instances.

[Patrick Massot]

In any case, there is certainly no reason why data.set.finite needs all this algebra.

[Patrick Massot]

Maybe we should simply port everything and stop worrying, but it's hard to think there is nothing to fix here.

[Heather Macbeth]

Since the very first filter files import finiteness, we should definitely fix this! There is no reason for basic topology to import basic algebra.

[Patrick Massot]

This is creepy. Heather seems to be spying on my computer and knows how I found about that horrible graph.

[Patrick Massot]

Of course I first generated filter.pdf

[Jireh Loreaux]

Perhaps a stupid question: why do the very first filter files import finiteness?

[Heather Macbeth]

Among other reasons, because the cofinite filter is defined in them. This could be avoided.

[Yaël Dillies]

I have plans to split up finiteness. I will update you in the next two days.

[Heather Macbeth]

Also, because there are lemmas about Sups of finsets in order.conditionally_complete_lattice (this could be avoided), and order.copy imports conditionally_complete_lattice (this could be avoided), and order.filter.basic imports order.copy (this could be avoided).

[Patrick Massot]

Perhaps a stupid question: why do the very first filter files import finiteness?

By definition, the set of members of a filter is stable under (binary) intersection. One of the very first consequences you want to state is stability under finite intersections.

[Patrick Massot]

And really this isn't only about filters. Stating that a set is finite is a really really basic thing in mathematics.

[Kyle Miller]

I remember @Yury G. Kudryashov had plans to make docs#set.finite be defined in terms of docs#finite, so that we could remove the data.fintype.basic dependency of data.set.finite and try to lower these things.

When I reorganized this module back in May, my goal was to get things thematically in order and to figure out dependencies. An obvious thing to split out now are all the fintype instances for sets -- data.set.finite has long been a mismash of set.finite and things about finite sets.

[Kyle Miller]

Organizationally, many of the set.finite constructors come from these finite or fintype instances, but these don't have to be in the module that defines set.finite

[Yaël Dillies]

Yes, that's exactly my thought.

[Jireh Loreaux]

Patrick, sure, finiteness is very basic, but I often consider filters as similarly basic, but your finite intersection argument definitely convinced me.

[Adam Topaz]

Of course, everyone's favorite definition of a finite set is that every ultrafilter is principal ;)

[Adam Topaz]

(Maybe I've been thinking about condensed mathematics too much)

[Kevin Buzzard]

I think that in ZF it's consistent that every ultrafilter on the naturals is principal :-)

[Junyan Xu]

https://en.wikipedia.org/wiki/Ultrafilter_(set_theory)#Weaker_statements says

ZF alone does not even imply that there exists a non-principal ultrafilter on some set.

[Jireh Loreaux]

yeah, the ultrafilter lemma is equivalent to the Boolean prime ideal theorem

[Junyan Xu]

The Wikipedia page says this is strictly weaker than the ultrafilter lemma, but ZF still doesn't imply it.

[Jireh Loreaux]

oooo, interesting!

[Yaël Dillies]

#17574 for the list part of the monster.

[Heather Macbeth]

Beyond #17574, it looks like half of data.list.basic doesn't depend on any algebra at all, just

import data.option.basic
import logic.nontrivial
import order.basic

See branch#hrmacbeth-minimal-list. I have never looked at this file and can't tell whether the algebra-independent half has any coherence or content. Could someone who has comment on whether this split is worthwhile?

[Heather Macbeth]

(The "algebra" in the other half, with imports

import algebra.order.with_zero
import data.nat.order.lemmas
import data.set.function

seems to be mostly addition and subtraction of natural numbers.)

[Mario Carneiro]

I'm inclined to say that you should have data.nat.basic lemmas available (assuming that doesn't pull in the algebraic hierarchy). That should give you a much bigger fraction of the file

[Heather Macbeth]

Currently data.nat.basic imports

import order.basic
import algebra.group_with_zero.basic
import algebra.ring.defs

[Mario Carneiro]

also note that most of data.nat.basic is in Std now, so it is "free" from a untangling-imports perspective (but this hasn't been reflected in lean 3)

[Mario Carneiro]

maybe data.nat.basic needs a split then?

[Mario Carneiro]

I'm pretty sure most of data.nat.basic is "stuff that should have been in core" (i.e. no dependencies), that's the stuff that is in Std now and which should be split off

[Heather Macbeth]

Indeed. But this is getting clearly into Scott's territory so let's wait til he wakes up.

[Scott Morrison]

Oh dear, I don't want my enthusiasm for splitting files to prevent other people splitting files!!!

[Scott Morrison]

So maybe I should just say: yes, obviously data.nat.basic and data.list.basic deserve splitting, and we should do it real-soon-now. :-)

[Yaël Dillies]

Well I had a split for data.fintype.basic but you got yours out first :sweat_smile:

[Heather Macbeth]

I started a branch aiming to remove

algebra.group_with_zero.divisibility
algebra.order.with_zero
algebra.ring.divisibility
data.set.basic

from the (indirect) imports of data.list.basic. Progress so far: branch#list-nat-order

Is this worth persevering with?

[Heather Macbeth]

So far so good, so I opened #17616.

[Heather Macbeth]

#17691 is another small PR towards untangling finiteness.

[Heather Macbeth]

Another PR working on the imports of data.list.*: #17702