baseChange — Mathlib

English

If f is surjective, then the base change of f along a polynomial variable map is surjective.

Русский

Если f сюръективен, то базовое изменение f вдоль отображения по переменной многочлена сюръективно.

LaTeX

$$$\\text{Surjective}(f) \\Rightarrow \\text{Surjective}(\\text{TensorProduct.map}(\\mathrm{id}, f))$$$

Lean4

instance baseChange [hfa : FiniteType R A] : Algebra.FiniteType B (B ⊗[R] A) :=
  by
  rw [iff_quotient_mvPolynomial''] at *
  obtain ⟨n, f, hf⟩ := hfa
  let g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := Algebra.TensorProduct.map (AlgHom.id B B) f
  have : Function.Surjective g := baseChangeAux_surj B hf
  use n, AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom
  simpa

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