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

public import Mathlib.Data.Real.Basic
public import Mathlib.RingTheory.HahnSeries.Multiplication
public import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
public import Mathlib.Algebra.MvPolynomial.Eval
public import Mathlib.Order.WellFoundedSet
public import CombinatorialGames.NatOrdinal.Pow

/-!
# Algebraic independence in $\widehat{\mathrm P}$

`K((ℝ^{≤0}))` is the ring of Hahn series with real exponents `≤ 0` over a field `K`
[LM24, §1.2]. Berarducci's *ordinal value* `v_J` [Ber00, Def. 5.2] is determined by the class of
a series modulo `J + K`: `v_J(b) = 0` if `b ∈ J`, the ideal generated by the monomials `t^x`,
`x < 0` [Ber00, Def. 5.1]; `v_J(b) = 1` if `b ∈ (J + K) \ J`; otherwise `v_J(b)` is the least
order type of the support of a series congruent to `b` modulo `J + K`. Its values are `0` or
additively principal ordinals `ω^α`, and `J_{ω^α} := {b : v_J(b) < ω^α}`.

For each `α`, `P_α := J_{ω^(α+1)} / J_{ω^α}` is the vector space of principal RV-elements of
degree `α`. Their direct sum is
`P̂ := ⨁_α P_α`, graded by the natural sum of ordinals: `v_J(bc) ≤ v_J(b) ⊕ v_J(c)`
[Ber00, Thm. 5.8], so the product of classes of degrees `α` and `β` is a class of degree `α ⊕ β`.
A *minimal homogeneous family* in `P̂` is a family of classes `B ∈ P_{deg B}` of positive
degrees whose members of each degree `β` are linearly independent modulo
`(P̂_+)² ∩ P_β = ∑_{i ⊕ j = β, i, j ≠ 0} P_i P_j`, the square of the ideal of positive degree in
degree `β` (the decomposable elements, `IsDecomposable`).

**Algebraic independence** (the injective half of the polynomiality of `P̂`). Every minimal
homogeneous family `𝓑` is algebraically independent. Thus the
subalgebra it generates is a polynomial algebra; if `𝓑` generates `P̂`, then `P̂` itself is a
polynomial algebra. In terms of series: a polynomial `F` homogeneous of degree `α` (for
`deg X_B = deg B`) with `v_J(F(b_𝓑)) < ω^α`, where `b_B` represents `B`, is zero.

The proposition `MinimalFamiliesAlgebraicallyIndependent` expresses this statement through
representatives: a class of degree `α` is a series `b` with `v_J(b) < ω^(α+1)`, and two such
series represent the same class exactly when their difference lies in `J_{ω^α}`.

## References

* A. Berarducci, *Factorization in generalized power series*, Trans. Amer. Math. Soc. 352 (2000)
  553–577, cited as [Ber00].
* S. L'Innocente, V. Mantova, *A factorisation theory for generalised power series and omnific
  integers*, Adv. Math. 442 (2024) 109513, cited as [LM24].
-/

open Ordinal
open scoped NatOrdinal

@[expose] public noncomputable section

namespace ConwayRefinement.Standalone.PrincipalRVAlgebraicIndependence

universe u v

variable {K : Type u} [Field K]

/-! ### The ring -/

variable (K) in
/-- `K((ℝ^{≤0}))`: Hahn series with real exponents `≤ 0` [LM24, §1.2], as a `K`-subalgebra of
`K((ℝ))`. -/
def nonpos : Subalgebra K (HahnSeries ℝ K) where
  carrier := {x | x.support ⊆ Set.Iic 0}
  algebraMap_mem' k := by
    intro g hg
    rw [HahnSeries.algebraMap_apply] at hg
    have hg0 : g = 0 := HahnSeries.support_single_subset hg
    simp [hg0]
  add_mem' := fun {x y} hx hy g hg ↦ by
    rcases HahnSeries.support_add_subset x y hg with h | h
    exacts [hx h, hy h]
  mul_mem' := fun {x y} hx hy g hg ↦ by
    obtain ⟨i, hi, j, hj, rfl⟩ := HahnSeries.support_mul_subset hg
    exact Set.mem_Iic.mpr (add_nonpos (Set.mem_Iic.mp (hx hi)) (Set.mem_Iic.mp (hy hj)))

/-- `<` well-orders the support, as a generalised power series requires [LM24, §1.2]. -/
theorem supportIsWellOrder (x : HahnSeries ℝ K) :
    IsWellOrder x.support (Subrel (· < ·) (· ∈ x.support)) := by
  refine { wf := x.isPWO_support.isWF, trichotomous := fun _ _ hab hba ↦ ?_ }
  exact Subtype.ext (le_antisymm (le_of_not_gt hba) (le_of_not_gt hab))

/-- The order type of the well-ordered support of `x` [LM24, §2.2]. -/
def ot (x : HahnSeries ℝ K) : Ordinal.{0} :=
  @Ordinal.type x.support (Subrel (· < ·) (· ∈ x.support)) (supportIsWellOrder x)

/-! ### The ordinal value -/

/-- The ideal `J` generated by the monomials `t^x`, `x < 0` [Ber00, Def. 5.1]: the series whose
support is bounded away from `0`. -/
def MemJ (x : nonpos K) : Prop :=
  ∃ s < (0 : ℝ), (x : HahnSeries ℝ K).support ⊆ Set.Iic s

/-- Congruence to a constant modulo `J`: membership in Berarducci's subgroup `J + K`. -/
def IsNearConstant (x : nonpos K) : Prop :=
  ∃ k : K, MemJ (x - algebraMap K (nonpos K) k)

open scoped Classical in
/-- **Berarducci's ordinal value** `v_J` [Ber00, Def. 5.2]: `0` on `J`, `1` on `(J + K) \ J`, and
otherwise the least order type of the support of a series congruent to `x` modulo `J + K`. -/
def ordinalValue (x : nonpos K) : NatOrdinal :=
  if MemJ x then 0
  else if IsNearConstant x then 1
  else sInf {o | ∃ c : nonpos K,
    IsNearConstant (x - c) ∧ NatOrdinal.of (ot (c : HahnSeries ℝ K)) = o}

/-! ### Classes, decomposables, and minimal homogeneous families -/

variable {ι : Type v}

/-- `x` is *decomposable at degree `α`*: modulo `J_{ω^α}`, a finite sum of products `u_k w_k` of
representatives of classes of positive degrees `β_k ⊕ β'_k = α` — a representative of an element
of `(P̂_+)² ∩ P_α = ∑_{i ⊕ j = α, i, j ≠ 0} P_i P_j`, the square of the ideal of positive degree
in degree `α`. -/
def IsDecomposable (α : NatOrdinal) (x : nonpos K) : Prop :=
  ∃ (n : ℕ) (β β' : Fin n → NatOrdinal) (u w : Fin n → nonpos K),
    (∀ k, β k ≠ 0 ∧ β' k ≠ 0 ∧ β k + β' k = α) ∧
    (∀ k, ordinalValue (u k) < ω^ (β k + 1)) ∧ (∀ k, ordinalValue (w k) < ω^ (β' k + 1)) ∧
    ordinalValue (x - ∑ k, u k * w k) < ω^ α

/-- A minimal homogeneous family in `P̂`, through representatives: `b i` represents a class of
positive degree `deg i`, and the classes of any fixed degree are linearly independent modulo the
decomposables of that degree. -/
structure IsMinimalHomogeneousFamily (deg : ι → NatOrdinal) (b : ι → nonpos K) : Prop where
  /-- Every generator has positive degree. -/
  ne_zero : ∀ i, deg i ≠ 0
  /-- `b i` represents a class of degree `deg i`. -/
  mem : ∀ i, ordinalValue (b i) < ω^ (deg i + 1)
  /-- The generators of degree `β` are linearly independent modulo the decomposables. -/
  independent : ∀ (β : NatOrdinal) (c : ι →₀ K), (∀ i ∈ c.support, deg i = β) →
    IsDecomposable β (c.sum fun i k ↦ algebraMap K (nonpos K) k * b i) → c = 0

variable (K) in
/-- **Algebraic independence in `P̂`.** For every minimal homogeneous family, given through
representatives `b i` of classes of degrees `deg i`, a polynomial `F ∈ K[X_i]` homogeneous of
degree `α` whose evaluation `F(b)` lies in `J_{ω^α}` is zero.

The conclusion is asserted in characteristic zero. -/
abbrev MinimalFamiliesAlgebraicallyIndependent : Prop :=
  CharZero K →
    ∀ {ι : Type} (deg : ι → NatOrdinal) (b : ι → nonpos K),
      IsMinimalHomogeneousFamily deg b →
      ∀ (α : NatOrdinal) (F : MvPolynomial ι K), MvPolynomial.IsWeightedHomogeneous deg F α →
        ordinalValue (MvPolynomial.aeval b F) < ω^ α → F = 0

end ConwayRefinement.Standalone.PrincipalRVAlgebraicIndependence

/-!
## Formal proof

Proof module: `PrincipalRVAlgebraicIndependenceProof`.

* `MinimalFamiliesAlgebraicallyIndependent` → `MinimalFamiliesAlgebraicallyIndependent.proof`
-/