Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Polynomial automorphism

Conjectura.Defs.Mathematics.AlgebraicGeometry.PolynomialAutomorphism

/-
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
-/
import Conjectura.Defs.Mathematics.AlgebraicGeometry.RegularFunction

/-! # Polynomial automorphism

## Source

Adapted for Conjectura from [formal-conjectures](https://github.com/google-deepmind/formal-conjectures) (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.
-/

namespace Conjectura.AlgebraicGeometry

/-- 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 σ

end Conjectura.AlgebraicGeometry