-- Permuting the rows of a matrix multiplies its determinant by the sign of
-- the permutation: composition with the inverse of σ is a bijection of the
-- permutations, each Leibniz term of the permuted matrix is the term of the
-- original at the shifted permutation times the sign of σ
-- 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.DeterminantRowPermutation
import PermutationSignCompose
import DeterminantLinearity

-- A permutation composed with its inverse on either side is the identity.
theorem permutations.converse_compose (n : Nat) (σ : Set)
  requires permutation : σ ∈ permutations(n)
  shows compose(converse(σ, n, n), σ, n, n, n) = identity(n)
proof
  have function := permutations.function with permutation
  have inverse := permutations.converse with permutation
  have inverseFunction := permutations.function with inverse
  have composed := permutations.compose at n, σ, converse(σ, n, n) with permutation, inverse
  have composedFunction := permutations.function with composed
  have idFunction := identity.function at n
  have same : ∀ x ∈ n, compose(converse(σ, n, n), σ, n, n, n)(x) = identity(n)(x)
    intros x hx
    have value := compose.apply at converse(σ, n, n), σ, n, n, n, x
      with function, inverseFunction, hx
    have cancel := permutations.inverse_apply at n, σ, x with permutation, hx
    have idValue := identity.apply at x, n with hx
    rw [value, cancel, idValue]
    rfl
  exact FunctionBetween.ext with composedFunction, idFunction, same

theorem permutations.compose_converse (n : Nat) (σ : Set)
  requires permutation : σ ∈ permutations(n)
  shows compose(σ, converse(σ, n, n), n, n, n) = identity(n)
proof
  have function := permutations.function with permutation
  have inverse := permutations.converse with permutation
  have inverseFunction := permutations.function with inverse
  have composed := permutations.compose at n, converse(σ, n, n), σ with inverse, permutation
  have composedFunction := permutations.function with composed
  have idFunction := identity.function at n
  have same : ∀ x ∈ n, compose(σ, converse(σ, n, n), n, n, n)(x) = identity(n)(x)
    intros x hx
    have value := compose.apply at σ, converse(σ, n, n), n, n, n, x
      with inverseFunction, function, hx
    have cancel := permutations.apply_inverse at n, σ, x with permutation, hx
    have idValue := identity.apply at x, n with hx
    rw [value, cancel, idValue]
    rfl
  exact FunctionBetween.ext with composedFunction, idFunction, same

-- Composition with the inverse of σ, p ↦ p ∘ σ⁻¹, on the permutations.
defgraph permutationShift (n σ : Set) (p ∈ permutations(n)) : permutations(n) :=
  compose(p, converse(σ, n, n), n, n, n)
requires permutation : σ ∈ permutations(n)
proof
  have inverse := permutations.converse with permutation
  exact permutations.compose at n, converse(σ, n, n), p with inverse, assumption

theorem permutationShift.apply (n : Nat) (σ p i : Set)
  requires permutation : σ ∈ permutations(n)
  requires hp : p ∈ permutations(n)
  requires hi : i ∈ n
  shows permutationShift(n, σ)(p)(i) = p(converse(σ, n, n)(i))
proof
  have inverse := permutations.converse with permutation
  have inverseFunction := permutations.function with inverse
  have function := permutations.function with hp
  have value := permutationShift.value at n, σ, p with permutation, hp
  rw value
  exact compose.apply with inverseFunction, function, hi

-- Shifting then composing with σ restores the permutation.
theorem permutationShift.compose (n : Nat) (σ p : Set)
  requires permutation : σ ∈ permutations(n)
  requires hp : p ∈ permutations(n)
  shows compose(permutationShift(n, σ)(p), σ, n, n, n) = p
proof
  have inverse := permutations.converse with permutation
  have value := permutationShift.value at n, σ, p with permutation, hp
  have associative := permutations.compose_associative at n, σ, converse(σ, n, n), p
  have cancel := permutations.converse_compose at n, σ with permutation
  have unit := permutations.compose_identity_right at n, p with hp
  rw [value, ← associative, cancel, unit]
  rfl

theorem permutationShift.bijective (n : Nat) (σ : Set)
  requires permutation : σ ∈ permutations(n)
  shows BijectiveBetween(permutationShift(n, σ), permutations(n), permutations(n))
proof
  have function := permutationShift.function at n, σ with permutation
  have inverse := permutations.converse with permutation
  have injective : InjectiveBetween(permutationShift(n, σ), permutations(n), permutations(n))
    have cancel : ∀ p ∈ permutations(n), ∀ q ∈ permutations(n),
        permutationShift(n, σ)(p) = permutationShift(n, σ)(q) → p = q
      intros p hp q hq same
      have restoreP := permutationShift.compose at n, σ, p with permutation, hp
      have restoreQ := permutationShift.compose at n, σ, q with permutation, hq
      rw [← restoreP, ← restoreQ, same]
      rfl
    exact Injective.of_pointwise with function, cancel
  have surjective : SurjectiveBetween(permutationShift(n, σ), permutations(n), permutations(n))
    constructor
    . exact function
    . intros r hr
      have preimage := permutations.compose at n, σ, r with permutation, hr
      witness compose(r, σ, n, n, n)
      constructor
      . exact preimage
      . have value := permutationShift.value at n, σ, compose(r, σ, n, n, n)
          with permutation, preimage
        have associative := permutations.compose_associative at n, converse(σ, n, n), σ, r
        have cancel := permutations.compose_converse at n, σ with permutation
        have unit := permutations.compose_identity_right at n, r with hr
        have related := FunctionBetween.relates_apply with function, preimage
        rw [value, ← associative, cancel, unit] at related
        exact related
  exact ⟨injective, surjective⟩

-- Permuting the rows of a matrix by σ multiplies the determinant by the
-- sign of σ.
theorem determinant.row_permutation (A add zero neg mul one : Set) (n : Nat) (M N σ : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires matrixM : RingMatrix(n, A, M)
  requires matrixN : RingMatrix(n, A, N)
  requires permutation : σ ∈ permutations(n)
  requires rows : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = M[σ(i), j]
  shows determinant(n, A, add, zero, neg, mul, one, N) =
    call2(mul, permutationSign(n, A, add, zero, neg, mul, one, σ),
      determinant(n, A, add, zero, neg, mul, one, M))
proof
  have finite := Finite.natural at n
  have permutationsFinite := permutations.finite at n with finite
  have termsN := determinantTerms.function at n, A, add, zero, neg, mul, one, N
    with ring, finite, matrixN
  have termsM := determinantTerms.function at n, A, add, zero, neg, mul, one, M
    with ring, finite, matrixM
  have shiftBijective := permutationShift.bijective at n, σ with permutation
  have shiftFunction := permutationShift.function at n, σ with permutation
  have shifted := compose.function at determinantTerms(n, A, add, zero, neg, mul, one, M),
    permutationShift(n, σ), permutations(n), permutations(n), A with shiftFunction, termsM
  have signClosed := permutationSign.closed at A, add, zero, neg, mul, one, n, σ with ring, finite
  have sigmaBijective := permutations.bijective with permutation
  have sigmaFunction := permutations.function with permutation
  -- Each term of N is the sign of σ times the term of M at the shifted
  -- permutation.
  have entries : ∀ p ∈ permutations(n),
      determinantTerms(n, A, add, zero, neg, mul, one, N)(p) =
      call2(mul, permutationSign(n, A, add, zero, neg, mul, one, σ),
        compose(determinantTerms(n, A, add, zero, neg, mul, one, M),
          permutationShift(n, σ), permutations(n), permutations(n), A)(p))
    intros p hp
    have shiftIn := FunctionBetween.apply_closed with shiftFunction, hp
    have composed := compose.apply at determinantTerms(n, A, add, zero, neg, mul, one, M),
      permutationShift(n, σ), permutations(n), permutations(n), A, p
      with shiftFunction, termsM, hp
    have termN := determinantTerms.value at n, A, add, zero, neg, mul, one, N, p
      with ring, finite, matrixN, hp
    have termM := determinantTerms.value at n, A, add, zero, neg, mul, one, M,
      permutationShift(n, σ)(p) with ring, finite, matrixM, shiftIn
    have pBijective := permutations.bijective with hp
    have shiftBij := permutations.bijective with shiftIn
    have entriesN := permutationEntries.function at n, A, N, p with matrixN, pBijective
    have entriesM := permutationEntries.function at n, A, M, permutationShift(n, σ)(p)
      with matrixM, shiftBij
    have products : ∀ i ∈ n, permutationEntries(n, A, N, p)(i) =
        permutationEntries(n, A, M, permutationShift(n, σ)(p))(σ(i))
      intros i hi
      have imageIn := permutations.apply_closed with permutation, hi
      have valueN := permutationEntries.value at n, A, N, p, i with matrixN, pBijective, hi
      have valueM := permutationEntries.value at n, A, M, permutationShift(n, σ)(p), σ(i)
        with matrixM, shiftBij, imageIn
      have shiftValue := permutationShift.apply at n, σ, p, σ(i) with permutation, hp, imageIn
      have cancel := permutations.inverse_apply at n, σ, i with permutation, hi
      have row := rows with i, hi, p(i), (permutations.apply_closed with hp, hi)
      rw [valueN, valueM, shiftValue, cancel, row]
      rfl
    have productEq := finiteRingProduct.reindex at n, n, A, add, zero, neg, mul, one,
      permutationEntries(n, A, N, p), permutationEntries(n, A, M, permutationShift(n, σ)(p)), σ
      with ring, finite, entriesN, entriesM, sigmaBijective, products
    have restore := permutationShift.compose at n, σ, p with permutation, hp
    have signSplit := permutationSign.compose at A, add, zero, neg, mul, one, n,
      permutationShift(n, σ)(p), σ with ring, shiftIn, permutation
    rw restore at signSplit
    have signShift := permutationSign.closed at A, add, zero, neg, mul, one, n,
      permutationShift(n, σ)(p) with ring, finite
    have productClosed := finiteRingProduct.closed at n, A, add, zero, neg, mul, one,
      permutationEntries(n, A, M, permutationShift(n, σ)(p)) with ring, finite, entriesM
    rw [termN, composed, termM, productEq, signSplit]
    ring
  have scaled := finiteRingSum.scale_eq at permutations(n), A, add, zero, neg, mul, one,
    compose(determinantTerms(n, A, add, zero, neg, mul, one, M),
      permutationShift(n, σ), permutations(n), permutations(n), A),
    determinantTerms(n, A, add, zero, neg, mul, one, N),
    permutationSign(n, A, add, zero, neg, mul, one, σ)
    with ring, permutationsFinite, shifted, termsN, signClosed, entries
  have values : ∀ p ∈ permutations(n),
      compose(determinantTerms(n, A, add, zero, neg, mul, one, M),
        permutationShift(n, σ), permutations(n), permutations(n), A)(p) =
      determinantTerms(n, A, add, zero, neg, mul, one, M)(permutationShift(n, σ)(p))
    intros p hp
    exact compose.apply at determinantTerms(n, A, add, zero, neg, mul, one, M),
      permutationShift(n, σ), permutations(n), permutations(n), A, p
      with shiftFunction, termsM, hp
  have reindexed := finiteRingSum.reindex at permutations(n), permutations(n), A, add, zero,
    neg, mul, one,
    compose(determinantTerms(n, A, add, zero, neg, mul, one, M),
      permutationShift(n, σ), permutations(n), permutations(n), A),
    determinantTerms(n, A, add, zero, neg, mul, one, M), permutationShift(n, σ)
    with ring, permutationsFinite, shifted, termsM, shiftBijective, values
  simp [determinant]