Oka predicates

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

Main results

• Ideal.IsOka.isPrime_of_maximal_not: if an ideal is maximal for not satisfying an Oka predicate, then it is prime.
• Ideal.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

• [SPA18]: The Stacks project, tag 05K7
• [LR09]: 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 {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.

theorem Ideal.IsOka.forall_of_forall_prime {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 a ring R verify:

1. All prime ideals of R satisfy an Oka predicate P.
2. One ideal not satisfying P implies that there is an ideal maximal for not satisfying P.

Then all the ideals of R satisfy P.

theorem Ideal.IsOka.forall_of_forall_prime' {R : Type u_1} [CommSemiring R] {P : Ideal R → Prop} (hP : IsOka P) (hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) => x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I) (hprime : ∀ (I : Ideal R), I.IsPrime → P I) (I : Ideal R) : P I

A variant of forall_of_forall_prime with a different spelling of the condition hmax.