# Documentation

Mathlib.Data.MvPolynomial.Comap

# comap operation on MvPolynomial#

This file defines the comap function on MvPolynomial.

MvPolynomial.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* [CommSemiring R] (the coefficients)

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

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

Instances For
@[simp]
theorem MvPolynomial.comap_apply {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : →ₐ[R] ) (x : τR) (i : σ) :
= ↑() (f ())
@[simp]
theorem MvPolynomial.comap_id_apply {σ : Type u_1} {R : Type u_4} [] (x : σR) :
theorem MvPolynomial.comap_id (σ : Type u_1) (R : Type u_4) [] :
theorem MvPolynomial.comap_comp_apply {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [] (f : →ₐ[R] ) (g : →ₐ[R] ) (x : υR) :
=
theorem MvPolynomial.comap_comp {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [] (f : →ₐ[R] ) (g : →ₐ[R] ) :
theorem MvPolynomial.comap_eq_id_of_eq_id {σ : Type u_1} {R : Type u_4} [] (f : →ₐ[R] ) (hf : ∀ (φ : ), f φ = φ) (x : σR) :
= x
theorem MvPolynomial.comap_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (x : τR) :
= x f
noncomputable def MvPolynomial.comapEquiv {σ : 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.

Instances For
@[simp]
theorem MvPolynomial.comapEquiv_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : ≃ₐ[R] ) :
@[simp]
theorem MvPolynomial.comapEquiv_symm_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : ≃ₐ[R] ) :
().symm =