English
If fibers of a map f are connected and closedness is preserved under preimage of closed sets, then the preimage of a connected component is connected.
Русский
Если множества-части фибр карты f связны и сохраняют замкнутость через предобраз, то предобраз связной компоненты является связным.
LaTeX
$$$preimage\_connectedComponent\_connected\; (f)\; (connectedFibre) \Rightarrow IsConnected(f^{-1}(connectedComponent t))$$$
Lean4
/-- The preimage of a connected component is preconnected if the function has connected fibers
and a subset is closed iff the preimage is. -/
theorem preimage_connectedComponent_connected (connected_fibers : ∀ t : β, IsConnected (f ⁻¹' { t }))
(hcl : ∀ T : Set β, IsClosed T ↔ IsClosed (f ⁻¹' T)) (t : β) : IsConnected (f ⁻¹' connectedComponent t) := by
-- The following proof is essentially https://stacks.math.columbia.edu/tag/0377
-- although the statement is slightly different
have hf : Surjective f := Surjective.of_comp fun t : β => (connected_fibers t).1
refine ⟨Nonempty.preimage connectedComponent_nonempty hf, ?_⟩
have hT : IsClosed (f ⁻¹' connectedComponent t) := (hcl (connectedComponent t)).1 isClosed_connectedComponent
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hT]
intro u v hu hv huv uv_disj
let T₁ := {t' ∈ connectedComponent t | f ⁻¹' { t' } ⊆ u}
let T₂ := {t' ∈ connectedComponent t | f ⁻¹' { t' } ⊆ v}
have fiber_decomp : ∀ t' ∈ connectedComponent t, f ⁻¹' { t' } ⊆ u ∨ f ⁻¹' { t' } ⊆ v :=
by
intro t' ht'
apply isPreconnected_iff_subset_of_disjoint_closed.1 (connected_fibers t').2 u v hu hv
· exact Subset.trans (preimage_mono (singleton_subset_iff.2 ht')) huv
rw [uv_disj.inter_eq, inter_empty]
have T₁_u : f ⁻¹' T₁ = f ⁻¹' connectedComponent t ∩ u :=
by
apply eq_of_subset_of_subset
· rw [← biUnion_preimage_singleton]
refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
exact ht'.1
rintro a ⟨hat, hau⟩
constructor
· exact mem_preimage.1 hat
refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_right fun h => ?_
exact
uv_disj.subset_compl_right hau
(h rfl)
-- This proof is exactly the same as the above (modulo some symmetry)
have T₂_v : f ⁻¹' T₂ = f ⁻¹' connectedComponent t ∩ v :=
by
apply eq_of_subset_of_subset
· rw [← biUnion_preimage_singleton]
refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2
rw [hf.preimage_subset_preimage_iff, singleton_subset_iff]
exact ht'.1
rintro a ⟨hat, hav⟩
constructor
· exact mem_preimage.1 hat
· refine (fiber_decomp (f a) (mem_preimage.1 hat)).resolve_left fun h => ?_
exact
uv_disj.subset_compl_left hav
(h rfl)
-- Now we show T₁, T₂ are closed, cover connectedComponent t and are disjoint.
have hT₁ : IsClosed T₁ := (hcl T₁).2 (T₁_u.symm ▸ IsClosed.inter hT hu)
have hT₂ : IsClosed T₂ := (hcl T₂).2 (T₂_v.symm ▸ IsClosed.inter hT hv)
have T_decomp : connectedComponent t ⊆ T₁ ∪ T₂ := fun t' ht' =>
by
rw [mem_union t' T₁ T₂]
rcases fiber_decomp t' ht' with htu | htv
· left; exact ⟨ht', htu⟩
· right; exact ⟨ht', htv⟩
have T_disjoint : Disjoint T₁ T₂ := by
refine Disjoint.of_preimage hf ?_
rw [T₁_u, T₂_v, disjoint_iff_inter_eq_empty, ← inter_inter_distrib_left, uv_disj.inter_eq, inter_empty]
-- Now we do cases on whether (connectedComponent t) is a subset of T₁ or T₂ to show
-- that the preimage is a subset of u or v.
rcases
(isPreconnected_iff_subset_of_fully_disjoint_closed isClosed_connectedComponent).1 isPreconnected_connectedComponent
T₁ T₂ hT₁ hT₂ T_decomp T_disjoint with
h | h
· left
rw [Subset.antisymm_iff] at T₁_u
suffices f ⁻¹' connectedComponent t ⊆ f ⁻¹' T₁ from (this.trans T₁_u.1).trans inter_subset_right
exact preimage_mono h
· right
rw [Subset.antisymm_iff] at T₂_v
suffices f ⁻¹' connectedComponent t ⊆ f ⁻¹' T₂ from (this.trans T₂_v.1).trans inter_subset_right
exact preimage_mono h
