Is this statement about filters true?

Stream: maths

[Etienne Marion]

Hi, I'm struggling to prove the following statement:

import Mathlib

open Filter Topology

example {X Y : Type*} [AddCommGroup X] [TopologicalSpace X] [ContinuousAdd X]
    (s : AddSubgroup X) (x y : X) (hs : Dense (s : Set X)) :
    Tendsto (fun a : s × s ↦ (a.1 + a.2 : X)) (((𝓝 x).comap ((↑) : s → X)) ×ˢ ((𝓝 y).comap ((↑) : s → X))) (𝓝 (x + y)) := by
  sorry

I am not sure whether it is true or not. What do you think? Maybe it requires more assumption on the topology?

[Patrick Massot]

Of course it’s true. But it has nothing to do with s being dense.

[Patrick Massot]

Asking for s to be dense is a remnant of the old time where ⊥ was not a filter and you could not have stated this.

[Patrick Massot]

Maybe you are missing docs#Filter.comap_prodMap_prod ?

[Patrick Massot]

And you need to use that https://q.uiver.app/#q=WzAsMyxbMCwwLCJzIMOXIHMiXSxbMCwxLCJYIMOXIFgiXSxbMSwwLCJYIl0sWzAsMSwizrkgw5cgzrkiLDJdLFswLDIsIitfcyJdLFsxLDIsIitfWCIsMl1d commutes.

[Patrick Massot]

which is rfl (or maybe ext; rfl…).

[Patrick Massot]

Note is also has nothing to do with s being a subgroup. Is it really what you wanted to state?

[Etienne Marion]

Thanks for your answer. This is indeed the statement I intended to prove. I had already found these ingredients but I did not use them in the right way it seems :sweat_smile: Also I agree that the density hypothesis is useless, I was struggling without it and as in my context it was true I thought maybe it would help. The subgroup hypothesis is necessary in my context but that doesn't matter. Anyway thanks for your reply as it convinced me that it was true and I managed the proof!

import Mathlib

open Filter Topology

example {X : Type*} [AddCommGroup X] [TopologicalSpace X] [ContinuousAdd X]
    (s : Set X) (x y : X) :
    Tendsto (fun a : s × s ↦ (a.1 + a.2 : X)) (((𝓝 x).comap ((↑) : s → X)) ×ˢ ((𝓝 y).comap ((↑) : s → X))) (𝓝 (x + y)) := by
  have : (fun x : s × s ↦ (x.1 : X) + x.2) = (fun x ↦ x.1 + x.2) ∘ (Prod.map Subtype.val Subtype.val) := by
    ext x; simp
  rw [← comap_prodMap_prod, this, ← tendsto_map'_iff, ← nhds_prod_eq]
  exact (continuous_add.tendsto (x, y)).mono_left map_comap_le

[Patrick Massot]

I checked with Lean and actually my commutative diagram is sufficiently rfl that Lean does not need it. So you can go with

example {X : Type*} [AddCommGroup X] [TopologicalSpace X] [ContinuousAdd X]
    (s : Set X) (x y : X) :
    Tendsto (fun a : s × s ↦ (a.1 + a.2 : X)) (((𝓝 x).comap ((↑) : s → X)) ×ˢ ((𝓝 y).comap ((↑) : s → X))) (𝓝 (x + y)) := by
  rw [← Filter.comap_prodMap_prod, ← nhds_prod_eq]
  exact tendsto_add.comp tendsto_comap

[Etienne Marion]

I see, thanks!

[Patrick Massot]

where docs#Filter.tendsto_comap is the co-unit of the adjunction between direct image and inverse image but phrased as a Tendsto.