English
A Frobenius element at Q induces a Frobenius endomorphism on the quotient S/Q; in particular, there is a natural structure of an R/under-R-algebra on S/Q preserved by this induced Frobenius.
Русский
Фробениус-элемент по Q индуцирует на частном кольце S/Q образ Фробениуса; в частности, на S/Q сохраняется структура R/under R-алгебры под этим индуцированным Фробениусом.
LaTeX
$$There exists an algebra homomorphism $\operatorname{restrict}: (S/Q) \to (S/Q)$ over $R/_{under R}R$ that is Frobenius at $Q$ on the quotient.$$
Lean4
/-- A Frobenius element at `Q` restricts to the Frobenius map on `S ⧸ Q`. -/
def restrict : S ⧸ Q →ₐ[R ⧸ Q.under R] S ⧸ Q
where
toRingHom := Ideal.quotientMap Q φ H.le_comap
commutes'
x := by
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
exact DFunLike.congr_arg (Ideal.Quotient.mk Q) (φ.commutes x)
