-- Maximal ideals and quotient fields, with canonical inverses in 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.Quotient
import Construction
import Ring.Quotient
import Ring.IdealAdjoin

theorem IsMaximalIdeal.unit_modulo (A add zero neg mul one I x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)
  requires hx : x ∈ A
  requires outside : ¬(x ∈ I)
  shows ∃ a ∈ A, Congruent(add, neg, I, call2(mul, a, x), one)
proof
  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsMaximalIdeal, IsProperIdeal]
  have bounded := IsIdeal.subset_carrier with ideal
  obtain ⟨i, hi, a, ha, equation⟩ := IsMaximalIdeal.bezout at A, add, zero, neg, mul, one, I, x with *
  have iInA := bounded with i, hi
  have negative := IsIdeal.neg_closed with *
  have difference : call2(add, call2(mul, a, x), neg(one)) = neg(i)
    rw equation
    ring
  refine ⟨a, ha, ?_⟩
  unfold Congruent
  rwa difference

theorem idealQuotient.is_field_of_maximal (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)
  shows IsField((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])
proof
  have proper : IsProperIdeal(A, add, zero, neg, mul, one, I) by simp [IsMaximalIdeal]
  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsProperIdeal]
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have oneInA := IsMonoid.unit_in_carrier with monoid
  have closed : IsMagma(A, mul) by simp [IsMonoid, IsSemigroup]
  have equivalence := idealRelation.equivalence with *
  have compatible := idealRelation.mul_compatible with *
  have quotientRing := idealQuotient.comm_ring with *
  have nontrivial := idealQuotient.nontrivial_iff.backward with ring, ideal, proper
  unfold IsField
  refine ⟨quotientRing, nontrivial, ?_⟩
  intros X hX nonzero
  obtain ⟨x, hx, shape⟩ := quotient.representative with hX
  have outside : ¬(x ∈ I)
    intro member
    have equal := idealClass.eq_zero.backward with ring, ideal, hx, member
    apply nonzero
    cc
  obtain ⟨a, ha, congruence⟩ := IsMaximalIdeal.unit_modulo at A, add, zero, neg, mul, one, I, x with *
  have productInA := IsRing.mul_closed with ha, hx
  have equal := idealClass.eq_iff_congruent.backward with ring, ideal, productInA, oneInA, congruence
  have aIn := quotient.contains_class with ha
  have left := quotientBinary.classes with ha, hx
  have right := quotientBinary.classes with hx, ha
  have commutes := IsCommRing.mul_comm with hx, ha
  witness ⟦a⟧[A, idealRelation(A, add, neg, I)]
  unfold IsInverse
  refine ⟨hX, ⟨aIn, ⟨?_, ?_⟩⟩⟩
  . cc
  . cc

theorem idealQuotient.maximal_of_is_field (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires field : IsField((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])
  shows IsMaximalIdeal(A, add, zero, neg, mul, one, I)
proof
  have nontrivial := IsField.nontrivial with field
  have proper := idealQuotient.nontrivial_iff.forward with *
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have oneInA := IsMonoid.unit_in_carrier with monoid
  have closed : IsMagma(A, mul) by simp [IsMonoid, IsSemigroup]
  have equivalence := idealRelation.equivalence with *
  have compatible := idealRelation.mul_compatible with *
  unfold IsMaximalIdeal
  refine ⟨proper, ?_⟩
  intros J properJ contains
  have idealJ : IsIdeal(A, add, zero, neg, mul, J) by simp [IsProperIdeal]
  have boundedJ := IsIdeal.subset_carrier with idealJ
  apply Subset.antisymmetric
    intros x hx
    have xInA := boundedJ with x, hx
    by_contra outside
    have xClassIn := quotient.contains_class at A, idealRelation(A, add, neg, I), x with *
    have nonzero : ⟦x⟧[A, idealRelation(A, add, neg, I)] ≠ ⟦zero⟧[A, idealRelation(A, add, neg, I)]
      intro equal
      have member := idealClass.eq_zero.forward with ring, ideal, xInA, equal
      exact outside with member
    obtain ⟨Y, inverse⟩ := IsField.inverse_exists with field, xClassIn, nonzero
    have yClassIn := inverse.right.left
    obtain ⟨y, hy, shape⟩ := quotient.representative with yClassIn
    have left := inverse.right.right.left
    have multiply := quotientBinary.classes at A, idealRelation(A, add, neg, I), mul, y, x with *
    have equal : ⟦call2(mul, y, x)⟧[A, idealRelation(A, add, neg, I)] = ⟦one⟧[A, idealRelation(A, add, neg, I)] by cc
    have productInA := IsRing.mul_closed at A, add, zero, neg, mul, one, y, x with *
    have congruence := idealClass.eq_iff_congruent.forward with ring, ideal, productInA, oneInA, equal
    have differenceInJ : call2(add, call2(mul, y, x), neg(one)) ∈ J
      exact contains with call2(add, call2(mul, y, x), neg(one)), congruence
    have productInJ := IsIdeal.mul_left_closed with hy, hx
    have negative := IsIdeal.neg_closed at A, add, zero, neg, mul, J, call2(add, call2(mul, y, x), neg(one)) with *
    have sum := IsIdeal.add_closed at A, add, zero, neg, mul, J, call2(mul, y, x), neg(call2(add, call2(mul, y, x), neg(one))) with *
    have oneInJ : one ∈ J
      ring_nf at sum
      exact sum
    exact properJ.right with oneInJ
  . exact contains

theorem idealQuotient.is_field_iff_maximal (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows IsField((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔ IsMaximalIdeal(A, add, zero, neg, mul, one, I)
proof
  constructor
  . intro field
    exact idealQuotient.maximal_of_is_field with *
  . intro maximal
    exact idealQuotient.is_field_of_maximal with *

def idealQuotientInverse (A add zero neg mul one I : Set) : Set :=
  fieldInverse((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])

theorem idealQuotient.field_of_maximal (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)
  shows IsFieldWithInverse((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)],
    idealQuotientInverse(A, add, zero, neg, mul, one, I))
proof
  have structure := idealQuotient.is_field_of_maximal with *
  have field := IsField.field with structure
  unfold idealQuotientInverse
  exact field