mathlib documentation

data.mv_polynomial.comap

comap operation on mv_polynomial

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:

def mv_polynomial.comap {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] :
(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_id (σ : Type u_1) (R : Type u_4) [comm_semiring 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_comp {σ : 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) :

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) :

def mv_polynomial.comap_equiv {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] :
(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
@[simp]
theorem mv_polynomial.comap_equiv_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R ≃ₐ[R] mv_polynomial τ R) :

@[simp]
theorem mv_polynomial.comap_equiv_symm_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : mv_polynomial σ R ≃ₐ[R] mv_polynomial τ R) :