-- Ring homomorphisms preserve finite sums and products, pointwise (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.FiniteHom
import FiniteProduct
import Group.Power

section Homomorphisms
variable (A add zero neg mul one B plus z minus times unit h : 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(h, R, S)

theorem indexedRingSum.map (w v f : Set, n : Nat)
  shows WeightedValues(w, f, A, n) →
    (∀ i ∈ n, v(f(i)) = h(w(f(i)))) →
    h(indexedRingSum(w, f, add, zero, n)) = indexedRingSum(v, f, plus, z, n)
proof
  induction n
  | zero =>
    intros values equations
    rw [indexedRingSum, indexedRingSum]
    exact IsRingHom.zero with hom
  | succ(k) using ih =>
    intros values equations
    have prefix := WeightedValues.prefix at w, f, A, k with *
    have last := WeightedValues.last at w, f, A, k with *
    have smaller : ∀ i ∈ k, v(f(i)) = h(w(f(i)))
      intros i hi
      have next := membership.into_successor at i, k with *
      exact equations with i, next
    have lastEquation := equations with k, membership.self_successor at k with *
    have previous := ih with prefix, smaller
    have closure := indexedRingSum.closed at A, add, zero, neg, mul, one, w, f, k with *
    have prefixIn := closure with prefix
    have preserved := IsRingHom.add at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, indexedRingSum(w, f, add, zero, k), w(f(k)) with *
    rw [indexedRingSum, indexedRingSum, preserved, previous, lastEquation]
    rfl

theorem finiteRingSum.map (V w v : Set)
  requires finite : Finite(V)
  requires weightsW : w : V → R
  requires weightsV : v : V → S
  requires entries : ∀ i ∈ V, v(i) = h(w(i))
  shows h(finiteRingSum(V, R, w)) = finiteRingSum(V, S, v)
proof
  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *
  obtain ⟨n, natural, f, enumeration, equationW⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have values := WeightedValues.of_functions with weightsW, function
  have equationV := finiteRingSum.enumeration at V, B, plus, z, minus, times, unit, v, f, n with *
  have equations : ∀ i ∈ n, v(f(i)) = h(w(f(i)))
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact entries with f(i), member
  have preserved := indexedRingSum.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, w, v, f, n with *
  rw [equationW, equationV]
  exact preserved with values, equations

theorem indexedRingProduct.map (w v f : Set, n : Nat)
  shows WeightedValues(w, f, A, n) →
    (∀ i ∈ n, v(f(i)) = h(w(f(i)))) →
    h(indexedRingProduct(w, f, mul, one, n)) = indexedRingProduct(v, f, times, unit, n)
proof
  induction n
  | zero =>
    intros values equations
    rw [indexedRingProduct, indexedRingProduct]
    exact IsRingHom.one with hom
  | succ(k) using ih =>
    intros values equations
    have prefix := WeightedValues.prefix at w, f, A, k with *
    have last := WeightedValues.last at w, f, A, k with *
    have smaller : ∀ i ∈ k, v(f(i)) = h(w(f(i)))
      intros i hi
      have next := membership.into_successor at i, k with *
      exact equations with i, next
    have lastEquation := equations with k, membership.self_successor at k with *
    have previous := ih with prefix, smaller
    have closure := indexedRingProduct.closed at A, add, zero, neg, mul, one, w, f, k with *
    have prefixIn := closure with prefix
    have preserved := IsRingHom.mul at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, indexedRingProduct(w, f, mul, one, k), w(f(k)) with *
    rw [indexedRingProduct, indexedRingProduct, preserved, previous, lastEquation]
    rfl

theorem finiteRingProduct.map (V w v : Set)
  requires finite : Finite(V)
  requires weightsW : w : V → R
  requires weightsV : v : V → S
  requires entries : ∀ i ∈ V, v(i) = h(w(i))
  shows h(finiteRingProduct(V, R, w)) = finiteRingProduct(V, S, v)
proof
  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *
  obtain ⟨n, natural, f, enumeration, equationW⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have values := WeightedValues.of_functions with weightsW, function
  have equationV := finiteRingProduct.enumeration at V, B, plus, z, minus, times, unit, v, f, n with *
  have equations : ∀ i ∈ n, v(f(i)) = h(w(f(i)))
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact entries with f(i), member
  have preserved := indexedRingProduct.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, w, v, f, n with *
  rw [equationW, equationV]
  exact preserved with values, equations

theorem IsRingHom.pow (x : Set, n : Nat)
  requires element : x ∈ R
  shows h(monoidPow(R, x, n)) = monoidPow(S, h(x), n)
proof
  induction n
  | zero =>
    rw [monoidPow.zero, monoidPow.zero]
    exact IsRingHom.one with hom
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with source
    have multiplicative := IsRing.multiplicative with ordinary
    have product := IsRingHom.mul at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, monoidPow(R, x, k) with *
    rw [monoidPow.succ, monoidPow.succ, product, ih]
    rfl

end Homomorphisms