This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||
|
Galois Insertions
editNeed to add the definition (and properties?) of Galois insertions, that is Galois connections with a composition of adjoins being the identity function. VictorPorton (talk) 22:45, 17 December 2012 (UTC)
Definition
editThere was some confusion about the definition (whether it is "F(a) <= b if and only if a ≤ G(b)" or "F(a) <= b if and only if G(b) ≤ a"). I changed it back to the former version (sorry Axel), since it is more common in the order-theory literature I know of. This definition is also the only one that is currently cited in other articles (see adjoint functors, heyting algebra and order theory glossary). However, to make it still possible to use the historical definition, I include this one too. It should be called antitone Galois connection in Wikipedia.
At least the following authors use the current definition of Galois connection in a book published after 1990: Abramski, Borceux, Davey, Gierz, Hofmann, Jung, Keimel, Lawson, Mislove, Priestley, Scott. Especially [Davey & Priestley] is probably the introductory text-book in this field.
--Markus Krötzsch 20:53, 3 Feb 2004 (UTC)
- That's fine, we should definitely use the modern definition. When I found the discrepancy, I went back to the original papers and copied their antitone definition, not realizing that conventions had changed in the meantime. AxelBoldt 15:56, 14 Feb 2004 (UTC)
- I don't think that conventions changed completely. Where it is convenient (in some applications, such as formal concept analysis) the antitone definition is used as well. So it might be good to mention "monotone" or "antitone" in articles that use Galois connections. --Markus Krötzsch 18:55, 29 Mar 2004 (UTC)
The definition is lacking in a few ways. First, "monotone" is not the opposite of "antitone". "Monotone increasing" is the opposite, and the word for that is "isotone". Second, it is invalid to claim that "Galois connection" should mean isotone mappings; that is one perspective but not fully representative of the literature. I will edit the article to say "isotone Galois connection" and "antitone Galois connection" to reflect the range of usage. It's too bad if other articles assume a "Galois connection" is isotone; this article should be correct. The others can be fixed. Zaslav (talk) 19:49, 21 February 2022 (UTC)
Uniqueness of adjoints
editIn the Definition section is said As detailed below, each part of a Galois connection uniquely determines the other mapping.
But below there are no proof nor any details nor any reference about each part of a Galois connection uniquely determining the other.
The proof needs to be added. —Preceding unsigned comment added by Porton (talk • contribs) 12:15, 13 June 2009 (UTC)
Applications in programming
editIt would be nice if somebody could amplify about applications, including the application cited to programming. My vague understanding is that it has something to do with programming semantics, perhaps denotational semantics where data objects form a complete partial order and operations on them are partial functions. I seem to recall that Galois connections are used in relation to formal methods, perhaps to ensure that program refinements preserve some correctness properties (liveness and safety) from the unrefined to the refined domain, but I don't know the details. I heard this from somebody who audited a course in program semantics at Oxford U, which used Galois connections as a unifying concept.
Fred Kintanar
Cebu City
- I'm afraid we have to wait until someone shows up who has audited that course at Oxford U. Can't you give a call to your friend? :-) AxelBoldt 15:53, 14 Feb 2004 (UTC)
As part of the whole Tony Hoare tradition, there are 'weakest preconditions' for something to happen with a program, and so on. This leads very quickly (if somewhat superficially) to the use of Galois connections. I don't see anything substantive about this on WP, currently.
Charles Matthews 09:16, 5 Apr 2004 (UTC)
Definitions, again
editAbout the definitions (again):
We currently have F(a) <= b if and only if G(b) ≤ a for antitone Galois connections. In contrast, a book on my desk (Ganter & Wille) says it should be b <= F(a) if and only if a ≤ G(b). This is not the same, since orders may be partial ("not ≤" is not the same as "≥"). Is the definition in the article also used somewhere (it certainly affects the results, since one gets no closure operators in this case, but obtains their duals -- kernel operators -- instead)? If not, it's an error and needs to be corrected. --Markus Krötzsch 23:39, 19 Feb 2005 (UTC)
Is it possible to change ≤ and <= to ≤a and ≤b to make it clear that there are 2 different orders that are related to the sets A and B.
Like this: (A,≤a) and (B,≤b) F(a) ≤b b if and only if a ≤a G(b).
The red lettered text denoting a yet-to-be-written-article appearing in this article reads: adjoint functor theorem for order theory. The one-sentence description of its application here is vaguely reminiscent of the Freyd Adjoint Functor Theorem described in the article on Adjoint functors. Are these theorems one and the same? I'm seeking concurrence before making this change. Vonkje 00:24, 2 August 2005 (UTC)
Another resource, a better notation
editHi. There is a document about Galois connections, written by Roland Backhouse, which uses a different (better, IMO) notation. The link is: http://www.cs.nott.ac.uk/~rcb/G53PAL/FPandGC.pdf
- The notation in this article is a mess, but not much more so than what other authors use. For starters, the *-notation is only used in Erné, but not in Davey and Priestley or in Gierz et al. What's worse, is that the notation in this article places the asterisk in the opposite way than Erné. On the bright side, the terms "upper" and "lower" are from Gierz, and they make way more mnemonic sense compared with those the Davey and Pristely (left/right) or Erné (adjoint/coadjoint). Pcap ping 22:13, 5 August 2009 (UTC)
Merge proposal
editPer this discussion it has been proposed that this article be merged with Residuated mapping. However the topic hasn't been discussed for the past two months in the respective talk-pages. I suggest to either continue the discussion here (untill some kind of consensus is reached) or remove the tag from the article. --Omnipaedista (talk) 06:26, 29 October 2009 (UTC)
Power set example
editThe power set example doesn't seem right -- I think the names of things are changed mid-explanation and it makes no sense. Could someone less confused than me take a look and try to fix it? 128.193.60.168 (talk) 02:43, 10 November 2009 (UTC)
Definition by composition of relations?
editAm I right that that galois connections could be defined using composition of relations? I.e.:
Let be two Posets.
is a galois connection iff .
iff iff
and
iff iff
I.e. is a galois connection iff ?
One might even write iff .
Is there any such definition in literature?
-- 188.192.84.97 (talk) 14:26, 9 December 2011 (UTC)
- Perhaps this one: Jacques Riguet (1948) "Relations binaires, fermetures, correspondances de Galois", Bulletin de la Société Mathématique de France 76: 114–55. — Rgdboer (talk) 21:44, 27 April 2018 (UTC)
Suggest to cite "own" article in section "Applications in the theory of programming"
editIn section Galois connection#Applications in the theory of programming, I added two references to the original papers of Cousot and Cousot, and one to a tech. report correcting a false theorem of their 1977 paper. Following an advice of User:Deltahedron on my talk page, I deleted the tech. report reference where I was a co-author. Below follows the text before deletion; I'd like to restore it if there are no objections. - Jochen Burghardt (talk) 21:09, 1 February 2014 (UTC)
Galois connections may be used to describe many forms of abstraction in the theory of abstract interpretation of programming languages.[1][2]
- ^ Patrick Cousot, Radhia Cousot (1977). "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints". Proc. 4th ACM Symp. on Principles of Programming Languages (POPL) (PDF). pp. 238–252.
{{cite book}}
: Unknown parameter|month=
ignored (help)
For a counterexample for the false theorem in Sect.7 (p.243 top right), see: Jochen Burghardt, Florian Kammüller, Jeff W. Sanders (2000). Isomorphism of Galois Embeddings (Technical report). GMD. p. 73. ISSN 1435-2702. 122.{{cite tech report}}
: Unknown parameter|month=
ignored (help)CS1 maint: multiple names: authors list (link)- ^ Patrick Cousot, Radhia Cousot (1979). "Systematic Design of Program Analysis Frameworks". Proc. 6th ACM Symp. on Principles of Programming Languages (POPL) (PDF). ACM Press. pp. 269–282.
{{cite book}}
: Unknown parameter|month=
ignored (help)
F or G invertible implies each is the inverse of the other
editThe article states "if F or G is invertible, then each is the inverse of the other, i.e. F = G–1", this being stated as a consequence of the formulas and . My issue is that the word "invertible" was linked to the article Bijection, but the fact is only clear to me if F or G is invertible with a monotone inverse (the inverse function of a monotone bijection is not in general monotone), since then we have
- and similarly
Maybe I am missing something and one can make a different argument to conclude that if F or G is invertible just as a function (i.e. is a bijection) then F and G are each other's inverses (I haven't tried to look for a counterexample). Could somebody in the know please fill me in, and also update the article to clarify (and then remove the "Clarify" tag that I added). Thanks. Joel Brennan (talk) 21:06, 7 December 2021 (UTC)