Semialgebraic partial equivalences #
The inverse of a semialgebraic partial equivalence is semialgebraic on its target. Its graph is obtained by exchanging input and output coordinates; projection closure supplies semialgebraicity of the target. In particular this applies to local inverses without requiring a globally defined semialgebraic inverse.
theorem
PartialEquiv.isSemialgebraicOn_symm
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommRing R]
[LinearOrder R]
[TauCeti.HasSemialgebraicProjections R]
[Finite σ]
(e : PartialEquiv (σ → R) (τ → R))
(he : TauCeti.IsSemialgebraicOn (↑e) e.source)
:
TauCeti.IsSemialgebraicOn (↑e.symm) e.target
A semialgebraic partial equivalence with finitely many input coordinates has a semialgebraic inverse on its target. No continuity assumption is needed.
@[simp]
theorem
PartialEquiv.isSemialgebraicOn_symm_iff
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommRing R]
[LinearOrder R]
[TauCeti.HasSemialgebraicProjections R]
[Finite σ]
[Finite τ]
(e : PartialEquiv (σ → R) (τ → R))
:
Semialgebraicity of a partial equivalence on its source is equivalent to semialgebraicity of its inverse on its target, in finite coordinate spaces.