no. 1
Towards formal Baer criteria
Misselbeck-Wessel, Daniel1 ; Rinaldi, Davide
1 Dipartimento di Informatica, Università degli Studi di Verona, Strada le Grazie 15, 37134 Verona, Italy
Confluentes Mathematici, Tome 14 (2022) no. 1, pp. 49-63.

Baer’s criterion helps to identify the injective objects in a category of modules by reducing the problem of map extension to a certain subclass of morphisms. Due to its notorious reliance on Zorn’s lemma, it is inherently non-constructive. However, we put Baer’s criterion on constructive grounds by couching it in point-free terms. Classical principles which will be developed alongside readily allow to gain back the conventional version. Several case studies further indicate a fair applicability.

Reçu le :
Révisé le :
Accepté le :
Publié le :
DOI : 10.5802/cml.82
Classification : 13C11, 06D22, 03F65
Mots clés : Injective module, Baer’s criterion, point-free topology, inductive definition, constructive algebra
Misselbeck-Wessel, Daniel 1 ; Rinaldi, Davide 

1 Dipartimento di Informatica, Università degli Studi di Verona, Strada le Grazie 15, 37134 Verona, Italy 
@article{CML_2022__14_1_49_0,
     author = {Misselbeck-Wessel, Daniel and Rinaldi, Davide},
     title = {Towards formal {Baer} criteria},
     journal = {Confluentes Mathematici},
     pages = {49--63},
     publisher = {Institut Camille Jordan},
     volume = {14},
     number = {1},
     year = {2022},
     doi = {10.5802/cml.82},
     language = {en},
     url = {http://www.numdam.org/articles/10.5802/cml.82/}
}
TY  - JOUR
AU  - Misselbeck-Wessel, Daniel
AU  - Rinaldi, Davide
TI  - Towards formal Baer criteria
JO  - Confluentes Mathematici
PY  - 2022
SP  - 49
EP  - 63
VL  - 14
IS  - 1
PB  - Institut Camille Jordan
UR  - http://www.numdam.org/articles/10.5802/cml.82/
DO  - 10.5802/cml.82
LA  - en
ID  - CML_2022__14_1_49_0
ER  - 
%0 Journal Article
%A Misselbeck-Wessel, Daniel
%A Rinaldi, Davide
%T Towards formal Baer criteria
%J Confluentes Mathematici
%D 2022
%P 49-63
%V 14
%N 1
%I Institut Camille Jordan
%U http://www.numdam.org/articles/10.5802/cml.82/
%R 10.5802/cml.82
%G en
%F CML_2022__14_1_49_0
Misselbeck-Wessel, Daniel; Rinaldi, Davide. Towards formal Baer criteria. Confluentes Mathematici, Tome 14 (2022) no. 1, pp. 49-63. doi : 10.5802/cml.82. http://www.numdam.org/articles/10.5802/cml.82/

[1] Aczel, Peter Aspects of general topology in constructive set theory, Ann. Pure Appl. Logic, Volume 137 (2006) no. 1–3, pp. 3-29 | DOI | MR | Zbl

[2] Aczel, Peter; Rathjen, Michael Notes on Constructive Set Theory (2000) (Report No. 40) (Technical report)

[3] Aczel, Peter; Rathjen, Michael Constructive set theory (2010) https://www1.maths.leeds.ac.uk/~rathjen/book.pdf (Book draft)

[4] Aczel, Peter; van den Berg, Benno; Granström, Johan; Schuster, Peter Are there enough injective sets?, Studia Logica (2012) | Zbl

[5] Balbes, Raymond Projective and injective distributive lattices, Pacific J. Math., Volume 21 (1967) no. 3, pp. 405-420 | DOI | MR | Zbl

[6] Banaschewski, Bernhard; Bruns, Günter Injective hulls in the category of distributive lattices, J. Reine Angew. Mathematik, Volume 232 (1968), pp. 102-109 | MR | Zbl

[7] Bell, J. L. Zorn’s lemma and complete Boolean algebras in intuitionistic type theories, J. Symb. Log., Volume 62 (1997) no. 4, pp. 1265-1279 | MR | Zbl

[8] Blass, Andreas Injectivity, projectivity, and the axiom of choice, Trans. Amer. Math. Soc., Volume 255 (1979), pp. 31-59 | MR | Zbl

[9] Cederquist, Jan; Coquand, Thierry Entailment relations and distributive lattices, Logic Colloquium ’98. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9–15, 1998 (Buss, Samuel R.; Hájek, Petr; Pudlák, Pavel, eds.) (Lect. Notes Logic), Volume 13, A. K. Peters, Natick, MA, 2000, pp. 127-139 | MR | Zbl

[10] Coquand, Thierry A direct proof of the localic Hahn-Banach theorem, 2000 http://www.cse.chalmers.se/~coquand/formal.html

[11] Coquand, Thierry Geometric Hahn–Banach theorem, Math. Proc. Cambridge Philos. Soc., Volume 140 (2006) no. 2, pp. 313-315 | DOI | MR | Zbl

[12] Coquand, Thierry; Lombardi, Henri A logical approach to abstract algebra., Math. Structures Comput. Sci., Volume 16 (2006), pp. 885-900 | DOI | MR | Zbl

[13] Coquand, Thierry; Sambin, Giovanni; Smith, Jan; Valentini, Silvio Inductively generated formal topologies, Ann. Pure Appl. Logic, Volume 124 (2003), pp. 71-106 | DOI | MR | Zbl

[14] Coquand, Thierry; Zhang, Guo-Qiang Sequents, frames, and completeness, Computer Science Logic (Fischbachau, 2000) (Clote, Peter G.; Schwichtenberg, Helmut, eds.) (Lecture Notes in Comput. Sci.), Volume 1862, Springer, Berlin, 2000, pp. 277-291 | DOI | MR | Zbl

[15] Coste, Michel; Lombardi, Henri; Roy, Marie-Françoise Dynamical method in algebra: Effective Nullstellensätze., Ann. Pure Appl. Logic, Volume 111 (2001) no. 3, pp. 203-256 | DOI | Zbl

[16] Crosilla, Laura; Schuster, Peter Finite Methods in Mathematical Practice, Formalism and Beyond. On the Nature of Mathematical Discourse (Link, G., ed.) (Logos), Volume 23, Walter de Gruyter, Boston and Berlin, 2014, pp. 351-410 | DOI | MR | Zbl

[17] Curi, Giovanni On some peculiar aspects of the constructive theory of point-free spaces, Math. Log. Quart., Volume 56 (2010) no. 4, pp. 375-387 | DOI | MR | Zbl

[18] Curi, Giovanni On the existence of Stone-Čech Compactification, J. Symbolic Logic, Volume 75 (2010) no. 4, pp. 1137-1146 | DOI | MR | Zbl

[19] Curi, Giovanni On Tarski’s fixed point theorem, Proc. Amer. Math. Soc., Volume 143 (2015) no. 10, pp. 4439-4455 | DOI | MR | Zbl

[20] Fourman, Michael; Grayson, Robin Formal spaces, The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981) (Stud. Logic Found. Math.), Volume 110, North-Holland, Amsterdam, 1982, pp. 107-122 | DOI | MR

[21] Hodges, Wilfried Krull implies Zorn, J. Lond. Math. Soc., Volume 19 (1979), pp. 285-287 | DOI | MR | Zbl

[22] Johnstone, Peter T. Stone Spaces., Cambridge Studies in Advanced Mathematics, 3, Cambridge University Press, 1982

[23] Johnstone, Peter T. Sketches of an Elephant: A Topos Theory Compendium. Vol. 2, Oxford Logic Guides, 44, The Clarendon Press Oxford University Press, Oxford, 2002

[24] Lombardi, Henri; Quitté, Claude Commutative Algebra: Constructive Methods. Finite Projective Modules, Algebra and Applications, 20, Springer Netherlands, Dordrecht, 2015

[25] Mulvey, Christopher J.; Wick-Pelletier, Joan A globalization of the Hahn–Banach theorem, Adv. Math., Volume 89 (1991), pp. 1-59 | DOI | MR | Zbl

[26] Negri, Sara Proof analysis beyond geometric theories: from rule systems to systems of rules, J. Logic Comput., Volume 26 (2014) no. 2, pp. 513-537 | DOI | MR | Zbl

[27] Negri, Sara; von Plato, Jan Cut Elimination in the Presence of Axioms, Bull. Symb. Log., Volume 4 (1998) no. 4, pp. 418-435 | DOI | MR | Zbl

[28] Prest, Mike Model Theory and Modules, London Mathematical Society Lecture Note Series, Cambridge University Press, 1988 | DOI

[29] Rinaldi, Davide; Wessel, Daniel Extension by conservation. Sikorski’s theorem, Log. Methods Comput. Sci., Volume 14 (2018) no. 4:8, pp. 1-17 | MR | Zbl

[30] Rinaldi, Davide; Wessel, Daniel Cut elimination for entailment relations, Arch. Math. Logic, Volume 58 (2019) no. 5–6, pp. 605-625 | DOI | MR | Zbl

[31] Rudin, Walter Functional Analysis, McGraw-Hill, New York, 1991

[32] Sambin, Giovanni Some points in formal topology, Theoret. Comput. Sci., Volume 305 (2003) no. 1–3, pp. 347-408 | MR | Zbl

[33] Schlagbauer, Konstantin; Schuster, Peter; Wessel, Daniel Der Satz von Hahn–Banach per Disjunktionselimination, Confluentes Math., Volume 11 (2019) no. 1, pp. 79-93 | DOI | Numdam | MR | Zbl

[34] Schuster, Peter; Wessel, Daniel Syntax for Semantics: Krull’s Maximal Ideal Theorem, Paul Lorenzen: Mathematician and Logician (Heinzmann, Gerhard; Wolters, Gereon, eds.) (Log. Epistemol. Unity Sci.), Volume 51, Springer, Cham, 2021, pp. 77-102 | MR | Zbl

[35] Scott, Dana Completeness and axiomatizability in many-valued logic, Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. California, Berkeley, Calif., 1971) (Henkin, Leon; Addison, John; Chang, C.C.; Craig, William; Scott, Dana; Vaught, Robert, eds.), Amer. Math. Soc., Providence, RI, 1974, pp. 411-435 | Zbl

[36] Sharpe, David William; Vámos, Peter Injective modules, Cambridge Tracts in Mathematics and Mathematical Physics, 62, Cambridge University Press, Cambridge, 1972

[37] Sikorski, Roman Boolean Algebras, Ergebnisse der Mathematik und ihrer Grenzgebiete. Band 25, Springer-Verlag Berlin Heidelberg, 1969 | DOI

[38] Wessel, Daniel A hybrid concept of entailment relation (2018) (Technical report)

Cité par Sources :