Rearranging files in `data/`

Stream: general

[Anne Baanen]

I still don't understand the split between data/polynomial, algebra/polynomial and ring_theory/polynomial, to be honest...

[Patrick Massot]

I still don't understand data...

[Damiano Testa]

Besides feeling silly, I am comforted by the fact that more people find the split weird!

[Yaël Dillies]

Some things definitely belong under data, like list, multiset, finset, sym, sym2... I do not quite see why polynomial should be one of them.

[Yaël Dillies]

Arguably, finsupp does belong under data. So the philosophy I suggest is to view finsupp as the data analog to polynomial, and polynomial as the ring theory analog to finsupp.

[Anne Baanen]

IMO data.equiv is the least understandable, why do we collect a random set of isomorphisms there instead of the structures that they preserve?

[Yaël Dillies]

I have been actively working against this, by putting properties of docs#order_iso under order.hom..

[Anne Baanen]

That is: move data/equiv/mul_add.lean → algebra/group/equiv.lean, ring.lean → algebra/ring/equiv.lean, module.lean → algebra/module/equiv.lean, etc.

[Yaël Dillies]

Yes please!

[Yaël Dillies]

(just note that there is now a algebra.hom. folder, so maybe those should rather be algebra.hom.module.equiv, algebra.hom.group.equiv, or be merged with the existing files there, which to me sounds best)

[Anne Baanen]

Perhaps even rename (the slimmed-down version of) data/equiv to logic/equiv?

[Yaël Dillies]

While we're at it, docs#continuous_map imports docs#homeomorph, and to me it should clearly be the other way around.

[Notification Bot]

12 messages were moved here from #Is there code for X? > char_p instance on polynomials by Anne Baanen.

[Anne Baanen]

Ok, I'll try and rearrange data/equiv after I finish eating my lunch!

[Eric Rodriguez]

file#data/equiv/embedding is basically just used for the cardinality of the embeddings, I'm not sure where it could go

[Anne Baanen]

I think I'll move docs#encodable and docs#denumerable to logic/ directly, rather than logic/equiv.

[Anne Baanen]

Eric Rodriguez said:

file#data/equiv/embedding is basically just used for the cardinality of the embeddings, I'm not sure where it could go

I think this can stay in logic/equiv/embedding.lean, or perhaps logic/embedding/equiv.lean.

[Anne Baanen]

#12929

[Kevin Buzzard]

Yaël Dillies said:

Arguably, finsupp does belong under data. So the philosophy I suggest is to view finsupp as the data analog to polynomial, and polynomial as the ring theory analog to finsupp.

This reminds of fin n v zmod n. They're different in an edge case but otherwise they're defeq, although one feels like data and one like ring theory.