John Hughes (Oct 26 2025 at 14:02): John Hughes (Oct 26 2025 at 14:02):Mimicking Ballarin's approach to algebra, I've been defining morphisms and isomorphisms for projective planes. I've run into some problems/questions (in bold below). Here's my starting point:
theory locale_example
imports Main
begin
locale projective_plane_data =
fixes Points :: "'p set" and Lines :: "'l set" and incid :: "'p ⇒ 'l ⇒ bool" (infix "⊲" 60)
begin
definition (in projective_plane_data) pcollinear :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
where "pcollinear A B C = (if (A ∈ Points ∧ B ∈ Points ∧ C ∈ Points)
then (∃ l. l ∈ Lines ∧ A ⊲ l ∧ B ⊲ l ∧ C ⊲ l) else undefined)"
end
locale projective_plane = projective_plane_data Points Lines incid
for
Points :: "'p set" and
Lines :: "'l set" and
incid :: "'p ⇒ 'l ⇒ bool" (infix "⊲" 60) +
assumes
p1: "⟦P ≠ Q; P ∈ Points; Q ∈ Points⟧ ⟹ (∃!k. k ∈ Lines ∧ P ⊲ k ∧ Q ⊲ k)" and
p2: "⟦k ∈ Lines; n ∈ Lines⟧ ⟹ ∃P. (P ∈ Points ∧ P ⊲ k ∧ P ⊲ n)" and
p3: "∃P Q R. P ∈ Points ∧ Q ∈ Points ∧ R ∈ Points ∧ P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ (pcollinear P Q R)" and
p4: "⟦k ∈ Lines; U = {P. (P ∈ Points ∧ P ⊲ k)} ⟧ ⟹ ∃Q R S. Q ∈ U ∧ R ∈ U ∧ S ∈ U ∧ distinct [Q, R, S]"
begin
end
locale pp_morphism =
source: projective_plane "Points1" "Lines1" "incid1" +
target: projective_plane "Points2" "Lines2" "incid2"
for Points1 and Lines1 and incid1 and Points2 and Lines2 and incid2 +
fixes "f"
assumes
m1: "⟦P ∈ Points1⟧ ⟹ (f P) ∈ Points2" and
m2: "⟦P ∈ Points1; Q ∈ Points1; R ∈ Points1; source.pcollinear P Q R⟧ ⟹ target.pcollinear (f P) (f Q) (f R)"
begin
end
locale pp_isomorphism = pp_morphism Points1 Lines1 incid1 Points2 Lines2 incid2 f
for Points1 Lines1 incid1 Points2 Lines2 incid2 f +
assumes
m3: "bij_betw f Points1 Points2"
begin
end
Basically, a morphism is a map on points that preserves collinearity; an isomorphism is one that is also a bijection.
Side-question: is there a reason to use sublocale to relate isomorphism to morphism? Reading the tutorial on locales didn't really make this clear to me.
I'd now like to define an automorphism, which is basically an isomorphism of a projective plane to itself. The identity map on Points is a good example. I'd like to write something like
locale pp_automorphism = pp_isomorphism Points1 Lines1 incid1 Points1 Lines1 incid1 f
for Points1 Lines1 incid1 Points2 Lines2 incid2 f
begin
end
but that doesn't seem to work entirely, because the type assigned by Isabelle is
locale pp_automorphism
fixes Points1 :: "'a set"
and Lines1 :: "'b set"
and incid1 :: "'a ⇒ 'b ⇒ bool"
and Points2 :: "'c"
and Lines2 :: "'d"
and incid2 :: "'e"
and f :: "'a ⇒ 'a"
assumes "pp_automorphism Points1 Lines1 incid1 f"
where you can see that Points2 and Points1 have different types, even though property m1 would suggest that they should be the same.
Can someone suggest anything to fix this up here?
If I edit the definition a bit to include a fourth "property" like this:
locale pp_automorphism = pp_isomorphism Points1 Lines1 incid1 Points1 Lines1 incid1 f
for Points1 Lines1 incid1 Points2 Lines2 incid2 f +
assumes
m4: "Points1 = Points2 ∧ Lines1 = Lines2 ∧ incid1 = incid2"
begin
end
then the resulting types all look correct, but I thought that the content of this property was implicit in what I'd already said.
Is this a correct approach, or is there some other way to achieve the type-result that I'm aiming for?
Mathias Fleury (Oct 26 2025 at 17:29):In this:
locale pp_automorphism
fixes Points1 :: "'a set"
and Lines1 :: "'b set"
and incid1 :: "'a ⇒ 'b ⇒ bool"
and Points2 :: "'c"
and Lines2 :: "'d"
and incid2 :: "'e"
and f :: "'a ⇒ 'a"
assumes "pp_automorphism Points1 Lines1 incid1 f"
you are not assuming anything about Points2. What you want is probably:
locale pp_automorphism =
pp_isomorphism Points1 Lines1 incid1 Points2 Lines2 incid2 f
for Points1 :: "'a set"
and Lines1 :: "'b set"
and incid1 :: "'a ⇒ 'b ⇒ bool"
and Points2 :: "'a set"
and Lines2 :: "'b set"
and incid2 :: "'a ⇒ 'b ⇒ bool"
and f :: "'a ⇒ 'a"
Or more likely you have copy-pasted a Points2 too much in pp_automorphism and it should be:
locale pp_automorphism = pp_isomorphism Points1 Lines1 incid1 Points1 Lines1 incid1 f
for Points1 Lines1 incid1 f
Side-question: is there a reason to use
sublocaleto relate isomorphism to morphism? Reading the tutorial on locales didn't really make this clear to me.
No because pp_isomorphism = pp_morphism. But sometimes two objects that are unrelated in the locale hierarchy behave the same. Then you want to add a sublocale
John Hughes (Oct 26 2025 at 18:18):Thanks for the answer about the sublocale.
Regarding your comments: The code after your "In this" isn't something that I typed -- it's Isabelle's output in response to what I typed above. When I wrote
locale pp_automorphism = pp_isomorphism Points1 Lines1 incid1 Points1 Lines1 incid1 f
for Points1 Lines1 incid1 Points2 Lines2 incid2 f
begin
end
what I was trying to express was that in defining pp_automorphism, I wanted a locale with only three arguments, but then I wanted to use the locale pp_isomorphism using Points1 Lines1 incid1 to define the first projective plane, and then use those same three things to define the second projective plane. I thought that this was what the for clause would do, but apparently I was mistaken.
Looking back at it, I can't imagine why I thought this would give me a 3-argument locale... but that's what I really want. After all, we don't say "consider an automorphism of the group G with itself," because an automorphism IS a map from G to itself. I'd like to refer to the projective plane in question only once, and have it serve as both source and target for the morphism if that's possible.
To put it slightly differently, I'd like the analogue of the Algebra text that says something like this:
A homomorphism from a group G to a group H is a map such that <various conditions>; we denote the set of all such homomorphisms Hom(G, H).
An automorphism of G is a homomorphism from G to itself; we denote the set of all such automorphisms Aut(G).
For now I'm doing only the first clause of each sentence, of course. (I'd hoped Ballarin's algebra work would give me something to copy, but unfortunately Jacobson doesn't seem to talk about automorphisms!)
Mathias Fleury (Oct 26 2025 at 19:13):You should just remove the stuff ending with a 2 arguments in the for of:
locale pp_automorphism = pp_isomorphism Points1 Lines1 incid1 Points1 Lines1 incid1 f
for Points1 Lines1 incid1 Points2 Lines2 incid2 f
begin
end
Then everything will make sense
John Hughes (Oct 27 2025 at 01:45):I grant you that seems to work, but I don't actually understand why, but I certainly appreciate your telling me how to get to what I needed. For others who might be following, the final text was this:
locale pp_automorphism = pp_isomorphism Points1 Lines1 incid1 Points1 Lines1 incid1
for Points1 Lines1 incid1
begin
end
The Points2 Lines2 incid2 are not bound
Mathias Fleury (Oct 27 2025 at 10:44):but because of their name, their presence confused you
John Hughes (Oct 27 2025 at 22:52):Right. I actually added a "assumes" to say Points2 = Points1, Lines2 = Lines1, incid2 = inclid1, and that resolved the type-inferences the way that I had expected. (It also represents what I'm thinking about when I talk about an automorphism of projective planes!)
Last updated: Nov 13 2025 at 04:27 UTC