First pull request

Stream: mathlib4

[Jonas van der Schaaf]

I wrote my first pull request yesterday, but it doesn't pass the CI tests. I get the following warning:

warning: Mathlib/ModelTheory/Types.lean:13:0: Modules starting with Mathlib.ModelTheory are not allowed to import modules starting with Mathlib.Topology. This module depends on Mathlib.Topology.Defs.Basic

Why is importing files from Topology not allowed in ModelTheory?

Of course, any feedback on the lean code is also welcome. I'm sure my code is less than optimal :innocent:.

[Ruben Van de Velde]

The goal is to avoid every part of mathlib depending on every other part like a bowl of spaghetti. I don't know much about this particular case though. Would you say the dependency on topology is fundamental to what you're doing?

[Kevin Buzzard]

The simplest approach might be to put the material in the Topology directory rather than where you have currently put it.

For example the reals are defined in Data/Real/Basic.lean but the topological space structure on it is defined (via the metric space structure) in Topology/MetricSpace/Pseudo/Defs.lean rather than in Data/Real.

[Aaron Liu]

I feel like this is definitely model theory and I would be confused if I was looking for it and found it under topology instead of model theory

[Aaron Liu]

like for example docs#krullTopology is in FieldTheory/KrullTopology it's not under Topology

[Kevin Buzzard]

It's model theory but it's also topology!

[Aaron Liu]

I've seen the real numbers come up naturally in topology

[Aaron Liu]

I've never seen the model-theory types come up in topology

[Aaron Liu]

but well :shrug: I'm not a model theorist maybe this is secretly topology

[Kevin Buzzard]

yeah Topology/Instances does seem to be about concrete types rather than things like CompleteType T α. I don't know how much topology model theorists need. If they need a bunch of facts from topology then we might have to revisit the restriction (which was added in #23088 in the file Mathlib/Tactic/Linter/DirectoryDependency.lean by @Anne Baanen ).

[Jonas van der Schaaf]

I won't dare say how much topology is needed. I think it's better to let more seasoned model theorists than me weigh in on this (I think I spotted a few, can I just tag people in here?).

[Matthew Ballard]

At the least there should be a new file/folder, I don’t know how smart the linter is though…

[Ruben Van de Velde]

Yeah, we could exempt ModelTheory/Topology, for example