-- Algebraic elements become integral after inverting a leading coefficient (ZF).
-- 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.AlgebraicLocalization
import HornerRelations
import PrincipalLocalization
import Set.OrderTransport

section Normalization
variable (A add z neg mul one B plus o minus times unit f T x a y : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring S := (B, plus, o, minus, times, unit)
notation ring L := S ↾ T
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis subring : IsSubring(S, T)
hypothesis coefficients : ∀ c ∈ R, f(c) ∈ T
hypothesis element : x ∈ S
hypothesis leading : a ∈ R
hypothesis inverseIn : y ∈ T
hypothesis inverse : IsInverse(B, times, unit, f(a), y)

theorem IntegralOver.of_invertible_leading (cs : List(A))
  requires relation : polynomialHorner{A}(f, plus, times, x, a, cs) = o
  shows IntegralOver(identity(T), L, S, x)
proof
  have smaller : IsCommRing(L)
    exact IsSubring.comm_ring with *
  have inclusion : IsRingHom(identity(T), L, S)
    exact IsSubring.inclusion_hom with *
  have function := IsRingHom.function with hom
  have corestricted := FunctionBetween.codomain_of_values with function, coefficients
  have agreement : ∀ c ∈ R, f(c) = identity(T)(f(c))
    intros c member
    have inT := coefficients with c, member
    symm
    exact identity.apply with *
  have changed := monicValue.change_coefficients at A, T, plus, times, f, identity(T), f, f(a), x, cs with *
  have identityY := identity.apply at y, T with *
  have data := inverse
  unfold IsInverse at data
  have leadingOne : S[identity(T)(y) * f(a)] = S[1] by cc
  have scaleClosed : ∀ c ∈ T, L[y * c] ∈ T
    intros c member
    have ordinary := IsCommRing.ring with smaller
    exact IsRing.mul_closed with ordinary, inverseIn, member
  have scaled := ringScale.closed at T, restrict(times, T × T), y, listMap{A}(f, cs) with *
  have scaledValue := hornerValue.scale at T, restrict(plus, T × T), o, restrict(minus, T), restrict(times, T × T), unit, B, plus, o, minus, times, unit, identity(T), x, y, f(a), listMap{A}(f, cs) with *
  rw leadingOne at scaledValue
  unfold polynomialHorner at relation
  have vanishes : monicValue{T}(identity(T), plus, times, f(a), x, listMap{A}(f, cs)) = o by cc
  rw vanishes at scaledValue
  have yIn := data.right.left
  have zeroProduct : S[identity(T)(y) * 0] = S[0]
    rw identityY
    ring
  rw zeroProduct at scaledValue
  unfold IntegralOver
  refine ⟨element, ringScale{T}(restrict(times, T × T), y, listMap{A}(f, cs)), scaled, scaledValue⟩

end Normalization
section Fields
variable (A add z neg mul one B plus o minus times unit f : Set)
notation ring R := (A, add, z, neg, mul, one)
notation ring S := (B, plus, o, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis field : IsField(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis injective : InjectiveBetween(f, R, S)

theorem IsRingHom.domain_of_field_embedding
  shows IsIntegralDomain(R)
proof
  have zeroIn : R[0] ∈ R by typecheck
  have oneIn : R[1] ∈ R by typecheck
  have zero := IsRingHom.zero with hom
  have one := IsRingHom.one with hom
  have targetNontrivial := IsField.nontrivial with field
  have distinct := Nontrivial.distinct with targetNontrivial
  have sourceDistinct : R[0] ≠ R[1]
    intro equal
    apply distinct
    cc
  have nontrivial : Nontrivial(R)
    unfold Nontrivial
    refine ⟨zeroIn, oneIn, sourceDistinct⟩
  have targetDomain := IsField.no_zero_divisors with field
  have noZero : NoZeroDivisors(A, mul, z)
    intros a ha b hb vanishes
    have mapped := IsRingHom.mul with hom, ha, hb
    have imageA := IsRingHom.closed with hom, ha
    have imageB := IsRingHom.closed with hom, hb
    have productZero : S[f(a) * f(b)] = S[0] by cc
    have alternatives := targetDomain with f(a), f(b), productZero
    cases alternatives with leftZero | rightZero
    . have equal : f(a) = f(R[0])
        cc
      have original := Injective.apply_cancel with injective, ha, equal
      left
      exact original
    . have equal : f(b) = f(R[0])
        cc
      have original := Injective.apply_cancel with injective, hb, equal
      right
      exact original
  unfold IsIntegralDomain
  refine ⟨source, nontrivial, noZero⟩

theorem AlgebraicOver.exists_principal_integral (x : Set)
  requires algebraic : AlgebraicOver(f, R, S, x)
  shows ∃ a ∈ R, a ≠ R[0] ∧
    IntegralOver(identity(localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a)))), localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a))), S, x)
proof
  have target := IsField.comm_ring with field
  have function := IsRingHom.function with hom
  have imageRing : IsSubring(S, functionImage(f, R, S))
    exact IsRingHom.image_subring with *
  have zeroIn : R[0] ∈ R by typecheck
  have zero := IsRingHom.zero with hom
  have element := algebraic.left
  obtain ⟨a, leading, nonzero, cs, list, relation⟩ := algebraic.right
  have inImage := functionImage.value at f, R, S, a with *
  have image := IsRingHom.closed with hom, leading
  have imageNonzero : f(a) ≠ S[0]
    intro vanishes
    have equal : f(a) = f(R[0]) by cc
    have original := Injective.apply_cancel with injective, leading, equal
    exact nonzero with original
  have denominators := denominatorPowers.denominators with *
  have localized := localizationWithin.subring with target, imageRing, denominators
  have contains := localizationWithin.contains with target, imageRing, denominators
  have coefficients : ∀ c ∈ R, f(c) ∈ localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a)))
    intros c member
    have value := functionImage.value at f, R, S, c with *
    exact contains with f(c), value
  obtain ⟨y, inverse⟩ := IsField.inverse_exists at B, plus, o, minus, times, unit, f(a) with *
  have ordinary := IsCommRing.ring with target
  have monoid := IsRing.multiplicative with ordinary
  have power : monoidPow(S, f(a), (1:Nat)) = f(a)
    rw [monoidPow.succ, monoidPow.zero]
    ring
  have natural := Naturals.constructor.succ with Naturals.constructor.zero
  have denominator : f(a) ∈ denominatorPowers(S, f(a))
    apply denominatorPowers.membership.backward
    refine ⟨image, (1:Nat), natural, ?_⟩
    symm
    exact power
  have inverseIn := localizationWithin.inverse_mem with target, imageRing, denominators, denominator, inverse
  have integral := IntegralOver.of_invertible_leading with *
  refine ⟨a, leading, nonzero, integral⟩

end Fields