Grace/Cumulus/Algebra/Ring/DeterminantRowPermutation.g17

Open in Workbench Download source

Imports

PermutationSignCompose · DeterminantLinearity

Declarations

Source

1-- Permuting the rows of a matrix multiplies its determinant by the sign of2-- the permutation: composition with the inverse of σ is a bijection of the3-- permutations, each Leibniz term of the permuted matrix is the term of the4-- original at the shifted permutation times the sign of σ5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Ring.DeterminantRowPermutation11import PermutationSignCompose12import DeterminantLinearity1314-- A permutation composed with its inverse on either side is the identity.15theorem permutations.converse_compose (n : Nat) (σ : Set)16  requires permutation : σ ∈ permutations(n)17  shows compose(converse(σ, n, n), σ, n, n, n) = identity(n)18proof19  have function := permutations.function with permutation20  have inverse := permutations.converse with permutation21  have inverseFunction := permutations.function with inverse22  have composed := permutations.compose at n, σ, converse(σ, n, n) with permutation, inverse23  have composedFunction := permutations.function with composed24  have idFunction := identity.function at n25  have same : ∀ x ∈ n, compose(converse(σ, n, n), σ, n, n, n)(x) = identity(n)(x)26    intros x hx27    have value := compose.apply at converse(σ, n, n), σ, n, n, n, x28      with function, inverseFunction, hx29    have cancel := permutations.inverse_apply at n, σ, x with permutation, hx30    have idValue := identity.apply at x, n with hx31    rw [value, cancel, idValue]32    rfl33  exact FunctionBetween.ext with composedFunction, idFunction, same3435theorem permutations.compose_converse (n : Nat) (σ : Set)36  requires permutation : σ ∈ permutations(n)37  shows compose(σ, converse(σ, n, n), n, n, n) = identity(n)38proof39  have function := permutations.function with permutation40  have inverse := permutations.converse with permutation41  have inverseFunction := permutations.function with inverse42  have composed := permutations.compose at n, converse(σ, n, n), σ with inverse, permutation43  have composedFunction := permutations.function with composed44  have idFunction := identity.function at n45  have same : ∀ x ∈ n, compose(σ, converse(σ, n, n), n, n, n)(x) = identity(n)(x)46    intros x hx47    have value := compose.apply at σ, converse(σ, n, n), n, n, n, x48      with inverseFunction, function, hx49    have cancel := permutations.apply_inverse at n, σ, x with permutation, hx50    have idValue := identity.apply at x, n with hx51    rw [value, cancel, idValue]52    rfl53  exact FunctionBetween.ext with composedFunction, idFunction, same5455-- Composition with the inverse of σ, p ↦ p ∘ σ⁻¹, on the permutations.56defgraph permutationShift (n σ : Set) (p ∈ permutations(n)) : permutations(n) :=57  compose(p, converse(σ, n, n), n, n, n)58requires permutation : σ ∈ permutations(n)59proof60  have inverse := permutations.converse with permutation61  exact permutations.compose at n, converse(σ, n, n), p with inverse, assumption6263theorem permutationShift.apply (n : Nat) (σ p i : Set)64  requires permutation : σ ∈ permutations(n)65  requires hp : p ∈ permutations(n)66  requires hi : i ∈ n67  shows permutationShift(n, σ)(p)(i) = p(converse(σ, n, n)(i))68proof69  have inverse := permutations.converse with permutation70  have inverseFunction := permutations.function with inverse71  have function := permutations.function with hp72  have value := permutationShift.value at n, σ, p with permutation, hp73  rw value74  exact compose.apply with inverseFunction, function, hi7576-- Shifting then composing with σ restores the permutation.77theorem permutationShift.compose (n : Nat) (σ p : Set)78  requires permutation : σ ∈ permutations(n)79  requires hp : p ∈ permutations(n)80  shows compose(permutationShift(n, σ)(p), σ, n, n, n) = p81proof82  have inverse := permutations.converse with permutation83  have value := permutationShift.value at n, σ, p with permutation, hp84  have associative := permutations.compose_associative at n, σ, converse(σ, n, n), p85  have cancel := permutations.converse_compose at n, σ with permutation86  have unit := permutations.compose_identity_right at n, p with hp87  rw [value, ← associative, cancel, unit]88  rfl8990theorem permutationShift.bijective (n : Nat) (σ : Set)91  requires permutation : σ ∈ permutations(n)92  shows BijectiveBetween(permutationShift(n, σ), permutations(n), permutations(n))93proof94  have function := permutationShift.function at n, σ with permutation95  have inverse := permutations.converse with permutation96  have injective : InjectiveBetween(permutationShift(n, σ), permutations(n), permutations(n))97    have cancel : ∀ p ∈ permutations(n), ∀ q ∈ permutations(n),98        permutationShift(n, σ)(p) = permutationShift(n, σ)(q) → p = q99      intros p hp q hq same100      have restoreP := permutationShift.compose at n, σ, p with permutation, hp101      have restoreQ := permutationShift.compose at n, σ, q with permutation, hq102      rw [← restoreP, ← restoreQ, same]103      rfl104    exact Injective.of_pointwise with function, cancel105  have surjective : SurjectiveBetween(permutationShift(n, σ), permutations(n), permutations(n))106    constructor107    . exact function108    . intros r hr109      have preimage := permutations.compose at n, σ, r with permutation, hr110      witness compose(r, σ, n, n, n)111      constructor112      . exact preimage113      . have value := permutationShift.value at n, σ, compose(r, σ, n, n, n)114          with permutation, preimage115        have associative := permutations.compose_associative at n, converse(σ, n, n), σ, r116        have cancel := permutations.compose_converse at n, σ with permutation117        have unit := permutations.compose_identity_right at n, r with hr118        have related := FunctionBetween.relates_apply with function, preimage119        rw [value, ← associative, cancel, unit] at related120        exact related121  exact ⟨injective, surjective⟩122123-- Permuting the rows of a matrix by σ multiplies the determinant by the124-- sign of σ.125theorem determinant.row_permutation (A add zero neg mul one : Set) (n : Nat) (M N σ : Set)126  requires ring : IsCommRing(A, add, zero, neg, mul, one)127  requires matrixM : RingMatrix(n, A, M)128  requires matrixN : RingMatrix(n, A, N)129  requires permutation : σ ∈ permutations(n)130  requires rows : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = M[σ(i), j]131  shows determinant(n, A, add, zero, neg, mul, one, N) =132    call2(mul, permutationSign(n, A, add, zero, neg, mul, one, σ),133      determinant(n, A, add, zero, neg, mul, one, M))134proof135  have finite := Finite.natural at n136  have permutationsFinite := permutations.finite at n with finite137  have termsN := determinantTerms.function at n, A, add, zero, neg, mul, one, N138    with ring, finite, matrixN139  have termsM := determinantTerms.function at n, A, add, zero, neg, mul, one, M140    with ring, finite, matrixM141  have shiftBijective := permutationShift.bijective at n, σ with permutation142  have shiftFunction := permutationShift.function at n, σ with permutation143  have shifted := compose.function at determinantTerms(n, A, add, zero, neg, mul, one, M),144    permutationShift(n, σ), permutations(n), permutations(n), A with shiftFunction, termsM145  have signClosed := permutationSign.closed at A, add, zero, neg, mul, one, n, σ with ring, finite146  have sigmaBijective := permutations.bijective with permutation147  have sigmaFunction := permutations.function with permutation148  -- Each term of N is the sign of σ times the term of M at the shifted149  -- permutation.150  have entries : ∀ p ∈ permutations(n),151      determinantTerms(n, A, add, zero, neg, mul, one, N)(p) =152      call2(mul, permutationSign(n, A, add, zero, neg, mul, one, σ),153        compose(determinantTerms(n, A, add, zero, neg, mul, one, M),154          permutationShift(n, σ), permutations(n), permutations(n), A)(p))155    intros p hp156    have shiftIn := FunctionBetween.apply_closed with shiftFunction, hp157    have composed := compose.apply at determinantTerms(n, A, add, zero, neg, mul, one, M),158      permutationShift(n, σ), permutations(n), permutations(n), A, p159      with shiftFunction, termsM, hp160    have termN := determinantTerms.value at n, A, add, zero, neg, mul, one, N, p161      with ring, finite, matrixN, hp162    have termM := determinantTerms.value at n, A, add, zero, neg, mul, one, M,163      permutationShift(n, σ)(p) with ring, finite, matrixM, shiftIn164    have pBijective := permutations.bijective with hp165    have shiftBij := permutations.bijective with shiftIn166    have entriesN := permutationEntries.function at n, A, N, p with matrixN, pBijective167    have entriesM := permutationEntries.function at n, A, M, permutationShift(n, σ)(p)168      with matrixM, shiftBij169    have products : ∀ i ∈ n, permutationEntries(n, A, N, p)(i) =170        permutationEntries(n, A, M, permutationShift(n, σ)(p))(σ(i))171      intros i hi172      have imageIn := permutations.apply_closed with permutation, hi173      have valueN := permutationEntries.value at n, A, N, p, i with matrixN, pBijective, hi174      have valueM := permutationEntries.value at n, A, M, permutationShift(n, σ)(p), σ(i)175        with matrixM, shiftBij, imageIn176      have shiftValue := permutationShift.apply at n, σ, p, σ(i) with permutation, hp, imageIn177      have cancel := permutations.inverse_apply at n, σ, i with permutation, hi178      have row := rows with i, hi, p(i), (permutations.apply_closed with hp, hi)179      rw [valueN, valueM, shiftValue, cancel, row]180      rfl181    have productEq := finiteRingProduct.reindex at n, n, A, add, zero, neg, mul, one,182      permutationEntries(n, A, N, p), permutationEntries(n, A, M, permutationShift(n, σ)(p)), σ183      with ring, finite, entriesN, entriesM, sigmaBijective, products184    have restore := permutationShift.compose at n, σ, p with permutation, hp185    have signSplit := permutationSign.compose at A, add, zero, neg, mul, one, n,186      permutationShift(n, σ)(p), σ with ring, shiftIn, permutation187    rw restore at signSplit188    have signShift := permutationSign.closed at A, add, zero, neg, mul, one, n,189      permutationShift(n, σ)(p) with ring, finite190    have productClosed := finiteRingProduct.closed at n, A, add, zero, neg, mul, one,191      permutationEntries(n, A, M, permutationShift(n, σ)(p)) with ring, finite, entriesM192    rw [termN, composed, termM, productEq, signSplit]193    ring194  have scaled := finiteRingSum.scale_eq at permutations(n), A, add, zero, neg, mul, one,195    compose(determinantTerms(n, A, add, zero, neg, mul, one, M),196      permutationShift(n, σ), permutations(n), permutations(n), A),197    determinantTerms(n, A, add, zero, neg, mul, one, N),198    permutationSign(n, A, add, zero, neg, mul, one, σ)199    with ring, permutationsFinite, shifted, termsN, signClosed, entries200  have values : ∀ p ∈ permutations(n),201      compose(determinantTerms(n, A, add, zero, neg, mul, one, M),202        permutationShift(n, σ), permutations(n), permutations(n), A)(p) =203      determinantTerms(n, A, add, zero, neg, mul, one, M)(permutationShift(n, σ)(p))204    intros p hp205    exact compose.apply at determinantTerms(n, A, add, zero, neg, mul, one, M),206      permutationShift(n, σ), permutations(n), permutations(n), A, p207      with shiftFunction, termsM, hp208  have reindexed := finiteRingSum.reindex at permutations(n), permutations(n), A, add, zero,209    neg, mul, one,210    compose(determinantTerms(n, A, add, zero, neg, mul, one, M),211      permutationShift(n, σ), permutations(n), permutations(n), A),212    determinantTerms(n, A, add, zero, neg, mul, one, M), permutationShift(n, σ)213    with ring, permutationsFinite, shifted, termsM, shiftBijective, values214  simp [determinant]215