Theory Ring_Zariski_ZF_3

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2023  Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Rings - Zariski Topology - maps›

theory Ring_Zariski_ZF_3 imports Ring_Zariski_ZF Ring_ZF_3 Topology_ZF_2

begin

lemma (in ring_homo) spectrum_surj:
  defines "g ≡ λu∈target_ring.Spec. f-``u"
  assumes "f∈surj(R,S)"
  shows "g: target_ring.Spec → V(ker)"
proof-
  have "g: target_ring.Spec → {f-``u. u∈target_ring.Spec}" using lam_funtype
    unfolding g_def by auto moreover
  {
    fix t assume "t∈{f-``u. u∈target_ring.Spec}"
    then obtain u where u:"u:target_ring.Spec" "t=f-``u" by auto
    from u(1) have u2:"u◃⇩pR⇩t" unfolding target_ring.Spec_def by auto
    then have "(f-``u)◃⇩pR⇩o" using preimage_prime_ideal_surj
      assms(2) by auto moreover
    then have "f-``u ∈ origin_ring.ideals"
      unfolding origin_ring.primeIdeal_def
      using origin_ring.ideal_dest_subset by auto
    ultimately have "f-``u ∈ origin_ring.Spec" unfolding origin_ring.Spec_def
      by auto
    moreover from u2 have "𝟬⇩S ∈ u" unfolding
      target_ring.primeIdeal_def using target_ring.ideal_dest_zero
      by auto
    then have "{𝟬⇩S} ⊆ u" by auto
    then have "f-``{𝟬⇩S} ⊆ f-``u" by auto
    moreover have "f-``u ⊆ R" using func1_1_L15[OF
      surj_is_fun[OF assms(2)]] by auto
    ultimately have "f-``u ∈ origin_ring.closeBasic(f-``{𝟬⇩S})"
      using origin_ring.closeBasic_def[of "f-``{𝟬⇩S}"]
      by force
    with u(2) have "t∈origin_ring.closeBasic(f-``{𝟬⇩S})" by auto
  }
  then have "{f-``u. u∈target_ring.Spec} ⊆ origin_ring.closeBasic(f-``{𝟬⇩S})" by auto
  ultimately show ?thesis using func1_1_L1B by auto
qed

lemma (in ring_homo) spectrum_surj_bij:
  defines "g ≡ λu∈target_ring.Spec. f-``u"
  assumes "f∈surj(R,S)"
  shows "g∈bij(target_ring.Spec, V(ker))"
proof-
  {
    fix s t assume st:"s∈target_ring.Spec" "t∈target_ring.Spec"
      "g`s = g`t"
    then have "f-``s = f-``t" using beta unfolding g_def by auto
    then have "f``(f-``s) = f``(f-``t)" by auto
    moreover from st(1,2) have "s ⊆ S" "t ⊆S"
      unfolding target_ring.Spec_def origin_ring.Spec_def
      by auto
    moreover note assms(2) st(1,2)
    ultimately have "s=t" using surj_image_vimage
      unfolding target_ring.Spec_def origin_ring.Spec_def 
      by auto
  }
  then have "g∈inj(target_ring.Spec, origin_ring.closeBasic(f-``{𝟬⇩S}))"
    unfolding inj_def using spectrum_surj assms(2) unfolding g_def by auto
  moreover
  {
    fix t assume t:"t∈origin_ring.closeBasic(f-``{𝟬⇩S})"
    then have tt:"t∈origin_ring.Spec" "f-``{𝟬⇩S} ⊆ t"
      using origin_ring.closeBasic_def func1_1_L6A[OF surj_is_fun]
      assms(2) by auto
    {
      fix y assume y:"y∈f-``(f``t)"
      then have y:"y∈R" "f`y∈f``t" using func1_1_L15
        surj_is_fun[OF assms(2)] by auto
      from y(2) obtain x where x:"x∈t" "f`y = f`x"
        using func_imagedef[OF surj_is_fun]
        assms(2) tt(1) unfolding origin_ring.Spec_def by auto
      from x(2) have "(f`y)\<rs>⇩S(f`x) = (f`x)\<rs>⇩S(f`x)" by auto
      then have "(f`y)\<rs>⇩S(f`x) = 𝟬⇩S" using target_ring.Ring_ZF_1_L3(7)
        apply_type[OF surj_is_fun] assms(2) x(1) tt(1)
        unfolding origin_ring.Spec_def by auto
      then have "f`(y\<rs>⇩Rx) = 𝟬⇩S" using homomor_dest_subs
        x(1) tt(1) y(1) unfolding origin_ring.Spec_def by auto moreover
      from x(1) tt(1) have "x∈R" unfolding origin_ring.Spec_def by auto
      with y(1) have "y\<rs>⇩Rx ∈R" using origin_ring.Ring_ZF_1_L4(2) by auto
      ultimately have "y\<rs>⇩Rx ∈ f-``{𝟬⇩S}" using func1_1_L15
        surj_is_fun[OF assms(2)] by auto
      then have "y\<rs>⇩Rx ∈t" using tt(2) by auto moreover
      have "t◃R⇩o" using tt(1) unfolding origin_ring.Spec_def by auto
      ultimately have "x\<ra>⇩R(y\<rs>⇩Rx) ∈t" using x(1)
        origin_ring.ideal_dest_sum by auto
      then have "y∈t" using origin_ring.Ring_ZF_2_L1A(5)
        y(1) ‹x∈R› by auto
    }
    then have "f-``(f``t) = t" using func1_1_L9[of f R S t]
      surj_is_fun[OF assms(2)] tt(1) unfolding origin_ring.Spec_def
      by auto moreover
    then have "(f``t)◃⇩pR⇩t" using prime_ideal_quot_3[of "f``t"]
      assms(2) tt(1) unfolding origin_ring.Spec_def
      using image_ideal_surj[of t] origin_ring.primeIdeal_def[of t]
      by auto
    then have "(f``t)◃⇩pR⇩t" "(f``t)◃R⇩t"
      using target_ring.primeIdeal_def[of "f``t"]
      by auto
    then have "(f``t):target_ring.Spec"
      unfolding target_ring.Spec_def using target_ring.ideal_dest_subset
      by auto moreover
    then have "f-``(f``t) = g`(f``t)" unfolding g_def
      using beta by auto
    ultimately have "g`(f``t) = t" "(f``t):target_ring.Spec" by auto
    then have "∃p∈target_ring.Spec. g`p = t" by auto
  }
  ultimately show "g:bij(target_ring.Spec, V(ker))"
    unfolding bij_def surj_def inj_def by auto
qed

definition (in ring_homo) top_origin ("τ⇩o") where
  "top_origin ≡ {origin_ring.openBasic(J) . J ∈ origin_ring.ideals}"
  
definition (in ring_homo) top_target ("τ⇩t") where
  "top_target ≡ {target_ring.openBasic(J) . J ∈ target_ring.ideals}"

definition (in ring_homo) spec_cont where
 "spec_cont(h) ≡ IsContinuous(τ⇩t, τ⇩o, h)"

lemma (in ring_homo) spectrum_surj_cont:
  defines "g ≡ λu∈target_ring.Spec. f-``u"
  assumes "f∈surj(R,S)"
  shows "IsContinuous(τ⇩t, τ⇩o {restricted to}(V(ker)), g)"
  unfolding IsContinuous_def top_target_def RestrictedTo_def top_origin_def
proof(safe)
  fix x assume ass:"x◃R⇩o" "x ⊆ R"
  have "origin_ring.openBasic(x) = {u∈origin_ring.Spec. ¬(x ⊆ u)}"
    unfolding origin_ring.openBasic_def[OF ass(2)] by auto
  have "g-``(origin_ring.openBasic(x)) = {t∈target_ring.Spec. g`t ∈ origin_ring.openBasic(x)}" 
    using spectrum_surj assms(2) unfolding g_def
    using func1_1_L15 by auto
  then have G:"g-``(origin_ring.openBasic(x)) = {t∈target_ring.Spec. f-``t ∈ origin_ring.openBasic(x)}"
    using beta unfolding g_def by auto
  have "(f``x)◃R⇩t" using image_ideal_surj assms(2) ass(1) by auto
  then have H:"f``x∈target_ring.ideals" using
    target_ring.ideal_dest_subset by auto
  then have F:"target_ring.openBasic(f``x) = {t∈target_ring.Spec. ¬(f``x ⊆ t)}"
    using target_ring.openBasic_def by auto
  {
    fix s assume "s∈{t∈target_ring.Spec. f-``t ∈ origin_ring.openBasic(x)}"
    then have s:"s∈target_ring.Spec" "f-``s ∈ origin_ring.openBasic(x)"
      by auto
    from this(2) have E:"f-``s ∈origin_ring.Spec" "¬(x ⊆ f-``s)"
      using origin_ring.openBasic_def ass(1) origin_ring.ideal_dest_subset
      by auto
    {
      assume "f``x ⊆ s"
      then have "f-``(f``x) ⊆ f-``s" by auto
      then have "x ⊆ f-``s" using func1_1_L9[OF surj_is_fun]
        assms(2) ass(1) origin_ring.ideal_dest_subset by force
      with E(2) have False by auto
    }
    then have "¬(f``x ⊆ s)" by auto
    with s(1) have "s∈{t∈target_ring.Spec. ¬(f``x ⊆ t)}"
      by auto
  }
  then have "{t ∈ target_ring.Spec . f -`` t ∈ origin_ring.openBasic(x)} ⊆ {t∈target_ring.Spec. ¬(f``x ⊆ t)}"
    by auto moreover
  {
    fix s assume "s∈{t∈target_ring.Spec. ¬(f``x ⊆ t)}"
    then have s:"s∈target_ring.Spec" "¬(f``x ⊆ s)" by auto
    have "origin_ring.openBasic(x) = {t∈origin_ring.Spec. ¬(x ⊆ t)}"
      using origin_ring.openBasic_def ass(1) origin_ring.ideal_dest_subset
      by auto
    {
      assume "x ⊆ f-``s"
      then have "f``x ⊆ f``(f-``s)" by auto
      then have "f``x ⊆ s" using surj_image_vimage
        assms(2) s(1) unfolding target_ring.Spec_def
          target_ring.primeIdeal_def target_ring.ideal_dest_subset
        by auto
      with s(2) have False by auto
    }
    then have "¬(x ⊆ f-``s)" by auto
    moreover
    from s(1) have "(f-``s) ◃⇩pR⇩o" unfolding target_ring.Spec_def
      using preimage_prime_ideal_surj assms(2) by auto
    then have "(f-``s)∈origin_ring.Spec" unfolding origin_ring.Spec_def
      origin_ring.primeIdeal_def using origin_ring.ideal_dest_subset
      by auto
    ultimately have "f-``s∈origin_ring.openBasic(x)"
      using origin_ring.openBasic_def ass(1)
      origin_ring.ideal_dest_subset by auto
    then have "s∈{t ∈ target_ring.Spec . f -`` t ∈ origin_ring.openBasic(x)}"
      using s(1) by auto
  }
  then have "{t ∈ target_ring.Spec . ¬ f `` x ⊆ t} ⊆ {t ∈ target_ring.Spec . f -`` t ∈ origin_ring.openBasic(x)}"
    by auto
  ultimately have "{t ∈ target_ring.Spec . ¬ f `` x ⊆ t} = {t ∈ target_ring.Spec . f -`` t ∈ origin_ring.openBasic(x)}"
    by auto
  with F have "target_ring.openBasic(f``x) = {t ∈ target_ring.Spec . f -`` t ∈ origin_ring.openBasic(x)}"
    by auto
  with G have T:"target_ring.openBasic(f``x) = g-`` origin_ring.openBasic(x)" by auto
  have "g-``(origin_ring.closeBasic(f -`` {𝟬⇩S})) = {t∈target_ring.Spec. g`t ∈ origin_ring.closeBasic(f -`` {𝟬⇩S})}" 
    using spectrum_surj assms(2) unfolding g_def
    using func1_1_L15 by auto
  then have "g-``(origin_ring.closeBasic(f -`` {𝟬⇩S})) = {t∈target_ring.Spec. f-``t ∈ origin_ring.closeBasic(f -`` {𝟬⇩S})}" 
    using beta unfolding g_def by auto
  then have E:"g-``(origin_ring.closeBasic(f -`` {𝟬⇩S})) = {t∈target_ring.Spec. f-``t ∈ {q∈origin_ring.Spec. (f -`` {𝟬⇩S}) ⊆ q}}" 
    unfolding origin_ring.closeBasic_def[OF func1_1_L3[OF surj_is_fun[OF assms(2)]]] by auto
  {
    fix s assume s:"s∈target_ring.openBasic(f``x)"
    with E have ss:"s∈target_ring.Spec" "¬(f``x ⊆ s)" 
      using target_ring.openBasic_def func1_1_L6(2) surj_is_fun[OF assms(2)] by auto
    from this(1) have "g`s ∈ origin_ring.closeBasic(f -`` {𝟬⇩S})" using spectrum_surj[OF assms(2)]
      apply_type[of g target_ring.Spec "λu. origin_ring.closeBasic(f -`` {𝟬⇩S})"] unfolding g_def
      by auto
    with ss(1) have "f-``s ∈ origin_ring.closeBasic(f -`` {𝟬⇩S})" using beta
      unfolding g_def by auto
    moreover 
    from ss(1) have "s◃R⇩t" unfolding target_ring.Spec_def
      target_ring.primeIdeal_def by auto
    then have "𝟬⇩S ∈s" using target_ring.ideal_dest_zero by auto
    then have "{𝟬⇩S} ⊆ s" by auto
    then have "f-``{𝟬⇩S} ⊆ f-``s" by auto
    moreover
    have "f-``{𝟬⇩S} ⊆ R" using func1_1_L15[OF
      surj_is_fun[OF assms(2)], of "{𝟬⇩S}"] by auto
    ultimately have "f-``s ∈ {q∈origin_ring.Spec. (f -`` {𝟬⇩S}) ⊆ q}"
      using origin_ring.closeBasic_def by auto
    then have "s∈{t∈target_ring.Spec. f-``t ∈ {q∈origin_ring.Spec. (f -`` {𝟬⇩S}) ⊆ q}}"
      using ss(1) by auto
    then have "s∈g-``(origin_ring.closeBasic(f -`` {𝟬⇩S}))" using E by auto
  }
  then have "target_ring.openBasic(f``x) ⊆ g-``(origin_ring.closeBasic(f -`` {𝟬⇩S}))" by auto
  then have "g-``(origin_ring.closeBasic(f -`` {𝟬⇩S}))∩target_ring.openBasic(f``x) = target_ring.openBasic(f``x)"
    by auto
  with T have "g-``(origin_ring.closeBasic(f -`` {𝟬⇩S})) ∩ g -`` origin_ring.openBasic(x) = target_ring.openBasic(f``x)"
    by auto moreover
  have "g-``(origin_ring.closeBasic(f -`` {𝟬⇩S})) ∩ g -`` origin_ring.openBasic(x) =
    g-``(origin_ring.closeBasic(f -`` {𝟬⇩S}) ∩ origin_ring.openBasic(x))"
    using invim_inter_inter_invim[OF spectrum_surj[OF assms(2)]]
    unfolding g_def by auto
  ultimately have "g -``
       (origin_ring.closeBasic(f -`` {𝟬⇩S}) ∩
        origin_ring.openBasic(x)) = target_ring.openBasic(f``x)"
    by auto
  with H show "g -``
       (origin_ring.closeBasic(f -`` {𝟬⇩S}) ∩
        origin_ring.openBasic(x)) ∈
           RepFun(target_ring.ideals, target_ring.openBasic)"
    by auto
qed

lemma (in ring_homo) spectrum_surj_open:
  defines "g ≡ λu∈target_ring.Spec. f-``u"
  assumes "f∈surj(R,S)"
  shows "∀U∈τ⇩t. g``U ∈ τ⇩o {restricted to} V(ker)"
proof
  fix U assume U:"U∈τ⇩t"
  then obtain I where I:"I◃R⇩t" "I⊆S" 
    "U=target_ring.openBasic(I)" unfolding top_target_def
    by auto
  from I(3) have sub:"U ⊆ target_ring.Spec" 
    using target_ring.openBasic_def[OF I(2)] by auto
  {
    fix t assume t:"t∈g``U"
    then obtain u where u:"u∈U" "t=g`u"
      using func_imagedef spectrum_surj[OF assms(2)] sub
      unfolding g_def by auto
    then have t:"t=f-``u" using beta sub unfolding g_def by auto
    with sub u(1) have "t◃⇩pR⇩o" unfolding target_ring.Spec_def
      using preimage_prime_ideal_surj[OF _ assms(2), of u]
      by auto
    then have p:"t∈origin_ring.Spec" unfolding origin_ring.Spec_def
      unfolding origin_ring.primeIdeal_def
      using origin_ring.ideal_dest_subset by auto
    from u(1) I(2,3) have Iu:"¬ (I ⊆ u)" using target_ring.openBasic_def
      by auto
    {
      assume "f-``I ⊆ t"
      then have "f``(f-``I) ⊆ f``t" by auto
      then have "I ⊆ f``t" using surj_image_vimage[OF assms(2)] I(2) by auto
      with t have "I ⊆ f``(f-``u)" by auto
      moreover from u(1) sub have "u ⊆ S"
        unfolding target_ring.Spec_def by auto
      ultimately have "I ⊆ u" using surj_image_vimage[OF assms(2)]
        by auto
      with Iu have False by auto
    }
    then have "¬(f-``I ⊆ t)" by auto
    with p have "t∈origin_ring.openBasic(f-``I)"
      using origin_ring.openBasic_def func1_1_L6A[OF surj_is_fun]
      assms(2) by auto
  }
  then have "g``U ⊆ origin_ring.openBasic(f-``I)" by auto moreover
  {
    fix t assume t:"t∈origin_ring.openBasic(f-``I)" "t∈V(ker)"
    have "f-``I ⊆ R" using func1_1_L6A[OF surj_is_fun]
      assms(2) by auto
    with t have p:"t∈origin_ring.Spec" "¬(f-``I ⊆ t)"
      using origin_ring.openBasic_def by auto
    from t(2) have kt:"ker ⊆ t" using origin_ring.closeBasic_def
      func1_1_L3 f_is_fun by auto
    {
      fix x assume "x∈f-``(f``t)"
      then have t:"f`x∈f``t" "x∈R" using func1_1_L15
        surj_is_fun[OF assms(2)] by auto
      then obtain s where s:"f`x = f`s" "s∈t" using
        func_imagedef[OF surj_is_fun[OF assms(2)]]
        p(1) unfolding origin_ring.Spec_def by auto
      from s(2) have ss:"s∈R" using p(1) 
        unfolding origin_ring.Spec_def by auto
      from s(1) have "(f`x) \<rs>⇩S (f`s) = 𝟬⇩S" using
        target_ring.Ring_ZF_1_L3(7)[OF apply_type[OF 
            surj_is_fun[OF assms(2)]
        t(2)]] by auto
      then have "f`(x\<rs>⇩Rs) = 𝟬⇩S" using homomor_dest_subs
        t(2) ss by auto moreover
      from t(2) ss have "x\<rs>⇩Rs ∈R" using origin_ring.Ring_ZF_1_L4(2) by auto
      ultimately have "x\<rs>⇩Rs ∈ f-``{𝟬⇩S}" using func1_1_L15
        surj_is_fun[OF assms(2)] by auto
      then have "x\<rs>⇩Rs ∈ t" using kt by auto
      then have "s\<ra>⇩R(x\<rs>⇩Rs) ∈ t" 
        using origin_ring.ideal_dest_sum
        s(2) p(1) unfolding origin_ring.Spec_def by auto
      then have "x∈t" using origin_ring.Ring_ZF_2_L1A(5)
        ss t(2) by auto
    }
    then have eq:"f-``(f``t) = t"
      using func1_1_L9[OF surj_is_fun[OF assms(2)]
      origin_ring.ideal_dest_subset[of t]] p(1) unfolding origin_ring.Spec_def
      origin_ring.primeIdeal_def by auto
    then have "(f `` t)◃R⇩t ⟹ (f``t)◃⇩pR⇩t"
      using prime_ideal_quot_3[of "f``t"] assms(2)
      p(1) unfolding origin_ring.Spec_def by auto
    then have id:"(f``t)◃⇩pR⇩t" "(f `` t)◃R⇩t" using image_ideal_surj
      p(1) assms(2) unfolding origin_ring.Spec_def by auto
    {
      assume "I ⊆ f``t"
      then have "f-``I ⊆ f-``(f``t)" by auto
      with eq have "f-``I ⊆ t" by auto
      with p(2) have False by auto
    }
    then have "¬(I ⊆ f``t)" by auto
    then have "f``t∈target_ring.openBasic(I)"
      using id target_ring.ideal_dest_subset unfolding target_ring.openBasic_def[OF I(2)]
      target_ring.Spec_def by auto
    then have q:"f``t ∈U" using I(3) by auto
    then have q2:"f``t∈target_ring.Spec" using sub by auto
    from q have "g`(f``t) ∈g``U" using func1_1_L15D[OF bij_is_fun
      [OF spectrum_surj_bij[OF assms(2)]], of "f``t" U]
      unfolding g_def using sub by auto
    then have "f-``(f``t) ∈ g``U" using beta[of "f``t"
      target_ring.Spec "λo. f-``o"] q2
      unfolding g_def by auto
    with eq have "t∈g``U" by auto
  }
  then have "V(ker)∩D(f -`` I) ⊆ g``U" by auto
  ultimately
  have "V(ker)∩D(f -`` I) = g``U"
    using func1_1_L6(2)[OF bij_is_fun[OF
    spectrum_surj_bij[OF assms(2)]],of U] 
    unfolding g_def by blast
  moreover
  from I(1) have "(f-``(I)) ◃R" and "(f-``(I)) ⊆ R" 
    using preimage_ideal(2)  origin_ring.ideal_dest_subset by simp_all
  then have "V(ker)∩D(f-``(I)) ∈ {V(ker) ∩ A . A ∈ τ⇩o}"
    unfolding top_origin_def by auto
  ultimately show "g``U:  τ⇩o{restricted to}V(ker)"
    unfolding RestrictedTo_def by auto
qed

text‹A quotient ring has a spectrum homeomorphic
to a closed subspace of the spectrum of the base ring.
Specifically, the closed subspace associated to the
ideal by which we quotient.›

corollary (in ring_homo) surj_homeomorphism:
  assumes "f∈surj(R,S)"
  defines "g ≡ λu∈target_ring.Spec. f -`` u"
  shows "IsAhomeomorphism(τ⇩t, τ⇩o{restricted to}V(ker), g)"
proof-
  have "⋃(τ⇩o{restricted to}V(ker)) = origin_ring.Spec ∩ V(ker)" unfolding
    top_origin_def RestrictedTo_def using origin_ring.total_spec
    by auto
  then have "⋃(τ⇩o{restricted to}V(ker)) = V(ker)"
    using origin_ring.closeBasic_def func1_1_L3 f_is_fun
     by auto moreover
  have "⋃τ⇩t = target_ring.Spec" unfolding top_target_def
    using target_ring.total_spec by auto
  ultimately show ?thesis using bij_cont_open_homeo[of g τ⇩t "τ⇩o{restricted to}V(ker)"]
    spectrum_surj_bij[OF assms(1)] spectrum_surj_open[OF assms(1)]
    spectrum_surj_cont[OF assms(1)]
    unfolding g_def by auto
qed
  
end