-- Algebraic elements over an algebraically closed field lie in its image.
-- 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.Rigidity
import AlgebraicClosure
import Polynomial.HornerHom

section Fields
variable (A add zero neg mul one B plus z minus times unit f x : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis closed : IsAlgebraicallyClosed(R)
hypothesis field : IsField(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis element : x ∈ S

theorem monicValue.root_nonempty (cs : List(A))
  requires root : monicValue{A}(f, plus, times, unit, x, cs) = S[0]
  shows cs ≠ []
proof
  intro empty
  rw [empty, monicValue] at root
  have nontrivial := IsField.nontrivial with field
  have distinct := Nontrivial.distinct with nontrivial
  apply distinct
  symm
  exact root

-- Dividing by a base-field root lowers the degree. A field has no zero divisors,
-- so either x is that root's image or the quotient still vanishes at x.
theorem monicValue.root_in_image_of_length (n : Nat) (cs : List(A))
  requires size : length{A}(cs) = n
  requires root : monicValue{A}(f, plus, times, unit, x, cs) = S[0]
  shows ∃ a ∈ R, f(a) = x
proof
  induction n generalizing cs
  | zero =>
    intros cs list size root
    have nonempty := monicValue.root_nonempty at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, cs with *
    have alternatives := List.cases with list
    cases alternatives with empty | cons
    . exfalso
      exact nonempty with empty
    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons
      rw shape at size
      rw length.cons at size
      exfalso
      apply Naturals.disjoint.zero.succ at length{A}(tail)
      symm
      exact size
  | succ(k) using ih =>
    intros cs list size root
    have nonempty := monicValue.root_nonempty at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, cs with *
    have alternatives := List.cases with list
    cases alternatives with empty | cons
    . exfalso
      exact nonempty with empty
    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons
      have tailSize : length{A}(tail) = k
        rw shape at size
        rw length.cons at size
        exact Naturals.injective.succ with size
      obtain ⟨a, center, baseRoot⟩ := IsAlgebraicallyClosed.root at A, add, zero, neg, mul, one, cs with *
      have baseField := IsAlgebraicallyClosed.field with closed
      have source := IsField.comm_ring with baseField
      have ordinary := IsCommRing.ring with source
      have multiplicative := IsRing.multiplicative with ordinary
      have initial := IsMonoid.unit_in_carrier with multiplicative
      have target := IsField.comm_ring with field
      have targetRing := IsCommRing.ring with target
      have imageA := IsRingHom.closed with hom, center
      have imageOne := IsRingHom.closed with hom, initial
      have oneValue := IsRingHom.one with hom
      have zeroValue := IsRingHom.zero with hom
      have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, one, a, tail with *
      have quotientLength := hornerQuotient.length at A, add, zero, neg, mul, one, one, a, tail with *
      have quotientSize : length{A}(hornerQuotient{A}(add, mul, one, a, tail)) = k by cc
      have division := hornerValue.synthetic_division at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, one, a, x, c, tail with *
      have baseValue : hornerAt{A}(add, mul, one, a, c :: tail) = R[0]
        rw shape at baseRoot
        simp [hornerAt]
      rw oneValue at division
      rw baseValue at division
      rw zeroValue at division
      rw shape at root
      rw root at division
      have value := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(one), hornerQuotient{A}(add, mul, one, a, tail) with *
      rw oneValue at value
      have negative := IsRing.neg_closed with targetRing, imageA
      have difference := IsRing.add_closed with targetRing, element, negative
      have productZero : S[(x - f(a)) * monicValue{A}(f, plus, times, unit, x, hornerQuotient{A}(add, mul, one, a, tail))] = S[0]
        linear_combination -division
      have noZero := IsField.no_zero_divisors with field
      have factors := noZero with S[x - f(a)], difference, monicValue{A}(f, plus, times, unit, x, hornerQuotient{A}(add, mul, one, a, tail)), value, productZero
      cases factors with same | remaining
      . have equal : f(a) = x
          linear_combination -same
        refine ⟨a, center, equal⟩
      . exact ih with hornerQuotient{A}(add, mul, one, a, tail), quotient, quotientSize, remaining

theorem monicValue.root_in_image (cs : List(A))
  requires root : monicValue{A}(f, plus, times, unit, x, cs) = S[0]
  shows ∃ a ∈ R, f(a) = x
proof
  have size : length{A}(cs) = length{A}(cs) by rfl
  exact monicValue.root_in_image_of_length with *

end Fields

section Extensions
variable (A add zero neg mul one B plus z minus times unit f : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)

theorem IsAlgebraicallyClosed.algebraic_in_image (x : Set)
  requires closed : IsAlgebraicallyClosed(R)
  requires field : IsField(S)
  requires hom : IsRingHom(f, R, S)
  requires algebraic : AlgebraicOver(f, R, S, x)
  shows ∃ a ∈ R, f(a) = x
proof
  have baseField := IsAlgebraicallyClosed.field with closed
  have target := IsField.comm_ring with field
  have integral := AlgebraicOver.integral with baseField, target, hom, algebraic
  have element := integral.left
  obtain ⟨cs, list, root⟩ := integral.right
  exact monicValue.root_in_image with *

-- There are no proper algebraic field extensions of an algebraically closed field.
theorem IsAlgebraicallyClosed.algebraic_extension_surjective
  requires closed : IsAlgebraicallyClosed(R)
  requires field : IsField(S)
  requires hom : IsRingHom(f, R, S)
  requires algebraic : ∀ y ∈ S, AlgebraicOver(f, R, S, y)
  shows SurjectiveBetween(f, R, S)
proof
  have function := IsRingHom.function with hom
  unfold SurjectiveBetween
  refine ⟨function, ?_⟩
  intros y member
  have relation := algebraic with y, member
  obtain ⟨a, inR, value⟩ := IsAlgebraicallyClosed.algebraic_in_image at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, y with *
  have graph := FunctionBetween.relates_apply with function, inR
  rw value at graph
  refine ⟨a, inR, graph⟩

end Extensions