mathlib3 documentation

data.mv_polynomial.comap

comap operation on mv_polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the comap function on mv_polynomial.

mv_polynomial.comap is a low-tech example of a map of "algebraic varieties," modulo the fact that mathlib does not yet define varieties.

Notation #

As in other polynomial files, we typically use the notation:

noncomputable def mv_polynomial.comap {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R →ₐ[R] mv_polynomial τ R) :
R) σ R

Given an algebra hom f : mv_polynomial σ R →ₐ[R] mv_polynomial τ R and a variable evaluation v : τ → R, comap f v produces a variable evaluation σ → R.

Equations
@[simp]
theorem mv_polynomial.comap_apply {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R →ₐ[R] mv_polynomial τ R) (x : τ R) (i : σ) :
@[simp]
theorem mv_polynomial.comap_id_apply {σ : Type u_1} {R : Type u_4} [comm_semiring R] (x : σ R) :
theorem mv_polynomial.comap_comp_apply {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R →ₐ[R] mv_polynomial τ R) (g : mv_polynomial τ R →ₐ[R] mv_polynomial υ R) (x : υ R) :
theorem mv_polynomial.comap_eq_id_of_eq_id {σ : Type u_1} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R →ₐ[R] mv_polynomial σ R) (hf : (φ : mv_polynomial σ R), f φ = φ) (x : σ R) :
theorem mv_polynomial.comap_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ τ) (x : τ R) :
noncomputable def mv_polynomial.comap_equiv {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R ≃ₐ[R] mv_polynomial τ R) :
R) R)

If two polynomial types over the same coefficient ring R are equivalent, there is a bijection between the types of functions from their variable types to R.

Equations