Theory Binary_Sum_Topology

theory Binary_Sum_Topology
  imports "HOL-Analysis.Abstract_Topology"
begin

section ‹Binary coproduct topology›

text ‹
  Topological pushouts are constructed by first equipping the disjoint sum with
  its coproduct topology and only then quotienting by the glue relation. This
  short theory records that coproduct topology together with the basic
  continuity lemmas used by the later pushout arguments.
›

definition binary_sum_topology :: "'a topology => 'b topology => ('a + 'b) topology"
where
  "binary_sum_topology X Y =
     topology (λU.
       U ⊆ Inl ` topspace X ∪ Inr ` topspace Y ∧
       openin X {x. Inl x ∈ U} ∧
       openin Y {y. Inr y ∈ U})"

lemma is_binary_sum_topology:
  "istopology (λU.
      U ⊆ Inl ` topspace X ∪ Inr ` topspace Y ∧
      openin X {x. Inl x ∈ U} ∧
      openin Y {y. Inr y ∈ U})"
proof -
  have inl_Int: "{x. Inl x ∈ S ∩ T} = {x. Inl x ∈ S} ∩ {x. Inl x ∈ T}" for S T
    by auto
  have inr_Int: "{y. Inr y ∈ S ∩ T} = {y. Inr y ∈ S} ∩ {y. Inr y ∈ T}" for S T
    by auto
  have inl_Union: "{x. Inl x ∈ ⋃𝒦} = (⋃U∈𝒦. {x. Inl x ∈ U})" for 𝒦
    by auto
  have inr_Union: "{y. Inr y ∈ ⋃𝒦} = (⋃U∈𝒦. {y. Inr y ∈ U})" for 𝒦
    by auto
  show ?thesis
    unfolding istopology_def inl_Int inr_Int inl_Union inr_Union
    by blast
qed

lemma openin_binary_sum_topology:
  "openin (binary_sum_topology X Y) U ⟷
    U ⊆ Inl ` topspace X ∪ Inr ` topspace Y ∧
    openin X {x. Inl x ∈ U} ∧
    openin Y {y. Inr y ∈ U}"
  by (auto simp: binary_sum_topology_def is_binary_sum_topology)

lemma topspace_binary_sum_topology [simp]:
  "topspace (binary_sum_topology X Y) = Inl ` topspace X ∪ Inr ` topspace Y"
proof
  have top_open: "openin (binary_sum_topology X Y) (topspace (binary_sum_topology X Y))"
    by simp
  show "topspace (binary_sum_topology X Y) ⊆ Inl ` topspace X ∪ Inr ` topspace Y"
    using top_open unfolding openin_binary_sum_topology by blast
  have eqX: "{x. Inl x ∈ Inl ` topspace X ∪ Inr ` topspace Y} = topspace X"
    by auto
  have eqY: "{y. Inr y ∈ Inl ` topspace X ∪ Inr ` topspace Y} = topspace Y"
    by auto
  have "openin (binary_sum_topology X Y) (Inl ` topspace X ∪ Inr ` topspace Y)"
    unfolding openin_binary_sum_topology eqX eqY by simp
  then show "Inl ` topspace X ∪ Inr ` topspace Y ⊆ topspace (binary_sum_topology X Y)"
    by (rule openin_subset)
qed

lemma subset_topspace_binary_sum_inl:
  "(Inl :: 'a ⇒ 'a + 'b) ` topspace X ⊆ topspace (binary_sum_topology X Y)"
  by simp

lemma subset_topspace_binary_sum_inr:
  "(Inr :: 'b ⇒ 'a + 'b) ` topspace Y ⊆ topspace (binary_sum_topology X Y)"
  by simp

lemma continuous_map_binary_sum_inl:
  "continuous_map X (binary_sum_topology X Y) (Inl :: 'a ⇒ 'a + 'b)"
proof -
  have image: "(Inl :: 'a ⇒ 'a + 'b) ` topspace X ⊆ topspace (binary_sum_topology X Y)"
    by simp
  have preimage:
    "∀U. openin (binary_sum_topology X Y) U ⟶ openin X {x ∈ topspace X. Inl x ∈ U}"
  proof (intro allI impI)
    fix U
    assume U: "openin (binary_sum_topology X Y) U"
    have openU: "openin X {x. Inl x ∈ U}"
      using U by (simp add: openin_binary_sum_topology)
    have subsetX: "{x. Inl x ∈ U} ⊆ topspace X"
      using openU by (rule openin_subset)
    have eq: "{x ∈ topspace X. Inl x ∈ U} = {x. Inl x ∈ U}"
      using subsetX by auto
    have "openin X {x ∈ topspace X. Inl x ∈ U}"
      unfolding eq using openU by simp
    then show "openin X {x ∈ topspace X. Inl x ∈ U}" .
  qed
  from image preimage show ?thesis
    by (simp add: continuous_map)
qed

lemma continuous_map_binary_sum_inr:
  "continuous_map Y (binary_sum_topology X Y) (Inr :: 'b ⇒ 'a + 'b)"
proof -
  have image: "(Inr :: 'b ⇒ 'a + 'b) ` topspace Y ⊆ topspace (binary_sum_topology X Y)"
    by simp
  have preimage:
    "∀U. openin (binary_sum_topology X Y) U ⟶ openin Y {y ∈ topspace Y. Inr y ∈ U}"
  proof (intro allI impI)
    fix U
    assume U: "openin (binary_sum_topology X Y) U"
    have openU: "openin Y {y. Inr y ∈ U}"
      using U by (simp add: openin_binary_sum_topology)
    have subsetY: "{y. Inr y ∈ U} ⊆ topspace Y"
      using openU by (rule openin_subset)
    have eq: "{y ∈ topspace Y. Inr y ∈ U} = {y. Inr y ∈ U}"
      using subsetY by auto
    have "openin Y {y ∈ topspace Y. Inr y ∈ U}"
      unfolding eq using openU by simp
    then show "openin Y {y ∈ topspace Y. Inr y ∈ U}" .
  qed
  from image preimage show ?thesis
    by (simp add: continuous_map)
qed

lemma open_map_binary_sum_inl:
  "open_map X (binary_sum_topology X Y) (Inl :: 'a ⇒ 'a + 'b)"
  unfolding open_map_def openin_binary_sum_topology
  using openin_subset openin_subopen by (force simp: image_iff)

lemma open_map_binary_sum_inr:
  "open_map Y (binary_sum_topology X Y) (Inr :: 'b ⇒ 'a + 'b)"
  unfolding open_map_def openin_binary_sum_topology
  using openin_subset openin_subopen by (force simp: image_iff)

lemma continuous_map_from_binary_sum_topology:
  assumes f: "continuous_map X Z f"
    and g: "continuous_map Y Z g"
  shows "continuous_map (binary_sum_topology X Y) Z (case_sum f g)"
proof -
  from f have f_image: "f ` topspace X ⊆ topspace Z"
    by (simp add: continuous_map)
  from g have g_image: "g ` topspace Y ⊆ topspace Z"
    by (simp add: continuous_map)
  have case_image:
    "case_sum f g ` topspace (binary_sum_topology X Y) = f ` topspace X ∪ g ` topspace Y"
  proof
    show "case_sum f g ` topspace (binary_sum_topology X Y) ⊆ f ` topspace X ∪ g ` topspace Y"
      by (auto simp: topspace_binary_sum_topology)
    show "f ` topspace X ∪ g ` topspace Y ⊆ case_sum f g ` topspace (binary_sum_topology X Y)"
    proof
      fix z
      assume "z ∈ f ` topspace X ∪ g ` topspace Y"
      then consider
        (left) x where "x ∈ topspace X" "z = f x"
      | (right) y where "y ∈ topspace Y" "z = g y"
        by auto
      then show "z ∈ case_sum f g ` topspace (binary_sum_topology X Y)"
      proof cases
        case (left x)
        have "Inl x ∈ topspace (binary_sum_topology X Y)"
          using left by (auto simp: topspace_binary_sum_topology)
        then have "case_sum f g (Inl x) ∈ case_sum f g ` topspace (binary_sum_topology X Y)"
          by (rule imageI)
        then show ?thesis
          using left by simp
      next
        case (right y)
        have "Inr y ∈ topspace (binary_sum_topology X Y)"
          using right by (auto simp: topspace_binary_sum_topology)
        then have "case_sum f g (Inr y) ∈ case_sum f g ` topspace (binary_sum_topology X Y)"
          by (rule imageI)
        then show ?thesis
          using right by simp
      qed
    qed
  qed
  have image: "case_sum f g ` topspace (binary_sum_topology X Y) ⊆ topspace Z"
  proof -
    have case_subset: "f ` topspace X ∪ g ` topspace Y ⊆ topspace Z"
      using f_image g_image by blast
    from case_image case_subset show ?thesis
      by blast
  qed
  have preimage:
    "∀U. openin Z U ⟶
      openin (binary_sum_topology X Y) {z ∈ topspace (binary_sum_topology X Y). case_sum f g z ∈ U}"
  proof (intro allI impI)
    fix U
    assume U: "openin Z U"
    from f U have openX: "openin X {x ∈ topspace X. f x ∈ U}"
      by (simp add: continuous_map)
    from g U have openY: "openin Y {y ∈ topspace Y. g y ∈ U}"
      by (simp add: continuous_map)
    let ?W = "{z ∈ topspace (binary_sum_topology X Y). case_sum f g z ∈ U}"
    have subsetW: "?W ⊆ topspace (binary_sum_topology X Y)"
      by auto
    have eqX: "{x. Inl x ∈ ?W} = {x ∈ topspace X. f x ∈ U}"
      by auto
    have eqY: "{y. Inr y ∈ ?W} = {y ∈ topspace Y. g y ∈ U}"
      by auto
    show "openin (binary_sum_topology X Y) ?W"
      unfolding openin_binary_sum_topology eqX eqY
      using subsetW openX openY by simp
  qed
  from image preimage show ?thesis
    by (simp add: continuous_map)
qed

end