Location of algebraic subobjects

Stream: mathlib4

[Yaël Dillies]

Currently, we have

• subobjects defined in the folder of the corresponding object: docs#Subalgebra, docs#Sublattice, docs#CompleteSublattice, docs#Submodule
• subobjects defined in an ObjectTheory folder which starts with them: docs#Subgroup, docs#Subring, docs#Subfield

I am claiming the latter are the abnormal ones, as there's not much foo-theoretic stuff happening with just the definition of subfoo. This causes confusion as to what files are advanced and what files are basic, see eg https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Today's.20insane.20Mathlib.20import.20dependency by @Scott Morrison.

[Yaël Dillies]

#11104 is an attempt at sanitising the situation, by moving the definition of Subfoo to Something.Foo.Subfoo, rather than FooTheory.Subfoo.

[Eric Wieser]

This sounds fine to me, but I remember people arguing in favor of *Theory folders at some point.

[Eric Wieser]

I guess the week or two of silence means that no one cares about the rename?

[Yaël Dillies]

I assume so :shrug: