James Hanson (Mar 17 2024 at 03:07): James Hanson (Mar 17 2024 at 03:07):Say I'm working with a locale representing groups:
locale group =
fixes
G :: 'a
mult :: 'a => 'a => 'a
assumes
...
Suppose furthermore that I want to think about the automorphism group of a given group, so I define something like this:
definition
set_of_automorphisms :: "('a => 'a) set"
where ...
Now I'd like to say that the automorphisms of a group themselves form a group under composition. It seems like I should be doing this by declaring some kind of sublocale or interpretation, but I haven't been able to determine from the examples I've found online whether this makes sense or not and how I would go about doing it if it does.
Mathias Fleury (Mar 17 2024 at 07:04):You mean something like that:
locale group =
fixes
G :: "'a set" and
mult :: "'a => 'a => 'a"
context group
begin
definition
set_of_automorphisms :: "('a => 'a) set"
where
"set_of_automorphisms = undefined"
interpretation automorphism: group where G = set_of_automorphisms and mult = "(o)"
done
term automorphism.set_of_automorphisms
end
main issue is that interpretation do not live outside of the context
Mathias Fleury (Mar 17 2024 at 07:13):(sublocale do not work, because it creates a cycle)
James Hanson (Mar 17 2024 at 16:05):Is there a difference between these?
definition (in group)
set_of_automorphisms :: "('a => 'a) set"
where "set_of_automorphisms = undefined"
vs.
context group
begin
definition
set_of_automorphisms :: "('a => 'a) set"
where "set_of_automorphisms = undefined"
end
I think the answer is no, but it also seems like there's no syntax of the form:
interpretation (in group) automorphism: group where G = set_of_automorphisms and mult = "(o)"
James Hanson said:
Is there a difference between these?
definition (in group) set_of_automorphisms :: "('a => 'a) set" where "set_of_automorphisms = undefined"vs.
context group begin definition set_of_automorphisms :: "('a => 'a) set" where "set_of_automorphisms = undefined" end
no difference
Mathias Fleury (Mar 17 2024 at 16:14):James Hanson said:
I think the answer is no, but it also seems like there's no syntax of the form:
interpretation (in group) automorphism: group where G = set_of_automorphisms and mult = "(o)"
would not make sense, because the interpretation would not live long enough to be useful. Try this:
locale group =
fixes
G :: "'a set" and
mult :: "'a => 'a => 'a"
context group
begin
definition
set_of_automorphisms :: "('a => 'a) set"
where
"set_of_automorphisms = undefined"
interpretation automorphism: group where G = set_of_automorphisms and mult = "(o)"
done
term automorphism.set_of_automorphisms
end
context group
begin
term automorphism.set_of_automorphisms
(*fails because interpretation is not living long enough*)
end
So how would I show that the automorphism group is a group in a reusable way? Is this not in general the right way to structure that kind of fact?
James Hanson (Mar 17 2024 at 16:54):I think a closer analog of my actual use case might be metric spaces. Say I have a locale for (possibly incomplete) metric spaces, then I want to be able to talk about the completion of a metric space which is itself also a metric space. So my thinking is that I would have a locale for complete_metric_space extending metric_space and I want to say that complete_metric_space can be interpreted in metric_space in the obvious way (although I'm not sure I'm using the word 'interpreted' in a technically correct way in the sense of Isabelle/HOL).
Mathias Fleury (Mar 17 2024 at 17:18):section 7.1 of https://isabelle.in.tum.de/doc/locales.pdf ?
James Hanson (Mar 20 2024 at 16:10):This is what I was originally confused by, but I think I understand it now. Thank you.
Last updated: Dec 21 2024 at 16:20 UTC