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} [CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ 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.

Equations

• MvPolynomial.comap f x i = (MvPolynomial.aeval x) (f (MvPolynomial.X i))

@[simp]

theorem MvPolynomial.comap_apply {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (x : τ → R) (i : σ) : MvPolynomial.comap f x i = (MvPolynomial.aeval x) (f (MvPolynomial.X i))

@[simp]

theorem MvPolynomial.comap_id_apply {σ : Type u_1} {R : Type u_4} [CommSemiring R] (x : σ → R) : MvPolynomial.comap (AlgHom.id R (MvPolynomial σ R)) x = x

theorem MvPolynomial.comap_id (σ : Type u_1) (R : Type u_4) [CommSemiring R] : MvPolynomial.comap (AlgHom.id R (MvPolynomial σ R)) = id

theorem MvPolynomial.comap_comp_apply {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [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)

theorem MvPolynomial.comap_comp {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R) : MvPolynomial.comap (g.comp f) = MvPolynomial.comap f ∘ MvPolynomial.comap g

theorem MvPolynomial.comap_eq_id_of_eq_id {σ : Type u_1} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (hf : ∀ (φ : MvPolynomial σ R), f φ = φ) (x : σ → R) : MvPolynomial.comap f x = x

theorem MvPolynomial.comap_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (x : τ → R) : MvPolynomial.comap (MvPolynomial.rename f) x = x ∘ f

noncomputable def MvPolynomial.comapEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ 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

• MvPolynomial.comapEquiv f = { toFun := MvPolynomial.comap ↑f, invFun := MvPolynomial.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MvPolynomial.comapEquiv_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R) : ⇑(MvPolynomial.comapEquiv f) = MvPolynomial.comap ↑f

@[simp]

theorem MvPolynomial.comapEquiv_symm_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R) : ⇑(MvPolynomial.comapEquiv f).symm = MvPolynomial.comap ↑f.symm