English
The auxiliary sequence untiltAux extracts the nth component of a lift of the nth perfection component from O/p, with 0th term equal to 1 and the (n+1)th term given by a p^n-th power of a chosen lift.
Русский
Вспомогательная последовательность untiltAux извлекает n-ую компоненту из выбранного подъема из O/p, нулевая компонента равна единице, а (n+1)-ая равна p^n-ой степени лифта.
LaTeX
$${O : Type u} → [CommRing O] → {p : Nat} → [Fact (Nat.Prime p)] → [Fact (Not (IsUnit p.cast))] → PreTilt O p → Nat → O$$
Lean4
/-- The auxiliary sequence to define the untilt map. The `(n + 1)`-th term
is the `p^n`-th powers of arbitrary lifts in `O` of the `n`-th component
from the perfection of `O/p`.
-/
def untiltAux (x : PreTilt O p) (n : ℕ) : O :=
match n with
| 0 => 1
| n + 1 => (Quotient.out (coeff (ModP O p) _ n x)) ^ (p ^ n)
