Cleaning up `Data`

Stream: mathlib4

[Michael Rothgang]

Question of the day: where should Data/Matrix/DoublyStochastic live? Opinions welcome! This may be related to the purpose of the Data directory, which is rather broad at the moment.

[Kevin Buzzard]

What decides whether work goes into Data/Matrix or LinearAlgebra/Matrix?

[Michael Rothgang]

I don't know! "If it imports something from LinearAlgebra, it goes there"?

[Eric Wieser]

For mostly leaf files does it matter that much?

[Yaël Dillies]

I would argue that anything under Data should be about... data structures. Probably most of Data.Matrix should move

[Yaël Dillies]

Data.Matrix.DoublyStochastic should IMO live in Analysis.Convex.Matrix or alike

[Michael Rothgang]

Any objections to moving Data/Complex/FiniteDimensional to Analysis? Most of it is linear algebra, but docs#Complex.rank_rat_complex uses the cardinality of the complex numbers (which uses the cardinality of the real numbers, which uses a convergent series, i.e. analysis).

[Kim Morrison]

I agree here: the Mathlib Matrix should not live in Data at all. :-) If there was a Matrix living in Data it should be Vector (Vector α m) n, or some structure for efficiently representing sparse matrices.

[Michael Rothgang]

Great! I have a PR which makes Data not import Analysis: once #28948 and #28955 are merged, it will be ready for review.

[Michael Rothgang]

That PR (#28953) is now unblocked

[Michael Rothgang]

Where should Data.Real.Irrationalmove? It imports RingTheory.Algebraic.Basis (to say that transcendental numbers are irrational); that doesn't feel like Data territory to me. Or should the file be split?

[Michael Rothgang]

Similar question about Data.Real.GoldenRatio: the material itself is quite elementary; it depends on Real.Irrational, though.

[Kevin Buzzard]

GoldenRatio really is data! But so is pi -- where is that defined? As for Data/Real/Irrational, maybe it should go in RingTheory/Real ?

[Michael Rothgang]

Real.pi is defined in Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic.

[Ruben Van de Velde]

It may be data, but it's not a data structure

[Jireh Loreaux]

Arguably Irrational could be split into Irrational and Transcendental, but I'm not sure how worthwhile such a split is at the moment.

[Yaël Dillies]

Irrational and Transcendental feel like they belong in NumberTheory

[Yaël Dillies]

I assume we'll eventually have NumberTheory.DiophApprox

[Michael Stoll]

There is Mathlib.NumberTheory.DiophantineApproximation.{Basic|ContinuedFractions}.

[Bhavik Mehta]

Transcendental feels more like algebra than number theory to me

[Bhavik Mehta]

Ah, it's in RingTheory already, that makes sense too

[Michael Rothgang]

#29002 proposes moving it to RingTheory/Real: I'm still on the fence if this is the best location.

[Michael Rothgang]

#28966 is next in the list, and moves most fo Data/Matrix

[Michael Rothgang]

Michael Rothgang said:

#29002 proposes moving it to RingTheory/Real: I'm still on the fence if this is the best location.

Four-week review ping

[Riccardo Brasca]

Does it make sense to also move Mathlib.Data.Real.GoldenRatio?

[Kim Morrison]

RingTheory/Real seems an improvement.

[Michael Rothgang]

#30498 moves GoldenRatio to Mathlib/NumberTheory

[Ruben Van de Velde]

Michael Rothgang said:

#30498 moves GoldenRatio to Mathlib/NumberTheory

Doesn't build

[Michael Rothgang]

Thanks; fixed now!

[Michael Rothgang]

Looking over open t-data PRs, I wonder: should Data.Real.Sqrt be in this directory, or elsewhere?

[Michael Rothgang]

Same question for Data.Nat.Factorisation: one could argue this is elementary number theory.

[Ruben Van de Velde]

How about Data.Nat.Prime? :innocent:

[Kim Morrison]

None of these three should be in Data: there are not about data types.