MvPolynomial.comap_comp_apply

theorem MvPolynomial.comap_comp_apply : ∀ {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [inst : CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R) (x : υ → R), MvPolynomial.comap (g.comp f) x = MvPolynomial.comap f (MvPolynomial.comap g x)

The theorem `MvPolynomial.comap_comp_apply` states that for any three types `σ`, `τ`, and `υ`, and for any type `R` equipped with a commutative semiring structure, given two algebra homomorphisms `f` from multivariate polynomials over `σ` and `R` to multivariate polynomials over `τ` and `R`, and `g` from multivariate polynomials over `τ` and `R` to multivariate polynomials over `υ` and `R`, and a variable evaluation `x : υ → R`, then the comap of the composition of `g` and `f`, evaluated at `x`, is equal to the comap of `f` evaluated at the comap of `g` evaluated at `x`. In other words, the operation of taking the comap (preimage under a function) of a composition of two functions is the same as composing the comaps of the two functions, an instance of the principle that "the preimage of a composition is the composition of the preimages".

More concisely: For any commutative semirings R, and multivariate polynomial homomorphisms f : R[σ] -> R[τ] and g : R[τ] -> R[υ], the composition of their comaps (preimages under the functions) evaluated at an evaluation map x : υ -> R is equal to the comap of their composition evaluated at x.