# mathlib3documentation

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:

• σ : Type* (indexing the variables)

• R : Type* [comm_semiring R] (the coefficients)

noncomputable def mv_polynomial.comap {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : →ₐ[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} (f : →ₐ[R] ) (x : τ R) (i : σ) :
@[simp]
theorem mv_polynomial.comap_id_apply {σ : Type u_1} {R : Type u_4} (x : σ R) :
theorem mv_polynomial.comap_id (σ : Type u_1) (R : Type u_4)  :
theorem mv_polynomial.comap_comp_apply {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} (f : →ₐ[R] ) (g : →ₐ[R] ) (x : υ R) :
theorem mv_polynomial.comap_comp {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} (f : →ₐ[R] ) (g : →ₐ[R] ) :
theorem mv_polynomial.comap_eq_id_of_eq_id {σ : Type u_1} {R : Type u_4} (f : →ₐ[R] ) (hf : (φ : R), f φ = φ) (x : σ R) :
= x
theorem mv_polynomial.comap_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ τ) (x : τ R) :
= x f
noncomputable def mv_polynomial.comap_equiv {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : ≃ₐ[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
@[simp]
theorem mv_polynomial.comap_equiv_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : ≃ₐ[R] ) :
@[simp]
theorem mv_polynomial.comap_equiv_symm_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : ≃ₐ[R] ) :