section‹Disjoint sum of arbitarily many spaces› theory Sum_Topology imports Abstract_Topology begin definition sum_topology :: "('a ⇒ 'b topology) ⇒ 'a set ⇒ ('a × 'b) topology" where "sum_topology X I ≡ topology (λU. U ⊆ Sigma I (topspace ∘ X) ∧ (∀i ∈ I. openin (X i) {x. (i,x) ∈ U}))" lemma is_sum_topology: "istopology (λU. U ⊆ Sigma I (topspace ∘ X) ∧ (∀i∈I. openin (X i) {x. (i, x) ∈ U}))" proof - have 1: "{x. (i, x) ∈ S ∩ T} = {x. (i, x) ∈ S} ∩ {x::'b. (i, x) ∈ T}" for S T and i::'a by auto have 2: "{x. (i, x) ∈ ⋃ 𝒦} = (⋃K∈𝒦. {x::'b. (i, x) ∈ K})" for 𝒦 and i::'a by auto show ?thesis unfolding istopology_def 1 2 by blast qed lemma openin_sum_topology: "openin (sum_topology X I) U ⟷ U ⊆ Sigma I (topspace ∘ X) ∧ (∀i ∈ I. openin (X i) {x. (i,x) ∈ U})" by (auto simp: sum_topology_def is_sum_topology) lemma openin_disjoint_union: "openin (sum_topology X I) (Sigma I U) ⟷ (∀i ∈ I. openin (X i) (U i))" using openin_subset by (force simp: openin_sum_topology) lemma topspace_sum_topology [simp]: "topspace(sum_topology X I) = Sigma I (topspace ∘ X)" by (metis comp_apply openin_disjoint_union openin_subset openin_sum_topology openin_topspace subset_antisym) lemma openin_sum_topology_alt: "openin (sum_topology X I) U ⟷ (∃T. U = Sigma I T ∧ (∀i ∈ I. openin (X i) (T i)))" by (bestsimp simp: openin_sum_topology dest: openin_subset) lemma forall_openin_sum_topology: "(∀U. openin (sum_topology X I) U ⟶ P U) ⟷ (∀T. (∀i ∈ I. openin (X i) (T i)) ⟶ P(Sigma I T))" by (auto simp: openin_sum_topology_alt) lemma exists_openin_sum_topology: "(∃U. openin (sum_topology X I) U ∧ P U) ⟷ (∃T. (∀i ∈ I. openin (X i) (T i)) ∧ P(Sigma I T))" by (auto simp: openin_sum_topology_alt) lemma closedin_sum_topology: "closedin (sum_topology X I) U ⟷ U ⊆ Sigma I (topspace ∘ X) ∧ (∀i ∈ I. closedin (X i) {x. (i,x) ∈ U})" (is "?lhs = ?rhs") proof assume L: ?lhs then have U: "U ⊆ Sigma I (topspace ∘ X)" using closedin_subset by fastforce then have "∀i∈I. {x. (i, x) ∈ U} ⊆ topspace (X i)" by fastforce moreover have "openin (X i) (topspace (X i) - {x. (i, x) ∈ U})" if "i∈I" for i apply (subst openin_subopen) using L that unfolding closedin_def openin_sum_topology by (bestsimp simp: o_def subset_iff) ultimately show ?rhs by (simp add: U closedin_def) next assume R: ?rhs then have "openin (X i) {x. (i, x) ∈ topspace (sum_topology X I) - U}" if "i∈I" for i apply (subst openin_subopen) using that unfolding closedin_def openin_sum_topology by (bestsimp simp: o_def subset_iff) then show ?lhs by (simp add: R closedin_def openin_sum_topology) qed lemma closedin_disjoint_union: "closedin (sum_topology X I) (Sigma I U) ⟷ (∀i ∈ I. closedin (X i) (U i))" using closedin_subset by (force simp: closedin_sum_topology) lemma closedin_sum_topology_alt: "closedin (sum_topology X I) U ⟷ (∃T. U = Sigma I T ∧ (∀i ∈ I. closedin (X i) (T i)))" using closedin_subset unfolding closedin_sum_topology by auto blast lemma forall_closedin_sum_topology: "(∀U. closedin (sum_topology X I) U ⟶ P U) ⟷ (∀t. (∀i ∈ I. closedin (X i) (t i)) ⟶ P(Sigma I t))" by (metis closedin_sum_topology_alt) lemma exists_closedin_sum_topology: "(∃U. closedin (sum_topology X I) U ∧ P U) ⟷ (∃T. (∀i ∈ I. closedin (X i) (T i)) ∧ P(Sigma I T))" by (simp add: closedin_sum_topology_alt) blast lemma open_map_component_injection: "i ∈ I ⟹ open_map (X i) (sum_topology X I) (λx. (i,x))" unfolding open_map_def openin_sum_topology using openin_subset openin_subopen by (force simp: image_iff) lemma closed_map_component_injection: assumes "i ∈ I" shows "closed_map(X i) (sum_topology X I) (λx. (i,x))" proof - have "closedin (X j) {x. j = i ∧ x ∈ U}" if "⋀U S. closedin U S ⟹ S ⊆ topspace U" and "closedin (X i) U" and "j ∈ I" for U j using that by (cases "j=i") auto then show ?thesis using closedin_subset assms by (force simp: closed_map_def closedin_sum_topology image_iff) qed lemma continuous_map_component_injection: "i ∈ I ⟹ continuous_map(X i) (sum_topology X I) (λx. (i,x))" apply (clarsimp simp: continuous_map_def openin_sum_topology) by (smt (verit, best) Collect_cong mem_Collect_eq openin_subset subsetD) lemma subtopology_sum_topology: "subtopology (sum_topology X I) (Sigma I S) = sum_topology (λi. subtopology (X i) (S i)) I" unfolding topology_eq proof (intro strip iffI) fix T assume *: "openin (subtopology (sum_topology X I) (Sigma I S)) T" then obtain U where U: "∀i∈I. openin (X i) (U i) ∧ T = Sigma I U ∩ Sigma I S" by (auto simp: openin_subtopology openin_sum_topology_alt) have "T = (SIGMA i:I. U i ∩ S i)" proof show "T ⊆ (SIGMA i:I. U i ∩ S i)" by (metis "*" SigmaE Sigma_Int_distrib2 U openin_imp_subset subset_iff) show "(SIGMA i:I. U i ∩ S i) ⊆ T" using U by fastforce qed then show "openin (sum_topology (λi. subtopology (X i) (S i)) I) T" by (simp add: U openin_disjoint_union openin_subtopology_Int) next fix T assume *: "openin (sum_topology (λi. subtopology (X i) (S i)) I) T" then obtain U where "∀i∈I. ∃T. openin (X i) T ∧ U i = T ∩ S i" and Teq: "T = Sigma I U" by (auto simp: openin_subtopology openin_sum_topology_alt) then obtain B where "⋀i. i∈I ⟹ openin (X i) (B i) ∧ U i = B i ∩ S i" by metis then show "openin (subtopology (sum_topology X I) (Sigma I S)) T" by (auto simp: openin_subtopology openin_sum_topology_alt Teq) qed lemma embedding_map_component_injection: "i ∈ I ⟹ embedding_map (X i) (sum_topology X I) (λx. (i,x))" by (metis injective_open_imp_embedding_map continuous_map_component_injection open_map_component_injection inj_onI prod.inject) lemma topological_property_of_sum_component: assumes major: "P (sum_topology X I)" and minor: "⋀X S. ⟦P X; closedin X S; openin X S⟧ ⟹ P(subtopology X S)" and PQ: "⋀X Y. X homeomorphic_space Y ⟹ (P X ⟷ Q Y)" shows "(∀i ∈ I. Q(X i))" proof - have "Q(X i)" if "i ∈ I" for i proof - have "P(subtopology (sum_topology X I) (Pair i ` topspace (X i)))" by (meson closed_map_component_injection closed_map_def closedin_topspace major minor open_map_component_injection open_map_def openin_topspace that) then show ?thesis by (metis PQ embedding_map_component_injection embedding_map_imp_homeomorphic_space homeomorphic_space_sym that) qed then show ?thesis by metis qed end