Polynomial automorphism

IsPolynomialAutomorphismdef

A polynomial automorphism is a RegularFunction with a two-sided inverse that is itself a regular function. This is strictly stronger than being bijective on points: the inverse must be given by polynomials.

def IsPolynomialAutomorphism {k σ : Type*} [CommRing k]
    (F : RegularFunction k σ σ) : Prop :=
  ∃ G : RegularFunction k σ σ,
    G.comp F = RegularFunction.id k σ ∧ F.comp G = RegularFunction.id k σ

Builds on

Regular function

Used by

Jacobian conjecture

import Conjectura.Defs.Mathematics.AlgebraicGeometry.PolynomialAutomorphism · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits