Distance-generated fields and reflection symmetry

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_IrreduciblePlaneFunctionField
import Definitions.Def_Esgk_SelfCurveReflectionInvariance
import Definitions.Def_Esgk_SelfCurveTwoAnchorFunctionField
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
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

open PachDeZeeuw.Algebraic

namespace IrreduciblePlanePolynomial


theorem associated_xAxisReflectionPolynomial_of_secondCoordinate_not_mem
    (C : IrreduciblePlanePolynomial ℝ) {r : ℝ} (hr : r ≠ 0)
    (hy : C.coordinate 1 ∉
      Esgk.twoAnchorDistanceField (C.coordinate 0) (C.coordinate 1) r) :
    Associated C.polynomial (xAxisReflectionPolynomialHom C.polynomial) := by
  obtain ⟨σ, _hσne, hσx, hσy, _hσsq⟩ :=
    C.exists_twoAnchorReflection hr hy
  let q : PlanePoly →ₐ[ℝ] C.FunctionField :=
    (IsScalarTower.toAlgHom ℝ C.CoordinateRing C.FunctionField).comp
      (Ideal.Quotient.mkₐ ℝ
        (Ideal.span ({C.polynomial} : Set PlanePoly)))
  let σR : C.FunctionField →ₐ[ℝ] C.FunctionField :=
    σ.toAlgHom.restrictScalars ℝ
  have hcomp : σR.comp q = q.comp xAxisReflectionPolynomialHom := by
    ext i
    fin_cases i
    · simp only [AlgHom.comp_apply]
      rw [AlgHom.restrictScalars_apply, AlgEquiv.toAlgHom_apply]
      simpa [q, coordinate, coordinateClass,
        xAxisReflectionPolynomialHom, xAxisReflectionVariables] using hσx
    · simp only [AlgHom.comp_apply]
      rw [AlgHom.restrictScalars_apply, AlgEquiv.toAlgHom_apply]
      simpa [q, coordinate, coordinateClass,
        xAxisReflectionPolynomialHom, xAxisReflectionVariables] using hσy
  have hpzero : q C.polynomial = 0 := by
    change algebraMap C.CoordinateRing C.FunctionField
      (Ideal.Quotient.mk _ C.polynomial) = 0
    rw [Ideal.Quotient.eq_zero_iff_mem.mpr
      (Ideal.mem_span_singleton_self C.polynomial), map_zero]
  have hrefzero : q (xAxisReflectionPolynomialHom C.polynomial) = 0 := by
    have hpoly := AlgHom.congr_fun hcomp C.polynomial
    simpa [hpzero] using hpoly.symm
  have hrefQuotZero :
      Ideal.Quotient.mk
          (Ideal.span ({C.polynomial} : Set PlanePoly))
          (xAxisReflectionPolynomialHom C.polynomial) = 0 := by
    apply IsFractionRing.injective C.CoordinateRing C.FunctionField
    rw [map_zero]
    change q (xAxisReflectionPolynomialHom C.polynomial) = 0
    exact hrefzero
  have hrefmem :
      xAxisReflectionPolynomialHom C.polynomial ∈
        Ideal.span ({C.polynomial} : Set PlanePoly) :=
    Ideal.Quotient.eq_zero_iff_mem.mp hrefQuotZero
  have hdvd : C.polynomial ∣ xAxisReflectionPolynomialHom C.polynomial := by
    obtain ⟨a, ha⟩ := Ideal.mem_span_singleton'.mp hrefmem
    exact ⟨a, by simpa [mul_comm] using ha.symm⟩
  exact C.irreducible.associated_of_dvd
    ((xAxisReflectionPolynomial_irreducible_iff C.polynomial).2 C.irreducible)
    hdvd


theorem xAxisReflection_image_zeroSet_eq_of_secondCoordinate_not_mem
    (C : IrreduciblePlanePolynomial ℝ) {r : ℝ} (hr : r ≠ 0)
    (hy : C.coordinate 1 ∉
      Esgk.twoAnchorDistanceField (C.coordinate 0) (C.coordinate 1) r) :
    xAxisReflectionPoint '' PlaneCurveZeroSet C.polynomial =
      PlaneCurveZeroSet C.polynomial := by
  have hzero :
      PlaneCurveZeroSet C.polynomial =
        PlaneCurveZeroSet (xAxisReflectionPolynomialHom C.polynomial) :=
    zeroSet_eq_of_associated
      (C.associated_xAxisReflectionPolynomial_of_secondCoordinate_not_mem hr hy)
  apply Set.Subset.antisymm
  · rintro z ⟨w, hw, rfl⟩
    have hwq :
        w ∈ PlaneCurveZeroSet (xAxisReflectionPolynomialHom C.polynomial) := by
      rw [← hzero]
      exact hw
    exact mem_zeroSet_xAxisReflectionPolynomial_iff.mp hwq
  · intro z hz
    have hzq :
        z ∈ PlaneCurveZeroSet (xAxisReflectionPolynomialHom C.polynomial) := by
      rw [← hzero]
      exact hz
    refine ⟨xAxisReflectionPoint z,
      mem_zeroSet_xAxisReflectionPolynomial_iff.mp hzq, ?_⟩
    exact xAxisReflectionPoint_involutive z


theorem secondCoordinate_mem_twoAnchorDistanceField_of_xAxisReflection_image_zeroSet_ne
    (C : IrreduciblePlanePolynomial ℝ) {r : ℝ} (hr : r ≠ 0)
    (hns :
      xAxisReflectionPoint '' PlaneCurveZeroSet C.polynomial ≠
        PlaneCurveZeroSet C.polynomial) :
    C.coordinate 1 ∈
      Esgk.twoAnchorDistanceField (C.coordinate 0) (C.coordinate 1) r := by
  by_contra hy
  exact hns
    (C.xAxisReflection_image_zeroSet_eq_of_secondCoordinate_not_mem hr hy)


theorem twoAnchorDistanceField_eq_top_of_xAxisReflection_image_zeroSet_ne
    (C : IrreduciblePlanePolynomial ℝ) {r : ℝ} (hr : r ≠ 0)
    (hns :
      xAxisReflectionPoint '' PlaneCurveZeroSet C.polynomial ≠
        PlaneCurveZeroSet C.polynomial) :
    Esgk.twoAnchorDistanceField (C.coordinate 0) (C.coordinate 1) r = ⊤ := by
  let L : IntermediateField ℝ C.FunctionField :=
    Esgk.twoAnchorDistanceField (C.coordinate 0) (C.coordinate 1) r
  have hx : C.coordinate 0 ∈ L :=
    Esgk.firstCoordinate_mem_twoAnchorDistanceField
      (C.coordinate 0) (C.coordinate 1) hr
  have hy : C.coordinate 1 ∈ L :=
    C.secondCoordinate_mem_twoAnchorDistanceField_of_xAxisReflection_image_zeroSet_ne
      hr hns
  apply top_unique
  rw [← C.adjoin_coordinates_eq_top]
  rw [IntermediateField.adjoin_le_iff]
  intro z hz
  change z ∈ L
  rcases Set.mem_insert_iff.mp hz with hz | hz
  · simpa only [hz] using hx
  · simpa only [Set.mem_singleton_iff.mp hz] using hy

end IrreduciblePlanePolynomial

end Esgk