[STATEMENT]
lemma induced_morphism_is_well_defined:
  assumes "stfx.rel (V,q) (V',q')"
  shows "stx.class_of (f\<^sup>\<inverse> X V) (\<phi>\<^sub>f V q) = stx.class_of (f\<^sup>\<inverse> X V') (\<phi>\<^sub>f V' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stx.class_of (f \<^sup>\<inverse> X V) (\<phi>\<^sub>f V q) = stx.class_of (f \<^sup>\<inverse> X V') (\<phi>\<^sub>f V' q')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stx.class_of (f \<^sup>\<inverse> X V) (\<phi>\<^sub>f V q) = stx.class_of (f \<^sup>\<inverse> X V') (\<phi>\<^sub>f V' q')
[PROOF STEP]
obtain W where W: "is_open\<^sub>Y W" "f x \<in> W" "W \<subseteq> V" "W \<subseteq> V'"
    and eq: "\<rho>\<^sub>Y V W q = \<rho>\<^sub>Y V' W q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>is_open\<^sub>Y W; f x \<in> W; W \<subseteq> V; W \<subseteq> V'; \<rho>\<^sub>Y V W q = \<rho>\<^sub>Y V' W q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms stfx.rel_def
[PROOF STATE]
proof (prove)
using this:
stfx.rel (V, q) (V', q')
stfx.rel ?x ?y \<equiv> (fst ?x \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U} \<and> fst ?y \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U}) \<and> (snd ?x \<in> \<O>\<^sub>Y (fst ?x) \<and> snd ?y \<in> \<O>\<^sub>Y (fst ?y)) \<and> (\<exists>W. W \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U} \<and> W \<subseteq> fst ?x \<inter> fst ?y \<and> \<rho>\<^sub>Y (fst ?x) W (snd ?x) = \<rho>\<^sub>Y (fst ?y) W (snd ?y))

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>is_open\<^sub>Y W; f x \<in> W; W \<subseteq> V; W \<subseteq> V'; \<rho>\<^sub>Y V W q = \<rho>\<^sub>Y V' W q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_open\<^sub>Y W
f x \<in> W
W \<subseteq> V
W \<subseteq> V'
\<rho>\<^sub>Y V W q = \<rho>\<^sub>Y V' W q'

goal (1 subgoal):
 1. stx.class_of (f \<^sup>\<inverse> X V) (\<phi>\<^sub>f V q) = stx.class_of (f \<^sup>\<inverse> X V') (\<phi>\<^sub>f V' q')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stx.class_of (f \<^sup>\<inverse> X V) (\<phi>\<^sub>f V q) = stx.class_of (f \<^sup>\<inverse> X V') (\<phi>\<^sub>f V' q')
[PROOF STEP]
proof (rule stx.class_of_eqI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. (f \<^sup>\<inverse> X V, \<phi>\<^sub>f V q) \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
 2. (f \<^sup>\<inverse> X V', \<phi>\<^sub>f V' q') \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
 3. ?W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}
 4. ?W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'
 5. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) ?W (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') ?W (\<phi>\<^sub>f V' q')
[PROOF STEP]
show "(f \<^sup>\<inverse> X V, \<phi>\<^sub>f V q) \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<^sup>\<inverse> X V, \<phi>\<^sub>f V q) \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
[PROOF STEP]
using is_continuous phi_in_O assms stfx.rel_def stx.is_elem
[PROOF STATE]
proof (prove)
using this:
is_open\<^sub>Y ?U \<Longrightarrow> is_open\<^sub>X (f \<^sup>\<inverse> X ?U)
\<lbrakk>is_open\<^sub>Y ?V; ?q \<in> \<O>\<^sub>Y ?V\<rbrakk> \<Longrightarrow> \<phi>\<^sub>f ?V ?q \<in> \<O>\<^sub>X (f \<^sup>\<inverse> X ?V)
stfx.rel (V, q) (V', q')
stfx.rel ?x ?y \<equiv> (fst ?x \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U} \<and> fst ?y \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U}) \<and> (snd ?x \<in> \<O>\<^sub>Y (fst ?x) \<and> snd ?y \<in> \<O>\<^sub>Y (fst ?y)) \<and> (\<exists>W. W \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U} \<and> W \<subseteq> fst ?x \<inter> fst ?y \<and> \<rho>\<^sub>Y (fst ?x) W (snd ?x) = \<rho>\<^sub>Y (fst ?y) W (snd ?y))
x \<in> X

goal (1 subgoal):
 1. (f \<^sup>\<inverse> X V, \<phi>\<^sub>f V q) \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<^sup>\<inverse> X V, \<phi>\<^sub>f V q) \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X

goal (4 subgoals):
 1. (f \<^sup>\<inverse> X V', \<phi>\<^sub>f V' q') \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
 2. ?W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}
 3. ?W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'
 4. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) ?W (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') ?W (\<phi>\<^sub>f V' q')
[PROOF STEP]
show "(f \<^sup>\<inverse> X V', \<phi>\<^sub>f V' q') \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<^sup>\<inverse> X V', \<phi>\<^sub>f V' q') \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
[PROOF STEP]
using is_continuous phi_in_O assms stfx.rel_def stx.is_elem
[PROOF STATE]
proof (prove)
using this:
is_open\<^sub>Y ?U \<Longrightarrow> is_open\<^sub>X (f \<^sup>\<inverse> X ?U)
\<lbrakk>is_open\<^sub>Y ?V; ?q \<in> \<O>\<^sub>Y ?V\<rbrakk> \<Longrightarrow> \<phi>\<^sub>f ?V ?q \<in> \<O>\<^sub>X (f \<^sup>\<inverse> X ?V)
stfx.rel (V, q) (V', q')
stfx.rel ?x ?y \<equiv> (fst ?x \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U} \<and> fst ?y \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U}) \<and> (snd ?x \<in> \<O>\<^sub>Y (fst ?x) \<and> snd ?y \<in> \<O>\<^sub>Y (fst ?y)) \<and> (\<exists>W. W \<in> {U. is_open\<^sub>Y U \<and> f x \<in> U} \<and> W \<subseteq> fst ?x \<inter> fst ?y \<and> \<rho>\<^sub>Y (fst ?x) W (snd ?x) = \<rho>\<^sub>Y (fst ?y) W (snd ?y))
x \<in> X

goal (1 subgoal):
 1. (f \<^sup>\<inverse> X V', \<phi>\<^sub>f V' q') \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<^sup>\<inverse> X V', \<phi>\<^sub>f V' q') \<in> Sigma {U. is_open\<^sub>X U \<and> x \<in> U} \<O>\<^sub>X

goal (3 subgoals):
 1. ?W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}
 2. ?W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'
 3. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) ?W (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') ?W (\<phi>\<^sub>f V' q')
[PROOF STEP]
show "f \<^sup>\<inverse> X W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<^sup>\<inverse> X W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}
[PROOF STEP]
using W is_continuous stx.is_elem
[PROOF STATE]
proof (prove)
using this:
is_open\<^sub>Y W
f x \<in> W
W \<subseteq> V
W \<subseteq> V'
is_open\<^sub>Y ?U \<Longrightarrow> is_open\<^sub>X (f \<^sup>\<inverse> X ?U)
x \<in> X

goal (1 subgoal):
 1. f \<^sup>\<inverse> X W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<^sup>\<inverse> X W \<in> {U. is_open\<^sub>X U \<and> x \<in> U}

goal (2 subgoals):
 1. f \<^sup>\<inverse> X W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'
 2. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
show "f \<^sup>\<inverse> X W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<^sup>\<inverse> X W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
is_open\<^sub>Y W
f x \<in> W
W \<subseteq> V
W \<subseteq> V'

goal (1 subgoal):
 1. f \<^sup>\<inverse> X W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<^sup>\<inverse> X W \<subseteq> f \<^sup>\<inverse> X V \<inter> f \<^sup>\<inverse> X V'

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
interpret Y: morphism_sheaves_of_rings Y is_open\<^sub>Y \<O>\<^sub>Y \<rho>\<^sub>Y
     d add_str\<^sub>Y mult_str\<^sub>Y zero_str\<^sub>Y one_str\<^sub>Y
     local.im_sheaf im_sheaf_morphisms b
      add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<phi>\<^sub>f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_sheaves_of_rings Y is_open\<^sub>Y \<O>\<^sub>Y \<rho>\<^sub>Y d add_str\<^sub>Y mult_str\<^sub>Y zero_str\<^sub>Y one_str\<^sub>Y local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<phi>\<^sub>f
[PROOF STEP]
by (rule is_morphism_of_sheaves)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
have "\<rho>\<^sub>X (f\<^sup>\<inverse> X V) (f\<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V W q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V W q)
[PROOF STEP]
using assms Y.comm_diagrams W
[PROOF STATE]
proof (prove)
using this:
stfx.rel (V, q) (V', q')
\<lbrakk>is_open\<^sub>Y ?U; is_open\<^sub>Y ?V; ?V \<subseteq> ?U; ?x \<in> \<O>\<^sub>Y ?U\<rbrakk> \<Longrightarrow> (im_sheaf_morphisms ?U ?V \<circ> \<phi>\<^sub>f ?U) ?x = (\<phi>\<^sub>f ?V \<circ> \<rho>\<^sub>Y ?U ?V) ?x
is_open\<^sub>Y W
f x \<in> W
W \<subseteq> V
W \<subseteq> V'

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V W q)
[PROOF STEP]
by (simp add: stfx.rel_def im_sheaf_morphisms_def o_def)
[PROOF STATE]
proof (state)
this:
\<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V W q)

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V W q)

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
have "\<dots> = \<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sub>f W (\<rho>\<^sub>Y V W q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q')
[PROOF STEP]
by (simp add: eq)
[PROOF STATE]
proof (state)
this:
\<phi>\<^sub>f W (\<rho>\<^sub>Y V W q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q')

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi>\<^sub>f W (\<rho>\<^sub>Y V W q) = \<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q')

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
have "\<dots> = \<rho>\<^sub>X (f\<^sup>\<inverse> X V') (f\<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q') = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
using assms Y.comm_diagrams W
[PROOF STATE]
proof (prove)
using this:
stfx.rel (V, q) (V', q')
\<lbrakk>is_open\<^sub>Y ?U; is_open\<^sub>Y ?V; ?V \<subseteq> ?U; ?x \<in> \<O>\<^sub>Y ?U\<rbrakk> \<Longrightarrow> (im_sheaf_morphisms ?U ?V \<circ> \<phi>\<^sub>f ?U) ?x = (\<phi>\<^sub>f ?V \<circ> \<rho>\<^sub>Y ?U ?V) ?x
is_open\<^sub>Y W
f x \<in> W
W \<subseteq> V
W \<subseteq> V'

goal (1 subgoal):
 1. \<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q') = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
by (simp add: stfx.rel_def im_sheaf_morphisms_def o_def)
[PROOF STATE]
proof (state)
this:
\<phi>\<^sub>f W (\<rho>\<^sub>Y V' W q') = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
show "\<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')"
[PROOF STATE]
proof (prove)
using this:
\<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')

goal (1 subgoal):
 1. \<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<rho>\<^sub>X (f \<^sup>\<inverse> X V) (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V q) = \<rho>\<^sub>X (f \<^sup>\<inverse> X V') (f \<^sup>\<inverse> X W) (\<phi>\<^sub>f V' q')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stx.class_of (f \<^sup>\<inverse> X V) (\<phi>\<^sub>f V q) = stx.class_of (f \<^sup>\<inverse> X V') (\<phi>\<^sub>f V' q')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma induced_morphism_eq:
  assumes "C \<in> stfx.carrier_stalk"
  obtains V q where "(V,q) \<in> C" "induced_morphism C = stx.class_of (f\<^sup>\<inverse> X V) (\<phi>\<^sub>f V q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V q. \<lbrakk>(V, q) \<in> C; induced_morphism C = stx.class_of (f \<^sup>\<inverse> X V) (\<phi>\<^sub>f V q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, lifting) assms induced_morphism_def prod.exhaust_sel restrict_apply
            stfx.carrier_stalk_def stfx.neighborhoods_eq stfx.rel_carrier_Eps_in(1))


[STATEMENT]
lemma induced_morphism_eval:
  assumes "C \<in> stfx.carrier_stalk" and "r \<in> C"
  shows "induced_morphism C = stx.class_of (f\<^sup>\<inverse> X (fst r)) (\<phi>\<^sub>f (fst r) (snd r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. induced_morphism C = stx.class_of (f \<^sup>\<inverse> X (fst r)) (\<phi>\<^sub>f (fst r) (snd r))
[PROOF STEP]
by (smt (verit, best) assms induced_morphism_eq induced_morphism_is_well_defined
          prod.exhaust_sel stfx.carrier_direct_limE stfx.carrier_stalk_def stfx.neighborhoods_eq stfx.rel_I1)


[STATEMENT]
lemma (in sheaf_of_rings) induced_morphism_with_id_is_id:
  assumes "x \<in> S"
  shows "\<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
       = (\<lambda>C\<in>(stalk.carrier_stalk is_open \<FF> \<rho> x). C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub> = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub> = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
interpret im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open "identity S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open (identity S)
[PROOF STEP]
by (metis homeomorphism.axioms(3) id_is_homeomorphism im_sheaf_def inverse_map_identity
        sheaf_of_rings_axioms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub> = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
interpret codom: ringed_space S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ringed_space S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
[PROOF STEP]
by (meson im_sheaf.axioms(1) im_sheaf_axioms ringed_space_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub> = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
interpret ind_mor_btw_stalks S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S
       is_open \<FF> \<rho> b add_str mult_str zero_str one_str "identity S" "\<lambda>U. identity (\<FF> U)" x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_mor_btw_stalks S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U)) x
[PROOF STEP]
apply intro_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 2. ind_mor_btw_stalks_axioms S x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have "ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (local.im_sheaf U) (add_im_sheaf U)
          (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U)" if "is_open U" for U
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U)
[PROOF STEP]
by (smt (verit, best) id_is_mor_pr_rngs im_sheaf.add_im_sheaf_def im_sheaf.im_sheaf_def
            im_sheaf.mult_im_sheaf_def im_sheaf_axioms local.topological_space_axioms
            morphism_presheaves_of_rings.is_ring_morphism one_im_sheaf_def that
            topological_space.open_preimage_identity zero_im_sheaf_def)
[PROOF STATE]
proof (state)
this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (local.im_sheaf ?U1) (add_im_sheaf ?U1) (mult_im_sheaf ?U1) (zero_im_sheaf ?U1) (one_im_sheaf ?U1)

goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (local.im_sheaf ?U1) (add_im_sheaf ?U1) (mult_im_sheaf ?U1) (zero_im_sheaf ?U1) (one_im_sheaf ?U1)

goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have "\<forall>U V. is_open U \<longrightarrow>
           is_open V \<longrightarrow>
           V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)
[PROOF STEP]
by (smt (verit, best) comp_apply im_sheaf_morphisms_def is_map_from_is_homomorphism
            local.im_sheaf_def map.map_closed open_preimage_identity restrict_apply')
[PROOF STATE]
proof (state)
this:
\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)

goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (local.im_sheaf ?U1) (add_im_sheaf ?U1) (mult_im_sheaf ?U1) (zero_im_sheaf ?U1) (one_im_sheaf ?U1)
\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)
[PROOF STEP]
have "morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str
          zero_str one_str local.im_sheaf im_sheaf_morphisms add_im_sheaf mult_im_sheaf
          zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
using this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (local.im_sheaf ?U1) (add_im_sheaf ?U1) (mult_im_sheaf ?U1) (zero_im_sheaf ?U1) (one_im_sheaf ?U1)
\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)

goal (1 subgoal):
 1. morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
using this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (local.im_sheaf ?U1) (add_im_sheaf ?U1) (mult_im_sheaf ?U1) (zero_im_sheaf ?U1) (one_im_sheaf ?U1)
\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x)

goal (1 subgoal):
 1. (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U)) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_ringed_spaces_axioms_def
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. morphism_sheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by intro_locales
[PROOF STATE]
proof (state)
this:
morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_mor_btw_stalks_axioms S x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_mor_btw_stalks_axioms S x
[PROOF STEP]
by (meson assms ind_mor_btw_stalks_axioms.intro)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. induced_morphism = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
have "(let r = SOME r. r \<in> C
        in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r))
            (identity (\<FF> (fst r)) (snd r))) = C"
    (is "?L= _")
    if "C\<in>stalk.carrier_stalk is_open \<FF> \<rho> x" for C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
interpret stk:stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
                      "neighborhoods x" x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (neighborhoods x) x
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>U. U \<in> neighborhoods x \<Longrightarrow> is_open U
 2. \<And>U V. \<lbrakk>U \<in> neighborhoods x; V \<in> neighborhoods x\<rbrakk> \<Longrightarrow> \<exists>W\<in>neighborhoods x. W \<subseteq> U \<inter> V
 3. x \<in> S
 4. neighborhoods x = {U. is_open U \<and> x \<in> U}
[PROOF STEP]
using is_elem neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
x \<in> S
neighborhoods ?x \<equiv> {U. is_open U \<and> ?x \<in> U}

goal (4 subgoals):
 1. \<And>U. U \<in> neighborhoods x \<Longrightarrow> is_open U
 2. \<And>U V. \<lbrakk>U \<in> neighborhoods x; V \<in> neighborhoods x\<rbrakk> \<Longrightarrow> \<exists>W\<in>neighborhoods x. W \<subseteq> U \<inter> V
 3. x \<in> S
 4. neighborhoods x = {U. is_open U \<and> x \<in> U}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
define r where "r=(SOME x. x \<in> C)"
[PROOF STATE]
proof (state)
this:
r = (SOME x. x \<in> C)

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
have r:"r \<in> C" "r \<in> Sigma (neighborhoods x) \<FF>" and "C = stk.class_of (fst r) (snd r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> C &&& r \<in> Sigma (neighborhoods x) \<FF>) &&& C = stk.class_of (fst r) (snd r)
[PROOF STEP]
using stk.rel_carrier_Eps_in[OF that[unfolded stk.carrier_stalk_def]]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> C) \<in> C
(SOME x. x \<in> C) \<in> Sigma (neighborhoods x) \<FF>
C = stk.class_of (fst (SOME x. x \<in> C)) (snd (SOME x. x \<in> C))

goal (1 subgoal):
 1. (r \<in> C &&& r \<in> Sigma (neighborhoods x) \<FF>) &&& C = stk.class_of (fst r) (snd r)
[PROOF STEP]
unfolding r_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> C) \<in> C
(SOME x. x \<in> C) \<in> Sigma (neighborhoods x) \<FF>
C = stk.class_of (fst (SOME x. x \<in> C)) (snd (SOME x. x \<in> C))

goal (1 subgoal):
 1. ((SOME x. x \<in> C) \<in> C &&& (SOME x. x \<in> C) \<in> Sigma (neighborhoods x) \<FF>) &&& C = stk.class_of (fst (SOME x. x \<in> C)) (snd (SOME x. x \<in> C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> C
r \<in> Sigma (neighborhoods x) \<FF>
C = stk.class_of (fst r) (snd r)

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
have "?L = stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))
[PROOF STEP]
unfolding r_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk.class_of (identity S \<^sup>\<inverse> S (fst (SOME r. r \<in> C))) (identity (\<FF> (fst (SOME r. r \<in> C))) (snd (SOME r. r \<in> C))) = stk.class_of (identity S \<^sup>\<inverse> S (fst (SOME x. x \<in> C))) (identity (\<FF> (fst (SOME x. x \<in> C))) (snd (SOME x. x \<in> C)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
have "... =  stk.class_of (fst r) (snd r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r)) = stk.class_of (fst r) (snd r)
[PROOF STEP]
by (metis open_preimage_identity r(1) restrict_apply stk.carrier_direct_limE
          stk.carrier_stalk_def stk.rel_I1 stk.rel_def stk.subset_of_opens that)
[PROOF STATE]
proof (state)
this:
stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r)) = stk.class_of (fst r) (snd r)

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r)) = stk.class_of (fst r) (snd r)

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
have "... = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk.class_of (fst r) (snd r) = C
[PROOF STEP]
using \<open>C = stk.class_of (fst r) (snd r)\<close>
[PROOF STATE]
proof (prove)
using this:
C = stk.class_of (fst r) (snd r)

goal (1 subgoal):
 1. stk.class_of (fst r) (snd r) = C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stk.class_of (fst r) (snd r) = C

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C

goal (1 subgoal):
 1. (let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(let r = SOME r. r \<in> C in stk.class_of (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?C1 \<in> stalk.carrier_stalk is_open \<FF> \<rho> x \<Longrightarrow> (let r = SOME r. r \<in> ?C1 in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = ?C1

goal (1 subgoal):
 1. induced_morphism = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?C1 \<in> stalk.carrier_stalk is_open \<FF> \<rho> x \<Longrightarrow> (let r = SOME r. r \<in> ?C1 in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = ?C1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?C1 \<in> stalk.carrier_stalk is_open \<FF> \<rho> x \<Longrightarrow> (let r = SOME r. r \<in> ?C1 in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = ?C1

goal (1 subgoal):
 1. induced_morphism = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
unfolding induced_morphism_def
[PROOF STATE]
proof (prove)
using this:
?C1 \<in> stalk.carrier_stalk is_open \<FF> \<rho> x \<Longrightarrow> (let r = SOME r. r \<in> ?C1 in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = ?C1

goal (1 subgoal):
 1. (\<lambda>C\<in>stalk.carrier_stalk is_open \<FF> \<rho> (identity S x). let r = SOME r. r \<in> C in direct_lim.class_of \<FF> \<rho> {U. is_open U \<and> x \<in> U} (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
using is_elem neighborhoods_def
[PROOF STATE]
proof (prove)
using this:
?C1 \<in> stalk.carrier_stalk is_open \<FF> \<rho> x \<Longrightarrow> (let r = SOME r. r \<in> ?C1 in direct_lim.class_of \<FF> \<rho> (neighborhoods x) (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = ?C1
x \<in> S
neighborhoods ?x \<equiv> {U. is_open U \<and> ?x \<in> U}

goal (1 subgoal):
 1. (\<lambda>C\<in>stalk.carrier_stalk is_open \<FF> \<rho> (identity S x). let r = SOME r. r \<in> C in direct_lim.class_of \<FF> \<rho> {U. is_open U \<and> x \<in> U} (identity S \<^sup>\<inverse> S (fst r)) (identity (\<FF> (fst r)) (snd r))) = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
induced_morphism = identity (stalk.carrier_stalk is_open \<FF> \<rho> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in locally_ringed_space) induced_morphism_with_id_is_local:
  assumes "x \<in> S" and V: "x \<in> V" "is_open V"
  shows "ind_mor_btw_stalks.is_local
S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str
(identity S) x V (\<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
have [simp]: "(identity S)\<^sup>\<inverse> S V = V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. identity S \<^sup>\<inverse> S V = V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> S
x \<in> V
is_open V

goal (1 subgoal):
 1. identity S \<^sup>\<inverse> S V = V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
identity S \<^sup>\<inverse> S V = V

goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
interpret stfx: stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
                    "{U. is_open U \<and> (identity S x) \<in> U}" "identity S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str {U. is_open U \<and> identity S x \<in> U} (identity S x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>U. U \<in> {U. is_open U \<and> identity S x \<in> U} \<Longrightarrow> is_open U
 2. \<And>U V. \<lbrakk>U \<in> {U. is_open U \<and> identity S x \<in> U}; V \<in> {U. is_open U \<and> identity S x \<in> U}\<rbrakk> \<Longrightarrow> \<exists>W\<in>{U. is_open U \<and> identity S x \<in> U}. W \<subseteq> U \<inter> V
 3. identity S x \<in> S
 4. {U. is_open U \<and> identity S x \<in> U} = {U. is_open U \<and> identity S x \<in> U}
[PROOF STEP]
qed (use assms in auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
have "local_ring stfx.carrier_stalk stfx.add_stalk stfx.mult_stalk (stfx.zero_stalk V) (stfx.one_stalk V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring stfx.carrier_stalk stfx.add_stalk stfx.mult_stalk (stfx.zero_stalk V) (stfx.one_stalk V)
[PROOF STEP]
by (smt (verit, best) assms restrict_apply' stalks_are_local stfx.is_local_def stfx.neighborhoods_eq)
[PROOF STATE]
proof (state)
this:
local_ring stfx.carrier_stalk stfx.add_stalk stfx.mult_stalk (stfx.zero_stalk V) (stfx.one_stalk V)

goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
interpret stx: stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str "{U. is_open U \<and> x \<in> U}" "x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str {U. is_open U \<and> x \<in> U} x
[PROOF STEP]
using \<open>x \<in> S\<close> stfx.stalk_axioms
[PROOF STATE]
proof (prove)
using this:
x \<in> S
stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str {U. is_open U \<and> identity S x \<in> U} (identity S x)

goal (1 subgoal):
 1. stalk S is_open \<FF> \<rho> b add_str mult_str zero_str one_str {U. is_open U \<and> x \<in> U} x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
interpret local_ring stx.carrier_stalk stx.add_stalk stx.mult_stalk
              "stx.zero_stalk ((identity S)\<^sup>\<inverse> S V)" "stx.one_stalk ((identity S)\<^sup>\<inverse> S V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_ring stx.carrier_stalk stx.add_stalk stx.mult_stalk (stx.zero_stalk (identity S \<^sup>\<inverse> S V)) (stx.one_stalk (identity S \<^sup>\<inverse> S V))
[PROOF STEP]
using V stalks_are_local stx.is_local_def stx.neighborhoods_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> V
is_open V
\<lbrakk>?x \<in> ?U; is_open ?U\<rbrakk> \<Longrightarrow> stalk.is_local is_open \<FF> \<rho> add_str mult_str zero_str one_str (neighborhoods ?x) ?x ?U
stx.is_local ?U \<equiv> local_ring stx.carrier_stalk stx.add_stalk stx.mult_stalk (stx.zero_stalk ?U) (stx.one_stalk ?U)
neighborhoods x = {U. is_open U \<and> x \<in> U}

goal (1 subgoal):
 1. local_ring stx.carrier_stalk stx.add_stalk stx.mult_stalk (stx.zero_stalk (identity S \<^sup>\<inverse> S V)) (stx.one_stalk (identity S \<^sup>\<inverse> S V))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
interpret imS: im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open "identity S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open (identity S)
[PROOF STEP]
by (metis homeomorphism.axioms(3) id_is_homeomorphism im_sheaf_def inverse_map_identity
        sheaf_of_rings_axioms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
have rh: "\<And>U. is_open U \<Longrightarrow>
             ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (imS.im_sheaf U)
              (imS.add_im_sheaf U) (imS.mult_im_sheaf U) (imS.zero_im_sheaf U) (imS.one_im_sheaf U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (imS.im_sheaf U) (imS.add_im_sheaf U) (imS.mult_im_sheaf U) (imS.zero_im_sheaf U) (imS.one_im_sheaf U)
[PROOF STEP]
unfolding imS.add_im_sheaf_def imS.mult_im_sheaf_def imS.one_im_sheaf_def
              imS.zero_im_sheaf_def imS.im_sheaf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> (identity S \<^sup>\<inverse> S U)) +\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<cdot>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<zero>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<one>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub>
[PROOF STEP]
using id_is_mor_pr_rngs morphism_presheaves_of_rings.is_ring_morphism
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
\<lbrakk>morphism_presheaves_of_rings ?X ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?\<FF>' ?\<rho>' ?b' ?add_str' ?mult_str' ?zero_str' ?one_str' ?fam_morphisms; ?is_open ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (?fam_morphisms ?U) (?\<FF> ?U) (?add_str ?U) (?mult_str ?U) (?zero_str ?U) (?one_str ?U) (?\<FF>' ?U) (?add_str' ?U) (?mult_str' ?U) (?zero_str' ?U) (?one_str' ?U)

goal (1 subgoal):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> (identity S \<^sup>\<inverse> S U)) +\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<cdot>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<zero>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub> \<one>\<^bsub>identity S \<^sup>\<inverse> S U\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (imS.im_sheaf ?U1) (imS.add_im_sheaf ?U1) (imS.mult_im_sheaf ?U1) (imS.zero_im_sheaf ?U1) (imS.one_im_sheaf ?U1)

goal (1 subgoal):
 1. ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) x V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub>
[PROOF STEP]
interpret ind_mor_btw_stalks S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S
    is_open \<FF> \<rho> b add_str mult_str zero_str one_str "identity S" "\<lambda>U. identity (\<FF> U)" x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_mor_btw_stalks S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U)) x
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 2. ind_mor_btw_stalks_axioms S x
[PROOF STEP]
show "morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str
              S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_ringed_spaces_axioms_def morphism_sheaves_of_rings_def
        morphism_presheaves_of_rings_def morphism_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<and> presheaf_of_rings S is_open imS.im_sheaf imS.im_sheaf_morphisms b imS.add_im_sheaf imS.mult_im_sheaf imS.zero_im_sheaf imS.one_im_sheaf \<and> (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (imS.im_sheaf U) (imS.add_im_sheaf U) (imS.mult_im_sheaf U) (imS.zero_im_sheaf U) (imS.one_im_sheaf U)) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (imS.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x))
[PROOF STEP]
using rh
[PROOF STATE]
proof (prove)
using this:
is_open ?U1 \<Longrightarrow> ring_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<cdot>\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> \<one>\<^bsub>?U1\<^esub> (imS.im_sheaf ?U1) (imS.add_im_sheaf ?U1) (imS.mult_im_sheaf ?U1) (imS.zero_im_sheaf ?U1) (imS.one_im_sheaf ?U1)

goal (1 subgoal):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<and> presheaf_of_rings S is_open imS.im_sheaf imS.im_sheaf_morphisms b imS.add_im_sheaf imS.mult_im_sheaf imS.zero_im_sheaf imS.one_im_sheaf \<and> (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (imS.im_sheaf U) (imS.add_im_sheaf U) (imS.mult_im_sheaf U) (imS.zero_im_sheaf U) (imS.one_im_sheaf U)) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (imS.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x))
[PROOF STEP]
by (auto simp add: presheaf_of_rings_axioms imS.presheaf_of_rings_axioms
             map.map_closed [OF is_map_from_is_homomorphism] imS.im_sheaf_morphisms_def)
[PROOF STATE]
proof (state)
this:
morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. ind_mor_btw_stalks_axioms S x
[PROOF STEP]
show "ind_mor_btw_stalks_axioms S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_mor_btw_stalks_axioms S x
[PROOF STEP]
by (simp add: assms(1) ind_mor_btw_stalks_axioms_def)
[PROOF STATE]
proof (state)
this:
ind_mor_btw_stalks_axioms S x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_local V induced_morphism
[PROOF STEP]
have "\<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) x\<^esub> = identity stx.carrier_stalk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. induced_morphism = identity stx.carrier_stalk
[PROOF STEP]
using induced_morphism_with_id_is_id stx.is_elem
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) ?x\<^esub> = identity (stalk.carrier_stalk is_open \<FF> \<rho> ?x)
x \<in> S

goal (1 subgoal):
 1. induced_morphism = identity stx.carrier_stalk
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
induced_morphism = identity stx.carrier_stalk

goal (1 subgoal):
 1. is_local V induced_morphism
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
induced_morphism = identity stx.carrier_stalk
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
induced_morphism = identity stx.carrier_stalk

goal (1 subgoal):
 1. is_local V induced_morphism
[PROOF STEP]
using id_is_local_ring_morphism is_local_def local_ring_axioms stx.is_elem
[PROOF STATE]
proof (prove)
using this:
induced_morphism = identity stx.carrier_stalk
local_ring ?A ?add ?mult ?zero ?one \<Longrightarrow> local_ring_morphism (identity ?A) ?A ?add ?mult ?zero ?one ?A ?add ?mult ?zero ?one
is_local ?V ?\<phi> \<equiv> local_ring_morphism ?\<phi> stfx.carrier_stalk stfx.add_stalk stfx.mult_stalk (stfx.zero_stalk ?V) (stfx.one_stalk ?V) stx.carrier_stalk stx.add_stalk stx.mult_stalk (stx.zero_stalk (identity S \<^sup>\<inverse> S ?V)) (stx.one_stalk (identity S \<^sup>\<inverse> S ?V))
local_ring stx.carrier_stalk stx.add_stalk stx.mult_stalk (stx.zero_stalk (identity S \<^sup>\<inverse> S V)) (stx.one_stalk (identity S \<^sup>\<inverse> S V))
x \<in> S

goal (1 subgoal):
 1. is_local V induced_morphism
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_local V induced_morphism

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in locally_ringed_space) id_to_mor_locally_ringed_spaces:
  shows "morphism_locally_ringed_spaces
            S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_locally_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Set_Theory.map (identity S) S S
 2. continuous_map_axioms S is_open is_open (identity S)
 3. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 4. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
interpret idim: im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open "identity S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open (identity S)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. identity S \<in> S \<rightarrow>\<^sub>E S
 2. \<And>U. is_open U \<Longrightarrow> is_open (identity S \<^sup>\<inverse> S U)
[PROOF STEP]
fix U
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. identity S \<in> S \<rightarrow>\<^sub>E S
 2. \<And>U. is_open U \<Longrightarrow> is_open (identity S \<^sup>\<inverse> S U)
[PROOF STEP]
assume "is_open U"
[PROOF STATE]
proof (state)
this:
is_open U

goal (2 subgoals):
 1. identity S \<in> S \<rightarrow>\<^sub>E S
 2. \<And>U. is_open U \<Longrightarrow> is_open (identity S \<^sup>\<inverse> S U)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open U
[PROOF STEP]
show "is_open (identity S \<^sup>\<inverse> S U)"
[PROOF STATE]
proof (prove)
using this:
is_open U

goal (1 subgoal):
 1. is_open (identity S \<^sup>\<inverse> S U)
[PROOF STEP]
by (simp add: open_inter preimage_identity_self)
[PROOF STATE]
proof (state)
this:
is_open (identity S \<^sup>\<inverse> S U)

goal (1 subgoal):
 1. identity S \<in> S \<rightarrow>\<^sub>E S
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Set_Theory.map (identity S) S S
 2. continuous_map_axioms S is_open is_open (identity S)
 3. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 4. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "Set_Theory.map (identity S) S S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (identity S) S S
[PROOF STEP]
by (simp add: Set_Theory.map_def)
[PROOF STATE]
proof (state)
this:
Set_Theory.map (identity S) S S

goal (3 subgoals):
 1. continuous_map_axioms S is_open is_open (identity S)
 2. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 3. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "continuous_map_axioms S is_open is_open (identity S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_map_axioms S is_open is_open (identity S)
[PROOF STEP]
by (simp add: continuous_map_axioms_def open_inter preimage_identity_self)
[PROOF STATE]
proof (state)
this:
continuous_map_axioms S is_open is_open (identity S)

goal (2 subgoals):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 2. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have gh: "group_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub>
          \<zero>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.zero_im_sheaf U)"
    if "is_open U" for U
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.zero_im_sheaf U)
[PROOF STEP]
using that id_is_mor_pr_rngs idim.add_im_sheaf_def idim.im_sheaf_def idim.zero_im_sheaf_def morphism_presheaves_of_rings.is_ring_morphism ring_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
is_open U
morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
idim.add_im_sheaf \<equiv> \<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
idim.im_sheaf ?V \<equiv> \<FF> (identity S \<^sup>\<inverse> S ?V)
idim.zero_im_sheaf \<equiv> \<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
\<lbrakk>morphism_presheaves_of_rings ?X ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?\<FF>' ?\<rho>' ?b' ?add_str' ?mult_str' ?zero_str' ?one_str' ?fam_morphisms; ?is_open ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (?fam_morphisms ?U) (?\<FF> ?U) (?add_str ?U) (?mult_str ?U) (?zero_str ?U) (?one_str ?U) (?\<FF>' ?U) (?add_str' ?U) (?mult_str' ?U) (?zero_str' ?U) (?one_str' ?U)
ring_homomorphism ?\<eta> ?R ?addition ?multiplication ?zero ?unit ?R' ?addition' ?multiplication' ?zero' ?unit' \<equiv> (Set_Theory.map ?\<eta> ?R ?R' \<and> ring ?R ?addition ?multiplication ?zero ?unit) \<and> ring ?R' ?addition' ?multiplication' ?zero' ?unit' \<and> group_homomorphism ?\<eta> ?R ?addition ?zero ?R' ?addition' ?zero' \<and> monoid_homomorphism ?\<eta> ?R ?multiplication ?unit ?R' ?multiplication' ?unit'

goal (1 subgoal):
 1. group_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.zero_im_sheaf U)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_open ?U1 \<Longrightarrow> group_homomorphism (identity (\<FF> ?U1)) (\<FF> ?U1) +\<^bsub>?U1\<^esub> \<zero>\<^bsub>?U1\<^esub> (idim.im_sheaf ?U1) (idim.add_im_sheaf ?U1) (idim.zero_im_sheaf ?U1)

goal (2 subgoals):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 2. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
have "morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str idim.im_sheaf idim.im_sheaf_morphisms idim.add_im_sheaf idim.mult_im_sheaf idim.zero_im_sheaf idim.one_im_sheaf (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str idim.im_sheaf idim.im_sheaf_morphisms idim.add_im_sheaf idim.mult_im_sheaf idim.zero_im_sheaf idim.one_im_sheaf (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> \<FF> U \<longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x))
[PROOF STEP]
proof (intro conjI strip)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
fix U
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
assume "is_open U"
[PROOF STATE]
proof (state)
this:
is_open U

goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open U
[PROOF STEP]
show "ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)"
[PROOF STATE]
proof (prove)
using this:
is_open U

goal (1 subgoal):
 1. ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)
[PROOF STEP]
using id_is_mor_pr_rngs idim.add_im_sheaf_def idim.im_sheaf_def idim.mult_im_sheaf_def idim.one_im_sheaf_def idim.zero_im_sheaf_def morphism_presheaves_of_rings.is_ring_morphism
[PROOF STATE]
proof (prove)
using this:
is_open U
morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
idim.add_im_sheaf \<equiv> \<lambda>V. +\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
idim.im_sheaf ?V \<equiv> \<FF> (identity S \<^sup>\<inverse> S ?V)
idim.mult_im_sheaf \<equiv> \<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
idim.one_im_sheaf \<equiv> \<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
idim.zero_im_sheaf \<equiv> \<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
\<lbrakk>morphism_presheaves_of_rings ?X ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?\<FF>' ?\<rho>' ?b' ?add_str' ?mult_str' ?zero_str' ?one_str' ?fam_morphisms; ?is_open ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (?fam_morphisms ?U) (?\<FF> ?U) (?add_str ?U) (?mult_str ?U) (?zero_str ?U) (?one_str ?U) (?\<FF>' ?U) (?add_str' ?U) (?mult_str' ?U) (?zero_str' ?U) (?one_str' ?U)

goal (1 subgoal):
 1. ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (idim.im_sheaf U) (idim.add_im_sheaf U) (idim.mult_im_sheaf U) (idim.zero_im_sheaf U) (idim.one_im_sheaf U)

goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
fix V x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
assume "is_open V" and "V \<subseteq> U" and "x \<in> \<FF> U"
[PROOF STATE]
proof (state)
this:
is_open V
V \<subseteq> U
x \<in> \<FF> U

goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> \<FF> U\<rbrakk> \<Longrightarrow> (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open V
V \<subseteq> U
x \<in> \<FF> U
[PROOF STEP]
show "(idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x"
[PROOF STATE]
proof (prove)
using this:
is_open V
V \<subseteq> U
x \<in> \<FF> U

goal (1 subgoal):
 1. (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
using \<open>is_open U\<close>
[PROOF STATE]
proof (prove)
using this:
is_open V
V \<subseteq> U
x \<in> \<FF> U
is_open U

goal (1 subgoal):
 1. (idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x
[PROOF STEP]
by (simp add: idim.im_sheaf_morphisms_def map.map_closed [OF is_map_from_is_homomorphism])
[PROOF STATE]
proof (state)
this:
(idim.im_sheaf_morphisms U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> \<rho> U V) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str idim.im_sheaf idim.im_sheaf_morphisms idim.add_im_sheaf idim.mult_im_sheaf idim.zero_im_sheaf idim.one_im_sheaf (\<lambda>U. identity (\<FF> U))

goal (2 subgoals):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 2. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str idim.im_sheaf idim.im_sheaf_morphisms idim.add_im_sheaf idim.mult_im_sheaf idim.zero_im_sheaf idim.one_im_sheaf (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show mrs: "morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str
                      S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings_axioms is_open \<FF> \<rho> add_str mult_str zero_str one_str idim.im_sheaf idim.im_sheaf_morphisms idim.add_im_sheaf idim.mult_im_sheaf idim.zero_im_sheaf idim.one_im_sheaf (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by (simp add: idim.im_sheaf_is_presheaf morphism_presheaves_of_rings_def morphism_ringed_spaces_axioms.intro morphism_sheaves_of_rings.intro presheaf_of_rings_axioms)
[PROOF STATE]
proof (state)
this:
morphism_ringed_spaces_axioms S \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str
                     is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
using induced_morphism_with_id_is_local
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> S; ?x \<in> ?V; is_open ?V\<rbrakk> \<Longrightarrow> ind_mor_btw_stalks.is_local S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) ?x ?V \<phi>\<^bsub>S is_open \<FF> \<rho> is_open \<FF> \<rho> (identity S) (\<lambda>U. identity (\<FF> U)) ?x\<^esub>

goal (1 subgoal):
 1. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by (simp add: morphism_locally_ringed_spaces_axioms_def)
[PROOF STATE]
proof (state)
this:
morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in locally_ringed_space) id_to_iso_locally_ringed_spaces:
  shows "iso_locally_ringed_spaces
            S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iso_locally_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iso_locally_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
interpret morphism_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
    S is_open \<FF> \<rho> b add_str mult_str zero_str one_str "identity S" "\<lambda>U. identity (\<FF> U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by (metis id_to_mor_locally_ringed_spaces morphism_locally_ringed_spaces_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iso_locally_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iso_locally_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
proof intro_locales
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
 2. iso_locally_ringed_spaces_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by (metis id_to_mor_locally_ringed_spaces morphism_locally_ringed_spaces_def)
[PROOF STATE]
proof (state)
this:
morphism_locally_ringed_spaces_axioms S is_open \<FF> \<rho> add_str mult_str zero_str one_str is_open \<FF> \<rho> add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. iso_locally_ringed_spaces_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "iso_locally_ringed_spaces_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iso_locally_ringed_spaces_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding iso_locally_ringed_spaces_axioms_def iso_sheaves_of_rings_def iso_presheaves_of_rings_def iso_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism S is_open S is_open (identity S) \<and> morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U)) \<and> (\<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x)))
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. homeomorphism S is_open S is_open (identity S)
 2. morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))
 3. \<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))
[PROOF STEP]
show "homeomorphism S is_open S is_open (identity S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homeomorphism S is_open S is_open (identity S)
[PROOF STEP]
using id_is_homeomorphism
[PROOF STATE]
proof (prove)
using this:
homeomorphism S is_open S is_open (identity S)

goal (1 subgoal):
 1. homeomorphism S is_open S is_open (identity S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
homeomorphism S is_open S is_open (identity S)

goal (2 subgoals):
 1. morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))
 2. \<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))
[PROOF STEP]
show mor:"morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
            local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
            (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
by (simp add: is_morphism_of_sheaves morphism_sheaves_of_rings.axioms)
[PROOF STATE]
proof (state)
this:
morphism_presheaves_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. \<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))
[PROOF STEP]
have "morphism_presheaves_of_rings S is_open
               local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
               \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
unfolding morphism_presheaves_of_rings_def morphism_presheaves_of_rings_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<and> presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str \<and> (\<forall>U. is_open U \<longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>) \<and> (\<forall>U V. is_open U \<longrightarrow> is_open V \<longrightarrow> V \<subseteq> U \<longrightarrow> (\<forall>x. x \<in> local.im_sheaf U \<longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x))
[PROOF STEP]
proof (intro conjI strip)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
 2. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 3. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 4. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
[PROOF STEP]
using im_sheaf_is_presheaf
[PROOF STATE]
proof (prove)
using this:
presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf

goal (1 subgoal):
 1. presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
presheaf_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf

goal (3 subgoals):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
 2. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 3. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
show "presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str
[PROOF STEP]
by (metis mor morphism_presheaves_of_rings_def)
[PROOF STATE]
proof (state)
this:
presheaf_of_rings S is_open \<FF> \<rho> b add_str mult_str zero_str one_str

goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
fix U
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
assume "is_open U"
[PROOF STATE]
proof (state)
this:
is_open U

goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open U
[PROOF STEP]
have "ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
using this:
is_open U

goal (1 subgoal):
 1. ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by (smt (verit, best) im_sheaf.add_im_sheaf_def im_sheaf.mult_im_sheaf_def im_sheaf_axioms local.im_sheaf_def mor morphism_presheaves_of_rings.is_ring_morphism one_im_sheaf_def open_preimage_identity zero_im_sheaf_def)
[PROOF STATE]
proof (state)
this:
ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (2 subgoals):
 1. \<And>U. is_open U \<Longrightarrow> ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
 2. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
show "ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
using this:
ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
using \<open>is_open U \<close> im_sheaf.add_im_sheaf_def im_sheaf_axioms local.im_sheaf_def mult_im_sheaf_def one_im_sheaf_def zero_im_sheaf_def
[PROOF STATE]
proof (prove)
using this:
ring_homomorphism (identity (\<FF> U)) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
is_open U
Comm_Ring.im_sheaf ?S ?is_open ?\<FF> ?\<rho> ?b ?add_str ?mult_str ?zero_str ?one_str ?S' ?is_open' ?f \<Longrightarrow> im_sheaf.add_im_sheaf ?S ?add_str ?f \<equiv> \<lambda>V. ?add_str (?f \<^sup>\<inverse> ?S V)
Comm_Ring.im_sheaf S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open (identity S)
local.im_sheaf ?V \<equiv> \<FF> (identity S \<^sup>\<inverse> S ?V)
mult_im_sheaf \<equiv> \<lambda>V. \<cdot>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
one_im_sheaf \<equiv> \<lambda>V. \<one>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>
zero_im_sheaf \<equiv> \<lambda>V. \<zero>\<^bsub>identity S \<^sup>\<inverse> S V\<^esub>

goal (1 subgoal):
 1. ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ring_homomorphism (identity (\<FF> U)) (local.im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
fix V x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
assume "is_open V" and "V \<subseteq> U" and "x \<in> local.im_sheaf U"
[PROOF STATE]
proof (state)
this:
is_open V
V \<subseteq> U
x \<in> local.im_sheaf U

goal (1 subgoal):
 1. \<And>U V x. \<lbrakk>is_open U; is_open V; V \<subseteq> U; x \<in> local.im_sheaf U\<rbrakk> \<Longrightarrow> (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open V
V \<subseteq> U
x \<in> local.im_sheaf U
[PROOF STEP]
show "(\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x"
[PROOF STATE]
proof (prove)
using this:
is_open V
V \<subseteq> U
x \<in> local.im_sheaf U

goal (1 subgoal):
 1. (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
using map.map_closed [OF is_map_from_is_homomorphism] \<open>is_open U\<close>
[PROOF STATE]
proof (prove)
using this:
is_open V
V \<subseteq> U
x \<in> local.im_sheaf U
\<lbrakk>is_open ?U1; is_open ?V1; ?V1 \<subseteq> ?U1; ?a \<in> local.im_sheaf ?U1\<rbrakk> \<Longrightarrow> im_sheaf_morphisms ?U1 ?V1 ?a \<in> local.im_sheaf ?V1
is_open U

goal (1 subgoal):
 1. (\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x
[PROOF STEP]
by (simp add: im_sheaf_morphisms_def local.im_sheaf_def)
[PROOF STATE]
proof (state)
this:
(\<rho> U V \<circ> identity (\<FF> U)) x = (identity (\<FF> V) \<circ> im_sheaf_morphisms U V) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. \<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
[PROOF STEP]
show "\<exists>\<psi>. morphism_presheaves_of_rings S is_open (im_sheaf.im_sheaf S \<FF> (identity S)) (im_sheaf.im_sheaf_morphisms S \<rho> (identity S)) b
              (im_sheaf.add_im_sheaf S add_str (identity S)) (im_sheaf.mult_im_sheaf S mult_str (identity S)) (im_sheaf.zero_im_sheaf S zero_str (identity S)) (im_sheaf.one_im_sheaf S one_str (identity S)) \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>im_sheaf.im_sheaf S \<FF> (identity S) U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))"
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))

goal (1 subgoal):
 1. \<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))
[PROOF STEP]
using local.im_sheaf_def
[PROOF STATE]
proof (prove)
using this:
morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str (\<lambda>U. identity (\<FF> U))
local.im_sheaf ?V \<equiv> \<FF> (identity S \<^sup>\<inverse> S ?V)

goal (1 subgoal):
 1. \<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>. morphism_presheaves_of_rings S is_open local.im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf \<FF> \<rho> b add_str mult_str zero_str one_str \<psi> \<and> (\<forall>U. is_open U \<longrightarrow> (\<forall>x\<in>local.im_sheaf U. (identity (\<FF> U) \<circ> \<psi> U) x = x) \<and> (\<forall>x\<in>\<FF> U. (\<psi> U \<circ> identity (\<FF> U)) x = x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iso_locally_ringed_spaces_axioms S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iso_locally_ringed_spaces S is_open \<FF> \<rho> b add_str mult_str zero_str one_str S is_open \<FF> \<rho> b add_str mult_str zero_str one_str (identity S) (\<lambda>U. identity (\<FF> U))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_classes'':
  "''C'' \<noteq> Object"
  "''C'' \<noteq> NullPointer"
  "''C'' \<noteq> OutOfMemory"
  "''C'' \<noteq> ClassCast"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''C'' \<noteq> Object &&& ''C'' \<noteq> NullPointer) &&& ''C'' \<noteq> OutOfMemory &&& ''C'' \<noteq> ClassCast
[PROOF STEP]
by (simp_all add: Object_def NullPointer_def OutOfMemory_def ClassCast_def)


[STATEMENT]
lemma i_max_2D: "i < Suc (Suc 0) \<Longrightarrow> i = 0 \<or> i = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Suc (Suc 0) \<Longrightarrow> i = 0 \<or> i = 1
[PROOF STEP]
by auto