Theory HOL-Analysis.Sum_Topology

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)  (iI. 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 "iI. {x. (i, x)  U}  topspace (X i)"
    by fastforce
  moreover have "openin (X i) (topspace (X i) - {x. (i, x)  U})" if "iI" 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 "iI" 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: "iI. 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 "iI. 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. iI  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