Topological inductive definitions (Q450944): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(4 intermediate revisions by 4 users not shown) | |||
Property / review text | |||
The concept of locale is a satisfactory substitute for the notion of topological space in an intuitionistic framework. However, the notion of locale is unsatisfactory in the framework of predicative mathematics. For this reason, the categories \textbf{FSP} of formal spaces and \textbf{FSP}\(_i\) of inductively generated formal spaces have been introduced and studied. These categories are equivalent to the category of locales in an impredicative setting, but both are incomplete in some sense. The article aims at proposing another category, \textbf{ImLoc}, the category of \textit{imaginary} locales to circumvent the problems of \textbf{FSP} and \textbf{FSP}\(_i\) in the predicative setting. It turns out that \textbf{ImLoc} contains both \textbf{FSP} and \textbf{FSP}\(_i\) as subcategories, and it is equivalent to the categories of locales in the intuitionistic impredicative framework, thus meeting the initial objective. In simple terms, \textbf{ImLoc} is the opposite of the category of frame presentations, which are structures given by a preordered set over the base of the intended space together with a generalised covering system. The result is that a frame presentation does not always allow to define a concrete frame meeting its structure, but it always allows to identify a structure of opens that may be realised by a concrete frame. For this reason, \textbf{ImLoc} contains enough objects and continuous functions between them to be complete as a category, thus fixing the problem of \textbf{FSP}, and to represent all the formal spaces of interest, overcoming the difficulties of \textbf{FSP}\(_i\). The paper concludes presenting a few applications: a point-free version of the Tychonoff embedding theorem, and some set-representation theorems. This article is of prime interest for every mathematician interested in the categorical description of formal topology in constructive and predicative terms. | |||
Property / review text: The concept of locale is a satisfactory substitute for the notion of topological space in an intuitionistic framework. However, the notion of locale is unsatisfactory in the framework of predicative mathematics. For this reason, the categories \textbf{FSP} of formal spaces and \textbf{FSP}\(_i\) of inductively generated formal spaces have been introduced and studied. These categories are equivalent to the category of locales in an impredicative setting, but both are incomplete in some sense. The article aims at proposing another category, \textbf{ImLoc}, the category of \textit{imaginary} locales to circumvent the problems of \textbf{FSP} and \textbf{FSP}\(_i\) in the predicative setting. It turns out that \textbf{ImLoc} contains both \textbf{FSP} and \textbf{FSP}\(_i\) as subcategories, and it is equivalent to the categories of locales in the intuitionistic impredicative framework, thus meeting the initial objective. In simple terms, \textbf{ImLoc} is the opposite of the category of frame presentations, which are structures given by a preordered set over the base of the intended space together with a generalised covering system. The result is that a frame presentation does not always allow to define a concrete frame meeting its structure, but it always allows to identify a structure of opens that may be realised by a concrete frame. For this reason, \textbf{ImLoc} contains enough objects and continuous functions between them to be complete as a category, thus fixing the problem of \textbf{FSP}, and to represent all the formal spaces of interest, overcoming the difficulties of \textbf{FSP}\(_i\). The paper concludes presenting a few applications: a point-free version of the Tychonoff embedding theorem, and some set-representation theorems. This article is of prime interest for every mathematician interested in the categorical description of formal topology in constructive and predicative terms. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Marco Benini / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F65 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 06D22 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 18B30 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 54B10 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6086891 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
inductive definitions | |||
Property / zbMATH Keywords: inductive definitions / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
point-free topology | |||
Property / zbMATH Keywords: point-free topology / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
constructive set theory | |||
Property / zbMATH Keywords: constructive set theory / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2011.12.005 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1990132849 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3310616 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3762311 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Aspects of general topology in constructive set theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Equalisers of Frames in Constructive Set Theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the \(T_{1}\) axiom and other separation properties in constructive point-free and point-set topology / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4039735 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Compact spaces and distributive lattices. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Inductively generated formal topologies. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the collection of points of a formal space / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Exact approximations to Stone-Čech compactification / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On some peculiar aspects of the constructive theory of point-free spaces / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the existence of Stone-Čech compactification / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3322099 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3050433 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Set theoretic foundations for constructive analysis / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Heyting-valued interpretations for constructive set theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3965241 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4828514 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: CZF and second order arithmetic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the constructive Dedekind reals / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Sheaves in geometry and logic: a first introduction to topos theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5718572 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5310884 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Maximal and partial points in formal spaces / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5477360 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3481701 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3978991 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proper maps of locales / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5718573 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 18:03, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Topological inductive definitions |
scientific article |
Statements
Topological inductive definitions (English)
0 references
26 September 2012
0 references
The concept of locale is a satisfactory substitute for the notion of topological space in an intuitionistic framework. However, the notion of locale is unsatisfactory in the framework of predicative mathematics. For this reason, the categories \textbf{FSP} of formal spaces and \textbf{FSP}\(_i\) of inductively generated formal spaces have been introduced and studied. These categories are equivalent to the category of locales in an impredicative setting, but both are incomplete in some sense. The article aims at proposing another category, \textbf{ImLoc}, the category of \textit{imaginary} locales to circumvent the problems of \textbf{FSP} and \textbf{FSP}\(_i\) in the predicative setting. It turns out that \textbf{ImLoc} contains both \textbf{FSP} and \textbf{FSP}\(_i\) as subcategories, and it is equivalent to the categories of locales in the intuitionistic impredicative framework, thus meeting the initial objective. In simple terms, \textbf{ImLoc} is the opposite of the category of frame presentations, which are structures given by a preordered set over the base of the intended space together with a generalised covering system. The result is that a frame presentation does not always allow to define a concrete frame meeting its structure, but it always allows to identify a structure of opens that may be realised by a concrete frame. For this reason, \textbf{ImLoc} contains enough objects and continuous functions between them to be complete as a category, thus fixing the problem of \textbf{FSP}, and to represent all the formal spaces of interest, overcoming the difficulties of \textbf{FSP}\(_i\). The paper concludes presenting a few applications: a point-free version of the Tychonoff embedding theorem, and some set-representation theorems. This article is of prime interest for every mathematician interested in the categorical description of formal topology in constructive and predicative terms.
0 references
inductive definitions
0 references
point-free topology
0 references
constructive set theory
0 references
0 references