Grace/Cumulus/Algebra/Ring/PermutationSign.g17

Open in Workbench Download source

Imports

DeterminantCancellation · Cardinal.InversionExchange

Declarations

Source

1-- Inversion-count signs under adjacent exchanges of permutation inputs (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Ring.PermutationSign8import DeterminantCancellation9import Cardinal.InversionExchange1011section Signs12variable (A add zero neg mul one : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)1516theorem permutationSign.adjacent (n a : Nat) (p : Set)17  requires ha : a ∈ n18  requires hb : succ(a) ∈ n19  requires permutation : p ∈ permutations(n)20  shows permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]21proof22  have finite := Finite.natural at n with *23  have originalFinite := inversions.finite at n, p with finite24  have pairedFinite := inversions.finite at n, permutationExchange(n, a, succ(a))(p) with finite25  have originalCount := cardinality.correct with originalFinite26  have pairedCount := cardinality.correct with pairedFinite27  have originalNatural := HasCardinality.natural with originalCount28  have pairedNatural := HasCardinality.natural with pairedCount29  have originalClosed := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *30  have pairedClosed := permutationSign.closed at A, add, zero, neg, mul, one, n, permutationExchange(n, a, succ(a))(p) with *31  unfold permutationSign at originalClosed32  unfold permutationSign at pairedClosed33  have count := inversions.adjacent_count with *34  unfold permutationSign35  cases count with increases | decreases36  . rw [increases, monoidPow.succ]37    ring38  . rw [decreases, monoidPow.succ]39    ring4041-- Induct on the upper position, conjugating the smaller exchange by the42-- adjacent exchange (b, b+1). Three sign reversals give one sign reversal.43theorem permutationSign.exchange_ordered_induction (n b : Nat)44  shows ∀ a, Nat(a) → a ∈ n → b ∈ n → a < b → ∀ p ∈ permutations(n),45    permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]46proof47  induction b48  | zero =>49    intros a natural ha hb below p permutation50    have impossible := membership.of_Less with natural, below51    rw nat.zero at impossible52    exfalso53    exact set.empty with impossible54  | succ(k) using ih =>55    intros a natural ha hb below p permutation56    have alternatives : a = k ∨ a ≠ k by tauto57    cases alternatives with same | different58    . rw same59      have hk : k ∈ n by rwa ← same60      exact permutationSign.adjacent with *61    . have smaller := Less.of_successor_upper_ne at a, k with *62      have ordinal := Ordinal.natural at n with *63      have transitive := Ordinal.transitive with ordinal64      have prefix := transitive with succ(k), hb65      have kBefore := membership.self_successor at k with *66      have hk := prefix with k, kBefore67      have lowerDistinct : k ≠ succ(k)68        intro equal69        have bad : k ∈ k by rwa ← equal at kBefore70        exact membership.irreflexive with bad71      have outerDistinct : a ≠ succ(k)72        intro equal73        have membership := membership.of_Less with natural, below74        rw ← equal at membership75        exact membership.irreflexive with membership76      have function := permutationExchange.function at n, k, succ(k) with *77      have middleFunction := permutationExchange.function at n, a, k with *78      have p1 := FunctionBetween.apply_closed with function, permutation79      have p2 := FunctionBetween.apply_closed with middleFunction, p180      have first := permutationSign.adjacent at A, add, zero, neg, mul, one, n, k, p with *81      have middle := ih with a, natural, ha, hk, smaller, permutationExchange(n, k, succ(k))(p), p182      have last := permutationSign.adjacent at A, add, zero, neg, mul, one, n, k, permutationExchange(n, a, k)(permutationExchange(n, k, succ(k))(p)) with *83      have conjugate := permutationExchange.conjugate at n, a, k, succ(k), p with *84      have value := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *85      rw [← conjugate, last, middle, first]86      ring8788theorem permutationSign.exchange (n : Nat) (a b p : Set)89  requires ha : a ∈ n90  requires hb : b ∈ n91  requires distinct : a ≠ b92  requires permutation : p ∈ permutations(n)93  shows permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]94proof95  have naturals := natural.member with *96  have naturalA := naturals with a, ha97  have naturalB := naturals with b, hb98  have comparison := Less.trichotomy at a, b with *99  cases comparison with before | remaining100  . have induction := permutationSign.exchange_ordered_induction at A, add, zero, neg, mul, one, n, b with *101    exact induction with a, naturalA, ha, hb, before, p, permutation102  . cases remaining with same | after103    . exfalso104      exact distinct with same105    . have induction := permutationSign.exchange_ordered_induction at A, add, zero, neg, mul, one, n, a with *106      have reverse := induction with b, naturalB, hb, ha, after, p, permutation107      have symmetric := permutationExchange.symmetric with ha, hb108      rwa symmetric109110theorem determinant.equal_rows (n : Nat) (a b M : Set)111  requires matrix : RingMatrix(n, R, M)112  requires ha : a ∈ n113  requires hb : b ∈ n114  requires distinct : a ≠ b115  requires rows : ∀ j ∈ n, M[a, j] = M[b, j]116  shows determinant(n, R, M) = R[0]117proof118  have 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)]119    intros p member120    exact permutationSign.exchange with *121  exact determinant.equal_rows_of_exchange_sign with *122123theorem determinant.equal_adjacent_rows (n a : Nat) (M : Set)124  requires matrix : RingMatrix(n, R, M)125  requires ha : a ∈ n126  requires hb : succ(a) ∈ n127  requires rows : ∀ j ∈ n, M[a, j] = M[succ(a), j]128  shows determinant(n, R, M) = R[0]129proof130  have distinct : a ≠ succ(a)131    have below : a < succ(a) by arith132    intro same133    have impossible : a < a by arith134    have excluded := Less.irreflexive at a with *135    exact excluded with impossible136  have signs : ∀ p ∈ permutations(n), permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]137    intros p member138    exact permutationSign.adjacent with *139  exact determinant.equal_rows_of_exchange_sign with *140141end Signs142