Lean4
/-- If `i : K →+* L` and `j : K →+* M` are ring homomorphisms of characteristic `p` rings, such that
`i` is `p`-radical, and `M` is a perfect ring, then `PerfectRing.liftAux`
is a ring homomorphism. This is similar to `IsAlgClosed.lift` and `IsSepClosed.lift`. -/
def lift : L →+* M where
toFun := liftAux i j p
map_one' := by simp [liftAux_apply i j p 1 0 1 (by rw [one_pow, map_one])]
map_mul' x1
x2 := by
obtain ⟨n1, y1, h1⟩ := IsPRadical.pow_mem i p x1
obtain ⟨n2, y2, h2⟩ := IsPRadical.pow_mem i p x2
rw [liftAux_apply i j p _ _ _ h1, liftAux_apply i j p _ _ _ h2,
liftAux_apply i j p (x1 * x2) (n1 + n2) (y1 ^ p ^ n2 * y2 ^ p ^ n1)
(by rw [map_mul, map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add, add_comm n2, mul_pow]),
map_mul, map_pow, map_pow, map_mul, ← iterateFrobeniusEquiv_def]
nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]
rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply, ← iterateFrobeniusEquiv_def,
RingEquiv.symm_apply_apply]
map_zero' := by simp [liftAux_apply i j p 0 0 0 (by rw [pow_zero, pow_one, map_zero])]
map_add' x1
x2 := by
obtain ⟨n1, y1, h1⟩ := IsPRadical.pow_mem i p x1
obtain ⟨n2, y2, h2⟩ := IsPRadical.pow_mem i p x2
rw [liftAux_apply i j p _ _ _ h1, liftAux_apply i j p _ _ _ h2,
liftAux_apply i j p (x1 + x2) (n1 + n2) (y1 ^ p ^ n2 + y2 ^ p ^ n1)
(by
rw [map_add, map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add, add_comm n2,
add_pow_expChar_pow]),
map_add, map_pow, map_pow, map_add, ← iterateFrobeniusEquiv_def]
nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]
rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply, ← iterateFrobeniusEquiv_def,
RingEquiv.symm_apply_apply]
