Normalization-ring isomorphism from a function-field isomorphism

Definition

Esgk_IrreduciblePlaneAffineNormalizationAutomorphism

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycommutative-algebrafunction-fields

This constructs the induced algebra isomorphism between affine normalization rings from an algebra isomorphism of their function fields.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_IntegralClosureAutomorphism
import Definitions.Def_Esgk_IrreduciblePlaneAffineNormalization
import Definitions.Def_Esgk_IrreduciblePlaneFunctionField
import Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


noncomputable section

namespace Esgk

namespace IrreduciblePlanePolynomial

variable {F : Type*} [Field F]


noncomputable def affineNormalizationRingAlgEquivOfFunctionFieldAlgEquiv
    (C : IrreduciblePlanePolynomial F)
    (e : C.FunctionField ≃ₐ[F] C.FunctionField)
    (hforward : ∀ a : C.CoordinateRing,
      IsIntegral C.CoordinateRing
        (e (algebraMap C.CoordinateRing C.FunctionField a)))
    (hbackward : ∀ a : C.CoordinateRing,
      IsIntegral C.CoordinateRing
        (e.symm (algebraMap C.CoordinateRing C.FunctionField a))) :
    C.affineNormalizationRing ≃ₐ[F] C.affineNormalizationRing :=
  integralClosureAlgEquiv e hforward hbackward


end IrreduciblePlanePolynomial

end Esgk

View graph