-- Group finite ring sums along a function, without Choice.
-- 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.Pushforward
import SumExtension
import Cardinal.FiniteImage

defgraph pushforwardWeights (D A add zero neg mul one h w c : Set) (d ∈ D) : A :=
  singleValue(A, zero, w(d), h(d), c)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires weights : w : D → A
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have value := FunctionBetween.apply_closed at w, D, A, d with *
  exact singleValue.closed at A, zero, w(d), h(d), c with *

defgraph finitePushforward (D C A add zero neg mul one h w : Set) (c ∈ C) : A :=
  finiteRingSum(D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c))
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires finite : Finite(D)
requires weights : w : D → A
proof
  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
  exact finiteRingSum.closed at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) with *

theorem finitePushforward.outside (D C A add zero neg mul one h w c : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weights : w : D → A
  requires index : c ∈ C
  requires absent : ¬(c ∈ functionImage(h, D, C))
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)(c) = zero
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
  have vanishes : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = zero
    intros d hd
    have coefficient := FunctionBetween.apply_closed at w, D, A, d with *
    have different : c ≠ h(d)
      intro equal
      have inImage : c ∈ functionImage(h, D, C) := functionImage.membership.backward with ⟨index, d, hd, equal⟩
      exact absent with inImage
    have term := singleValue.other with zeroIn, coefficient, different
    have value := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *
    cc
  have sumZero := finiteRingSum.zero with *
  have value := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
  cc

theorem finitePushforward.support (D C A add zero neg mul one h w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weights : w : D → A
  shows functionSupport(finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), C, zero) ⊆ functionImage(h, D, C)
proof
  intros c hc
  have data := functionSupport.membership.forward with hc
  have alternatives : c ∈ functionImage(h, D, C) ∨ ¬(c ∈ functionImage(h, D, C)) by tauto
  cases alternatives with present | absent
  . exact present
  . have vanishes := finitePushforward.outside with absent
    exfalso
    exact data.right with vanishes

theorem finitePushforward.map (D C A add zero neg mul one h w E : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weights : w : D → A
  requires indexMap : h : E → C
  requires domain : D ⊆ E
  shows CoefficientMap(finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), C, A, zero)
proof
  have function := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *
  have finiteImage := Finite.function_image with *
  have subset := finitePushforward.support at D, C, A, add, zero, neg, mul, one, h, w with *
  have supportFinite := Finite.subset with finiteImage, subset
  unfold CoefficientMap
  refine ⟨function, supportFinite⟩

section Linearity
variable (A add zero neg mul one : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
notation ring R := (A, add, zero, neg, mul, one)

theorem singleValue.add (a b j i : Set)
  requires valueA : a ∈ A
  requires valueB : b ∈ A
  shows singleValue(A, zero, a + b, j, i) = singleValue(A, zero, a, j, i) + singleValue(A, zero, b, j, i)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have sumIn := IsRing.add_closed at A, add, zero, neg, mul, one, a, b with *
  have alternatives : i = j ∨ i ≠ j by tauto
  cases alternatives with same | different
  . have sum := singleValue.same at A, zero, a + b, j, i with *
    have left := singleValue.same at A, zero, a, j, i with *
    have right := singleValue.same at A, zero, b, j, i with *
    cc
  . have sum := singleValue.other at A, zero, a + b, j, i with *
    have left := singleValue.other at A, zero, a, j, i with *
    have right := singleValue.other at A, zero, b, j, i with *
    rw [sum, left, right]
    ring

theorem pushforwardWeights.add (D h w v c : Set)
  requires weightsW : w : D → A
  requires weightsV : v : D → A
  shows pushforwardWeights(D, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c) =
    coefficientAdd(D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c))
proof
  have sumFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, w, v with *
  have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
  have selectedV := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, v, c with *
  have leftFunction := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c with *
  have rightFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c) with *
  apply FunctionBetween.ext with leftFunction, rightFunction
  intros d hd
  have wIn := FunctionBetween.apply_closed at w, D, A, d with *
  have vIn := FunctionBetween.apply_closed at v, D, A, d with *
  have source := coefficientAdd.value at D, A, add, zero, neg, mul, one, w, v, d with *
  have selectedSum := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c, d with *
  have valueW := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *
  have valueV := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, v, c, d with *
  have target := coefficientAdd.value at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c), d with *
  have distribute := singleValue.add at A, add, zero, neg, mul, one, w(d), v(d), h(d), c with *
  cc

theorem finitePushforward.add (D C h w v : Set)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : D → A
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v)) =
    coefficientAdd(C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), finitePushforward(D, C, A, add, zero, neg, mul, one, h, v))
proof
  have sumFunction := coefficientAdd.function at D, A, add, zero, neg, mul, one, w, v with *
  have pushW := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *
  have pushV := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, v with *
  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v) with *
  have rightFunction := coefficientAdd.function at C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), finitePushforward(D, C, A, add, zero, neg, mul, one, h, v) with *
  apply FunctionBetween.ext with leftFunction, rightFunction
  intros c hc
  have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
  have selectedV := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, v, c with *
  have weightSum := pushforwardWeights.add at A, add, zero, neg, mul, one, D, h, w, v, c with *
  have distribute := finiteRingSum.add at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, v, c) with *
  have leftValue := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, coefficientAdd(D, A, add, zero, neg, mul, one, w, v), c with *
  have valueW := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
  have valueV := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, v, c with *
  have rightValue := coefficientAdd.value at C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, w), finitePushforward(D, C, A, add, zero, neg, mul, one, h, v), c with *
  cc

end Linearity