ofAlgHom — Mathlib

English

From an algebra hom f: MvPolynomial I R →ₐ[R] S with surjectivity, build a Generators R S I.

Русский

По сюръективному алгебровому отображению f: MvPolynomial I R →ₐ[R] S строим Generators R S I.

LaTeX

$$ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective f) : Algebra.Generators R S I$$

Lean4

/-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective. -/
noncomputable def ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective f) : Generators R S I :=
  ofSurjective (f ∘ X) (by rwa [show aeval (f ∘ X) = f by ext; simp])

Похожие утверждения