PermutationExchange

Concrete row-exchange pairings for determinant cancellation (ZF)

Open in Workbench View on GitHub

1-- Concrete row-exchange pairings for determinant cancellation (ZF).2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module PermutationExchange7import Grace.Cumulus.Algebra.Ring.DeterminantCancellation89section Exchanges10variable (I a b : Set)11hypothesis ha : a ∈ I12hypothesis hb : b ∈ I1314theorem exchange_twice (i : Set)15  requires index : i ∈ I16  shows transposition(I, a, b)(transposition(I, a, b)(i)) = i17proof18  have involution := transposition.involution at I, a, b with *19  exact InvolutionOn.apply with *2021theorem pairing22  shows InvolutionOn(permutationExchange(I, a, b), permutations(I))23proof24  exact permutationExchange.involution with *2526theorem no_fixed_permutation (p : Set)27  requires distinct : a ≠ b28  requires permutation : p ∈ permutations(I)29  shows permutationExchange(I, a, b)(p) ≠ p30proof31  exact permutationExchange.free with *3233end Exchanges3435theorem coincident_choices (I a : Set)36  requires member : a ∈ I37  shows InvolutionOn(transposition(I, a, a), I)38proof39  exact transposition.involution with *4041section Determinants42variable (A add zero neg mul one M : Set)43notation ring R := (A, add, zero, neg, mul, one)44hypothesis ring : IsCommRing(R)4546theorem equal_rows_reduce_to_sign (n : Nat) (a b : Set)47  requires matrix : RingMatrix(n, R, M)48  requires ha : a ∈ n49  requires hb : b ∈ n50  requires distinct : a ≠ b51  requires rows : ∀ j ∈ n, M[a, j] = M[b, j]52  requires signs : ∀ p ∈ permutations(n), permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]53  shows determinant(n, R, M) = R[0]54proof55  exact determinant.equal_rows_of_exchange_sign with *5657end Determinants58