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:
σ : Type*(indexing the variables)R : Type*[comm_semiring R](the coefficients)
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)
(a : τ → R)
(a_1 : σ) :
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
- mv_polynomial.comap f = λ (x : τ → R) (i : σ), ⇑(mv_polynomial.aeval x) (⇑f (mv_polynomial.X i))
@[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 : σ) :
mv_polynomial.comap f x i = ⇑(mv_polynomial.aeval x) (⇑f (mv_polynomial.X i))
@[simp]
theorem
mv_polynomial.comap_id_apply
{σ : Type u_1}
{R : Type u_4}
[comm_semiring R]
(x : σ → R) :
mv_polynomial.comap (alg_hom.id R (mv_polynomial σ R)) x = x
theorem
mv_polynomial.comap_id
(σ : Type u_1)
(R : Type u_4)
[comm_semiring R] :
mv_polynomial.comap (alg_hom.id R (mv_polynomial σ R)) = id
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) :
mv_polynomial.comap (g.comp f) x = mv_polynomial.comap f (mv_polynomial.comap g x)
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) :
mv_polynomial.comap f x = x
theorem
mv_polynomial.comap_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(x : τ → R) :
mv_polynomial.comap (mv_polynomial.rename f) x = x ∘ f
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
- mv_polynomial.comap_equiv f = {to_fun := mv_polynomial.comap ↑f, inv_fun := mv_polynomial.comap ↑(f.symm), left_inv := _, right_inv := _}
@[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) :
⇑((mv_polynomial.comap_equiv f).symm) = mv_polynomial.comap ↑(f.symm)