- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Computes the Characteristic Set of a polynomial list \(l\).
Algorithm:
Set \(l_0 = l\).
Compute \(BS = BasicSet(l)\).
Compute remainders \(RS\) of \(l \setminus BS\) with respect to \(BS\).
If \(RS = \emptyset \), \(BS\) is the characteristic set.
If not, let \(l = l₀ ++ RS ++ BS\) and go to step 2.
Termination is guaranteed by the well-ordering of ranks.
Computes the Standard Basic Set of a list of polynomials.
The algorithm works by:
Sort the list and let \(BS = \emptyset \).
Pick the first (minimal) element \(B\) in the list.
Append \(B\) to the tail of the current basic set \(BS\).
Filter the remaining list to keep only elements reduced w.r.t. the new \(BS\) and go to step 2.
"S.takeConcat p" tries to construct a new Triangulated Set by taking a prefix of \(S\) and appending \(p\).
If \(p\) fits naturally at the end of \(S\), it behaves like "S.concat p".
If \(p\) conflicts with some element in \(S\) (in terms of class order), "takeConcat" finds the first element in \(S\) that has a higher or equal class than \(p\), truncates \(S\) before that element, and appends \(p\).
The rank of a Triangulated Set is a lexicographic sequence of ranks of its polynomials. More intuitively, \(S {\lt} T\) if one of the following two occurs:
There exists some \(k {\lt} S.length\) such that \(S_0 \sim T_0, S_1 \sim T_1, ..., S_{k-1} \sim T_{k-1}\), while \(S_k {\lt} T_k\).
\(S.length {\gt} T.length\) and \(\forall i {\lt} T.length, S_i \sim T_i\).