Theory Topological_Group_Examples

✐‹creator "Niklas Krofta"›
section ‹Examples of Topological Groups›
theory Topological_Group_Examples
  imports Topological_Group
begin

paragraph ‹Summary›
text ‹This section gives examples of topological groups.›

lemma (in group) discrete_topological_group:
  shows "topological_group G (discrete_topology (carrier G))"
proof -               
  let ?T = "discrete_topology (carrier G)"
  have "topspace ?T = carrier G" using topspace_discrete_topology by force
  moreover have "continuous_map (prod_topology ?T ?T) ?T (λ(σ,τ). σ ⊗ τ)" 
    unfolding prod_topology_discrete_topology[symmetric] by auto
  ultimately show ?thesis unfolding topological_group_def topological_group_axioms_def by fastforce
qed

lemma topological_group_real_power_space:
  defines "ℜ :: (real^'n) monoid ≡ ⦇carrier = UNIV, mult = (+), one = 0⦈"
  defines "T :: (real^'n) topology ≡ euclidean"
  shows "topological_group ℜ T"
proof -
  have "x ∈ Units ℜ" for x
  proof -
    have "x ⊗⇘ℜ⇙ -x = 𝟭⇘ℜ⇙" "-x ⊗⇘ℜ⇙ x = 𝟭⇘ℜ⇙" using ℜ_def by auto
    then show ?thesis unfolding Units_def ℜ_def by fastforce
  qed
  then have group: "group ℜ" by (unfold_locales) (auto simp: ℜ_def)
  then interpret group ℜ by auto
  have group_is_space: "topspace T = carrier ℜ"
    unfolding ℜ_def T_def by force
  have mul_continuous: "continuous_map (prod_topology T T) T (λ(x,y). x ⊗⇘ℜ⇙ y)"
    using continuous_map_add[OF continuous_map_fst continuous_map_snd]
    unfolding T_def ℜ_def by (simp add: case_prod_beta')
  have "(-x) ⊗⇘ℜ⇙ x = 𝟭⇘ℜ⇙" for x unfolding ℜ_def by auto
  then have "inv⇘ℜ⇙ x = -x" for x using inv_equality ℜ_def by simp
  moreover have "continuous_map T T uminus" unfolding T_def by force
  ultimately have "continuous_map T T (λx. inv⇘ℜ⇙ x)" by simp
  then show ?thesis using group_is_space mul_continuous group
    unfolding topological_group_def topological_group_axioms_def by blast
qed

definition unit_group :: "('a :: field) monoid" where
"unit_group = ⦇carrier = UNIV - {0}, mult = (*), one = 1⦈" 

lemma 
  group_unit_group: "group unit_group" and
  inv_unit_group: "x ∈ carrier unit_group ⟹ inv⇘unit_group⇙ x = inverse x"
proof -
  have "x ∈ Units unit_group" if "x ≠ 0" for x
  proof -
    have "x ⊗⇘unit_group⇙ 1/x = 𝟭⇘unit_group⇙" "1/x ⊗⇘unit_group⇙ x = 𝟭⇘unit_group⇙" 
      using that unfolding unit_group_def by auto
    then show ?thesis unfolding Units_def unit_group_def using that by fastforce
  qed
  then show "group unit_group" by (unfold_locales) (auto simp: unit_group_def)
  then interpret group unit_group by blast
  show "inv⇘unit_group⇙ x = inverse x" if "x ∈ carrier unit_group"
    using that inv_equality[of "inverse x"] unfolding unit_group_def by simp
qed

lemma topological_group_real_unit_group:
  defines "T :: real topology ≡ subtopology euclidean (UNIV - {0})"
  shows "topological_group unit_group T"
proof -
  let ?ℜ = "unit_group :: real monoid"
  have group_is_space: "topspace T = carrier ?ℜ" unfolding unit_group_def T_def by force
  have "continuous_map (prod_topology euclidean euclidean) euclidean (λ(x,y). x ⊗⇘?ℜ⇙ y)"
    using continuous_map_real_mult[OF continuous_map_fst continuous_map_snd]
    unfolding T_def unit_group_def by (simp add: case_prod_beta')
  then have "continuous_map (prod_topology T T) euclideanreal (λ(x,y). x ⊗⇘?ℜ⇙ y)"
    unfolding T_def subtopology_Times[symmetric] using continuous_map_from_subtopology by blast
  moreover have "(λ(x,y). x ⊗⇘?ℜ⇙ y) ∈ topspace (prod_topology T T) → UNIV - {0}"
    unfolding T_def unit_group_def by fastforce
  ultimately have mul_continuous: "continuous_map (prod_topology T T) T (λ(x,y). x ⊗⇘?ℜ⇙ y)"
    unfolding T_def using continuous_map_into_subtopology by blast
  have "continuous_map T euclideanreal inverse" 
    using continuous_map_real_inverse[of T id] unfolding T_def by auto
  moreover have "inverse ∈ topspace T → topspace T" unfolding T_def by fastforce
  ultimately have "continuous_map T T inverse" 
    unfolding T_def using continuous_map_into_subtopology by auto
  then have "continuous_map T T (λx. inv⇘?ℜ⇙ x)" 
    using group_is_space continuous_map_eq inv_unit_group by metis
  then show ?thesis using group_is_space mul_continuous group_unit_group
    unfolding topological_group_def topological_group_axioms_def by blast
qed

end