[STATEMENT]
lemma key_map_is_ring_morphism:
  assumes "\<pp> \<in> U" and "is_zariski_open U"
  shows "ring_homomorphism (key_map U)
(\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
proof (intro ring_homomorphism.intro)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at
 2. ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
 3. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
 4. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 5. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
show "Set_Theory.map (key_map U) (\<O> U) (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at
[PROOF STEP]
using key_map_is_map assms(1)
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> ?U \<Longrightarrow> Set_Theory.map (local.key_map ?U) (\<O> ?U) pi.carrier_local_ring_at
\<pp> \<in> U

goal (1 subgoal):
 1. Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at

goal (4 subgoals):
 1. ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
 2. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
 3. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 4. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
 2. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
 3. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 4. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
show "ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
[PROOF STEP]
using \<open>is_zariski_open U\<close> pr.is_ring_from_is_homomorphism
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
is_zariski_open ?U \<Longrightarrow> ring (\<O> ?U) (add_sheaf_spec ?U) (mult_sheaf_spec ?U) (zero_sheaf_spec ?U) (one_sheaf_spec ?U)

goal (1 subgoal):
 1. ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)

goal (3 subgoals):
 1. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
 2. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 3. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
 2. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 3. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
show "ring (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
by (simp add: pi.ring_axioms)
[PROOF STATE]
proof (state)
this:
ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (2 subgoals):
 1. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 2. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
 2. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
show "group_homomorphism (key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.zero_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at
 2. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 3. monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at
 4. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
show "Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at
[PROOF STEP]
by (simp add: assms(1) key_map_is_map)
[PROOF STATE]
proof (state)
this:
Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at

goal (3 subgoals):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 2. monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at
 3. Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
show "Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)"
      "Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) &&& Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
using pr.is_ring_from_is_homomorphism [OF \<open>is_zariski_open U\<close>]
[PROOF STATE]
proof (prove)
using this:
ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)

goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) &&& Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
unfolding ring_def Group_Theory.group_def abelian_group_def
[PROOF STATE]
proof (prove)
using this:
((Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) \<and> Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)) \<and> commutative_monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)) \<and> Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) \<and> ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)

goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) &&& Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
Group_Theory.group_axioms (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)

goal (1 subgoal):
 1. monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at
[PROOF STEP]
have 1: "(key_map U) (zero_sheaf_spec U) = pi.zero_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.key_map U (zero_sheaf_spec U) = pi.zero_local_ring_at
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
is_zariski_open U

goal (1 subgoal):
 1. local.key_map U (zero_sheaf_spec U) = pi.zero_local_ring_at
[PROOF STEP]
unfolding key_map_def pi.zero_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
is_zariski_open U

goal (1 subgoal):
 1. (\<lambda>s\<in>\<O> U. s \<pp>) (zero_sheaf_spec U) = local.zero_rel
[PROOF STEP]
by (metis (no_types, lifting) restrict_apply' zero_sheaf_spec_def zero_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (state)
this:
local.key_map U (zero_sheaf_spec U) = pi.zero_local_ring_at

goal (1 subgoal):
 1. monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at
[PROOF STEP]
have 2: "\<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow>
           (key_map U) (add_sheaf_spec U x y) = pi.add_local_ring_at (key_map U x) (key_map U y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (add_sheaf_spec U x y) = pi.add_local_ring_at (local.key_map U x) (local.key_map U y)
[PROOF STEP]
using add_sheaf_spec_in_sheaf_spec key_map_def assms pi.add_local_ring_at_def
        add_sheaf_spec_def spectrum_def zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<in> \<O> ?U; ?t \<in> \<O> ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> add_sheaf_spec ?U ?s ?t \<in> \<O> ?U
local.key_map ?U \<equiv> \<lambda>s\<in>\<O> ?U. s \<pp>
\<pp> \<in> U
is_zariski_open U
pi.add_local_ring_at \<equiv> local.add_rel
add_sheaf_spec ?U ?s ?s' \<equiv> \<lambda>\<pp>\<in>?U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (?s \<pp>) (?s' \<pp>)
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (add_sheaf_spec U x y) = pi.add_local_ring_at (local.key_map U x) (local.key_map U y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (add_sheaf_spec U ?x3 ?y3) = pi.add_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)

goal (1 subgoal):
 1. monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at
[PROOF STEP]
show "monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at
[PROOF STEP]
unfolding monoid_homomorphism_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y. x \<in> \<O> U \<longrightarrow> y \<in> \<O> U \<longrightarrow> local.key_map U (add_sheaf_spec U x y) = pi.add_local_ring_at (local.key_map U x) (local.key_map U y)) \<and> local.key_map U (zero_sheaf_spec U) = pi.zero_local_ring_at
[PROOF STEP]
by (auto simp: 1 2)
[PROOF STATE]
proof (state)
this:
monoid_homomorphism_axioms (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.add_local_ring_at pi.zero_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
group_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.zero_local_ring_at

goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
have "(key_map U) (one_sheaf_spec U) = pi.one_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
[PROOF STEP]
using one_sheaf_spec_def key_map_def pi.one_local_ring_at_def assms one_sheaf_spec_in_sheaf_spec spectrum_def
[PROOF STATE]
proof (prove)
using this:
one_sheaf_spec ?U \<equiv> \<lambda>\<pp>\<in>?U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
local.key_map ?U \<equiv> \<lambda>s\<in>\<O> ?U. s \<pp>
pi.one_local_ring_at \<equiv> local.one_rel
\<pp> \<in> U
is_zariski_open U
is_zariski_open ?U \<Longrightarrow> one_sheaf_spec ?U \<in> \<O> ?U
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}

goal (1 subgoal):
 1. local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at

goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at

goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
have "\<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow>
           (key_map U) (mult_sheaf_spec U x y) = pi.mult_local_ring_at (key_map U x) (key_map U y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U x y) = pi.mult_local_ring_at (local.key_map U x) (local.key_map U y)
[PROOF STEP]
using mult_sheaf_spec_in_sheaf_spec key_map_def assms pi.mult_local_ring_at_def
      mult_sheaf_spec_def spectrum_def zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<in> \<O> ?U; ?t \<in> \<O> ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> mult_sheaf_spec ?U ?s ?t \<in> \<O> ?U
local.key_map ?U \<equiv> \<lambda>s\<in>\<O> ?U. s \<pp>
\<pp> \<in> U
is_zariski_open U
pi.mult_local_ring_at \<equiv> local.mult_rel
mult_sheaf_spec ?U ?s ?s' \<equiv> \<lambda>\<pp>\<in>?U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (?s \<pp>) (?s' \<pp>)
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U x y) = pi.mult_local_ring_at (local.key_map U x) (local.key_map U y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U ?x3 ?y3) = pi.mult_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)

goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U ?x3 ?y3) = pi.mult_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)
[PROOF STEP]
show "monoid_homomorphism (key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.mult_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
using this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U ?x3 ?y3) = pi.mult_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)

goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
using pr.is_ring_from_is_homomorphism [OF \<open>is_zariski_open U\<close>] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U ?x3 ?y3) = pi.mult_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)
ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
\<pp> \<in> U

goal (1 subgoal):
 1. monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at
[PROOF STEP]
unfolding monoid_homomorphism_def monoid_homomorphism_axioms_def ring_def
[PROOF STATE]
proof (prove)
using this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U ?x3 ?y3) = pi.mult_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)
abelian_group (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) \<and> Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) \<and> ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
\<pp> \<in> U

goal (1 subgoal):
 1. (Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at \<and> Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)) \<and> Group_Theory.monoid pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at \<and> (\<forall>x y. x \<in> \<O> U \<longrightarrow> y \<in> \<O> U \<longrightarrow> local.key_map U (mult_sheaf_spec U x y) = pi.mult_local_ring_at (local.key_map U x) (local.key_map U y)) \<and> local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
[PROOF STEP]
using key_map_is_map pi.multiplicative.monoid_axioms
[PROOF STATE]
proof (prove)
using this:
local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> local.key_map U (mult_sheaf_spec U ?x3 ?y3) = pi.mult_local_ring_at (local.key_map U ?x3) (local.key_map U ?y3)
abelian_group (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) \<and> Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) \<and> ring_axioms (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U)
\<pp> \<in> U
\<pp> \<in> ?U \<Longrightarrow> Set_Theory.map (local.key_map ?U) (\<O> ?U) pi.carrier_local_ring_at
Group_Theory.monoid pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. (Set_Theory.map (local.key_map U) (\<O> U) pi.carrier_local_ring_at \<and> Group_Theory.monoid (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U)) \<and> Group_Theory.monoid pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at \<and> (\<forall>x y. x \<in> \<O> U \<longrightarrow> y \<in> \<O> U \<longrightarrow> local.key_map U (mult_sheaf_spec U x y) = pi.mult_local_ring_at (local.key_map U x) (local.key_map U y)) \<and> local.key_map U (one_sheaf_spec U) = pi.one_local_ring_at
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
monoid_homomorphism (local.key_map U) (\<O> U) (mult_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.mult_local_ring_at pi.one_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma key_map_is_coherent:
  assumes "V \<subseteq> U" and "is_zariski_open U" and "is_zariski_open V" and "\<pp> \<in> V" and "s \<in> \<O> U"
  shows "(key_map V \<circ> sheaf_spec_morphisms U V) s = key_map U s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.key_map V \<circ> sheaf_spec_morphisms U V) s = local.key_map U s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (local.key_map V \<circ> sheaf_spec_morphisms U V) s = local.key_map U s
[PROOF STEP]
have "sheaf_spec_morphisms U V s \<in> \<O> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V s \<in> \<O> V
[PROOF STEP]
using assms sheaf_spec_morphisms_are_maps map.map_closed
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> U
is_zariski_open U
is_zariski_open V
\<pp> \<in> V
s \<in> \<O> U
\<lbrakk>is_zariski_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (sheaf_spec_morphisms ?U ?V) (\<O> ?U) (\<O> ?V)
\<lbrakk>Set_Theory.map ?\<alpha> ?S ?T; ?a \<in> ?S\<rbrakk> \<Longrightarrow> ?\<alpha> ?a \<in> ?T

goal (1 subgoal):
 1. sheaf_spec_morphisms U V s \<in> \<O> V
[PROOF STEP]
by (metis (mono_tags, opaque_lifting))
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V s \<in> \<O> V

goal (1 subgoal):
 1. (local.key_map V \<circ> sheaf_spec_morphisms U V) s = local.key_map U s
[PROOF STEP]
thus "(key_map V \<circ> sheaf_spec_morphisms U V) s = key_map U s"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U V s \<in> \<O> V

goal (1 subgoal):
 1. (local.key_map V \<circ> sheaf_spec_morphisms U V) s = local.key_map U s
[PROOF STEP]
by (simp add: \<open>s \<in> \<O> U\<close> assms(4) key_map_def sheaf_spec_morphisms_def)
[PROOF STATE]
proof (state)
this:
(local.key_map V \<circ> sheaf_spec_morphisms U V) s = local.key_map U s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma key_ring_morphism:
  assumes "is_zariski_open V" and "\<pp> \<in> V"
  shows "\<exists>\<phi>. ring_homomorphism \<phi>
st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)
\<and>
(\<forall>U\<in>(top.neighborhoods \<pp>). \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = key_map U s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
have "ring (R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
by (simp add: pi.ring_axioms)
[PROOF STATE]
proof (state)
this:
ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
have "V \<in> top.neighborhoods \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> top.neighborhoods \<pp>
[PROOF STEP]
using assms top.neighborhoods_def sheaf_spec_is_presheaf
[PROOF STATE]
proof (prove)
using this:
is_zariski_open V
\<pp> \<in> V
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}
presheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal (1 subgoal):
 1. V \<in> top.neighborhoods \<pp>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
V \<in> top.neighborhoods \<pp>

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V \<in> top.neighborhoods \<pp>

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
have "\<And>U. U \<in> top.neighborhoods \<pp> \<Longrightarrow>
          ring_homomorphism (key_map U)
(\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
(R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) (pi.add_local_ring_at) (pi.mult_local_ring_at) (pi.zero_local_ring_at) (pi.one_local_ring_at)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. U \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
using key_map_is_ring_morphism top.neighborhoods_def sheaf_spec_is_presheaf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<pp> \<in> ?U; is_zariski_open ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (local.key_map ?U) (\<O> ?U) (add_sheaf_spec ?U) (mult_sheaf_spec ?U) (zero_sheaf_spec ?U) (one_sheaf_spec ?U) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}
presheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal (1 subgoal):
 1. \<And>U. U \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?U3 \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map ?U3) (\<O> ?U3) (add_sheaf_spec ?U3) (mult_sheaf_spec ?U3) (zero_sheaf_spec ?U3) (one_sheaf_spec ?U3) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?U3 \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map ?U3) (\<O> ?U3) (add_sheaf_spec ?U3) (mult_sheaf_spec ?U3) (zero_sheaf_spec ?U3) (one_sheaf_spec ?U3) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
have "\<And>U V x. \<lbrakk>U \<in> top.neighborhoods \<pp>; V \<in> top.neighborhoods \<pp>; V \<subseteq> U; x \<in> \<O> U\<rbrakk>
                          \<Longrightarrow> (key_map V \<circ> sheaf_spec_morphisms U V) x = key_map U x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>U \<in> top.neighborhoods \<pp>; V \<in> top.neighborhoods \<pp>; V \<subseteq> U; x \<in> \<O> U\<rbrakk> \<Longrightarrow> (local.key_map V \<circ> sheaf_spec_morphisms U V) x = local.key_map U x
[PROOF STEP]
using key_map_is_coherent
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?V \<subseteq> ?U; is_zariski_open ?U; is_zariski_open ?V; \<pp> \<in> ?V; ?s \<in> \<O> ?U\<rbrakk> \<Longrightarrow> (local.key_map ?V \<circ> sheaf_spec_morphisms ?U ?V) ?s = local.key_map ?U ?s

goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>U \<in> top.neighborhoods \<pp>; V \<in> top.neighborhoods \<pp>; V \<subseteq> U; x \<in> \<O> U\<rbrakk> \<Longrightarrow> (local.key_map V \<circ> sheaf_spec_morphisms U V) x = local.key_map U x
[PROOF STEP]
by (metis (no_types, lifting) mem_Collect_eq top.neighborhoods_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?U3 \<in> top.neighborhoods \<pp>; ?V3 \<in> top.neighborhoods \<pp>; ?V3 \<subseteq> ?U3; ?x3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> (local.key_map ?V3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?x3 = local.key_map ?U3 ?x3

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
V \<in> top.neighborhoods \<pp>
?U3 \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map ?U3) (\<O> ?U3) (add_sheaf_spec ?U3) (mult_sheaf_spec ?U3) (zero_sheaf_spec ?U3) (one_sheaf_spec ?U3) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
\<lbrakk>?U3 \<in> top.neighborhoods \<pp>; ?V3 \<in> top.neighborhoods \<pp>; ?V3 \<subseteq> ?U3; ?x3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> (local.key_map ?V3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?x3 = local.key_map ?U3 ?x3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
V \<in> top.neighborhoods \<pp>
?U3 \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map ?U3) (\<O> ?U3) (add_sheaf_spec ?U3) (mult_sheaf_spec ?U3) (zero_sheaf_spec ?U3) (one_sheaf_spec ?U3) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
\<lbrakk>?U3 \<in> top.neighborhoods \<pp>; ?V3 \<in> top.neighborhoods \<pp>; ?V3 \<subseteq> ?U3; ?x3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> (local.key_map ?V3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?x3 = local.key_map ?U3 ?x3

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
using assms local.sheaf_spec_is_presheaf zariski_open_is_subset
      st.universal_property_for_stalk[of "R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>" "pi.add_local_ring_at" "pi.mult_local_ring_at"
        "pi.zero_local_ring_at" "pi.one_local_ring_at" "key_map"]
[PROOF STATE]
proof (prove)
using this:
ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
V \<in> top.neighborhoods \<pp>
?U3 \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map ?U3) (\<O> ?U3) (add_sheaf_spec ?U3) (mult_sheaf_spec ?U3) (zero_sheaf_spec ?U3) (one_sheaf_spec ?U3) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at
\<lbrakk>?U3 \<in> top.neighborhoods \<pp>; ?V3 \<in> top.neighborhoods \<pp>; ?V3 \<subseteq> ?U3; ?x3 \<in> \<O> ?U3\<rbrakk> \<Longrightarrow> (local.key_map ?V3 \<circ> sheaf_spec_morphisms ?U3 ?V3) ?x3 = local.key_map ?U3 ?x3
is_zariski_open V
\<pp> \<in> V
presheaf_of_rings local.local.spectrum local.local.is_zariski_open local.local.sheaf_spec local.local.sheaf_spec_morphisms local.local.\<O>b local.local.add_sheaf_spec local.local.mult_sheaf_spec local.local.zero_sheaf_spec local.local.one_sheaf_spec
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec
\<lbrakk>ring pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at; \<And>U. U \<in> top.neighborhoods \<pp> \<Longrightarrow> ring_homomorphism (local.key_map U) (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at; \<And>U V s. \<lbrakk>U \<in> top.neighborhoods \<pp>; V \<in> top.neighborhoods \<pp>; V \<subseteq> U; s \<in> \<O> U\<rbrakk> \<Longrightarrow> (local.key_map V \<circ> sheaf_spec_morphisms U V) s = local.key_map U s\<rbrakk> \<Longrightarrow> \<forall>V\<in>top.neighborhoods \<pp>. \<exists>!u. ring_homomorphism u st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (u \<circ> st.canonical_fun U) s = local.key_map U s)

goal (1 subgoal):
 1. \<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<phi>. ring_homomorphism \<phi> st.carrier_stalk st.add_stalk st.mult_stalk (st.zero_stalk V) (st.one_stalk V) pi.carrier_local_ring_at pi.add_local_ring_at pi.mult_local_ring_at pi.zero_local_ring_at pi.one_local_ring_at \<and> (\<forall>U\<in>top.neighborhoods \<pp>. \<forall>s\<in>\<O> U. (\<phi> \<circ> st.canonical_fun U) s = local.key_map U s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma class_from_belongs_stalk:
  assumes "s \<in> st.carrier_stalk"
  obtains U s' where "is_zariski_open U" "\<pp> \<in> U" "s' \<in> \<O> U" "s = st.class_of U s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret dl: direct_lim Spec is_zariski_open sheaf_spec sheaf_spec_morphisms "\<O>b"
    add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec "top.neighborhoods \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. direct_lim Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec (top.neighborhoods \<pp>)
[PROOF STEP]
by (simp add: st.direct_lim_axioms top.neighborhoods_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret eq: equivalence "Sigma (top.neighborhoods \<pp>) sheaf_spec" "{(x, y). dl.rel x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence (Sigma (top.neighborhoods \<pp>) sheaf_spec) {(x, y). dl.rel x y}
[PROOF STEP]
using dl.rel_is_equivalence
[PROOF STATE]
proof (prove)
using this:
equivalence (Sigma (top.neighborhoods \<pp>) sheaf_spec) {(x, y). dl.rel x y}

goal (1 subgoal):
 1. equivalence (Sigma (top.neighborhoods \<pp>) sheaf_spec) {(x, y). dl.rel x y}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note dl.subset_of_opens [simp del]
[PROOF STATE]
proof (state)
this:
?U \<in> top.neighborhoods \<pp> \<Longrightarrow> is_zariski_open ?U

goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain U s' where seq: "s = eq.Class (U, s')" and U: "U \<in> top.neighborhoods \<pp>" and s': "s' \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>s = eq.Class (U, s'); U \<in> top.neighborhoods \<pp>; s' \<in> \<O> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<in> st.carrier_stalk

goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>s = eq.Class (U, s'); U \<in> top.neighborhoods \<pp>; s' \<in> \<O> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding st.carrier_stalk_def dl.carrier_direct_lim_def
[PROOF STATE]
proof (prove)
using this:
s \<in> eq.Partition

goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>s = eq.Class (U, s'); U \<in> top.neighborhoods \<pp>; s' \<in> \<O> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis SigmaD1 SigmaD2 eq.representant_exists old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
s = eq.Class (U, s')
U \<in> top.neighborhoods \<pp>
s' \<in> \<O> U

goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. is_zariski_open ?U3
 2. \<pp> \<in> ?U3
 3. ?s'3 \<in> \<O> ?U3
 4. s = st.class_of ?U3 ?s'3
[PROOF STEP]
show "is_zariski_open U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open U
[PROOF STEP]
using U dl.subset_of_opens
[PROOF STATE]
proof (prove)
using this:
U \<in> top.neighborhoods \<pp>
?U \<in> top.neighborhoods \<pp> \<Longrightarrow> is_zariski_open ?U

goal (1 subgoal):
 1. is_zariski_open U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_zariski_open U

goal (3 subgoals):
 1. \<pp> \<in> U
 2. ?s'3 \<in> \<O> U
 3. s = st.class_of U ?s'3
[PROOF STEP]
show "\<pp> \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> U
[PROOF STEP]
using U top.neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
U \<in> top.neighborhoods \<pp>
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}

goal (1 subgoal):
 1. \<pp> \<in> U
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (2 subgoals):
 1. ?s'3 \<in> \<O> U
 2. s = st.class_of U ?s'3
[PROOF STEP]
show "s' \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<in> \<O> U
[PROOF STEP]
using s'
[PROOF STATE]
proof (prove)
using this:
s' \<in> \<O> U

goal (1 subgoal):
 1. s' \<in> \<O> U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s' \<in> \<O> U

goal (1 subgoal):
 1. s = st.class_of U s'
[PROOF STEP]
show "s = st.class_of U s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = st.class_of U s'
[PROOF STEP]
using seq st.class_of_def top.neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
s = eq.Class (U, s')
st.class_of ?U ?s \<equiv> equivalence.Class (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y} (?U, ?s)
top.neighborhoods ?x \<equiv> {U. is_zariski_open U \<and> ?x \<in> U}

goal (1 subgoal):
 1. s = st.class_of U s'
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
s = st.class_of U s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma same_class_from_restrict:
  assumes "is_zariski_open U" "is_zariski_open V" "U \<subseteq> V" "s \<in> \<O> V" "\<pp> \<in> U"
  shows "st.class_of V s = st.class_of U (sheaf_spec_morphisms V U s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.class_of V s = st.class_of U (sheaf_spec_morphisms V U s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st.class_of V s = st.class_of U (sheaf_spec_morphisms V U s)
[PROOF STEP]
interpret eq: equivalence "Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec" "{(x, y). st.rel x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y}
[PROOF STEP]
using st.rel_is_equivalence
[PROOF STATE]
proof (prove)
using this:
equivalence (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y}

goal (1 subgoal):
 1. equivalence (Sigma {U. is_zariski_open U \<and> \<pp> \<in> U} sheaf_spec) {(x, y). st.rel x y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st.class_of V s = st.class_of U (sheaf_spec_morphisms V U s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.class_of V s = st.class_of U (sheaf_spec_morphisms V U s)
[PROOF STEP]
unfolding st.class_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq.Class (V, s) = eq.Class (U, sheaf_spec_morphisms V U s)
[PROOF STEP]
proof (rule eq.Class_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}
[PROOF STEP]
have \<section>:"sheaf_spec_morphisms V U s \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms V U s \<in> \<O> U
[PROOF STEP]
using assms map.map_closed pr.is_map_from_is_homomorphism
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
is_zariski_open V
U \<subseteq> V
s \<in> \<O> V
\<pp> \<in> U
\<lbrakk>Set_Theory.map ?\<alpha> ?S ?T; ?a \<in> ?S\<rbrakk> \<Longrightarrow> ?\<alpha> ?a \<in> ?T
\<lbrakk>is_zariski_open ?U; is_zariski_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (sheaf_spec_morphisms ?U ?V) (\<O> ?U) (\<O> ?V)

goal (1 subgoal):
 1. sheaf_spec_morphisms V U s \<in> \<O> U
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms V U s \<in> \<O> U

goal (1 subgoal):
 1. ((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sheaf_spec_morphisms V U s \<in> \<O> U
[PROOF STEP]
have "\<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)"
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms V U s \<in> \<O> U

goal (1 subgoal):
 1. \<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)
[PROOF STEP]
using assms(1) assms(3) assms(5)
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms V U s \<in> \<O> U
is_zariski_open U
U \<subseteq> V
\<pp> \<in> U

goal (1 subgoal):
 1. \<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)

goal (1 subgoal):
 1. ((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)
[PROOF STEP]
show "((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}"
[PROOF STATE]
proof (prove)
using this:
\<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)

goal (1 subgoal):
 1. ((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}
[PROOF STEP]
using \<section> assms
[PROOF STATE]
proof (prove)
using this:
\<exists>W. is_zariski_open W \<and> \<pp> \<in> W \<and> W \<subseteq> V \<and> W \<subseteq> U \<and> sheaf_spec_morphisms V W s = sheaf_spec_morphisms U W (sheaf_spec_morphisms V U s)
sheaf_spec_morphisms V U s \<in> \<O> U
is_zariski_open U
is_zariski_open V
U \<subseteq> V
s \<in> \<O> V
\<pp> \<in> U

goal (1 subgoal):
 1. ((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}
[PROOF STEP]
by (auto simp: st.rel_def)
[PROOF STATE]
proof (state)
this:
((V, s), U, sheaf_spec_morphisms V U s) \<in> {(x, y). st.rel x y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
st.class_of V s = st.class_of U (sheaf_spec_morphisms V U s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shrinking_from_belong_stalk:
  assumes "s \<in> st.carrier_stalk" and "t \<in> st.carrier_stalk"
  obtains U s' t' where "is_zariski_open U" "\<pp> \<in> U" "s' \<in> \<O> U" "s = st.class_of U s'"
    "t' \<in> \<O> U" "t = st.class_of U t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U s' t'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'; t' \<in> \<O> U; t = st.class_of U t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>U s' t'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'; t' \<in> \<O> U; t = st.class_of U t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain U s' where HU:"is_zariski_open U" "\<pp> \<in> U" "s' \<in> \<O> U" "s = st.class_of U s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) class_from_belongs_stalk
[PROOF STATE]
proof (prove)
using this:
s \<in> st.carrier_stalk
\<lbrakk>?s \<in> st.carrier_stalk; \<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; ?s = st.class_of U s'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_zariski_open U
\<pp> \<in> U
s' \<in> \<O> U
s = st.class_of U s'

goal (1 subgoal):
 1. (\<And>U s' t'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'; t' \<in> \<O> U; t = st.class_of U t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain V t' where HV:"is_zariski_open V" "\<pp> \<in> V" "t' \<in> \<O> V" "t = st.class_of V t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V t'. \<lbrakk>is_zariski_open V; \<pp> \<in> V; t' \<in> \<O> V; t = st.class_of V t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) class_from_belongs_stalk
[PROOF STATE]
proof (prove)
using this:
t \<in> st.carrier_stalk
\<lbrakk>?s \<in> st.carrier_stalk; \<And>U s'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; ?s = st.class_of U s'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>V t'. \<lbrakk>is_zariski_open V; \<pp> \<in> V; t' \<in> \<O> V; t = st.class_of V t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_zariski_open V
\<pp> \<in> V
t' \<in> \<O> V
t = st.class_of V t'

goal (1 subgoal):
 1. (\<And>U s' t'. \<lbrakk>is_zariski_open U; \<pp> \<in> U; s' \<in> \<O> U; s = st.class_of U s'; t' \<in> \<O> U; t = st.class_of U t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. is_zariski_open ?U3
 2. \<pp> \<in> ?U3
 3. ?s'3 \<in> \<O> ?U3
 4. s = st.class_of ?U3 ?s'3
 5. ?t'3 \<in> \<O> ?U3
 6. t = st.class_of ?U3 ?t'3
[PROOF STEP]
have "U \<inter> V \<subseteq> Spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<inter> V \<subseteq> Spec
[PROOF STEP]
using zariski_open_is_subset HU(1)
[PROOF STATE]
proof (prove)
using this:
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec
is_zariski_open U

goal (1 subgoal):
 1. U \<inter> V \<subseteq> Spec
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U \<inter> V \<subseteq> Spec

goal (6 subgoals):
 1. is_zariski_open ?U3
 2. \<pp> \<in> ?U3
 3. ?s'3 \<in> \<O> ?U3
 4. s = st.class_of ?U3 ?s'3
 5. ?t'3 \<in> \<O> ?U3
 6. t = st.class_of ?U3 ?t'3
[PROOF STEP]
show "\<pp> \<in> U \<inter> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> U \<inter> V
[PROOF STEP]
by (simp add: \<open>\<pp> \<in> U\<close> \<open>\<pp> \<in> V\<close>)
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U \<inter> V

goal (5 subgoals):
 1. is_zariski_open (U \<inter> V)
 2. ?s'3 \<in> \<O> (U \<inter> V)
 3. s = st.class_of (U \<inter> V) ?s'3
 4. ?t'3 \<in> \<O> (U \<inter> V)
 5. t = st.class_of (U \<inter> V) ?t'3
[PROOF STEP]
show UV: "is_zariski_open (U \<inter> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open (U \<inter> V)
[PROOF STEP]
using topological_space.open_inter
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>topological_space ?S ?is_open; ?is_open ?U; ?is_open ?V\<rbrakk> \<Longrightarrow> ?is_open (?U \<inter> ?V)

goal (1 subgoal):
 1. is_zariski_open (U \<inter> V)
[PROOF STEP]
by (simp add: \<open>is_zariski_open U\<close> \<open>is_zariski_open V\<close>)
[PROOF STATE]
proof (state)
this:
is_zariski_open (U \<inter> V)

goal (4 subgoals):
 1. ?s'3 \<in> \<O> (U \<inter> V)
 2. s = st.class_of (U \<inter> V) ?s'3
 3. ?t'3 \<in> \<O> (U \<inter> V)
 4. t = st.class_of (U \<inter> V) ?t'3
[PROOF STEP]
show "s = st.class_of (U \<inter> V) (sheaf_spec_morphisms U (U \<inter> V) s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = st.class_of (U \<inter> V) (sheaf_spec_morphisms U (U \<inter> V) s')
[PROOF STEP]
using HU UV \<open>\<pp> \<in> U \<inter> V\<close> same_class_from_restrict
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
\<pp> \<in> U
s' \<in> \<O> U
s = st.class_of U s'
is_zariski_open (U \<inter> V)
\<pp> \<in> U \<inter> V
\<lbrakk>is_zariski_open ?U; is_zariski_open ?V; ?U \<subseteq> ?V; ?s \<in> \<O> ?V; \<pp> \<in> ?U\<rbrakk> \<Longrightarrow> st.class_of ?V ?s = st.class_of ?U (sheaf_spec_morphisms ?V ?U ?s)

goal (1 subgoal):
 1. s = st.class_of (U \<inter> V) (sheaf_spec_morphisms U (U \<inter> V) s')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s = st.class_of (U \<inter> V) (sheaf_spec_morphisms U (U \<inter> V) s')

goal (3 subgoals):
 1. sheaf_spec_morphisms U (U \<inter> V) s' \<in> \<O> (U \<inter> V)
 2. ?t'3 \<in> \<O> (U \<inter> V)
 3. t = st.class_of (U \<inter> V) ?t'3
[PROOF STEP]
show "t = st.class_of (U \<inter> V) (sheaf_spec_morphisms V (U \<inter> V) t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = st.class_of (U \<inter> V) (sheaf_spec_morphisms V (U \<inter> V) t')
[PROOF STEP]
using HV UV \<open>\<pp> \<in> U \<inter> V\<close> same_class_from_restrict
[PROOF STATE]
proof (prove)
using this:
is_zariski_open V
\<pp> \<in> V
t' \<in> \<O> V
t = st.class_of V t'
is_zariski_open (U \<inter> V)
\<pp> \<in> U \<inter> V
\<lbrakk>is_zariski_open ?U; is_zariski_open ?V; ?U \<subseteq> ?V; ?s \<in> \<O> ?V; \<pp> \<in> ?U\<rbrakk> \<Longrightarrow> st.class_of ?V ?s = st.class_of ?U (sheaf_spec_morphisms ?V ?U ?s)

goal (1 subgoal):
 1. t = st.class_of (U \<inter> V) (sheaf_spec_morphisms V (U \<inter> V) t')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = st.class_of (U \<inter> V) (sheaf_spec_morphisms V (U \<inter> V) t')

goal (2 subgoals):
 1. sheaf_spec_morphisms U (U \<inter> V) s' \<in> \<O> (U \<inter> V)
 2. sheaf_spec_morphisms V (U \<inter> V) t' \<in> \<O> (U \<inter> V)
[PROOF STEP]
show "sheaf_spec_morphisms U (U \<inter> V) s' \<in> \<O> (U \<inter> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U (U \<inter> V) s' \<in> \<O> (U \<inter> V)
[PROOF STEP]
using HU(3) UV map.map_closed sheaf_spec_morphisms_are_maps
[PROOF STATE]
proof (prove)
using this:
s' \<in> \<O> U
is_zariski_open (U \<inter> V)
\<lbrakk>Set_Theory.map ?\<alpha> ?S ?T; ?a \<in> ?S\<rbrakk> \<Longrightarrow> ?\<alpha> ?a \<in> ?T
\<lbrakk>is_zariski_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (sheaf_spec_morphisms ?U ?V) (\<O> ?U) (\<O> ?V)

goal (1 subgoal):
 1. sheaf_spec_morphisms U (U \<inter> V) s' \<in> \<O> (U \<inter> V)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U (U \<inter> V) s' \<in> \<O> (U \<inter> V)

goal (1 subgoal):
 1. sheaf_spec_morphisms V (U \<inter> V) t' \<in> \<O> (U \<inter> V)
[PROOF STEP]
show "sheaf_spec_morphisms V (U \<inter> V) t' \<in> \<O> (U \<inter> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms V (U \<inter> V) t' \<in> \<O> (U \<inter> V)
[PROOF STEP]
using HV(3) UV map.map_closed sheaf_spec_morphisms_are_maps
[PROOF STATE]
proof (prove)
using this:
t' \<in> \<O> V
is_zariski_open (U \<inter> V)
\<lbrakk>Set_Theory.map ?\<alpha> ?S ?T; ?a \<in> ?S\<rbrakk> \<Longrightarrow> ?\<alpha> ?a \<in> ?T
\<lbrakk>is_zariski_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> Set_Theory.map (sheaf_spec_morphisms ?U ?V) (\<O> ?U) (\<O> ?V)

goal (1 subgoal):
 1. sheaf_spec_morphisms V (U \<inter> V) t' \<in> \<O> (U \<inter> V)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms V (U \<inter> V) t' \<in> \<O> (U \<inter> V)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed