Prime ideals #
Main definitions #
Throughout this file, P
is at least a preorder, but some sections require more
structure, such as a bottom element, a top element, or a join-semilattice structure.
Order.Ideal.PrimePair
: A pair of anOrder.Ideal
and anOrder.PFilter
which form a partition ofP
. This is useful as giving the data of a prime ideal is the same as giving the data of a prime filter.Order.Ideal.IsPrime
: a predicate for prime ideals. Dual to the notion of a prime filter.Order.PFilter.IsPrime
: a predicate for prime filters. Dual to the notion of a prime ideal.
References #
Tags #
ideal, prime
A pair of an Order.Ideal
and an Order.PFilter
which form a partition of P
.
- I : Order.Ideal P
- F : Order.PFilter P
- isCompl_I_F : IsCompl ↑self.I ↑self.F
Instances For
theorem
Order.Ideal.PrimePair.isCompl_I_F
{P : Type u_2}
[Preorder P]
(self : Order.Ideal.PrimePair P)
:
IsCompl ↑self.I ↑self.F
theorem
Order.Ideal.PrimePair.compl_I_eq_F
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
theorem
Order.Ideal.PrimePair.compl_F_eq_I
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
theorem
Order.Ideal.PrimePair.I_isProper
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
IF.I.IsProper
theorem
Order.Ideal.PrimePair.disjoint
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
Disjoint ↑IF.I ↑IF.F
theorem
Order.Ideal.PrimePair.I_union_F
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
theorem
Order.Ideal.PrimePair.F_union_I
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
theorem
Order.Ideal.isPrime_iff
{P : Type u_1}
[Preorder P]
(I : Order.Ideal P)
:
I.IsPrime ↔ I.IsProper ∧ Order.IsPFilter (↑I)ᶜ
class
Order.Ideal.IsPrime
{P : Type u_1}
[Preorder P]
(I : Order.Ideal P)
extends
Order.Ideal.IsProper
:
An ideal I
is prime if its complement is a filter.
- ne_univ : ↑I ≠ Set.univ
- compl_filter : Order.IsPFilter (↑I)ᶜ
Instances
theorem
Order.Ideal.IsPrime.compl_filter
{P : Type u_1}
:
∀ {inst : Preorder P} {I : Order.Ideal P} [self : I.IsPrime], Order.IsPFilter (↑I)ᶜ
def
Order.Ideal.IsPrime.toPrimePair
{P : Type u_1}
[Preorder P]
{I : Order.Ideal P}
(h : I.IsPrime)
:
Create an element of type Order.Ideal.PrimePair
from an ideal satisfying the predicate
Order.Ideal.IsPrime
.
Equations
- h.toPrimePair = { I := I, F := ⋯.toPFilter, isCompl_I_F := ⋯ }
Instances For
theorem
Order.Ideal.PrimePair.I_isPrime
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
IF.I.IsPrime
theorem
Order.Ideal.IsPrime.mem_or_mem
{P : Type u_1}
[SemilatticeInf P]
{I : Order.Ideal P}
(hI : I.IsPrime)
{x : P}
{y : P}
:
theorem
Order.Ideal.IsPrime.of_mem_or_mem
{P : Type u_1}
[SemilatticeInf P]
{I : Order.Ideal P}
[I.IsProper]
(hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I)
:
I.IsPrime
theorem
Order.Ideal.isPrime_iff_mem_or_mem
{P : Type u_1}
[SemilatticeInf P]
{I : Order.Ideal P}
[I.IsProper]
:
@[instance 100]
instance
Order.Ideal.IsMaximal.isPrime
{P : Type u_1}
[DistribLattice P]
{I : Order.Ideal P}
[I.IsMaximal]
:
I.IsPrime
Equations
- ⋯ = ⋯
theorem
Order.Ideal.IsPrime.mem_or_compl_mem
{P : Type u_1}
[BooleanAlgebra P]
{x : P}
{I : Order.Ideal P}
(hI : I.IsPrime)
:
theorem
Order.Ideal.IsPrime.mem_compl_of_not_mem
{P : Type u_1}
[BooleanAlgebra P]
{x : P}
{I : Order.Ideal P}
(hI : I.IsPrime)
(hxnI : x ∉ I)
:
theorem
Order.Ideal.isPrime_of_mem_or_compl_mem
{P : Type u_1}
[BooleanAlgebra P]
{I : Order.Ideal P}
[I.IsProper]
(h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I)
:
I.IsPrime
theorem
Order.Ideal.isPrime_iff_mem_or_compl_mem
{P : Type u_1}
[BooleanAlgebra P]
{I : Order.Ideal P}
[I.IsProper]
:
@[instance 100]
instance
Order.Ideal.IsPrime.isMaximal
{P : Type u_1}
[BooleanAlgebra P]
{I : Order.Ideal P}
[I.IsPrime]
:
I.IsMaximal
Equations
- ⋯ = ⋯
theorem
Order.PFilter.isPrime_iff
{P : Type u_1}
[Preorder P]
(F : Order.PFilter P)
:
F.IsPrime ↔ Order.IsIdeal (↑F)ᶜ
theorem
Order.PFilter.IsPrime.compl_ideal
{P : Type u_1}
:
∀ {inst : Preorder P} {F : Order.PFilter P} [self : F.IsPrime], Order.IsIdeal (↑F)ᶜ
def
Order.PFilter.IsPrime.toPrimePair
{P : Type u_1}
[Preorder P]
{F : Order.PFilter P}
(h : F.IsPrime)
:
Create an element of type Order.Ideal.PrimePair
from a filter satisfying the predicate
Order.PFilter.IsPrime
.
Equations
- h.toPrimePair = { I := ⋯.toIdeal, F := F, isCompl_I_F := ⋯ }
Instances For
theorem
Order.Ideal.PrimePair.F_isPrime
{P : Type u_1}
[Preorder P]
(IF : Order.Ideal.PrimePair P)
:
IF.F.IsPrime