product of (pre)connected spaces

Stream: maths

[Yury G. Kudryashov]

I'm trying to formalize https://ncatlab.org/nlab/show/connected+space#basic, Example 3.4. They deal with

example {α : Type*} {π : α → Type*} [∀ a, topological_space (π a)] [∀ a, connected_space (π a)] (U₁ U₂ : set (Π a, π a))
  (h₁ : is_open U₁) (h₂ : is_open U₂) (hne₁ : U₁.nonempty) (hne₂ : U₂.nonempty) (hd : disjoint U₁ U₂)
  (hU : U₁ ∪ U₂ = univ) : false

I don't understand how they prove that one can choose x ∈ U₁ and y ∈ U₂ that differ only at a finite number of indices.

Observe first that if so, then we could find $x_1\in U_1$ and $x_2 \in U_2$ whose coordinates differed only at a finite subset of $I$. This is since by the nature of the Tychonoff topology $\pi_i(U_1) = X_i$ and $\pi_i(U_2) = X_i$ for all but a finite number of $i \in I$.

[Yury G. Kudryashov]

What property of the Tychonoff topology do they use here? I interpreted their formulas as

example [∀ a, topological_space (π a)] {s : set (Π a, π a)}
  (hs : is_open s) : ∃ I : finset ι, ∀ f g₁ g₂, I.piecewise f g₁ ∈ s ↔ I.piecewise f g₂ ∈ s :=

but this doesn't seem to be true for s = ⋃ a, {f : Π a, π a | f a ∈ t a}, where t a : set (π a) is an open set.

[Adam Topaz]

@Yury G. Kudryashov we have docs#is_topological_basis_pi which could be helpful for this

[Yury G. Kudryashov]

So, the correct argument should say something like: take $x_1\in U_1$ and $x_2\in U_2$. For each of them, take a nhd from the basis. Then proceed as in ncatlab.

[Yury G. Kudryashov]

I should've tried to think about it again in the morning before posting a question.

[Adam Topaz]

Well, I don't think you can choose $x_1,x_2$ ahead of time. But you can show that for some $x_1$ and $x_2$ this property holds

[Adam Topaz]

The point is that $U_i$ contains a set of the form $\prod_i A_i$ where for all $i$, $A_i \subset X_i$ is open, and for all but finitely many of the $i$, one has $A_i = X_i$.

[Adam Topaz]

@Yury G. Kudryashov in case it helps

import topology.bases

variables {α : Type*} (X : α → Type*) [∀ i, topological_space (X i)]

open topological_space

theorem foobar (x y' : Π i, X i) (U : set (Π i, X i))
  (hU : is_open U) (hy' : y' ∈ U) :
  ∃ (y : Π i, X i) (hy : y ∈ U) (F : finset α),
  ∀ i, i ∉ F → x i = y i :=
begin
  have Ti : ∀ i, is_topological_basis { A : set (X i) | is_open A } :=
    λ i, is_topological_basis_opens,
  have T := is_topological_basis_pi Ti,
  obtain ⟨V,⟨Vs,F,hV,rfl⟩,hV2,hV3⟩ := T.exists_subset_of_mem_open hy' hU,
  classical,
  let y : Π i, X i := λ i, if hi : i ∈ F then y' i else x i,
  refine ⟨y,_,F,_⟩,
  { apply hV3, simp,
    intros i hi,
    dsimp [y],
    rw if_pos hi,
    simp at hV2,
    apply hV2 i hi },
  { intros i hi,
    dsimp [y],
    rw if_neg hi }
end

[Yury G. Kudryashov]

I was proving the same lemma.

[Adam Topaz]

I'm sure you could golf it to 5 lines ;)

[Yury G. Kudryashov]

I modified docs@filter.mem_infi' to give a bit more info, then wrote

lemma exists_mem_eventually_eq_cofinite_of_mem_nhds [Π a, topological_space (π a)]
  {s : set (Π a, π a)} {x : Π a, π a} (hs : s ∈ 𝓝 x) (y : Π a, π a) :
  ∃ z ∈ s, ∀ᶠ a in cofinite, (z : _) a = y a :=
begin
  simp only [nhds_pi, mem_infi', mem_comap] at hs,
  rcases hs with ⟨I, hI, V, hV, hV_univ, rfl, -⟩,
  choose t ht htV using hV,
  refine ⟨I.piecewise x y, mem_bInter $ λ i hi, _, mem_cofinite.2 (hI.subset _)⟩,
  { exact htV i (by simpa [hi] using (mem_of_mem_nhds (ht i))) },
  { exact compl_subset_comm.2 (λ i, piecewise_eq_of_not_mem _ _ _) }
end

[Yury G. Kudryashov]

The new mem_infi':

lemma mem_infi' {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔
  ∃ I : set ι, finite I ∧ ∃ V : ι → set α, (∀ i, V i ∈ s i) ∧
    (∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i :=
begin
  simp only [mem_infi, set_coe.forall', bInter_eq_Inter],
  refine ⟨_, λ ⟨I, If, V, hVs, _, hVU, _⟩, ⟨I, If, λ i, V i, λ i, hVs i, hVU⟩⟩,
  rintro ⟨I, If, V, hV, rfl⟩,
  refine ⟨I, If, λ i, if hi : i ∈ I then V ⟨i, hi⟩ else univ, λ i, _, λ i hi, _, _⟩,
  { split_ifs, exacts [hV _, univ_mem] },
  { exact dif_neg hi },
  { simp [Inter_dite, bInter_eq_Inter] }
end

[Yury G. Kudryashov]

Though I guess, it will work with the old mem_infi' as well.

[Yury G. Kudryashov]

(after minor modifications)

[Patrick Massot]

That new mem_infi' can definitely replace the old one.