/-
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.Algebra.MvPolynomial.Equiv
public import Mathlib.Data.Real.Basic
public import Mathlib.RingTheory.HahnSeries.Multiplication
public import Mathlib.RingTheory.Ideal.Quotient.Operations
public import Mathlib.RingTheory.Ideal.Span
public import Mathlib.RingTheory.UniqueFactorizationDomain.Defs

/-!
# The ring of germs is a polynomial ring

Let `J` be the ideal of `K((ℝ^{≤0}))` generated by the monomials `t^x`, `x < 0`.
The quotient `K((ℝ^{≤0}))/J` is Berarducci's ring of germs. In characteristic zero it is
isomorphic as a ring to a polynomial ring with coefficient field `K`; in particular it has
unique factorisation.

The polynomial presentation proves Berarducci's factorisation conjecture as stated in
[LM17, Conjecture 1.5].

## References

* A. Berarducci, *Factorization in generalized power series*, Trans. Amer. Math. Soc. 352 (2000),
  553–577, cited as [Ber00].
* S. L'Innocente, V. Mantova, *Factorisation of germ-like series*, J. Log. Anal. 9 (2017), cited
  as [LM17].
-/

@[expose] public noncomputable section

namespace ConwayRefinement.Standalone.GermPolynomial

universe u

variable {K : Type u} [Field K]

/-- The Hahn-series ring `K((ℝ^{≤0}))`. -/
def nonpos (K : Type u) [Field K] : Subring (HahnSeries ℝ K) where
  carrier := {x | x.support ⊆ Set.Iic 0}
  zero_mem' := by simp
  one_mem' := by
    intro g hg
    have hg0 : g = 0 := HahnSeries.support_single_subset hg
    simp [hg0]
  add_mem' := fun {x y} hx hy => by
    intro g hg
    rcases HahnSeries.support_add_subset x y hg with hg | hg
    · exact hx hg
    · exact hy hg
  neg_mem' := fun {x} hx => (HahnSeries.support_neg_subset x).trans hx
  mul_mem' := fun {x y} hx hy => by
    intro g hg
    obtain ⟨i, hi, j, hj, rfl⟩ := HahnSeries.support_mul_subset hg
    exact add_nonpos (show i ≤ 0 from hx hi) (show j ≤ 0 from hy hj)

/-- The elements of `K((ℝ^{≤0}))` are exactly the Hahn series supported in `(-∞, 0]`. -/
theorem mem_nonpos_iff (x : HahnSeries ℝ K) :
    x ∈ nonpos K ↔ x.support ⊆ Set.Iic 0 := (Iff.rfl)

variable (K) in
/-- Berarducci's ideal `J`: the ideal of `K((ℝ^{≤0}))` generated by the monomials `t^x`, `x < 0`. -/
def J : Ideal (nonpos K) :=
  Ideal.span {m : nonpos K |
    ∃ x : ℝ, x < 0 ∧ (m : HahnSeries ℝ K) = HahnSeries.single x 1}

variable (K) in
/-- Berarducci's ring of germs `K((ℝ^{≤0}))/J`. -/
abbrev Germ := nonpos K ⧸ J K

variable (K) in
/-- **Polynomial presentation of the ring of germs.** For some set `ι`, the ring
`K((ℝ^{≤0}))/J` is ring-isomorphic to `K[X_i : i ∈ ι]`. -/
abbrev GermIsPolynomialRing : Prop :=
  CharZero K → ∃ ι : Type (max u 1), Nonempty (MvPolynomial ι K ≃+* Germ K)

variable (K) in
/-- **Unique factorisation in the ring of germs** [LM17, Conjecture 1.5]: the ring of germs is a
domain; every nonzero germ is, up to a unit, a product of irreducible germs; and two products of
irreducible germs that agree up to a unit have the same factors up to order and associates.

The conclusion is asserted in characteristic zero. -/
abbrev GermHasUniqueFactorization : Prop :=
  CharZero K →
    IsDomain (Germ K) ∧
      (∀ a : Germ K, a ≠ 0 →
        ∃ f : Multiset (Germ K), (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) ∧
      ∀ f g : Multiset (Germ K), (∀ b ∈ f, Irreducible b) → (∀ b ∈ g, Irreducible b) →
        Associated f.prod g.prod → Multiset.Rel Associated f g

end ConwayRefinement.Standalone.GermPolynomial

/-!
## Formal proof

Proof module: `GermPolynomialRingProof`.

* `GermIsPolynomialRing` → `GermIsPolynomialRing.proof`
* `GermHasUniqueFactorization` → `GermHasUniqueFactorization.proof`
-/