-- Unital ring homomorphisms over separate pieces and their kernels: the
-- engine under Homomorphism, entirely 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.Ring.HomomorphismCore
import QuotientCore
import Relation.QuotientMap

-- IsRingHom(f, A, add, …, B, plus, …) is the homomorphism over separate
-- pieces; the bundled f : R →+* S is defined in Homomorphism and bridged
-- to this form. Preservation data is separate from source and target ring laws.
-- Zero and negation laws are included to make the interface directly usable.
predicate IsRingHom (f A add zero neg mul one B plus z minus times unit : Set) :=
  FunctionBetween(f, A, B) ∧ f(zero) = z ∧ f(one) = unit ∧
  (∀ x ∈ A, f(neg(x)) = minus(f(x))) ∧
  (∀ x ∈ A, ∀ y ∈ A, f(call2(add, x, y)) = plus(f(x), f(y))) ∧
  (∀ x ∈ A, ∀ y ∈ A, f(call2(mul, x, y)) = times(f(x), f(y)))

notation scoped IsRingHom(f, R, S) => IsRingHom(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S.carrier, S.add, S.zero, S.neg, S.mul, S.one)

predicate IsRingIso (f A add zero neg mul one B plus z minus times unit : Set) :=
  IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit) ∧
  BijectiveBetween(f, A, B)

notation scoped IsRingIso(f, R, S) => IsRingIso(f, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S.carrier, S.add, S.zero, S.neg, S.mul, S.one)

theorem IsRingHom.function (f A add zero neg mul one B plus z minus times unit : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows f : A → B
proof
  exact hom.left

theorem IsRingHom.zero (f A add zero neg mul one B plus z minus times unit : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows f(zero) = z
proof
  exact hom.right.left

theorem IsRingHom.one (f A add zero neg mul one B plus z minus times unit : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows f(one) = unit
proof
  exact hom.right.right.left

theorem IsRingHom.neg (f A add zero neg mul one B plus z minus times unit x : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires hx : x ∈ A
  shows f(neg(x)) = minus(f(x))
proof
  exact hom.right.right.right.left with x, hx

theorem IsRingHom.add (f A add zero neg mul one B plus z minus times unit x y : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(call2(add, x, y)) = plus(f(x), f(y))
proof
  exact hom.right.right.right.right.left with x, hx, y, hy

theorem IsRingHom.mul (f A add zero neg mul one B plus z minus times unit x y : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(call2(mul, x, y)) = times(f(x), f(y))
proof
  exact hom.right.right.right.right.right with x, hx, y, hy

theorem IsRingHom.closed (f A add zero neg mul one B plus z minus times unit x : Set)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires hx : x ∈ A
  shows f(x) ∈ B
proof
  have function := IsRingHom.function with hom
  exact FunctionBetween.apply_closed with *

def ringKernel (f A z : Set) : Set := {x ∈ A | f(x) = z}

theorem IsRingHom.kernel_ideal (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsIdeal(A, add, zero, neg, mul, ringKernel(f, A, z))
proof
  have sourceRing := IsCommRing.ring with source
  have targetRing := IsCommRing.ring with target
  have zeroIn := IsRing.zero_in_carrier at A, add, zero, neg, mul, one with *
  have zeroValue := IsRingHom.zero with hom
  unfold IsIdeal
  refine ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩
  . settle with Subset, ringKernel.membership
  . apply ringKernel.membership.backward at f, A, z, zero
    refine ⟨zeroIn, zeroValue⟩
  . intros x hx y hy
    obtain ⟨xIn, xValue⟩ := ringKernel.membership.forward with hx
    obtain ⟨yIn, yValue⟩ := ringKernel.membership.forward with hy
    have sumIn := IsRing.add_closed at A, add, zero, neg, mul, one, x, y with *
    have preserved := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *
    apply ringKernel.membership.backward
    refine ⟨sumIn, ?_⟩
    rw [preserved, xValue, yValue]
    ring
  . intros x hx
    obtain ⟨xIn, xValue⟩ := ringKernel.membership.forward with hx
    have negIn := IsRing.neg_closed at A, add, zero, neg, mul, one, x with *
    have preserved := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
    apply ringKernel.membership.backward
    refine ⟨negIn, ?_⟩
    rw [preserved, xValue]
    ring
  . intros a ha x hx
    obtain ⟨xIn, xValue⟩ := ringKernel.membership.forward with hx
    have aValueIn := IsRingHom.closed with ha
    have leftIn := IsRing.mul_closed at A, add, zero, neg, mul, one, a, x with *
    have rightIn := IsRing.mul_closed at A, add, zero, neg, mul, one, x,
      a with *
    have leftValue := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, a, x with *
    have rightValue := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, a with *
    constructor
    . apply ringKernel.membership.backward at f, A, z, call2(mul, a, x)
      refine ⟨leftIn, ?_⟩
      rw [leftValue, xValue]
      ring
    . apply ringKernel.membership.backward at f, A, z, call2(mul, x, a)
      refine ⟨rightIn, ?_⟩
      rw [rightValue, xValue]
      ring

theorem IsRingHom.sub (f A add zero neg mul one B plus z minus times unit x y : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows f(call2(add, x, neg(y))) = plus(f(x), minus(f(y)))
proof
  have ring := IsCommRing.ring with source
  have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, y with *
  have sum := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, neg(y) with *
  have inverse := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *
  cc

theorem IsRingHom.kernel_congruent (f A add zero neg mul one B plus z minus times unit x y : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows Congruent(add, neg, ringKernel(f, A, z), x, y) ↔ f(x) = f(y)
proof
  have ring := IsCommRing.ring with source
  have negative := IsRing.neg_closed at A, add, zero, neg, mul, one, y with *
  have difference := IsRing.add_closed at A, add, zero, neg, mul, one, x, neg(y) with *
  have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
  have fy := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *
  have mapped := IsRingHom.sub at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *
  constructor
  . intro member
    unfold Congruent at member
    have value := ringKernel.membership.forward with member
    have equation : plus(f(x), minus(f(y))) = z by cc
    linear_combination equation
  . intro equal
    unfold Congruent
    apply ringKernel.membership.backward
    refine ⟨difference, ?_⟩
    rw [mapped, equal]
    ring

theorem IsRingHom.respects_ideal (f A add zero neg mul one B plus z minus times unit I : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires killed : I ⊆ ringKernel(f, A, z)
  shows Respects(f, A, idealRelation(A, add, neg, I))
proof
  intros x hx y hy related
  have congruent := idealRelation.relates.forward with *
  have member := killed with call2(add, x, neg(y)), congruent
  have kernelCongruent : Congruent(add, neg, ringKernel(f, A, z), x, y) by exact member
  exact IsRingHom.kernel_congruent.forward with *

-- Users supply the three usual laws; zero and negation are derived.
theorem IsRingHom.of_add_mul_one (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires function : f : A → B
  requires additive : ∀ x ∈ A, ∀ y ∈ A, f(call2(add, x, y)) = plus(f(x), f(y))
  requires multiplicative : ∀ x ∈ A, ∀ y ∈ A, f(call2(mul, x, y)) = times(f(x), f(y))
  requires unital : f(one) = unit
  shows IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times,
    unit)
proof
  have ring := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ring
  have fZeroIn := FunctionBetween.apply_closed with *
  have zeroSum : call2(add, zero, zero) = zero by ring
  have mappedZero := additive with zero, zeroIn, zero, zeroIn
  rw zeroSum at mappedZero
  have zeroValue : f(zero) = z by linear_combination -mappedZero
  unfold IsRingHom
  refine ⟨function, ⟨zeroValue, ⟨unital, ⟨?_, ⟨additive, multiplicative⟩⟩⟩⟩⟩
  intros x hx
  have negIn := IsRing.neg_closed with hx
  have fxIn := FunctionBetween.apply_closed with hx
  have fnIn := FunctionBetween.apply_closed at f, A, B, neg(x) with *
  have inverse := IsRing.add_inverse_left with hx
  have mapped := additive with neg(x), negIn, x, hx
  rw [inverse, zeroValue] at mapped
  linear_combination -mapped

theorem IsRingHom.identity (A add zero neg mul one : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  shows IsRingHom(identity(A), A, add, zero, neg, mul, one, A, add, zero, neg, mul, one)
proof
  have function := identity.function at A
  have ring := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ring
  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, Identity]
  have zeroValue := identity.apply at zero, A with *
  have oneValue := identity.apply at one, A with *
  unfold IsRingHom
  refine ⟨function, ⟨zeroValue, ⟨oneValue, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩
  . intros x hx
    have negative := IsRing.neg_closed with hx
    have input := identity.apply with hx
    have output := identity.apply at neg(x), A with *
    cc
  . intros x hx y hy
    have closed := IsRing.add_closed with hx, hy
    have vx := identity.apply with hx
    have vy := identity.apply with hy
    have output := identity.apply at call2(add, x, y), A with *
    cc
  . intros x hx y hy
    have closed := IsRing.mul_closed with hx, hy
    have vx := identity.apply with hx
    have vy := identity.apply with hy
    have output := identity.apply at call2(mul, x, y), A with *
    cc

theorem IsRingHom.compose (f g A add zero neg mul one B plus z minus times unit C sum o inverse product e : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires first : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires second : IsRingHom(g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e)
  shows IsRingHom(compose(g, f, A, B, C), A, add, zero, neg, mul, one, C, sum, o, inverse, product, e)
proof
  have ff := IsRingHom.function with first
  have gf := IsRingHom.function with second
  have function := compose.function at g, f, A, B, C with *
  have ring := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier at A, add, zero, neg, mul, one with *
  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, Identity]
  have fZero := IsRingHom.zero with first
  have gZero := IsRingHom.zero with second
  have fOne := IsRingHom.one with first
  have gOne := IsRingHom.one with second
  have zeroValue := compose.apply at g, f, A, B, C, zero with *
  have oneValue := compose.apply at g, f, A, B, C, one with *
  unfold IsRingHom
  refine ⟨function, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩
  . cc
  . cc
  . intros x hx
    have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
    have closed := IsRing.neg_closed at A, add, zero, neg, mul, one, x with *
    have fNeg := IsRingHom.neg at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
    have gNeg := IsRingHom.neg at g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e, f(x) with *
    have input := compose.apply at g, f, A, B, C, x with *
    have output := compose.apply at g, f, A, B, C, neg(x) with *
    cc
  . intros x hx y hy
    have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
    have fy := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *
    have closed := IsRing.add_closed at A, add, zero, neg, mul, one, x, y with *
    have fOp := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *
    have gOp := IsRingHom.add at g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e, f(x), f(y) with *
    have vx := compose.apply at g, f, A, B, C, x with *
    have vy := compose.apply at g, f, A, B, C, y with *
    have output := compose.apply at g, f, A, B, C, call2(add, x, y) with *
    cc
  . intros x hx y hy
    have fx := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x with *
    have fy := IsRingHom.closed at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, y with *
    have closed := IsRing.mul_closed at A, add, zero, neg, mul, one, x, y with *
    have fOp := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, y with *
    have gOp := IsRingHom.mul at g, B, plus, z, minus, times, unit, C, sum, o, inverse, product, e, f(x), f(y) with *
    have vx := compose.apply at g, f, A, B, C, x with *
    have vy := compose.apply at g, f, A, B, C, y with *
    have output := compose.apply at g, f, A, B, C, call2(mul, x, y) with *
    cc

theorem IsRingIso.hom (f A add zero neg mul one B plus z minus times unit : Set)
  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times,
    unit)
proof
  simp [IsRingIso]

theorem IsRingIso.bijective (f A add zero neg mul one B plus z minus times unit : Set)
  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows BijectiveBetween(f, A, B)
proof
  simp [IsRingIso]

-- Isomorphisms are reversible; the inverse graph is the relational converse.
theorem IsRingIso.inverse (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires iso : IsRingIso(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  shows IsRingIso(converse(f, A, B), B, plus, z, minus, times, unit, A, add, zero, neg, mul, one)
proof
  have hom := IsRingIso.hom with iso
  have bijective := IsRingIso.bijective with iso
  have inverse := converse.function_of_bijective with bijective
  have inverseBijective := converse.bijective with bijective
  have ring := IsCommRing.ring with source
  have inverseHom : IsRingHom(converse(f, A, B), B, plus, z, minus, times, unit, A, add, zero, neg, mul, one)
    apply IsRingHom.of_add_mul_one with target, source, inverse
    . intros x hx y hy
      have px := FunctionBetween.apply_closed with inverse, hx
      have py := FunctionBetween.apply_closed with inverse, hy
      have fx := Bijective.apply_inverse with bijective, hx
      have fy := Bijective.apply_inverse with bijective, hy
      have closed := IsRing.add_closed at A, add, zero, neg, mul, one, converse(f, A, B)(x), converse(f, A, B)(y) with *
      have mapped := IsRingHom.add at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, converse(f, A, B)(x), converse(f, A, B)(y) with *
      have recovered := Bijective.inverse_apply with bijective, closed
      cc
    . intros x hx y hy
      have px := FunctionBetween.apply_closed with inverse, hx
      have py := FunctionBetween.apply_closed with inverse, hy
      have fx := Bijective.apply_inverse with bijective, hx
      have fy := Bijective.apply_inverse with bijective, hy
      have closed := IsRing.mul_closed at A, add, zero, neg, mul, one, converse(f, A, B)(x), converse(f, A, B)(y) with *
      have mapped := IsRingHom.mul at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, converse(f, A, B)(x), converse(f, A, B)(y) with *
      have recovered := Bijective.inverse_apply with bijective, closed
      cc
    . have oneIn : one ∈ A
        simp [IsCommRing, IsRing, IsMonoid, Identity]
      have mapped := IsRingHom.one with hom
      have recovered := Bijective.inverse_apply with bijective, oneIn
      cc
  unfold IsRingIso
  refine ⟨inverseHom, inverseBijective⟩