Create a backbone of Defs.lean files

[Vierkantor]

The import hierarchy in Mathlib is quite messy. A concrete issue we can focus on is that lot of files in Mathlib are structured around introducing a definition and then following up with a large collection of lemmas. This means that importing a definition often means also pulling in many unrelated definitions that interact with the intended result. Not only does this clustering make Mathlib slower to build after changes, it also means harder minimization of examples.

Ideally we'd maintain a stable "backbone" of Defs files, where each only contains definitions and the bare minimum of theory to get to the next level in the backbone. These could then be paired with Lemmas files that can be imported to get the full complement of results that would currently be imported alongside the defs.

Studying the import graph for a file can be a very useful tool in figuring out which bits of theory should be unnecessary for a definition.

[Vierkantor]

Here's an overview of existing Defs files in Mathlib alongside a quick assessment of their import graph.

Clean Defs files

(including open PRs, as of 2024-11-15)
These files only have definitions and very basic results, and contain only reasonable imports:

• ./Mathlib/Algebra/Algebra/Defs.lean
• ./Mathlib/Algebra/CharZero/Defs.lean
• ./Mathlib/Algebra/Field/Defs.lean
• ./Mathlib/Algebra/Field/Subfield/Defs.lean
• ./Mathlib/Algebra/Group/Commute/Defs.lean
• ./Mathlib/Algebra/Group/Defs.lean
• ./Mathlib/Algebra/Group/Hom/Defs.lean (the import of Mathlib.Algebra.Group.Pi.Basic is on the heavy side and the amount of theory in this file could be reduced; no obvious way to clean it up)
• ./Mathlib/Algebra/Group/Invertible/Defs.lean
• ./Mathlib/Algebra/Group/Subgroup/Defs.lean
• ./Mathlib/Algebra/Group/Submonoid/Defs.lean
• ./Mathlib/Algebra/Group/Submonoid/Defs.lean
• ./Mathlib/Algebra/Group/Subsemigroup/Defs.lean
• ./Mathlib/Algebra/Group/WithOne/Defs.lean
• ./Mathlib/Algebra/GroupWithZero/Defs.lean
• ./Mathlib/Algebra/Module/Defs.lean ([Merged by Bors] - chore(Algebra/Module): further split Defs.lean #18995)
• ./Mathlib/Algebra/Module/Equiv/Defs.lean
• ./Mathlib/Algebra/Module/LinearMap/Defs.lean (big file, but full of only definitions)
• ./Mathlib/Algebra/Module/Submodule/Defs.lean
• ./Mathlib/Algebra/MonoidAlgebra/Definitions.lean
• ./Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
• ./Mathlib/Algebra/Order/Field/Defs.lean
• ./Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean (a few surprising imports but they are all defs, good splitting target)
• ./Mathlib/Algebra/Order/Ring/Defs.lean (can do with some import cleanup)
• ./Mathlib/Algebra/Polynomial/Definitions.lean
• ./Mathlib/Algebra/Polynomial/Degree/Definitions.lean
• ./Mathlib/Algebra/Polynomial/Eval/Definitions.lean
• ./Mathlib/Algebra/Ring/Defs.lean
• ./Mathlib/Algebra/Ring/Int/Defs.lean
• ./Mathlib/Algebra/Ring/Subsemiring/Defs.lean
• ./Mathlib/Data/Array/Defs.lean (not a particularly usefully named file, but it is minimal.)
• ./Mathlib/Data/Countable/Defs.lean (although we might like to rearrange the instances, they are innocuous enough)
• ./Mathlib/Data/DFinsupp/Defs.lean
• ./Mathlib/Data/Finite/Defs.lean
• ./Mathlib/Data/Int/Cast/Defs.lean (should maybe be renamed to AddGroupWithOne.Defs?)
• ./Mathlib/Data/List/Defs.lean (might be a good splitting target but it does not have a lot of theory)
• ./Mathlib/Data/List/EditDistance/Defs.lean
• ./Mathlib/Data/Matrix/Defs.lean
• ./Mathlib/Data/NNRat/Defs.lean (quite a few imports but they're all needed for the instances)
• ./Mathlib/Data/Nat/Cast/Defs.lean
• ./Mathlib/Data/Nat/Prime/Defs.lean
• ./Mathlib/Data/Option/Defs.lean
• ./Mathlib/Data/PNat/Defs.lean
• ./Mathlib/Data/Rat/Defs.lean (on the theory-heavy side, but still reasonable)
• ./Mathlib/Data/Set/Defs.lean
• ./Mathlib/Data/Stream/Defs.lean
• ./Mathlib/Data/String/Defs.lean
• ./Mathlib/Data/Vector/Defs.lean
• ./Mathlib/Data/ZMod/Defs.lean (depends on Mathlib.Algebra.Group.Fin.Basic which could be split a bit more, but it's all rather harmless)
• ./Mathlib/GroupTheory/Coset/Defs.lean
• ./Mathlib/GroupTheory/GroupAction/Defs.lean
• ./Mathlib/GroupTheory/QuotientGroup/Defs.lean
• ./Mathlib/LinearAlgebra/Finsupp/Defs.lean (depends on Mathlib.Data.Finsupp.Basic, but that’s somewhat unavoidable)
• ./Mathlib/Logic/Equiv/Defs.lean (depends on Mathlib.Data.Quot, Mathlib.Data.Bool.Basic which have theory but it's rather fundamental theory)
• ./Mathlib/Logic/Function/Defs.lean
• ./Mathlib/Logic/Nontrivial/Defs.lean
• ./Mathlib/Logic/Small/Defs.lean
• ./Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
• ./Mathlib/Order/Bounds/Defs.lean
• ./Mathlib/Order/Defs.lean
• ./Mathlib/RingTheory/Congruence/Defs.lean
• ./Mathlib/RingTheory/Finiteness/Defs.lean (groups together Submodule, Ideal and Algebra definitions, but that’s probably okay)
• ./Mathlib/RingTheory/Ideal/Defs.lean
• ./Mathlib/RingTheory/Ideal/Quotient/Defs.lean
• ./Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean
• ./Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean
• ./Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Defs.lean
• ./Mathlib/RingTheory/LocalRing/Defs.lean
• ./Mathlib/RingTheory/Noetherian/Defs.lean
• ./Mathlib/RingTheory/NonUnitalSubring/Defs.lean
• ./Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean
• ./Mathlib/RingTheory/WittVector/Defs.lean (imports a lot of theory, all of which appears necessary)
• ./Mathlib/Topology/ContinuousMap/Defs.lean
• ./Mathlib/Topology/Defs/Basic.lean

Nearly clean defs

• ./Mathlib/Algebra/CharP/Defs.lean (lots of theory in the file itself and the imports; good splitting target)
• ./Mathlib/Algebra/Group/Semiconj/Defs.lean (somewhat theory-heavy)
• ./Mathlib/Algebra/Group/Units/Defs.lean (somewhat theory-heavy)
• ./Mathlib/Algebra/Ring/Subring/Defs.lean (should lose the dependency on Data.Int.Cast.Lemmas)
• ./Mathlib/Data/Finset/Defs.lean (depends on Mathlib.Data.Multiset.Nodup which is somewhat messy)
• ./Mathlib/LinearAlgebra/Quotient/Defs.lean (depends on Algebra.Submodule.Basic, good splitting target)
• ./Mathlib/NumberTheory/Harmonic/Defs.lean (there is some theory but it's pretty minor)
• ./Mathlib/Order/Filter/Defs.lean (defs require theory from Mathlib.Data.Set.Basic, which is on the expansive side)
• ./Mathlib/RingTheory/Localization/Defs.lean (could probably do without dependency on Mathlib.Algebra.GroupWithZero.NonZeroDivisors, but that's almost immediately needed for lots of results)
• ./Mathlib/RingTheory/Nilpotent/Defs.lean (imports seem slightly overpowered but almost at the right level)

These files are not definitions-only:

• ./Mathlib/Algebra/Central/Defs.lean (depends on Mathlib.Algebra.Algebra.Subalgebra.Basic)
• ./Mathlib/Algebra/EuclideanDomain/Defs.lean (depends on Mathlib.Algebra.Divisibility.Basic; good splitting target)
• ./Mathlib/Algebra/Group/Action/Defs.lean (contains a lot of results alongside its definition; overall just kind of messy)
• ./Mathlib/Algebra/GroupWithZero/Action/Defs.lean (lots of theory in this file; imports Mathlib.Algebra.Group.Action.Units, Mathlib.Algebra.Group.Equiv.Basic, Mathlib.Algebra.GroupWithZero.Units.Basic; good splitting target)
• ./Mathlib/Algebra/Lie/Semisimple/Defs.lean (depends on Mathlib.Algebra.Lie.Solvable)
• ./Mathlib/Algebra/MonoidAlgebra/Defs.lean (depends on Mathlib.Algebra.BigOperators.Finsupp, Mathlib.Algebra.Module.BigOperators, Mathlib.Data.Finsupp.Basic, Mathlib.LinearAlgebra.Finsupp. good splitting target)
• ./Mathlib/Algebra/Order/Field/Canonical/Defs.lean (depends on Mathlib.Algebra.Order.Sub.Basic)
• ./Mathlib/Algebra/Order/Group/Defs.lean (depends on Mathlib.Algebra.Order.Group.Unbundled.Basic)
• ./Mathlib/Algebra/Order/Module/Defs.lean (file itself and its imports have too much theory)
• ./Mathlib/Algebra/Order/Monoid/Defs.lean (depends on Mathlib.Algebra.Order.Monoid.Unbundled.Basic)
• ./Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean (file itself and its imports have too much theory)
• ./Mathlib/Algebra/Order/Sub/Defs.lean (almost entirely a theory file)
• ./Mathlib/Algebra/Ring/Hom/Defs.lean (depends on Mathlib.Algebra.Group.Pi.Basic, Mathlib.Algebra.Ring.Basic)
• ./Mathlib/Algebra/Ring/Semireal/Defs.lean (depends on Mathlib.Algebra.BigOperators.Group.Finset)
• ./Mathlib/Analysis/CStarAlgebra/Module/Defs.lean (depends on Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order)
• ./Mathlib/Analysis/Calculus/ContDiff/Defs.lean (depends on Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries)
• ./Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean (depends on Mathlib.Analysis.Calculus.Deriv.Basic)
• ./Mathlib/Combinatorics/Additive/AP/Three/Defs.lean (a lot of theory in the file itself)
• ./Mathlib/Combinatorics/Additive/Corner/Defs.lean (depends on Mathlib.Combinatorics.Additive.FreimanHom; good splitting target?)
• ./Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean (depends on Mathlib.CategoryTheory.CofilteredSystem, lots of theory in the file itself)
• ./Mathlib/Data/Finsupp/Defs.lean (depends on Mathlib.Algebra.Group.Indicator, Mathlib.Algebra.Group.Submonoid.Basic; good splitting target)
• ./Mathlib/Data/Int/Defs.lean (actually a theory file!)
• ./Mathlib/Data/NNReal/Defs.lean (depends on Mathlib.Data.Real.Archimedean; good splitting target?)
• ./Mathlib/Data/Nat/Defs.lean (actually a theory file!)
• ./Mathlib/Data/Nat/Factorization/Defs.lean (quite a lot of theory in the file and its imports)
• ./Mathlib/Data/Rat/Cast/Defs.lean (actually a theory file!)
• ./Mathlib/FieldTheory/RatFunc/Defs.lean (depends on Mathlib.RingTheory.Localization.FractionRing; good splitting target)
• ./Mathlib/Geometry/Manifold/ContMDiff/Defs.lean (depends on Mathlib.Geometry.Manifold.LocalInvariantProperties)
• ./Mathlib/Geometry/Manifold/MFDeriv/Defs.lean (depends on Mathlib.Geometry.Manifold.LocalInvariantProperties)
• ./Mathlib/GroupTheory/GroupExtension/Defs.lean (depends on Mathlib.GroupTheory.GroupAction.ConjAct, Mathlib.GroupTheory.SemidirectProduct which looks a bit excessive on first glance, but it might be the correct level of power)
• ./Mathlib/LinearAlgebra/Basis/Defs.lean (depends on Mathlib.LinearAlgebra.Finsupp.LinearCombination and Mathlib.LinearAlgebra.Span.Basic, and lots of theory in the file itself)
• ./Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean (depends on Mathlib.Algebra.Module.Projective; lots of theory in the file itself)
• ./Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean (depends on Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup; good splitting target)
• ./Mathlib/LinearAlgebra/RootSystem/Defs.lean (depends on Mathlib.LinearAlgebra.Dual; good splitting target?)
• ./Mathlib/MeasureTheory/Group/Defs.lean (depends on Mathlib.MeasureTheory.Measure.MeasureSpace; good splitting target?)
• ./Mathlib/MeasureTheory/MeasurableSpace/Defs.lean (all level-1 and level-2 dependencies contain a lot of theory)
• ./Mathlib/MeasureTheory/OuterMeasure/Defs.lean (depends on Mathlib.Topology.Instances.ENNReal which seems excessive; good splitting target?)
• ./Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
• ./Mathlib/Order/Interval/Finset/Defs.lean (depends on Mathlib.Order.Interval.Set.Image)
• ./Mathlib/Probability/Kernel/Defs.lean (basically all level-1 and level-2 dependencies need thorough splitting before)
• ./Mathlib/RingTheory/LocalRing/MaximalIdeal/Defs.lean (depends on Mathlib.RingTheory.LocalRing.Basic -> Mathlib.RingTheory.Ideal.Basic good splitting target)
• ./Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean (depends on Mathlib.RingTheory.Ideal.Quotient; good splitting target)
• ./Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean (all level-1 dependencies contain lots of theory)
• ./Mathlib/RingTheory/Norm/Defs.lean (depends on Mathlib.LinearAlgebra.Determinant; good splitting target)
• ./Mathlib/RingTheory/SimpleRing/Defs.lean (file itself is extremely simple but depends on Mathlib.Order.Atoms which is a bit messy; good splitting target)
• ./Mathlib/RingTheory/Trace/Defs.lean (depends on Mathlib.LinearAlgebra.Matrix.BilinearForm and Mathlib.LinearAlgebra.Trace which in turn depend on too much theory; good splitting target)
• ./Mathlib/Topology/Algebra/InfiniteSum/Defs.lean (file itself is nicely sparse, but depends on Mathlib.Algebra.BigOperators.Finprod, Mathlib.Order.Filter.AtTopBot.BigOperators, Mathlib.Topology.Separation)
• ./Mathlib/Topology/EMetricSpace/Defs.lean (depends on Mathlib.Data.ENNReal.Inv, Mathlib.Topology.UniformSpace.OfFun)
• ./Mathlib/Topology/MetricSpace/Defs.lean (depends on Mathlib.Topology.MetricSpace.Pseudo.Defs)
• ./Mathlib/Topology/MetricSpace/Pseudo/Defs.lean (depends on Mathlib.Data.ENNReal.Real)