Stream: Beginner Questions

Topic: locale for vector spaces

view this post on Zulip 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"

view this post on Zulip 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).

view this post on Zulip 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"

view this post on Zulip zibo yang (Apr 22 2021 at 06:05):

Thanks, I got it. let me think a while

view this post on Zulip 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: Aug 13 2022 at 05:18 UTC