-- Unital homomorphisms from a field into a nontrivial ring are injective (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.Embedding
import Homomorphism

section Fields
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 field : IsField(R)
hypothesis target : IsCommRing(S)
hypothesis nontrivial : Nontrivial(S)
hypothesis hom : IsRingHom(f, R, S)

theorem IsRingHom.field_reflects_zero (x : Set)
  requires member : x ∈ R
  requires vanishes : f(x) = S[0]
  shows x = R[0]
proof
  by_contra nonzero
  obtain ⟨y, inverse⟩ := IsField.inverse_exists at A, add, zero, neg, mul, one, x with *
  unfold IsInverse at inverse
  have yIn := inverse.right.left
  have product := inverse.right.right.left
  have mapped := IsRingHom.mul with hom, member, yIn
  have oneValue := IsRingHom.one with hom
  have imageY := IsRingHom.closed with hom, yIn
  have annihilate : S[0 * f(y)] = S[0] by ring
  have impossible : S[0] = S[1] by cc
  have distinct := Nontrivial.distinct with nontrivial
  exact distinct with impossible

theorem IsRingHom.field_injective
  shows InjectiveBetween(f, R, S)
proof
  have source := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with source
  have function := IsRingHom.function with hom
  constructor
  . exact function
  . intros x hx y hy b hb first second
    have valueX := FunctionBetween.apply_value with function, hx, first
    have valueY := FunctionBetween.apply_value with function, hy, second
    have negative := IsRing.neg_closed with ordinary, hy
    have difference := IsRing.add_closed with ordinary, hx, negative
    have mapped := IsRingHom.sub with source, hom, hx, hy
    have zero : S[f(x) - f(y)] = S[0]
      rw [valueX, valueY]
      ring
    have vanishes : f(R[x - y]) = S[0] by cc
    have equal := IsRingHom.field_reflects_zero with *
    have recover : R[(x - y) + y] = x by ring
    have remove : R[0 + y] = y by ring
    cc

theorem IsRingHom.field_iso_of_surjective
  requires onto : SurjectiveBetween(f, R, S)
  shows IsRingIso(f, R, S)
proof
  have injective := IsRingHom.field_injective with *
  have bijective : BijectiveBetween(f, R, S)
    unfold BijectiveBetween
    refine ⟨injective, onto⟩
  unfold IsRingIso
  refine ⟨hom, bijective⟩

end Fields