Stream: Beginner Questions

Topic: locale for vector spaces

zibo yang (Apr 21 2021 at 22:42):

Hi, I have a very stupid but weird question. If I get the locale like that:

locale real_vector_space = abelian_group V add zero
  for V and add (infixl "+" 70) and zero ("𝟬") +
  fixes scale:: "real ⇒ 'a ⇒ 'a" (infixr "⋅⇩ℝ" 75)
  assumes scale_add: "⟦x ∈ V; y ∈ V⟧ ⟹ r ⋅⇩ℝ (x + y) = r ⋅⇩ℝ x + r ⋅⇩ℝ y"
  and add_scale: "x ∈ V ⟹ (r + s) ⋅⇩ℝ x = r ⋅⇩ℝ x + s ⋅⇩ℝ x"
  and scale_scale: "x ∈ V ⟹ r ⋅⇩ℝ s ⋅⇩ℝ x = (r * s) ⋅⇩ℝ x"
  and one_scale: "x ∈ V ⟹ 1 ⋅⇩ℝ x = x"

then how can I prove

x ∈ V ⟹ r ⋅⇩ℝ x ∈ V

since I find it nothing feedback when I code like "using scale_def"

Mathias Fleury (Apr 22 2021 at 05:13):

Well, first, scale is not defined through a definition. Instead it is an arbitrary constant that has 4 properties (scale_add, add_scale, scale_scale, and one_scale). Hence there is no definition (I don't even see what you expect here).

Mathias Fleury (Apr 22 2021 at 05:20):

And for you actual question, you need to assume that ⋅⇩ℝ stays in V. If you look at the module definition in the Isabelle Library (~~/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy), this is what it is done:

locale module_on =
  fixes S and scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
  assumes [...]
    and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"

zibo yang (Apr 22 2021 at 06:05):

Thanks, I got it. let me think a while

Anthony Bordg (Apr 22 2021 at 08:51):

@zibo yang As pointed out by Mathias, in locale real_vector_space the closure property of scale has been forgotten and needs to be added among the assumptions within the locale.

Last updated: Apr 16 2024 at 04:18 UTC