-- Algebraically closed fields are infinite, by an explicit root-free polynomial.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Field.Infinite
import AlgebraicClosure
import Polynomial.MonicVanishing

section Fields
variable (A add zero neg mul one : Set)
notation ring R := (A, add, zero, neg, mul, one)

-- A monic polynomial vanishing on a finite cover cannot take the value -1.
-- Adding 1 to its constant coefficient contradicts algebraic closedness.
theorem IsAlgebraicallyClosed.infinite
  requires closed : IsAlgebraicallyClosed(R)
  shows ¬Finite(R)
proof
  have field := IsAlgebraicallyClosed.field with closed
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have multiplicative := IsRing.multiplicative with ordinary
  have unitIn := IsMonoid.unit_in_carrier with multiplicative
  have nontrivial := IsField.nontrivial with field
  have distinct := Nontrivial.distinct with nontrivial
  intro finite
  obtain ⟨xs, list, cover⟩ := Finite.list_cover with finite
  obtain ⟨c, coefficient, cs, coefficients, vanishes⟩ := hornerAt.monic_vanishing_on_list at A, add, zero, neg, mul, one, xs with *
  have shifted := IsRing.add_closed with ordinary, coefficient, unitIn
  have nonconstant : R[c + 1] :: cs ≠ []
    intro same
    have lengths : length{A}(R[c + 1] :: cs) = length{A}([])
      rw same
      rfl
    rw [length.cons, length.nil] at lengths
    have reversed : (0 : Nat) = succ(length{A}(cs)) by cc
    exact Naturals.disjoint.zero.succ at length{A}(cs) with reversed
  obtain ⟨x, element, root⟩ := IsAlgebraicallyClosed.root at A, add, zero, neg, mul, one, R[c + 1] :: cs with *
  have rootValue : hornerAt{A}(add, mul, one, x, R[c + 1] :: cs) = R[0]
    simp [hornerAt]
  have member := cover with x, element
  have old := vanishes with x, element, member
  have tailValue := hornerAt.closed at A, add, zero, neg, mul, one, one, x, cs with *
  rw hornerAt.cons at rootValue
  rw hornerAt.cons at old
  have rearrange : R[(c + 1) + x * hornerAt{A}(add, mul, one, x, cs)] = R[(c + x * hornerAt{A}(add, mul, one, x, cs)) + 1]
    ring
  rw [rootValue, old] at rearrange
  have unit : R[0 + 1] = R[1] by ring
  rw unit at rearrange
  exact distinct with rearrange

end Fields