-- Fieldness descends through an injective integral ring homomorphism (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.IntegralDescent
import IntegralInverse
import Construction
import Set.OrderTransport

section Maps
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)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis injective : InjectiveBetween(f, R, S)

theorem IsRingHom.reflects_inverse (a b : Set)
  requires memberA : a ∈ R
  requires memberB : b ∈ R
  requires inverse : IsInverse(B, times, unit, f(a), f(b))
  shows IsInverse(A, mul, one, a, b)
proof
  have ordinary := IsCommRing.ring with source
  have monoid := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with monoid
  have leftIn := IsRing.mul_closed with ordinary, memberB, memberA
  have rightIn := IsRing.mul_closed with ordinary, memberA, memberB
  have leftMap := IsRingHom.mul with hom, memberB, memberA
  have rightMap := IsRingHom.mul with hom, memberA, memberB
  have oneMap := IsRingHom.one with hom
  unfold IsInverse at inverse
  have leftValue : f(R[b * a]) = f(R[1]) by cc
  have rightValue : f(R[a * b]) = f(R[1]) by cc
  have left := Injective.apply_cancel with injective, leftIn, oneIn, leftValue
  have right := Injective.apply_cancel with injective, rightIn, oneIn, rightValue
  unfold IsInverse
  refine ⟨memberA, memberB, left, right⟩

end Maps

section Descent
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)
hypothesis source : IsCommRing(R)
hypothesis field : IsField(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis injective : InjectiveBetween(f, R, S)

theorem IsField.of_integral_extension
  requires integral : ∀ y ∈ S, IntegralOver(f, R, S, y)
  shows IsField(R)
proof
  have target := IsField.comm_ring with field
  have distinct := IsField.nontrivial with field
  have ordinary := IsCommRing.ring with source
  have monoid := IsRing.multiplicative with ordinary
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have oneIn := IsMonoid.unit_in_carrier with monoid
  have zeroValue := IsRingHom.zero with hom
  have oneValue := IsRingHom.one with hom
  have distinctTarget := Nontrivial.distinct with distinct
  have distinctSource : R[0] ≠ R[1]
    intro equal
    have impossible : S[0] = S[1] by cc
    exact distinctTarget with impossible
  have nontrivial : Nontrivial(R)
    unfold Nontrivial
    refine ⟨zeroIn, oneIn, distinctSource⟩
  unfold IsField
  refine ⟨source, nontrivial, ?_⟩
  intros a ha nonzero
  have imageA := IsRingHom.closed with hom, ha
  have imageNonzero : f(a) ≠ S[0]
    intro vanishes
    have equal : f(a) = f(R[0]) by cc
    have impossible := Injective.apply_cancel with injective, ha, zeroIn, equal
    exact nonzero with impossible
  obtain ⟨y, inverse⟩ := IsField.inverse_exists with field, imageNonzero
  have data := inverse
  have element := data.right.left
  have cancels := data.right.right.right
  have algebraic := integral with y, element
  obtain ⟨b, hb, value⟩ := IntegralOver.inverse_in_image with source, target, hom, ha, element, cancels, algebraic
  rw value at inverse
  have reflected := IsRingHom.reflects_inverse with source, target, hom, injective, ha, hb, inverse
  refine ⟨b, reflected⟩

end Descent