English
Under suitable hypotheses, liftAux defines a map L → M by sending x ∈ L to a certain p-th root image via i and j.
Русский
При определённых гипотезах liftAux задаёт отображение L → M, отправляющее элемент x в соответствующее p-й корень через i и j.
LaTeX
$$liftAux : L → M; \\text{defined by } x \\mapsto (iterateFrobeniusEquiv M p n)^{-1}(j(y)) \\text{ for suitable } (n,y) \\text{ with } i(y)=x^{p^n}$$
Lean4
/-- If `i : K →+* L` and `j : K →+* M` are ring homomorphisms of characteristic `p` rings, such that
`i` is `p`-radical (in fact only the `IsPRadical.pow_mem` is required) and `M` is a perfect ring,
then one can define a map `L → M` which maps an element `x` of `L` to `y ^ (p ^ -n)` if
`x ^ (p ^ n)` is equal to some element `y` of `K`. -/
def liftAux (x : L) : M :=
(iterateFrobeniusEquiv M p (Classical.choose (lift_aux i p x)).1).symm (j (Classical.choose (lift_aux i p x)).2)
