-- Kernels of surjective homomorphisms to fields are maximal (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.Homomorphism
import Quotient
import Ring.FirstIsomorphism

theorem IsRingHom.kernel_maximal (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires field : IsField(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires onto : SurjectiveBetween(f, A, B)
  shows IsMaximalIdeal(A, add, zero, neg, mul, one, ringKernel(f, A, z))
proof
  have target := IsField.comm_ring with field
  have nontrivial := IsField.nontrivial with field
  have distinct := Nontrivial.distinct with nontrivial
  have ideal := IsRingHom.kernel_ideal with source, target, hom
  have function := IsRingHom.function with hom
  have ordinary := IsCommRing.ring with source
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have unitValue := IsRingHom.one with hom
  have proper : IsProperIdeal(A, add, zero, neg, mul, one, ringKernel(f, A, z))
    constructor
    . exact ideal
    . intro member
      have data := ringKernel.membership.forward with member
      have impossible : z = unit by cc
      exact distinct with impossible
  unfold IsMaximalIdeal
  refine ⟨proper, ?_⟩
  intros J properJ contains
  have idealJ : IsIdeal(A, add, zero, neg, mul, J) by simp [IsProperIdeal]
  have bounded := IsIdeal.subset_carrier with idealJ
  apply Subset.antisymmetric
    intros x hx
    have xIn := bounded with x, hx
    by_contra outside
    have image := IsRingHom.closed with hom, xIn
    have nonzero : f(x) ≠ z
      intro equal
      have member : x ∈ ringKernel(f, A, z) := ringKernel.membership.backward with ⟨xIn, equal⟩
      exact outside with member
    obtain ⟨y, inverse⟩ := IsField.inverse_exists at B, plus, z, minus, times, unit, f(x) with *
    unfold IsInverse at inverse
    have yIn := inverse.right.left
    have surjection := onto
    obtain ⟨a, aIn, edge⟩ := surjection.right with y, yIn
    have imageA := FunctionBetween.apply_value with *
    have productIn := IsRing.mul_closed with ordinary, aIn, xIn
    have mapped := IsRingHom.mul with hom, aIn, xIn
    have equal : f(call2(mul, a, x)) = f(one) by cc
    have congruent := IsRingHom.kernel_congruent.backward with *
    have differenceInJ : call2(add, call2(mul, a, x), neg(one)) ∈ J
      exact contains with call2(add, call2(mul, a, x), neg(one)), congruent
    have productInJ := IsIdeal.mul_left_closed with idealJ, aIn, hx
    have negative := IsIdeal.neg_closed with idealJ, differenceInJ
    have sum := IsIdeal.add_closed with idealJ, productInJ, negative
    have oneInJ : one ∈ J
      ring_nf at sum
      exact sum
    exact properJ.right with oneInJ
  . exact contains