Topology without algebra

Stream: mathlib4

[Yaël Dillies]

Now that #19779 is merged, I was looking into not importing Monoid in topology, but assert_not_exists Monoid in Topology.Defs.Basic gives

Declaration Monoid is not allowed to be imported by this file.
It is defined in Mathlib.Algebra.Group.Defs,
  which is imported by Mathlib.Algebra.Group.Pi.Basic,
  which is imported by Mathlib.Lean.Meta.RefinedDiscrTree.Pi,
  which is imported by Mathlib.Lean.Meta.RefinedDiscrTree.Encode,
  which is imported by Mathlib.Lean.Meta.RefinedDiscrTree,
  which is imported by Mathlib.Tactic.FunProp.Theorems,
  which is imported by Mathlib.Tactic.FunProp.Attr,
  which is imported by Mathlib.Tactic.FunProp,
  which is imported by this file.

[Yaël Dillies]

Any thoughts on how to circumvent this issue? Should I split Algebra.Group.Pi.Basic into a notation-only file not importing Monoid vs the rest?

[Eric Wieser]

Why does Topology.Defs.Basic need Monoid?

[Eric Wieser]

I think the problem is that Mathlib.Lean.Meta.RefinedDiscrTree.Pi hard-codes a list of pi instances, rather than providing an extension point

[Eric Wieser]

(or perhaps looking at attributes on instances instead)

[Eric Wieser]

Note that @Jovan Gerbscheid's has a rewrite of RefinedDiscr in #11968, so a refactor in the meantime would probably not be appreciated

[Eric Wieser]

(In the PR Jovan did discuss dropping the import, but the proposed approach comes at the cost of replacing ``Pi.instAdd with `Pi.instAdd , which makes everything more fragile)

[Yaël Dillies]

It would be great to have an answer rather quickly as this is preventing further improvements to the import graph

[Eric Wieser]

You could remove the fun_prop import from topology/defs/basic

[Kevin Buzzard]

Is improving the import graph an urgent issue?

[Yaël Dillies]

No, but it's a long term one with many intermediate steps to perform

[Eric Wieser]

Yaël Dillies said:

Should I split Algebra.Group.Pi.Basic into a notation-only file not importing Monoid vs the rest?

I think we used to have this as Data.Pi? (edit: data.pi.algebra)

[Yaël Dillies]

It had a bit more than just notation (which is why I eventually merged it with the other algebra + pi file)

[Jovan Gerbscheid]

By the way, in the new version of RefinedDiscrTree (#11968), the extra import is just Mathlib.Algebra.Group.Operations, so this doesn't include Monoid.