A universal algorithm for Krull's theorem (Q2672666): Difference between revisions

From MaRDI portal
RedirectionBot (talk | contribs)
Removed claim: reviewed by (P1447): Item:Q592003
ReferenceBot (talk | contribs)
Changed an Item
 
(3 intermediate revisions by 3 users not shown)
Property / reviewed by
 
Property / reviewed by: Vladik Ya. Kreinovich / 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.ic.2021.104761 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W3157536011 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Interactive Learning-Based Realizability for Heyting Arithmetic with EM1 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Polynomials and radical ideals / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4944905 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Space of valuations / rank
 
Normal rank
Property / cites work
 
Property / cites work: A logical approach to abstract algebra / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lattice-ordered groups generated by an ordered group and regular systems of ideals / rank
 
Normal rank
Property / cites work
 
Property / cites work: Valuations and Dedekind's Prague theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Dynamical method in algebra: Effective Nullstellensätze / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4124833 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics / rank
 
Normal rank
Property / cites work
 
Property / cites work: On the Interpretation of Non-Finitist Proofs--Part I / rank
 
Normal rank
Property / cites work
 
Property / cites work: On the interpretation of non-finitist proofs–Part II / rank
 
Normal rank
Property / cites work
 
Property / cites work: Hidden constructions in abstract algebra. I: Integral dependance. / rank
 
Normal rank
Property / cites work
 
Property / cites work: Dynamical algebraic structures, pointfree topological spaces and Hilbert's program. (Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Commutative algebra: constructive methods. Finite projective modules. Translated from the French by Tania K. Roblot / rank
 
Normal rank
Property / cites work
 
Property / cites work: A course in constructive algebra / rank
 
Normal rank
Property / cites work
 
Property / cites work: A globalization of the Hahn-Banach theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof analysis beyond geometric theories: from rule systems to systems of rules / rank
 
Normal rank
Property / cites work
 
Property / cites work: Cut Elimination in the Presence of Axioms / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof-theoretical analysis of order relations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lorenzen’s Reshaping of Krull’s Fundamentalsatz for Integral Domains (1938–1953) / rank
 
Normal rank
Property / cites work
 
Property / cites work: Bar recursion over finite partial functions / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4986736 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The equivalence of bar recursion and open recursion / rank
 
Normal rank
Property / cites work
 
Property / cites work: Gödel's functional interpretation and the concept of learning / rank
 
Normal rank
Property / cites work
 
Property / cites work: On the computational content of Zorn's lemma / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5129941 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Well Quasi-orders and the Functional Interpretation / rank
 
Normal rank
Property / cites work
 
Property / cites work: An algorithmic approach to the existence of ideal objects in commutative algebra / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proving open properties by induction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nontrivial Uses of Trivial Rings / rank
 
Normal rank
Property / cites work
 
Property / cites work: A universal Krull-Lindenbaum theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION / rank
 
Normal rank
Property / cites work
 
Property / cites work: Eliminating disjunctions by disjunction elimination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4553278 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Cut elimination for entailment relations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3481701 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Hahn-Banach theorem by disjunction elimination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formal Zariski topology: Positivity and points / rank
 
Normal rank
Property / cites work
 
Property / cites work: Induction in Algebra: A First Case Study / rank
 
Normal rank
Property / cites work
 
Property / cites work: Induction in Algebra: a First Case Study / rank
 
Normal rank
Property / cites work
 
Property / cites work: The computational significance of Hausdorff's maximal chain principle / rank
 
Normal rank
Property / cites work
 
Property / cites work: Resolving finite indeterminacy / rank
 
Normal rank
Property / cites work
 
Property / cites work: Dynamic evaluation of integrity and the computational content of Krull's lemma / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4079581 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof mining and effective bounds in differential polynomial rings / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4220572 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5519134 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard / rank
 
Normal rank
Property / cites work
 
Property / cites work: Constructivism in mathematics. An introduction. Volume II / rank
 
Normal rank
Property / cites work
 
Property / cites work: Ordering groups constructively / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5109510 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Making the use of maximal ideals constructive / rank
 
Normal rank
Property / cites work
 
Property / cites work: Constructive commutative algebra. Projective modules over polynomial rings and dynamical Gröbner bases / rank
 
Normal rank

Latest revision as of 07:48, 29 July 2024

scientific article
Language Label Description Also known as
English
A universal algorithm for Krull's theorem
scientific article

    Statements

    A universal algorithm for Krull's theorem (English)
    0 references
    0 references
    13 June 2022
    0 references
    In analyzing integers, it is often useful to take into account that every integer can be uniquely represented as a product of primes. In many other commutative rings, it is not possible to select similar ``prime'' elements, but it turns out to be possible to have a similarly convenient representation by using additional ``ideal'' elements -- known as \textit{ideals}. Formally, an ideal is a set which is closed under addition and multiplication. In the integer case, an integer \(n\) corresponds to the ideal \(n{\mathbb Z}\) of all the integers which are divisible by \(n\). Ideals corresponding to a prime integer \(n\) have the property that if this ideal contains the product \(a\cdot b\), then it contains one of the factors; in the general case, this property is used as the definition of a \textit{prime ideal}. An ideal \(I\) is called \textit{radical} (from \textit{radix} -- the Latin word for root) if it is closed under taking roots, i.e., if whenever \(a^k\in I\) for some \(k\), we also have \(a\in I\). Integers have the following simple property: if a number \(r\) is divisible by all the prime factors of \(n\), then some power of \(r\) is divisible by \(n\); a similar property holds for subsets of \(\mathbb Z\). A natural generalization of this result to general commutative rings \(S\) is known as \textit{Krull's theorem}: for every set \(F\subseteq S\), if an element \(r\) is contained in all prime ideals containing \(F\), then \(r\) is also contained in the radical ideal generated by \(F\) -- i.e., in the intersection of all radical ideals containing \(F\). The usual proof of Krull's theorem is not constructive. The authors provide a constructive proof. Interestingly, this proof works not only for rings, but also in a more general context of an inference-type relation \(A\triangleright a\) between finite subsets \(A\subseteq S\) and elements \(a\in S\) -- namely, a relation for which \(\{a\}\triangleright a\), and for which \(B\triangleright b\) and \(A\cup \{b\}\triangleright a\) imply \(A\cup B\triangleright a\). The \textit{closure} \(\langle U\rangle\) is naturally defined as the set of all \(a\in S\) for which \(A\triangleright a\) for some \(A\subseteq S\). ``Closed'' sets -- i.e., sets for which \(\langle U\rangle=U\) -- are natural analogs of radical ideals and are thus called \textit{\(\triangleright\)-ideals}. Multiplication \(a\circ b\) is a binary operation for which \(A\cup \{a\}\triangleright c\) and \(B\cup \{b\} \triangleright c\) imply that \(A\cup B\cup \{a\circ b\}\triangleright c\). Prime \(\triangleright\)-deals are defined as usual. Then if we replace, in the formulation of Krull's theorem, radical ideals with \(\triangleright\)-ideals, we get a general result which is also true. The authors prove a constructive version of this general result. Specifically, they assume that the underlying set \(S\) is countable, \(S=\{s_0,s_1,\ldots\}\), and that the relation \(A\triangleright a\) has the form \(\exists x\,(A\triangleright_x a)\) for some ternary primitive recursive relation \(A\triangleright_x a\). As usual in constructive math, they interpret implication \(p\to q\) as the existence of an algorithm transforming a witness \(x\) for the condition \(p\) into a witness for the conclusion \(q\). The authors then provide an algorithm that inputs the witness for the condition of the generalized Krull's theorem and generates the witness for the theorem's conclusion. Several interesting particular cases are presented.
    0 references
    Krull's theorem
    0 references
    maximal ideals
    0 references
    program extraction
    0 references
    constructive algebra
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers