Warning that AlgebraicTopology can't import SetTheory

Stream: mathlib4

[Sebastian Kumar]

I was trying to make a pull request for my file showing that the sphere is simply connected here. However, the build is failing with the following error:
warning: Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnectedSphere.lean:12:0: Modules starting with Mathlib.AlgebraicTopology are not allowed to import modules starting with Mathlib.SetTheory. This module depends on Mathlib.SetTheory.Cardinal.Defs.

Why aren't algebraic topology files allowed to import set theory files? That seems like a weird restriction to me. Anyways, in my case I want to use the theorem isPathConnected_compl_singleton_of_one_lt_rank, which seems like a sensible result for one to use in algebraic topology. However, this result is located in Mathlib.Analysis.NormedSpace.Connected which apparently imports results from set theory. I've listed the chain of imports below in case it matters. The error message also says "Exceptions can be added to overrideAllowedImportDirs" but I am not entirely sure what that means.

This module depends on Mathlib.SetTheory.Cardinal.Defs which is imported by Mathlib.SetTheory.Cardinal.Order, which is imported by Mathlib.SetTheory.Cardinal.Basic, which is imported by Mathlib.SetTheory.Cardinal.ENat, which is imported by Mathlib.SetTheory.Cardinal.ToNat, which is imported by Mathlib.SetTheory.Cardinal.Finite, which is imported by Mathlib.LinearAlgebra.Quotient.Basic, which is imported by Mathlib.LinearAlgebra.Projection, which is imported by Mathlib.LinearAlgebra.Basis.VectorSpace, which is imported by Mathlib.LinearAlgebra.AffineSpace.Independent, which is imported by Mathlib.LinearAlgebra.AffineSpace.Basis, which is imported by Mathlib.Analysis.Convex.Combination, which is imported by Mathlib.Analysis.Convex.Topology, which is imported by Mathlib.Analysis.Normed.Module.Convex, which is imported by Mathlib.Analysis.NormedSpace.Connected, which is imported by this module.

[Michael Rothgang]

My understanding is that this check if not a hard and fast rule "you must never import SetTheory", but more rather "if you add a new import like this, please check if all files are placed right --- or perhaps some file should be in a different directory to begin with". At the scale of mathlib, it's really easy to cause a mess; forcing some deliberation is necessary to prevent that from happening too badly.

[Michael Rothgang]

How about you open a PR and your reviewer can help to determine the best way forward? (That might well mean adding an exception.)

[Yaël Dillies]

Honestly, it is a bit weird that we import cardinals to define docs#Nat.card. That seems very unnecessary. Simultaneously, cardinals are quite basic, and maybe we shouldn't shy away from them so much

[Michael Rothgang]

If you want to silence the linter, I'd edit Mathlib/Tactic/Linter/DirectoryDependency.lean and remove the line

(`Mathlib.AlgebraicTopology, `Mathlib.SetTheory)

on line 311.

[Kim Morrison]

What are the actual mathematical prerequisites of isPathConnected_compl_singleton_of_one_lt_rank? Could this be moved earlier?

[Kim Morrison]

One dubious step here is

which is imported by Mathlib.SetTheory.Cardinal.Finite,
which is imported by Mathlib.LinearAlgebra.Quotient.Basic,

Presumably it is possible to set up the basic theory of linear quotients without ever mentioning finiteness. Perhaps splitting this file would be helpful (if not for this PR, more generally).

[Kim Morrison]

#28277 manages to clean this up quite a bit.

It allows us to add assert_not_exists Cardinal in Mathlib.Analysis.Convex.Combination (the 4th last in the chain above).

Doing so in Mathlib.Analysis.Convex.Topology would be more complicated. It looks like the the import of Mathlib.GroupTheory.Coset.Card into Mathlib.GroupTheory.GroupAction.Quotient is the critical one. I would advise splitting Mathlib.GroupTheory.GroupAction.Quotient into one file containing the basic theory, and another file containing the orbit-stabilizer theorem and its consequences.

[Sebastian Kumar]

I should mention that, to make my pull request build, I also needed to allow AlgebraicTopology to depend on Geometry (because I use stereographic' from Geometry to prove properties like path connectedness for the sphere) and on NumberTheory because of the import chain:
This module depends on Mathlib.NumberTheory.Divisors which is imported by Mathlib.GroupTheory.OrderOfElement, which is imported by Mathlib.Analysis.Normed.Ring.Lemmas, which is imported by Mathlib.Analysis.Normed.Field.Lemmas, which is imported by Mathlib.Analysis.Normed.Module.Basic, which is imported by Mathlib.Analysis.Normed.Module.Convex, which is imported by Mathlib.Analysis.NormedSpace.Connected, which is imported by this module.

[Michael Rothgang]

Would it make sense to move the topological construction of stereographic projection to Topology, prove its continuity there, and keep just the smoothness proof in Geometry?

[Michael Rothgang]

The number theory import also feels a bit unobvious to me, but I don't have a good intuition yet whether it is avoidable.

[Yaël Dillies]

I don't see why normed rings should know about the order of an element

[Michael Rothgang]

Sorry, Sebastian, that you tripped on a small "import bomb". On the other hand, your PR made (at least me) realise further clean-up opportunities for mathlib :-)

[Kim Morrison]

Yaël Dillies said:

I don't see why normed rings should know about the order of an element

#28318 seems easy enough

[Kim Morrison]

I see that a lot of polynomial theory, starting at Polynomial.Coeff, imports CharP in a way that could probably be deferred quite a long way.

[Joël Riou]

In another PR related to combinatorial aspects of simplicial sets #28351, I will also need to import Mathlib.SetTheory.Ordinal.Rank in order to use docs#IsWellFounded.rank
https://github.com/joelriou/mathlib4/blob/75af19d7ca7cb2472da4687d1c7670b95f97f7b1/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RankNat.lean#L46-L48

[Kim Morrison]

Do you really need to detour via Ordinal there? You immediately prove that the ordinal is actually a nat: can you just redefine the rank function in some special case where you assume enough finiteness?

[Kim Morrison]

@Sebastian Kumar, now that we've merged a few PRs cutting imports out of your dependencies, would you mind merging master again, and giving us an update on how the dependency checker complains now?

[Joël Riou]

Kim Morrison said:

Do you really need to detour via Ordinal there? You immediately prove that the ordinal is actually a nat: can you just redefine the rank function in some special case where you assume enough finiteness?

By some moderate duplication of code, I was able to remove the dependency.

[Robin Carlier]

Is the fact that we can't import SetTheory in AlgebraicTolopogy a problem for studying interactions between locally presentable categories and model categories?

[Joël Riou]

No, this is unrelated (so far). It may be an issue as soon as I introduce finiteness conditions on simplicial sets (which corresponds to being presentable relative to the first infinite cardinal...), so that the small object argument becomes usable for simplicial sets.

[Kim Morrison]

Maybe we could split AlgebraicTopology (the directory, perhaps also the github label) into the "naive" part and the more set theoretic part? Only if people felt it was sufficiently natural to do so. We can of course relax the import restrictions, although I think so far the above experience has been that the restriction was really helpful to prompt us to un-snarl some unnecessary import thickets...

[Robin Carlier]

Given that the non-"naive" part of the folder is highly category-theoretic, wouldn't it make sense to move it inside CategoryTheory?
It would have the side-effect of moving quasicategories to CategoryTheory, which would make sense given that they are a model for higher categories (and hopefully, at some point quasi-category theory will pick up in mathlib, and then it would make no sense that CategoryTheory can import things that QuasiCategory can't, but this is of course for a future that is far from now).

[Kim Morrison]

CategoricalTopology/? :woman_shrugging:

[Joël Riou]

I do not think it makes sense to move AlgebraicTopology into CategoryTheory. It is a fact that algebraic topology uses category theory, and among these categorical methods, the small object argument makes use of regular cardinals, etc, but in the end, the point is to prove results about simplicial sets, topological spaces, etc. For example, I intend to prove the Whitehead theorem for CW-complexes as a consequence of the abstract version in homotopical algebra (which is already in #28392). As the proof that TopCat has a model category structure uses some of SetTheory, if we keep restricting imports, it means that the "naive" homotopy theory of topological spaces cannot use the Whitehead theorem. Eventually, the only reasonable solution I see is to remove the import restriction when it becomes necessary.

[Kim Morrison]

One thing we can do is use finer import restrictions, e.g. so AlgebraicTopology can only import from SetTheory/Cardinal, but not other subdirectories.

[Kim Morrison]

(Obviously with all of this the maths must happen, and at the end of the day the real logical dependencies win. We just need to keep up the defences against unnecessary dependencies.)

[Robin Carlier]

@Joël Riou I agree that things like Whitehead's theorem for CW complexes, and facts about topological spaces derived via simplicial methods make more sense in AlgebraicTopology.
I am however still not convinced it is the right home for simplicial sets/simplicial objects and quasicategories: I am not sure what's the best home for the former, but the latter are more relevant as category-theory objects.

[Joël Riou]

About quasicategories, I have been insisting that things that are specific to quasicategory should not be mixed with the files involving simplicial sets. Then, if this develops significantly, the subfolder AlgebraicTopology.Quasicategory could be moved out easily.

[Sebastian Kumar]

Kim Morrison said:

Sebastian Kumar, now that we've merged a few PRs cutting imports out of your dependencies, would you mind merging master again, and giving us an update on how the dependency checker complains now?

I did this and I am now getting the complaint:

This module depends on Mathlib.SetTheory.Cardinal.Defs
  which is imported by Mathlib.SetTheory.Cardinal.Order,
  which is imported by Mathlib.SetTheory.Cardinal.Basic,
  which is imported by Mathlib.SetTheory.Cardinal.ENat,
  which is imported by Mathlib.SetTheory.Cardinal.ToNat,
  which is imported by Mathlib.SetTheory.Cardinal.Finite,
  which is imported by Mathlib.GroupTheory.Coset.Card,
  which is imported by Mathlib.GroupTheory.GroupAction.Quotient,
  which is imported by Mathlib.Topology.Algebra.Group.Quotient,
  which is imported by Mathlib.Topology.Algebra.Module.Basic,
  which is imported by Mathlib.Analysis.Convex.Topology,
  which is imported by Mathlib.Analysis.Normed.Module.Convex,
  which is imported by Mathlib.Analysis.NormedSpace.Connected,
  which is imported by this module.

[Ruben Van de Velde]

Let's see if this works - #28529

[Ruben Van de Velde]

Looks like a pretty good improvement, though Mathlib.Analysis.Normed.Module.Convex still imports cardinals through another path

[Ruben Van de Velde]

the module 'Mathlib.SetTheory.Cardinal.Defs' is (transitively) imported via
Mathlib.SetTheory.Cardinal.Defs,
  which is imported by Mathlib.SetTheory.Cardinal.Order,
  which is imported by Mathlib.SetTheory.Cardinal.Basic,
  which is imported by Mathlib.SetTheory.Cardinal.ENat,
  which is imported by Mathlib.SetTheory.Cardinal.ToNat,
  which is imported by Mathlib.SetTheory.Cardinal.Finite,
  which is imported by Mathlib.Topology.Algebra.InfiniteSum.Group,
  which is imported by Mathlib.Topology.Algebra.InfiniteSum.NatInt,
  which is imported by Mathlib.Topology.Algebra.InfiniteSum.Order,
  which is imported by Mathlib.Topology.Instances.NNReal.Lemmas,
  which is imported by Mathlib.Topology.Instances.ENNReal.Lemmas,
  which is imported by Mathlib.Topology.Algebra.InfiniteSum.Real,
  which is imported by Mathlib.Analysis.SpecificLimits.Basic,
  which is imported by Mathlib.Topology.MetricSpace.HausdorffDistance,
  which is imported by Mathlib.Topology.MetricSpace.Thickening,
  which is imported by Mathlib.Analysis.Normed.Group.Pointwise,
  which is imported by this file.

[Ruben Van de Velde]

Oh, I thought this would be bad, but just moving tprod_const out of Mathlib.Topology.Algebra.InfiniteSum.Group seems like it pushes the needle at least as far as Mathlib.Topology.Instances.ENNReal.Lemmas. Might pull on that thread later, unless someone else has time earlier