Transport of a distance-image field along an ideal equality

Definition

Esgk_IrreduciblePlaneDistanceImageIdealTransport

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

algebraic-geometrycommutative-algebrafunction-fields

This constructs coordinate-ring and function-field algebra isomorphisms when two distance-image presentations have equal defining ideals.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_IrreduciblePlaneDistanceImageField
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 distanceImageCoordinateRingAlgEquivOfIdealEq
    (C₁ C₂ : IrreduciblePlanePolynomial F) (r₁ r₂ : F)
    (hIdeal : C₁.distanceImageIdeal r₁ = C₂.distanceImageIdeal r₂) :
    C₁.DistanceImageCoordinateRing r₁ ≃ₐ[F]
      C₂.DistanceImageCoordinateRing r₂ :=
  Ideal.quotientEquivAlgOfEq F hIdeal


noncomputable def distanceImageFunctionFieldAlgEquivOfIdealEq
    (C₁ C₂ : IrreduciblePlanePolynomial F) (r₁ r₂ : F)
    (hIdeal : C₁.distanceImageIdeal r₁ = C₂.distanceImageIdeal r₂) :
    C₁.DistanceImageFunctionField r₁ ≃ₐ[F]
      C₂.DistanceImageFunctionField r₂ :=
  IsFractionRing.algEquivOfAlgEquiv
    (distanceImageCoordinateRingAlgEquivOfIdealEq C₁ C₂ r₁ r₂ hIdeal)


end IrreduciblePlanePolynomial

end Esgk

View graph