-- Reindexing and zero-extension for grouped finite ring sums (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.PushforwardTransport
import Pushforward
import PushforwardComposition

theorem finitePushforward.reindex (D E C A add zero neg mul one h k w v f : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : E → A
  requires bijective : BijectiveBetween(f, D, E)
  requires indices : ∀ d ∈ D, h(d) = k(f(d))
  requires weights : ∀ d ∈ D, w(d) = v(f(d))
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) =
    finitePushforward(E, C, A, add, zero, neg, mul, one, k, v)
proof
  have equivalent : Equipotent(D, E)
    unfold Equipotent
    refine ⟨f, bijective⟩
  have finiteE := Finite.of_equipotent with finite, equivalent
  have inj := Bijective.injective with bijective
  have functionF := Injective.function with inj
  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *
  have rightFunction := finitePushforward.function at E, C, A, add, zero, neg, mul, one, k, 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 E, A, add, zero, neg, mul, one, k, v, c with *
  have pointwise : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = pushforwardWeights(E, A, add, zero, neg, mul, one, k, v, c)(f(d))
    intros d hd
    have inE := FunctionBetween.apply_closed at f, D, E, d with *
    have index := indices with d, hd
    have weight := weights with d, hd
    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *
    have right := pushforwardWeights.value at E, A, add, zero, neg, mul, one, k, v, c, f(d) with *
    cc
  have same := finiteRingSum.reindex at D, E, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(E, A, add, zero, neg, mul, one, k, v, c), f with *
  have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
  have right := finitePushforward.value at E, C, A, add, zero, neg, mul, one, k, v, c with *
  cc

theorem finitePushforward.restrict (D S 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
  requires subset : S ⊆ D
  requires vanishes : ∀ d ∈ D, ¬(d ∈ S) → w(d) = zero
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) =
    finitePushforward(S, C, A, add, zero, neg, mul, one, h, restrict(w, S))
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have finiteS := Finite.subset with finite, subset
  have closed : ∀ s ∈ S, w(s) ∈ A
    intros s hs
    have included := subset
    have member := included with s, hs
    exact FunctionBetween.apply_closed at w, D, A, s with *
  have restricted := restrict.function at w, D, A, S, A with *
  have leftFunction := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *
  have rightFunction := finitePushforward.function at S, C, A, add, zero, neg, mul, one, h, restrict(w, S) 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 selectedS := pushforwardWeights.function at S, A, add, zero, neg, mul, one, h, restrict(w, S), c with *
  have selectedClosed : ∀ s ∈ S, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(s) ∈ A
    intros s hs
    have included := subset
    have member := included with s, hs
    exact FunctionBetween.apply_closed at pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), D, A, s with *
  have selectedRestriction := restrict.function at pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), D, A, S, A with *
  have absent : ∀ d ∈ D, ¬(d ∈ S) → pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = zero
    intros d hd outside
    have sourceZero := vanishes with d, hd, outside
    have weight := FunctionBetween.apply_closed at w, D, A, d with *
    have value := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *
    have alternatives : c = h(d) ∨ c ≠ h(d) by tauto
    cases alternatives with same | different
    . have selected := singleValue.same at A, zero, w(d), h(d), c with *
      cc
    . have selected := singleValue.other at A, zero, w(d), h(d), c with *
      cc
  have sameWeights : restrict(pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), S) = pushforwardWeights(S, A, add, zero, neg, mul, one, h, restrict(w, S), c)
    apply FunctionBetween.ext with selectedRestriction, selectedS
    intros s hs
    have included := subset
    have member := included with s, hs
    have restriction := restrict.apply at pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), D, A, S, A, s with *
    have source := restrict.apply at w, D, A, S, A, s with *
    have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, s with *
    have right := pushforwardWeights.value at S, A, add, zero, neg, mul, one, h, restrict(w, S), c, s with *
    cc
  have sum := finiteRingSum.restrict at D, S, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) with *
  have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
  have right := finitePushforward.value at S, C, A, add, zero, neg, mul, one, h, restrict(w, S), c with *
  cc

theorem finitePushforward.zero_extension (D S C A add zero neg mul one h w v : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : S → A
  requires subset : S ⊆ D
  requires agreement : ∀ s ∈ S, w(s) = v(s)
  requires vanishes : ∀ d ∈ D, ¬(d ∈ S) → w(d) = zero
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) = finitePushforward(S, C, A, add, zero, neg, mul, one, h, v)
proof
  have closed : ∀ s ∈ S, w(s) ∈ A
    intros s hs
    have value := FunctionBetween.apply_closed with *
    have equal := agreement with s, hs
    rwa equal
  have restricted := restrict.function with *
  have same : restrict(w, S) = v
    apply FunctionBetween.ext with restricted, weightsV
    intros s hs
    have value := restrict.apply with *
    have equal := agreement with s, hs
    cc
  have sum := finitePushforward.restrict at D, S, C, A, add, zero, neg, mul, one, h, w with *
  rwa same at sum

theorem finitePushforward.singleton (C A add zero neg mul one h w x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : {x} → A
  shows finitePushforward({x}, C, A, add, zero, neg, mul, one, h, w) = coefficientSingle(C, A, zero, w(x), h(x))
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have finite := Finite.singleton at x
  have member := singleton.self at x
  have coefficient := FunctionBetween.apply_closed with *
  have pushed := finitePushforward.function at {x}, C, A, add, zero, neg, mul, one, h, w with *
  have single := coefficientSingle.function at C, A, zero, w(x), h(x) with *
  apply FunctionBetween.ext with pushed, single
  intros c hc
  have selected := pushforwardWeights.function at {x}, A, add, zero, neg, mul, one, h, w, c with *
  have sum := finiteRingSum.singleton at A, add, zero, neg, mul, one, pushforwardWeights({x}, A, add, zero, neg, mul, one, h, w, c), x with *
  have left := finitePushforward.value at {x}, C, A, add, zero, neg, mul, one, h, w, c with *
  have weight := pushforwardWeights.value at {x}, A, add, zero, neg, mul, one, h, w, c, x with *
  have right := coefficientSingle.value at C, A, zero, w(x), h(x), c with *
  cc

-- Recover a sparse coefficient map from an injectively indexed finite domain.
-- The domain may include entries of weight zero.
theorem finitePushforward.reconstruct (D C A add zero neg mul one h w p : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weights : w : D → A
  requires target : p : C → A
  requires values : ∀ d ∈ D, w(d) = p(h(d))
  requires injective : ∀ d ∈ D, ∀ e ∈ D, h(d) = h(e) → d = e
  requires covers : ∀ c ∈ C, p(c) ≠ zero → ∃ d ∈ D, h(d) = c
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w) = p
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have pushed := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, w with *
  apply FunctionBetween.ext with pushed, target
  intros c hc
  have coefficient := FunctionBetween.apply_closed at p, C, A, c with *
  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
  have value := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
  have alternatives : p(c) = zero ∨ p(c) ≠ zero by tauto
  cases alternatives with vanishing | nonzero
  . have allZero : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d) = zero
      intros d hd
      have weight := FunctionBetween.apply_closed at w, D, A, d with *
      have output := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *
      have source := values with d, hd
      have cases : c = h(d) ∨ c ≠ h(d) by tauto
      cases cases with same | different
      . have chosen := singleValue.same at A, zero, w(d), h(d), c with *
        cc
      . have chosen := singleValue.other at A, zero, w(d), h(d), c with *
        cc
    have sum := finiteRingSum.zero at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) with *
    cc
  . obtain ⟨d, hd, image⟩ := covers with c, hc, nonzero
    have single := coefficientSingle.function at D, A, zero, p(c), d with *
    have equal : pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) = coefficientSingle(D, A, zero, p(c), d)
      apply FunctionBetween.ext with selected, single
      intros e he
      have weight := FunctionBetween.apply_closed at w, D, A, e with *
      have output := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, e with *
      have source := values with e, he
      have cases : e = d ∨ e ≠ d by tauto
      cases cases with same | different
      . have index : c = h(e)
          cc
        have chosen := singleValue.same at A, zero, w(e), h(e), c with *
        have point := coefficientSingle.same at D, A, zero, p(c), d with *
        cc
      . have differentImage : c ≠ h(e)
          intro equalImage
          have equalIndices : h(e) = h(d) by cc
          have equal := injective with e, he, d, hd, equalIndices
          exact different with equal
        have chosen := singleValue.other at A, zero, w(e), h(e), c with *
        have point := coefficientSingle.other at D, A, zero, p(c), d, e with *
        cc
    have sum := finiteRingSum.single at D, A, add, zero, neg, mul, one, p(c), d with *
    cc

-- A group with exactly one source index has that source's coefficient.
theorem finitePushforward.unique_fiber (D C A add zero neg mul one h w d c : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weights : w : D → A
  requires source : d ∈ D
  requires target : c ∈ C
  requires image : h(d) = c
  requires unique : ∀ e ∈ D, h(e) = c → e = d
  shows finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)(c) = w(d)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have coefficient := FunctionBetween.apply_closed at w, D, A, d with *
  have selected := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
  have single := coefficientSingle.function at D, A, zero, w(d), d with *
  have equal : pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c) = coefficientSingle(D, A, zero, w(d), d)
    apply FunctionBetween.ext with selected, single
    intros e he
    have weight := FunctionBetween.apply_closed at w, D, A, e with *
    have output := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, e with *
    have alternatives : e = d ∨ e ≠ d by tauto
    cases alternatives with same | different
    . have index : c = h(e)
        cc
      have chosen := singleValue.same at A, zero, w(e), h(e), c with *
      have point := coefficientSingle.same at D, A, zero, w(d), d with *
      cc
    . have differentImage : c ≠ h(e)
        intro equality
        have forward : h(e) = c by cc
        have equal := unique with e, he, forward
        exact different with equal
      have chosen := singleValue.other at A, zero, w(e), h(e), c with *
      have point := coefficientSingle.other at D, A, zero, w(d), d, e with *
      cc
  have sum := finiteRingSum.single at D, A, add, zero, neg, mul, one, w(d), d with *
  have value := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
  cc