Oka predicates

This file introduces the notion of oka predicates and standard results about them.

Main results

• Ideal.isPrime_of_maximal_not_isOka: if an ideal is maximal for not satisfying an oka predicate then it is prime.
• IsOka.forall_of_forall_prime: if all prime ideals of a ring satisfy an oka predicate, then all its ideals also satisfy the predicate.

References

• [stacks-project]: The Stacks project, tag 05K7
• [lam_reyes_2009]: Oka and Ako ideal families in commutative rings, 2009

structure Ideal.IsOka {R : Type u_1} [CommSemiring R] (P : Ideal R → Prop) : Prop

A predicate P : Ideal R → Prop over the ideals of a ring R is said to be Oka if R satisfies it (P ⊤) and whenever we have I : Ideal R, P (I.colon (span {a}) and P (I ⊔ span {a}) for some a : R then P I.

• top : P ⊤
• oka {I : Ideal R} {a : R} : P (I ⊔ span {a}) → P (Submodule.colon I (span {a})) → P I

theorem Ideal.IsOka.isPrime_of_maximal_not_isOka {R : Type u_1} [CommSemiring R] {P : Ideal R → Prop} (hP : IsOka P) {I : Ideal R} (hI : Maximal (fun (x : Ideal R) => ¬P x) I) : I.IsPrime

If an ideal is maximal for not satisfying an oka predicate then it is prime.

Stacks Tag 05KE

theorem Ideal.IsOka.forall_of_forall_prime_isOka {R : Type u_1} [CommSemiring R] {P : Ideal R → Prop} (hP : IsOka P) (hmax : (∃ (I : Ideal R), ¬P I) → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) => ¬P x) I) (hprime : ∀ (I : Ideal R), I.IsPrime → P I) (I : Ideal R) : P I

If all prime ideals of a ring satisfy an oka predicate, then all its ideals also satisfy the predicate. hmax is generaly obtained using Zorn's lemma.