NormalPoint.lean

abbrev PointLocalRing
    {f : BivariatePolynomial K} (p : RationalPoint f)

def IsNormalAt
    {f : BivariatePolynomial K} (p : RationalPoint f) : Prop

abbrev CoordinateFunctionField (f : BivariatePolynomial K)

def coordinateFunctionFieldMap
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)] :
    CoordinateRing f →ₐ[K] CoordinateFunctionField f

def normalPointValuationSubring
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    ValuationSubring (CoordinateFunctionField f)

theorem normalPointValuationSubring_isDiscreteValuationRing
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    IsDiscreteValuationRing
      (normalPointValuationSubring hf p hnormal)

def normalPointDiscreteKValuation
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    DiscreteKValuation K (CoordinateFunctionField f) where
  valuationSubring := normalPointValuationSubring hf p hnormal
  isDiscreteValuationRing :=
    normalPointValuationSubring_isDiscreteValuationRing hf p hnormal
  algebraMap_mem := by
    intro x
    let : (pointIdeal p).IsMaximal := pointIdeal_isMaximal p
    let : (pointIdeal p).IsPrime := (pointIdeal_isMaximal p).isPrime
    have hnormal' : IsIntegrallyClosed (PointLocalRing p) := by
      simpa [IsNormalAt] using hnormal
    let : IsDiscreteValuationRing (PointLocalRing p) :=
      pointLocalRing_isDiscreteValuationRing_of_isIntegrallyClosed
        hf p hnormal'
    change
      (IsDiscreteValuationRing.maximalIdeal (PointLocalRing p)).valuation
          (CoordinateFunctionField f)
          (algebraMap K (CoordinateFunctionField f) x) ≤ 1
    have hconstant :
        algebraMap K (CoordinateFunctionField f) x =
          algebraMap (PointLocalRing p) (CoordinateFunctionField f)
            (algebraMap K (PointLocalRing p) x) := by
      rw [IsScalarTower.algebraMap_apply
        K (CoordinateRing f) (CoordinateFunctionField f)]
      rw [IsScalarTower.algebraMap_apply
        K (CoordinateRing f) (PointLocalRing p)]
      rw [IsScalarTower.algebraMap_apply
        (CoordinateRing f) (PointLocalRing p)
          (CoordinateFunctionField f)]
    rw [hconstant]
    exact
      (IsDiscreteValuationRing.maximalIdeal
        (PointLocalRing p)).valuation_le_one
          (K := CoordinateFunctionField f)
          (algebraMap K (PointLocalRing p) x)

def normalPointLocalRingEquiv
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    PointLocalRing p ≃ₐ[K]
      (normalPointDiscreteKValuation hf p hnormal).valuationSubring

def normalPointResidueEquiv
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    K ≃ₐ[K]
      (normalPointDiscreteKValuation hf p hnormal).ResidueField

theorem normalPoint_hasFiniteResidueDegree
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    HasFiniteResidueDegree K (CoordinateFunctionField f)
      (normalPointDiscreteKValuation hf p hnormal)

def normalPointPrimeDivisor
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    FunctionFieldPrimeDivisor K (CoordinateFunctionField f) where
  toDiscreteKValuation :=
    normalPointDiscreteKValuation hf p hnormal
  residueFinite :=
    normalPoint_hasFiniteResidueDegree hf p hnormal

theorem normalPointPrimeDivisor_degree
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    (normalPointPrimeDivisor hf p hnormal).degree = 1

theorem normalPointPrimeDivisor_finiteAlong
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    (normalPointPrimeDivisor hf p hnormal).FiniteAlong
      (coordinateFunctionFieldMap (K := K) (f := f))

theorem normalPointPrimeDivisor_centerAlong
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    (normalPointPrimeDivisor hf p hnormal).centerAlong
        (coordinateFunctionFieldMap (K := K) (f := f))
        (normalPointPrimeDivisor_finiteAlong hf p hnormal) =
      pointIdeal p

theorem normalPointValuationSubring_unique
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p)
    (w : FunctionFieldPrimeDivisor K (CoordinateFunctionField f))
    (hw : w.FiniteAlong
      (coordinateFunctionFieldMap (K := K) (f := f)))
    (hcenter :
      w.centerAlong
          (coordinateFunctionFieldMap (K := K) (f := f)) hw =
        pointIdeal p) :
    (normalPointPrimeDivisor hf p hnormal).valuationSubring =
      w.valuationSubring

theorem normalPointPrimeDivisor_unique
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p)
    (w : FunctionFieldPrimeDivisor K (CoordinateFunctionField f))
    (hw : w.FiniteAlong
      (coordinateFunctionFieldMap (K := K) (f := f)))
    (hcenter :
      w.centerAlong
          (coordinateFunctionFieldMap (K := K) (f := f)) hw =
        pointIdeal p) :
    w = normalPointPrimeDivisor hf p hnormal

theorem proposition_6_2_2_a
    {f : BivariatePolynomial K} (hf : Irreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    letI : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
    ∃! w : FunctionFieldPrimeDivisor K (CoordinateFunctionField f),
      ∃ hw : w.FiniteAlong
          (coordinateFunctionFieldMap (K := K) (f := f)),
        w.centerAlong
            (coordinateFunctionFieldMap (K := K) (f := f)) hw =
            pointIdeal p ∧
          w.degree = 1 := by
  let : IsDomain (CoordinateRing f) := coordinateRing_isDomain hf
  let v := normalPointPrimeDivisor hf p hnormal
  let hv : v.FiniteAlong
      (coordinateFunctionFieldMap (K := K) (f := f)) :=
    normalPointPrimeDivisor_finiteAlong hf p hnormal
  refine ⟨v, ?_, ?_⟩
  · exact
      ⟨hv,
        normalPointPrimeDivisor_centerAlong hf p hnormal,
        normalPointPrimeDivisor_degree hf p hnormal⟩
  · intro w hwitness
    obtain ⟨hw, hcenter, _⟩ := hwitness
    exact
      normalPointPrimeDivisor_unique
        hf p hnormal w hw hcenter

theorem proposition_6_2_2_a_of_isAbsolutelyIrreducible
    {f : BivariatePolynomial K} (hf : IsAbsolutelyIrreducible f)
    (p : RationalPoint f) (hnormal : IsNormalAt p) :
    let hirreducible : Irreducible f := hf.irreducible
    letI : IsDomain (CoordinateRing f) :=
      coordinateRing_isDomain hirreducible
    ∃! w : FunctionFieldPrimeDivisor K (CoordinateFunctionField f),
      ∃ hw : w.FiniteAlong
          (coordinateFunctionFieldMap (K := K) (f := f)),
        w.centerAlong
            (coordinateFunctionFieldMap (K := K) (f := f)) hw =
            pointIdeal p ∧
          w.degree = 1 := by
  exact proposition_6_2_2_a hf.irreducible p hnormal