Bases of topologies

Stream: mathlib4

[Antoine Chambert-Loir]

In mathlib, bases of a topology are parametrized. This makes the definition of a class such as “IsLinearTopology” difficult because the universe of the index set has to be prescribed in advance (if the class says exists i, i->Ideal R…, the universe of i is imposed…). On the other hand, the bases of a topology only depend on the range of the parametrization so that these universes problems are uninteresting.

[Kevin Buzzard]

You could do the usual nonsense of showing that if you have a basis with some crazy index set then there's an equivalent basis with an indexing set in the same universe as your space (by replacing the index set with its image)

[Anatole Dedecker]

The usual solution is to only consider families of the form Subtype.val indexed by some set

[Anatole Dedecker]

And then of course provide links with the indexed version, like Kevin suggests

[Yury G. Kudryashov]

Where do you see parametrized bases of topologies?

[Yury G. Kudryashov]

Are you talking about docs#TopologicalSpace.IsTopologicalBasis (not parametrized) or docs#Filter.HasBasis applied to docs#nhds ?

[Yury G. Kudryashov]

What condition do you want to write?

[Antoine Chambert-Loir]

It was in the file about no archimedean topologies. So that's very good if we can go in the Set-style way.

[Antoine Chambert-Loir]

We need to formalize a linear topology on a ring (basis of open nhds consisting of ideals).

[Yury G. Kudryashov]

Can you post a docs# link to the definition you're talking about?

[Antoine Chambert-Loir]

Not from my phone, alas...

[Antoine Chambert-Loir]

docs#SubmodulesBasis

[Yury G. Kudryashov]

What predicate do you want to write in terms of this basis? Can you write it with unspecified universes? Then I can help you fix the universes issue.

[Antoine Chambert-Loir]

Your initial answer that in the topology files, bases are written as subsets is much better than trying to solve moot universes issues. The basic index type that one wishes to consider is in a very small type, most often Type 0, and it is not in the expected Type u, and it would be ridiculous to lift it… So I'll rather go as I wanted and define the basis of ideals as a subset of ideals.

[Antoine Chambert-Loir]

Anyway, here is our initial definition of IdealBasis, using parametrized ideals :

/-- A family of ideals of a ring `α` is an `IdealBasis` if the ideals are both left- and
  right-ideals, and if every intersection of two of them contains another one. -/
structure IdealBasis {α : Type _} [Ring α] {ι : Type _} (B : ι → Ideal α) : Prop where
  /-- Every intersection of ideals in `B` contains an ideal in `B`. -/
  inter : ∀ i j, ∃ k, B k ≤ B i ⊓ B j
  /-- Every ideal in `B` is a right ideal. -/
  mul_right : ∀ i {a} r, a ∈ B i → a * r ∈ B i

and here is the class that says that a topology is linear:

class IsLinearTopology (α : Type u) [CommRing α] [τ : TopologicalSpace α]
   where
  ideals : Set (Ideal α)
  nonempty_ideals : Nonempty (ideals)
  isIdealBasis : IdealBasis (fun (J : ideals) ↦ (J : Ideal α))
  isTopology :  τ = isIdealBasis.toRingSubgroupsBasis.topology

after an attempt of the form

class IsLinearTopology (α : Type u) [CommRing α] [τ : TopologicalSpace α]
  toLinearTopology : ∃ (ι : Type*) [Nonempty ι]
    (J : ι → Ideal α) (hJ : IdealBasis J), τ = hJ.toRingSubgroupsBasis.topology

didn't work well.

But we will change IdealBasis to remove the function, and change the rest accordingly.

[Yury G. Kudryashov]

Assume that ι : Set (Ideal α) and J is Subtype.val.

[Junyan Xu]

I've been thinking about introducing two-sided ideal in mathlib; I'm inclined to take @Kevin Buzzard's Ideal.IsTwoSided and make it a typeclass. We'd the provide instances of this typeclass for RingHom.ker, Submodule.colon, Module.annihilator, Jacobson radical, etc. and generalize docs#Ideal.Quotient.commRing to allow Ring + Ideal.IsTwoSided. Initial plans also include generalizing results about local rings and connecting the Jacobson radical with simple modules.
(forgot to mention: generalize Nakayama's lemma (various forms); generalize @Jujian Zhang's #6277 to noncommutative rings and prove the Akizuki–Hopkins–Levitzki theorem; redefine Ideal.IsPrime, ...)

[Jireh Loreaux]

I would really prefer we don't do a half-baked approach to two-sided ideals, because Kevin's suggestion still doesn't fix the other issue: we can't have ideals in non-unital rings. If people besides me want two-sided ideals soon, I'll make it a priority.

[Johan Commelin]

Antoine Chambert-Loir said:

We need to formalize a linear topology on a ring (basis of open nhds consisting of ideals).

I think we have the analogue for topological groups already. I can try to find it later. Would be good to align the designs.

[Johan Commelin]

Aah, I was thinking of docs#GroupFilterBasis

[Johan Commelin]

Ooh docs#ModuleFilterBasis already exists! @Antoine Chambert-Loir That's not on-the-nose the concept that you are looking for, but it might be functionally equivalent? Would that work?

[Antoine Chambert-Loir]

We need the varians IdealBasis

[Johan Commelin]

But maybe using filter bases is still helpful? As opposed to topological bases?

[Antoine Chambert-Loir]

We'll see. It's always possible to redo things. Patrick Massot , what do you think?

[Johan Commelin]

I think that @Patrick Massot wrote the following sentence in the perfectoid paper:

we had to develop the theory of filter bases, which is not so useful for the abstract story, but very convenient to
define concrete instances, like the adic topology defined by an ideal I in a ring R. This I -adic topology is
characterised by the fact that neighbourhoods of zero are subsets containing a power of I .

[Johan Commelin]

So I assume that he'll be a fan of the filter version (-;

[Antoine Chambert-Loir]

I had the impression he also wrote the file on module bases, but we'll look at the filter basis stuff.

[Anatole Dedecker]

I think there is a misunderstanding here: docs#RingSubrougpsBasis, docs#SubmodulesBasis etc… are already about filter bases (for neighborhoods of zero), not topological bases. In fact, the associated topology is defined using docs#RingFilterBasis, docs#ModuleFilterBasis, …

[Anatole Dedecker]

I think the only reason docs#RingSubgroupsBasis doesn’t explicitly mention docs#FilterBasis or docs#Filter.HasBasis is that it would be harder to state "a filter basis made of ideals" than just redoing the condition by hand

[Antoine Chambert-Loir]

There's probably a misunderstanding, but my issue is that a docs#RingSubgroupsBasis or a docs#SubmodulesBasis are defined as families, while a docs#FilterBasis or a docs#RingBasis are defined as sets.

[Anatole Dedecker]

Yes I understand, I was talking only about the last few messages with Johan.

[Anatole Dedecker]

I think the right design choice here is to have IdealBasis defined in terms of families, but restricting families to subset in the definition of IsLinearTopology (from what I understand you had such a version at some point ?).

One reason we like indexed families so much in mathlib (e.g the most used piece of the filter bases API, docs#Filter.HasBasis) is that they compose well. If you have the set version, doing an operation on each set of your basis (e.g pulling it backwards through a ring hom) will be stated in terms of docs#Set.image, which is nasty in that it introduces useless existentials. I'm not at my computer right now so I can't cook up a good example, but I explained some of it in the docstring of Topology/UniformSpace/Equicontinuity.

[Antoine Chambert-Loir]

I understand that it is easier to manipulate functions than their Set.range.

[Anatole Dedecker]

I think it would be reasonable to redefine docs#ModuleFilterBasis in terms of docs#Filter.IsBasis instead of docs#FilterBasis, but these aren't really used as much as they are in the litterature (e.g Bourbaki, TVS) so I think it just hasn't been annoying enough for people to change it.

[Kevin Buzzard]

Re Junyan's comment above: don't take anything I suggest about ideals at all seriously: I have no real understanding of the issues here and my preference is definitely to keep Jireh happy as he's clearly thought about the issue a lot (we even have a roadmap, right?)

[Kevin Buzzard]

My main contribution here should be thought of as pushing through the commutative theory aggressively back in 2017/8 so I could go around telling people I'd defined schemes, without ever thinking for one minute about the noncommutative case. But it was an extremely different world back then.

[Patrick Massot]

I’d be very surprised if you need the topology basis and not only the neighborhood of zero basis.

[Antoine Chambert-Loir]

Well, as I wrote, I want a linear topology on a ring, so that's the kind of docs#RingFilterBasis given by ideals.
(BTW, there is a misprint in the documentation, an example of a RingFilterBasis is likely to be the neighborhoods of 0 rather than “identity” — which I interpret as 1). For docs#RingFilterBasis, everything is about sets, sets of sets…
and we need essentially that, except that we have ideals, and there is the dichotomy docs#SubmodulesBasis and docs#ModuleFilterBasis. (I believe we need the analogue of both, for Ideals, and I'm not sure — yet — that any RingFilterBasis would work. If we have to insist that they are ideals, then we need something like docs#IdealsBasis, except that they are parametrized and they add universe issues — the goal is to evaluate power series in any complete linearly topologized comm ring.)

[Patrick Massot]

The identity thing is clearly a copy-paste issue coming from the group case.