opposite of RingFilterBasis

Stream: mathlib4

[Kevin Buzzard]

The point of docs#RingFilterBasis is that if we have a bunch of subsets of a ring satisfying some axioms (e.g. "they all contain 0") then there's a topology on the ring making it a topological ring (i.e. +,-,* are continuous) and such that the given subsets are a basis of nhds of 0. I need the converse (for a topological ring, all the axioms are satisfied by the open nhds of 0) and right now I'm not even sure how to state it sensibly because it's not about the neighbourhoods of 0, it's about open neighbourhoods of 0. More precisely, do we have these? Or some version which is mathematically equivalent?

import Mathlib

section AntiRingFilterBasis

variable {R : Type*} [Ring R] [TopologicalSpace R] [TopologicalRing R]

/- The point of `RingFilterBasis` is "if these subsets of a ring satisfy some axioms
then there's a topological ring structure such that these subsets are a basis of
open neighbourhoods of 0".

The below lemmas are the converse to this.
-/

namespace TopologicalRing

open scoped Pointwise

lemma ringFilterBasis_add {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U := by
  sorry

lemma ringFilterBasis_neg {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V ⊆ (fun x ↦ -x) ⁻¹' U := by
  sorry

lemma ringFilterBasis_mul {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V * V ⊆ U := by
  sorry

lemma ringFilterBasis_mul_left (r : R) {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V ⊆ (fun x ↦ r * x) ⁻¹' U := by
  sorry

lemma ringFilterBasis_mul_right (r : R) {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V ⊆ (fun x ↦ x * r) ⁻¹' U := by
  sorry

end TopologicalRing

end AntiRingFilterBasis

They won't be hard to prove but before I set them as an FLT chore I thought I'd check that I wasn't wasting people's time.

[Junyan Xu]

Do you want 0 or 1 in ringFilterBasis_mul? (Apparently we do want 0.) There's docs#exists_open_nhds_one_mul_subset and the additive version. The others are about single-variable functions and you can simply take V to be the preimage of U.

[Patrick Massot]

Why do you want open neighborhood? Is it only because you are following an existing text where people write "open neighborhood” out of habit only?

[Anatole Dedecker]

This is HasBasis.isRingBasis in PR#18437, which is still waiting for review

[Anatole Dedecker]

Combined with docs#nhds_basis_opens of course

[Anatole Dedecker]

That said, these kind of statements are often not what you really want to use.

[Kevin Buzzard]

Here's more information then:

import Mathlib

section AntiRingFilterBasis

variable {R : Type*} [Ring R] [TopologicalSpace R] [TopologicalRing R]

/- The point of `RingFilterBasis` is "if these subsets of a ring satisfy some axioms
then there's a topological ring structure such that these subsets are the
open neighbourhoods of 0".

The below lemmas are the converse to this.
-/

namespace TopologicalRing

open scoped Pointwise

lemma ringFilterBasis_add {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U := by
  sorry

lemma ringFilterBasis_neg {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V ⊆ (fun x ↦ -x) ⁻¹' U := by
  sorry

lemma ringFilterBasis_mul {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V * V ⊆ U := by
  sorry

lemma ringFilterBasis_mul_left (r : R) {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V ⊆ (fun x ↦ r * x) ⁻¹' U := by
  sorry

lemma ringFilterBasis_mul_right (r : R) {U : Set R} (hUopen : IsOpen U) (hU0 : 0 ∈ U) :
    ∃ V : Set R, IsOpen V ∧ 0 ∈ V ∧ V ⊆ (fun x ↦ x * r) ⁻¹' U := by
  sorry

end TopologicalRing

end AntiRingFilterBasis

variable {ι : Type*}

namespace Ring

variable (R : ι → Type*) [∀ i, Ring (R i)] (A : (i : ι) → Subring (R i))

def RestrictedProduct := {x : (i : ι) → R i // ∀ᶠ i in Filter.cofinite, x i ∈ A i}

namespace RestrictedProduct

instance (R : ι → Type*) [∀ i, Ring (R i)] (A : (i : ι) → Subring (R i)) :
    Ring (RestrictedProduct R A) where
  add x y := ⟨fun i ↦ x.1 i + y.1 i, sorry⟩
  add_assoc := sorry
  zero := ⟨fun i ↦ 0, sorry⟩
  zero_add := sorry
  add_zero := sorry
  nsmul n x := ⟨fun i ↦ n • x.1 i, sorry⟩ -- is this a good idea or not? Someone who understands
                                          -- nsmul diamond issues should be asked about this.
  nsmul_zero := sorry -- ditto
  nsmul_succ := sorry -- ditto
  add_comm := sorry
  mul x y := ⟨fun i ↦ x.1 i * y.1 i, sorry⟩
  left_distrib := sorry
  right_distrib := sorry
  zero_mul := sorry
  mul_zero := sorry
  mul_assoc := sorry
  one := ⟨fun i ↦ 1, sorry⟩
  one_mul := sorry
  mul_one := sorry
  neg x := ⟨fun i ↦ -x.1 i, sorry⟩
  neg_add_cancel := sorry
  zsmul z x := ⟨fun i ↦ z • x.1 i, sorry⟩ -- similarly this should be checked.
  zsmul_zero' := sorry -- ditto
  zsmul_succ' := sorry -- ditto
  zsmul_neg' := sorry -- ditto

def structureMap : (∀ i, A i) →+* (RestrictedProduct R A) where
  toFun x := ⟨fun i ↦ (x i).1, sorry⟩
  map_zero' := rfl
  map_one' := rfl
  map_add' x y := rfl
  map_mul' x y := rfl

instance : Module (∀ i, A i) (RestrictedProduct R A) := (structureMap R A).toModule

section Topology

variable [∀ i, TopologicalSpace (R i)] [∀ i, TopologicalRing (R i)]
    (hAopen : ∀ i, IsOpen (A i : Set (R i)))

def ringFilterBasis : RingFilterBasis (RestrictedProduct R A) where
  sets := {U | ∃ V : Set (∀ i, A i), IsOpen V ∧ 0 ∈ V ∧ structureMap R A '' V = U}
  nonempty := ⟨_, ⊤, isOpen_univ, trivial, rfl⟩
  inter_sets := by
    rintro _ _ ⟨V, hVopen, hV0, rfl⟩ ⟨W, hWopen, hW0, rfl⟩
    exact ⟨structureMap R A '' (V ∩ W), ⟨V ∩ W, IsOpen.inter hVopen hWopen, Set.mem_inter hV0 hW0,
      rfl⟩, Set.image_inter_subset _ _ _⟩
  zero' {_} := by
    rintro ⟨V, hVopen, hV0, rfl⟩
    exact ⟨0, hV0, rfl⟩
  add' {_} := by
    rintro ⟨V, hVopen, hV0, rfl⟩
    obtain ⟨W, hWopen, hW0, hWadd⟩ := TopologicalRing.ringFilterBasis_add hVopen hV0
    refine ⟨_, ⟨W, hWopen, hW0, rfl⟩, ?_⟩
    rintro _ ⟨_, ⟨x, hx, rfl⟩, _, ⟨y, hy, rfl⟩, rfl⟩
    exact ⟨x + y, hWadd <| Set.add_mem_add hx hy, rfl⟩
  neg' {_} := by
    rintro ⟨V, hVopen, hV0, rfl⟩
    obtain ⟨W, hWopen, hW0, hWneg⟩ := TopologicalRing.ringFilterBasis_neg hVopen hV0
    refine ⟨_, ⟨W, hWopen, hW0, rfl⟩, ?_⟩
    rintro _ ⟨x, hx, rfl⟩
    exact ⟨-x, hWneg hx, rfl⟩
  conj' r {_} := by
    rintro ⟨V, hVopen, hV0, rfl⟩
    refine ⟨_, ⟨V, hVopen, hV0, rfl⟩, ?_⟩
    simp
  mul' {_} := by
    rintro ⟨V, hVopen, hV0, rfl⟩
    obtain ⟨W, hWopen, hW0, hWmul⟩ := TopologicalRing.ringFilterBasis_mul hVopen hV0
    refine ⟨_, ⟨W, hWopen, hW0, rfl⟩, ?_⟩ -- wtong, need smaller V
    rintro _ ⟨_, ⟨x, hx, rfl⟩, _, ⟨y, hy, rfl⟩, rfl⟩
    exact ⟨x * y, hWmul <| Set.mul_mem_mul hx hy, rfl⟩
  mul_left' r {_} := by
    rintro ⟨V, hVopen, hV0, rfl⟩
    -- strat: shrink V to make it ∏ᵢ Vᵢ with Vᵢ open in Aᵢ and Vᵢ = Aᵢ for all but finitely many i.
    -- Now define Wᵢ open in Aᵢ thus. If Vᵢ = Aᵢ and rᵢ ∈ Aᵢ then set Wᵢ = Aᵢ (this happens for
    -- all but finitely many i). Now what about the bad i?
    -- For these, apply `ringFilterBasis_mul_left` to Rᵢ, rᵢ and the image of Vᵢ to get
    -- Wᵢ with rᵢWᵢ ⊆ Vᵢ. Then ∏ᵢ Wᵢ works.
    sorry
  mul_right' := sorry -- probably have to repeat the argument mutatis mutandis.

instance : TopologicalSpace (RestrictedProduct R A) := (ringFilterBasis R A).topology

-- instance : TopologicalRing (RestrictedProduct R A) := inferInstance

/-
RingSubgroupsBasis.hasBasis_nhds_zero.{u_1, u_2} {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι]
  {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) : (𝓝 0).HasBasis (fun x ↦ True) fun i ↦ ↑(B i)
-/

-- PR and refactor `RingSubgroupsBasis.hasBasis_nhds_zero`
open Filter in
lemma _root_.RingFilterBasis.hasBasis_nhds_zero {A : Type*} [Ring A]
    (B : RingFilterBasis A) : HasBasis (@nhds A B.topology 0) (fun _ => True)
    fun (i : {S // S ∈ B.sets}) => i :=
  ⟨by
    intro s
    rw [B.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
    constructor
    · rintro ⟨t, h0, hi⟩
      exact ⟨⟨t, h0⟩, trivial, hi⟩
    · rintro ⟨i, -, hi⟩
      exact ⟨i.1, i.2, hi⟩⟩

lemma continuous_structureMap : Continuous (structureMap R A) := by
  -- this must help
  have := RingFilterBasis.hasBasis_nhds_zero (ringFilterBasis R A)
  sorry

lemma isOpenMap_structureMap : IsOpenMap (structureMap R A) := by
  sorry

end Topology

end Ring.RestrictedProduct

Mathematically, what's happening is the following. I have a bunch of rings $R_i$ each equipped with a subring $A_i$. I want to define the restricted product $\prod_i'R_i$ of the $R_i$ with respect to the $A_i$ (the dash represents "restricted product"); this is the subring of $\prod_i R_i$ consisting of elements which are in $A_i$ for all but finitely many $i$. Note that $\prod' R_i$ contains $\prod_i A_i$ as a subring.

What I now want to do is, if the $R_i$ are all topological rings and the $A_i$ are open subrings, to put a topology on the restricted product making it into a topological ring. Important note: the answer in general is not "give it the subspace topology coming from $\prod_i R_i$". In the books they just say "let $\prod_i A_i$ be open with the product topology". I want to make this construction in Lean using RingFilterBasis (because in my mind that's exactly what it's for), so I take the open nhds of 0 in $\prod_i A_i$, push them forward to $\prod'_i R_i$ and now I need to check the axioms. Each axiom for $\prod'_i R_i$ comes from the corresponding axiom for $\prod_i A_i$ or for the individual $R_i$, and both of these are topological rings, so in my approach outlined above I need to go backwards using the rings which I know are topological rings, in order to go forwards for the ring which I don't know yet is a topological ring.

I am very much open to other approaches.

[Junyan Xu]

For the Ring instance, why not just take the instance as a Subring of the Pi ring? That should be free of any diamond issues. For performance reasons, maybe you want to do something like

def Subring.restrictedProduct : Subring ((i : ι) → R i) := sorry
def RestrictedProduct : Type _ := Subring.restrictedProduct R A
instance : Ring (RestrictedProduct R A) := inferInstanceAs (Ring <| Subring.restrictedProduct R A)

[Kevin Buzzard]

Yes that's a much better idea -- thanks. It doesn't solve the topology question in this thread though.

[Andrew Yang]

docs#exists_open_nhds_zero_add_subset gives the additive one, and you might be able to mimic the proof of docs#exists_open_nhds_one_split to get the multiplicative one easily. For the other three, you can just take = instead of ⊆ right?

[Anatole Dedecker]

I think if you go the RingFilterBasis route, the right approach is to use #18437 instead of reinventing the wheel. I have another approach in mind though, let me think for a bit.

[Kevin Buzzard]

#18437

[Anatole Dedecker]

/me is working on restricted products (I'll open a draft PR later this afternoon)

[Anatole Dedecker]

#20021

The RestrictedProductDraft is a huge mess you shouldn't look at, the only reason it's still there is I want to save some missing lemmas that ended up not being useful.

[Anatole Dedecker]

The approach is the following: equip RestrPi R A (I shortened the name but I can revert that) with the inductive limit topology coming from the RestrPi.Pre R A S := {x : Π i, R i // ∀ i ∉ S, x i ∈ A i}, with S finite.

[Anatole Dedecker]

I had read about this a few weeks ago when Kevin started thinking about restricted products, but I was wondering how you would prove continuity of multiplication and addition since products and coinduced topology do not interact well at all. But Kevin's question from yesterday made me realize this had to come from openness of the A is.

Indeed, with some usual abstract nonsense, I prove that each Pre R A S is actually topologically embedded in the restricted product, and that embedding is open if all A is are. So when proving continuity we can just work as if we had not taken any inductive limit (this is completely analogous to what happens for spaces of distributions btw).

It took me some time to formulate this "as if we had not taken any inductive limit" in a usable way, but this morning I was struck with continuous_dom_prod_right, which says that the universal property of the inductive limit topology still holds (in this strict case) when you make the product with an arbitrary topological space. Thus RestrPi R A × RestrPi R A also has a nice universal property, and everything becomes abstract nonsense.

[Anatole Dedecker]

Just because the argument is nice, the fact that Pre R A S is embedded in RestrPi R A simply comes from the fact that the embedding Pre R A S → Π i, R i is the composition of the map Pre R A S → RestrPi R A (continuous by construction) and the map RestrPi R A → Π i, R i (continuous by universal property), and then we use docs#Topology.IsInducing.of_comp.

[Kevin Buzzard]

BTW if you want a basic test to see if your definition of topology is usable, it would be to show that if all the open subrings A_i are compact then the restricted product is locally compact.

[Kevin Buzzard]

And many thanks for doing this! It is an ongoing problem with FLT that because we are mostly doing "basic" stuff right now, I am continually finding that someone (e.g. me) is having to PR stuff to mathlib, so it's always a relief when someone else comes along and relieves me of a task like this. It feels a bit crappy opening an issue on FLT saying "please move all this code to mathlib because I don't want to maintain it"

[Anatole Dedecker]

In some sense it's at least as usable as what you were going to do, because you have the topological ring instance and the fact that the product of all A is embeds as an open subset (in particular you know the filter of neighborhoods of zero).

[Andrew Yang]

Is it possible to generalize this to arbitrary filters other than cofinite? I might need a version of this for a non-principal ultrafilter instead for FLT.

[Anatole Dedecker]

Well, depends on what you mean by "this". Putting the inductive limit topology definitely works, but AFAICT things seem to break down precisely on the nontrivial part because Π i, A i (or any of the Pre R A S where S is not finite) has no reason to be open for the inductive limit topology. Could you describe what topology you have in mind (e.g a basis of neighborhoods of zero)?

[Kevin Buzzard]

I suspect that Andrew doesn't need a topology, so it would just be the construction of the restricted product for groups or rings or additive groups or modules.

[Anatole Dedecker]

Ah, then sure that works.

[Anatole Dedecker]

I just pushed a proof of local compactness. I'll have to leave this on the side for the rest of this week though, so feel free to push to that branch.

[Anatole Dedecker]

I forgot to tell that I worked on another API for restricted products during the holiday which does incorporate arbitrary filters (although as I said most topological nice facts do not apply). It's in file RestrictedProduct2 of draft PR #20021. The nice thing about it is that there is no longer a need for the RestrPi.Pre type I had previously, since it's just a restricted product for a principal filter (and the topology matches). The more annoying one is that some things naturally appear as f ≤ 𝓟 s rather than s ∈ f , which is one rewrite away.

[Anatole Dedecker]

Also the way I do things we do put a topology on the restricted product for any filter, even though it's not well-behaved. This may be a problem if there is a better topology in that context.

[Anatole Dedecker]

I will make a proper PR probably rather soon, but I'm open to any input already.