@[reducible, inline]
abbrev
RegularFunction
(k : Type u_1)
[CommRing k]
(σ : Type u_2)
(τ : Type u_3)
:
Type (max (max u_3 u_1) u_2)
Implicitly use σ as an index set and k as coefficient ring.
Equations
- RegularFunction k σ τ = (τ → MvPolynomial σ k)
Instances For
noncomputable def
RegularFunction.Jacobian
{k : Type u_1}
[CommRing k]
{σ : Type u_2}
{τ : Type u_3}
(F : RegularFunction k σ τ)
:
Matrix σ τ (MvPolynomial σ k)
The Jacobian of a vector valued polynomial function, viewed as a polynomial.
Equations
- F.Jacobian = Matrix.of fun (i : σ) (j : τ) => (MvPolynomial.pderiv i) (F j)
Instances For
noncomputable def
RegularFunction.comp
{k : Type u_1}
[CommRing k]
{σ : Type u_2}
{τ : Type u_3}
{ι : Type u_4}
(F : RegularFunction k σ τ)
(G : RegularFunction k τ ι)
:
RegularFunction k σ ι
The composition of two vector valued polynomial functions.
Equations
- F.comp G i = (MvPolynomial.bind₁ F) (G i)
Instances For
theorem
jacobian_conjecture
{k : Type u_1}
[Field k]
[CharZero k]
{σ : Type u_2}
[Fintype σ]
(F : RegularFunction k σ σ)
(H : IsUnit F.Jacobian.det)
:
∃ (G : RegularFunction k σ σ), G.comp F = RegularFunction.id✝ k σ ∧ F.comp G = RegularFunction.id✝ k σ
The Jacobian Conjecture: any regular function
(i.e. vector valued polynomial function from) kⁿ → kᵐ
whose Jacobian is a non-zero constant has an inverse that
is given by a regular function, where k is a field of characteristic 0
noncomputable def
RegularFunction.aeval
{k : Type u_1}
[Field k]
{σ : Type u_2}
{τ : Type u_3}
{S₁ : Type u_5}
[CommSemiring S₁]
[Algebra k S₁]
(F : RegularFunction k σ τ)
:
(σ → S₁) → τ → S₁
The evaluation of a regular function f over k at some point a
with coordinates in some algebra over k
Equations
- F.aeval a t = (MvPolynomial.aeval a) (F t)
Instances For
theorem
comp_aeval
{k : Type u_1}
[Field k]
{σ : Type u_2}
{τ : Type u_3}
{ι : Type u_4}
(F : RegularFunction k σ τ)
(G : RegularFunction k τ ι)
(a : σ → k)
:
aeval is compatible with composition of regular functions