transcendental_supported_polynomial_aeval_X

English

Let i be an index, s a subset of indices, and f a polynomial over R such that f is transcendental over R. Then the multivariate aeval at X_i of f is transcendental over the subalgebra supported on s.

Русский

Пусть i — индекс, s — подмножество индексов, а f ∈ R[X] трансцендентально над R. Тогда aeval (X_i) f над подпольной структурой, поддерживаемой на s, является трансценентальным.

LaTeX

$$$$ (\forall i, s)(i \notin s) \to (hf : \text{Transcendental } R f) \Rightarrow \text{Transcendental } (\operatorname{supported} R s) (\operatorname{Polynomial.aeval}(X_i : \text{MvPolynomial } \sigma R) f). $$$$

Lean4

theorem transcendental_supported_polynomial_aeval_X {i : σ} {s : Set σ} (h : i ∉ s) {f : R[X]}
    (hf : Transcendental R f) : Transcendental (supported R s) (Polynomial.aeval (X i : MvPolynomial σ R) f) := by
  classical
  rw [transcendental_iff_injective] at hf ⊢
  let g := MvPolynomial.mapAlgHom (R := R) (σ := s) (Polynomial.aeval (R := R) f)
  replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
  let u :=
    (Subalgebra.val _).comp
          ((optionEquivRight R s).symm |>.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm) |>.trans
              (supportedEquivMvPolynomial _).symm).toAlgHom |>.comp
        g |>.comp
      ((optionEquivLeft R s).symm.trans (optionEquivRight R s)).toAlgHom
  let v :=
    ((Polynomial.aeval (R := supported R s) (Polynomial.aeval (X i : MvPolynomial σ R) f)).restrictScalars R).comp
      (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom
  replace hf : Function.Injective u :=
    by
    simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, Subalgebra.coe_val, AlgHom.coe_coe, AlgEquiv.coe_trans,
      Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
  have h1 :
    Polynomial.aeval (X i : MvPolynomial σ R) =
      ((Subalgebra.val _).comp (supportedEquivMvPolynomial _).symm.toAlgHom |>.comp
        (Polynomial.aeval (X ⟨i, s.mem_insert i⟩ : MvPolynomial (↑(insert i s)) R))) :=
    by ext1; simp
  have h2 : u = v := by
    simp only [u, v, g]
    ext1
    · ext1
      simp [Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq, optionEquivLeft_symm_apply]
    · simp [Set.subtypeInsertEquivOption, h1, optionEquivLeft_symm_apply]
  simpa only [h2, v, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, EquivLike.injective_comp,
    AlgHom.coe_restrictScalars'] using hf

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