Preconnection in sigma

Stream: Is there code for X?

[Yaël Dillies]

For X : α → Type*, how does one get to the fact that the connected components of sigma X are each in one of the X a?

[Johan Commelin]

I'm assuming that \alpha is discrete, and X a carries a topology for each a?

[Yaël Dillies]

Yup, I'm trying to prove

import topology.connected

lemma sigma.is_connected_iff {α : Type*} {X : α → Type*} [∀ a, topological_space (X a)]
  {s : set (Σ a, X a)} :
  is_connected s ↔ ∃ (a : α) (t : set (X a)), is_connected t ∧ s = sigma.mk _ '' t :=
begin
  refine ⟨λ hs, _, _⟩,
  { obtain ⟨⟨a, x⟩, hx⟩ := hs.nonempty,
    refine ⟨a, sigma.mk a ⁻¹' s, ⟨⟨x, hx⟩, _⟩, _⟩,
    sorry,
    sorry
  },
  { rintro ⟨a, t, ht, rfl⟩,
    exact ht.image _ continuous_sigma_mk.continuous_on }
end

Am I missing discrete α?

[Johan Commelin]

No, I guess you don't need it.

[Johan Commelin]

I just wanted to be sure that you weren't doing something weird with a topology on \alpha

[Yaël Dillies]

Ah yeah, no

[Johan Commelin]

You need to know that sigma.mk _ '' set.univ is open.

[Johan Commelin]

If s is connected and t is clopen, then s is contained in t or disjoint from t.

[Johan Commelin]

Some variant of that observation should go into mathlib.

[Yaël Dillies]

Hmm... >We don't seem to have that yet.

[Yaël Dillies]

Also, am I right in thinking the preimage of a preconnected set under a continuous embedding is preconnected?

[Johan Commelin]

@Yaël Dillies No, that doesn't work. You can embed a "half-moon" shape into the plane, and pull-back another "half-moon" shape that intersects the other one only at the two tips.

[Johan Commelin]

I can make it more precise if that counterexample is too vague.

[Johan Commelin]

Alternative: pull-back the area below the graph of sin under the embedding of the upper half-plane.

[Yaël Dillies]

Sad... So I need to add as a condition that the set lies entirely in the range of the embedding.

[Johan Commelin]

Where?

[Yaël Dillies]

For the preimage to be preconnected

[Johan Commelin]

But that lemma is not related to your OP right?

[Johan Commelin]

Oh, maybe it is for the version that you posted in code, for your construction of t

[Johan Commelin]

If you only want to know that s is contained in some X a, that's "easier"

[Yaël Dillies]

Oh?

[Johan Commelin]

If you have the lemma that I mentioned before, you only need to prove that sigma.mk a '' set.univ is clopen. But you'll need to do that anyway.

[Reid Barton]

Johan Commelin said:

You need to know that sigma.mk _ '' set.univ is open.

docs#open_embedding_sigma_mk

[Yaël Dillies]

Johan Commelin said:

If s is connected and t is clopen, then s is contained in t or disjoint from t.

We don't have that lemma, right?

[Yaël Dillies]

Also, how does that help me with is_preconnected (sigma.mk a ⁻¹' s)? I need to pullback preconnection at point or another, right?

[Yaël Dillies]

I pushed, feel free to explain me in further details/finish off yourself.