comap_comp_apply — Mathlib

English

For any map f : σ → τ and any x : τ → R, comap (rename f) x equals x ∘ f.

Русский

Для отображения f: σ → τ и любой x: τ → R, comap (rename f) x = x ∘ f.

LaTeX

$$$\\operatorname{comap}(\\mathrm{rename}\\, f)\, x = x \\circ f$$$

Lean4

theorem comap_comp_apply (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R)
    (x : υ → R) : comap (g.comp f) x = comap f (comap g x) :=
  by
  funext i
  trans aeval x (aeval (fun i => g (X i)) (f (X i)))
  · apply eval₂Hom_congr rfl rfl
    rw [AlgHom.comp_apply]
    suffices g = aeval fun i => g (X i) by rw [← this]
    exact aeval_unique g
  · simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom]
    refine eval₂Hom_congr ?_ rfl rfl
    ext r
    apply aeval_C

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