exists_rename_eq_of_vars_subset_range

English

If p.vars is contained in the range of f and f is injective, there exists q with rename f q = p.

Русский

Если множество переменных p находится внутри диапазона отображения f и f инъективно, существует q такой, что rename f q = p.

LaTeX

$$$ \exists q, rename\ f\ q = p $$$

Lean4

theorem exists_rename_eq_of_vars_subset_range (p : MvPolynomial σ R) (f : τ → σ) (hfi : Injective f)
    (hf : ↑p.vars ⊆ Set.range f) : ∃ q : MvPolynomial τ R, rename f q = p :=
  ⟨aeval (fun i : σ => Option.elim' 0 X <| partialInv f i) p,
    by
    change (rename f).toRingHom.comp _ p = RingHom.id _ p
    refine hom_congr_vars ?_ ?_ ?_
    · ext1
      simp [algebraMap_eq]
    · intro i hip _
      rcases hf hip with ⟨i, rfl⟩
      simp [partialInv_left hfi]
    · rfl⟩

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