Grace/Cumulus/Algebra/Ring/DeterminantCancellation.g17

Open in Workbench Download source

Imports

Determinant · Cancellation · Cardinal.PermutationExchange

Declarations

Source

1-- Sign-reversing pairings of the Leibniz determinant terms (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.DeterminantCancellation8import Determinant9import Cancellation10import Cardinal.PermutationExchange1112section Determinants13variable (A add zero neg mul one M : Set)14notation ring R := (A, add, zero, neg, mul, one)15hypothesis ring : IsCommRing(R)1617-- This isolates the combinatorial input to determinant cancellation. In the18-- repeated-row application, t will exchange those two row positions.19theorem determinant.cancel_pairs (n : Nat) (t : Set)20  requires matrix : RingMatrix(n, R, M)21  requires involution : InvolutionOn(t, permutations(n))22  requires free : ∀ p ∈ permutations(n), t(p) ≠ p23  requires signs : ∀ p ∈ permutations(n), permutationSign(n, A, add, zero, neg, mul, one, t(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]24  requires products : ∀ p ∈ permutations(n), finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, t(p))) = finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p))25  shows determinant(n, R, M) = R[0]26proof27  have finite := Finite.natural with *28  have finitePermutations := permutations.finite with finite29  have weights := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *30  have function := InvolutionOn.function with involution31  have opposite : ∀ p ∈ permutations(n), determinantTerms(n, A, add, zero, neg, mul, one, M)(t(p)) = R[-determinantTerms(n, A, add, zero, neg, mul, one, M)(p)]32    intros p member33    have paired := FunctionBetween.apply_closed with function, member34    have permutation := permutations.mem_iff.forward with member35    have entries := permutationEntries.function at n, A, M, p with *36    have product := finiteRingProduct.closed with ring, finite, entries37    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *38    have first := determinantTerms.value at n, A, add, zero, neg, mul, one, M, p with *39    have second := determinantTerms.value at n, A, add, zero, neg, mul, one, M, t(p) with *40    have changedSign := signs with p, member41    have sameProduct := products with p, member42    rw [first, second, changedSign, sameProduct]43    ring44  unfold determinant45  exact finiteRingSum.involution_free with *4647-- Equal rows preserve the product in each paired Leibniz term. The equality48-- comes from reindexing the finite product; no ordering of factors is used.49theorem permutationEntries.exchange_product (n : Nat) (a b p : Set)50  requires matrix : RingMatrix(n, R, M)51  requires ha : a ∈ n52  requires hb : b ∈ n53  requires permutation : p ∈ permutations(n)54  requires rows : ∀ j ∈ n, M[a, j] = M[b, j]55  shows finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, permutationExchange(n, a, b)(p))) =56    finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p))57proof58  have exchange := permutationExchange.function at n, a, b with *59  have paired := FunctionBetween.apply_closed with exchange, permutation60  have originalBijective := permutations.mem_iff.forward with permutation61  have pairedBijective := permutations.mem_iff.forward with paired62  have injective := Bijective.injective with originalBijective63  have function := Injective.function with injective64  have originalWeights := permutationEntries.function at n, A, M, p with *65  have pairedWeights := permutationEntries.function at n, A, M, permutationExchange(n, a, b)(p) with *66  have swap := transposition.bijective at n, a, b with *67  have swapFunction := transposition.function at n, a, b with *68  have atFirst := transposition.first at n, a, b with *69  have atSecond := transposition.second at n, a, b with *70  have values : ∀ i ∈ n, permutationEntries(n, A, M, permutationExchange(n, a, b)(p))(i) = permutationEntries(n, A, M, p)(transposition(n, a, b)(i))71    intros i index72    have swappedIndex := FunctionBetween.apply_closed with swapFunction, index73    have column := FunctionBetween.apply_closed with function, swappedIndex74    have firstValue := permutationEntries.value at n, A, M, permutationExchange(n, a, b)(p), i with *75    have secondValue := permutationEntries.value at n, A, M, p, transposition(n, a, b)(i) with *76    have exchanged := permutationExchange.apply at n, a, b, p, i with *77    have rowEquality := rows with p(transposition(n, a, b)(i)), column78    have alternatives : i = a ∨ i = b ∨ (i ≠ a ∧ i ≠ b) by tauto79    cases alternatives with same | remaining80    . cc81    . cases remaining with same | outside82      . cc83      . have unchanged := transposition.other with ha, hb, index, outside.left, outside.right84        cc85  exact finiteRingProduct.reindex with ring, pairedWeights, originalWeights, swap, values8687-- The only remaining combinatorial premise is the inversion-count sign law.88-- This conditional result is not an unconditional equal-rows theorem.89theorem determinant.equal_rows_of_exchange_sign (n : Nat) (a b : Set)90  requires matrix : RingMatrix(n, R, M)91  requires ha : a ∈ n92  requires hb : b ∈ n93  requires distinct : a ≠ b94  requires rows : ∀ j ∈ n, M[a, j] = M[b, j]95  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)]96  shows determinant(n, R, M) = R[0]97proof98  have involution := permutationExchange.involution at n, a, b with *99  have free : ∀ p ∈ permutations(n), permutationExchange(n, a, b)(p) ≠ p100    intros p member101    exact permutationExchange.free with *102  have products : ∀ p ∈ permutations(n), finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, permutationExchange(n, a, b)(p))) = finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p))103    intros p member104    exact permutationEntries.exchange_product with *105  exact determinant.cancel_pairs with *106107end Determinants108