Towards formal Baer criteria

Daniel Misselbeck-Wessel; Davide Rinaldi

doi:10.5802/cml.82

Daniel Misselbeck-Wessel ¹ ; Davide Rinaldi

¹ 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.

Résumé

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 : 2020-08-25
Révisé le : 2022-04-25
Accepté le : 2022-08-16
Publié le : 2022-11-21

DOI : 10.5802/cml.82

Classification : 13C11, 06D22, 03F65
Mots clés : Injective module, Baer’s criterion, point-free topology, inductive definition, constructive algebra

Affiliations des auteurs :

Daniel Misselbeck-Wessel ¹ ; Davide Rinaldi

¹ Dipartimento di Informatica, Università degli Studi di Verona, Strada le Grazie 15, 37134 Verona, Italy

Licence :

CC-BY-NC-ND 4.0

Droits d'auteur : Les auteurs conservent leurs droits

@article{CML_2022__14_1_49_0,
     author = {Daniel Misselbeck-Wessel and Davide Rinaldi},
     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 = {https://cml.centre-mersenne.org/articles/10.5802/cml.82/}
}

TY  - JOUR
AU  - Daniel Misselbeck-Wessel
AU  - Davide Rinaldi
TI  - Towards formal Baer criteria
JO  - Confluentes Mathematici
PY  - 2022
SP  - 49
EP  - 63
VL  - 14
IS  - 1
PB  - Institut Camille Jordan
UR  - https://cml.centre-mersenne.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 Daniel Misselbeck-Wessel
%A Davide Rinaldi
%T Towards formal Baer criteria
%J Confluentes Mathematici
%D 2022
%P 49-63
%V 14
%N 1
%I Institut Camille Jordan
%U https://cml.centre-mersenne.org/articles/10.5802/cml.82/
%R 10.5802/cml.82
%G en
%F CML_2022__14_1_49_0

Daniel Misselbeck-Wessel; Davide Rinaldi. Towards formal Baer criteria. Confluentes Mathematici, Tome 14 (2022) no. 1, pp. 49-63. doi : 10.5802/cml.82. https://cml.centre-mersenne.org/articles/10.5802/cml.82/

Bibliographie
Cité par

[1] Peter Aczel 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] Peter Aczel; Michael Rathjen Notes on Constructive Set Theory (2000) (Report No. 40) (Technical report)

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

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

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

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

[7] J. L. Bell 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] Andreas Blass Injectivity, projectivity, and the axiom of choice, Trans. Amer. Math. Soc., Volume 255 (1979), pp. 31-59 | MR | Zbl

[9] Jan Cederquist; Thierry Coquand 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 (Samuel R. Buss; Petr Hájek; Pavel Pudlák, eds.) (Lect. Notes Logic), Volume 13, A. K. Peters, Natick, MA, 2000, pp. 127-139 | MR | Zbl

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

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

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

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

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

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

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

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

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

[20] Michael Fourman; Robin Grayson 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] Wilfried Hodges Krull implies Zorn, J. Lond. Math. Soc., Volume 19 (1979), pp. 285-287 | DOI | MR | Zbl

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Cité par Sources :