Grace/Cumulus/Algebra/Ring/Determinant.g17

Open in Workbench Download source

Imports

FiniteProduct · Cardinal.Permutations · Group.Power

Declarations

Source

1-- The Leibniz determinant over arbitrary commutative rings, using finite sums (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.Determinant8import FiniteProduct9import Cardinal.Permutations10import Group.Power1112-- Matrices are function graphs on the finite square of indices.13predicate RingMatrix (I A M : Set) := FunctionBetween(M, I × I, A)1415notation scoped RingMatrix(I, R, M) => RingMatrix(I, R.carrier, M)1617theorem RingMatrix.entry (I A M i j : Set)18  requires matrix : RingMatrix(I, A, M)19  requires row : i ∈ I20  requires column : j ∈ I21  shows M[i, j] ∈ A22proof23  have pair := product.pair with row, column24  unfold RingMatrix at matrix25  exact FunctionBetween.apply_closed with matrix, pair2627theorem RingMatrix.ext (I A M N : Set)28  requires first : RingMatrix(I, A, M)29  requires second : RingMatrix(I, A, N)30  requires entries : ∀ i ∈ I, ∀ j ∈ I, M[i, j] = N[i, j]31  shows M = N32proof33  unfold RingMatrix at first34  unfold RingMatrix at second35  have values : ∀ p ∈ I × I, M(p) = N(p)36    intros p hp37    obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with hp38    rw shape39    exact entries with i, hi, j, hj40  exact FunctionBetween.ext with first, second, values4142defgraph permutationEntries (I A M p : Set) (i ∈ I) : A := M[i, p(i)]43requires matrix : RingMatrix(I, A, M)44requires permutation : BijectiveBetween(p, I, I)45proof46  have injective := Bijective.injective with permutation47  have function := Injective.function with injective48  have image := FunctionBetween.apply_closed with function, assumption49  have pair := product.pair at i, p(i), I, I with image50  unfold RingMatrix at matrix51  exact FunctionBetween.apply_closed with matrix, pair5253def permutationSign (I A add zero neg mul one p : Set) : Set :=54  monoidPow(mul, one, neg(one), cardinality(inversions(I, p)))5556notation scoped permutationSign(I, R, p) => permutationSign(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, p)5758section Rings59variable (A add zero neg mul one : Set)60notation ring R := (A, add, zero, neg, mul, one)61hypothesis ring : IsCommRing(R)6263theorem permutationSign.closed (I p : Set)64  requires finite : Finite(I)65  shows permutationSign(I, A, add, zero, neg, mul, one, p) ∈ R66proof67  have inversionsFinite := inversions.finite at I, p with finite68  have count := cardinality.correct with inversionsFinite69  have natural := count.left70  have ordinary := IsCommRing.ring with ring71  have multiplicative := IsRing.multiplicative with ordinary72  have unitIn := IsMonoid.unit_in_carrier with multiplicative73  have negative := IsRing.neg_closed with ordinary, unitIn74  unfold permutationSign75  exact monoidPow.closed with *7677theorem permutationSign.empty (p : Set)78  shows permutationSign(∅, A, add, zero, neg, mul, one, p) = R[1]79proof80  have count : cardinality(∅) = (0 : Nat)81    rw ← nat.zero82    exact cardinality.natural with Naturals.constructor.zero83  unfold permutationSign84  rw [inversions.empty, count, monoidPow.zero]85  rfl8687end Rings8889-- Explicit ring parameters let this graph be reused at every finite index set.90defgraph determinantTerms (I A add zero neg mul one M : Set) (p ∈ permutations(I)) : A :=91  call2(mul, permutationSign(I, A, add, zero, neg, mul, one, p), finiteRingProduct(I, A, add, zero, neg, mul, one, permutationEntries(I, A, M, p)))92requires ring : IsCommRing(A, add, zero, neg, mul, one)93requires finite : Finite(I)94requires matrix : RingMatrix(I, A, M)95proof96  have permutation := permutations.mem_iff.forward at I, p with assumption97  have entries := permutationEntries.function at I, A, M, p with *98  have product := finiteRingProduct.closed at I, A, add, zero, neg, mul, one, permutationEntries(I, A, M, p) with *99  have sign := permutationSign.closed at A, add, zero, neg, mul, one, I, p with *100  have ordinary := IsCommRing.ring with ring101  exact IsRing.mul_closed with ordinary, sign, product102103notation scoped determinantTerms(I, R, M) => determinantTerms(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)104105def determinant (n A add zero neg mul one M : Set) : Set :=106  finiteRingSum(permutations(n), A, add, zero, neg, mul, one, determinantTerms(n, A, add, zero, neg, mul, one, M))107108notation scoped determinant(n, R, M) => determinant(n, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)109110section Determinants111variable (A add zero neg mul one M : Set)112notation ring R := (A, add, zero, neg, mul, one)113hypothesis ring : IsCommRing(R)114115theorem determinant.closed (n : Nat)116  requires matrix : RingMatrix(n, R, M)117  shows determinant(n, R, M) ∈ R118proof119  have finite := Finite.natural with *120  have permutationsFinite := permutations.finite with finite121  have weights := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *122  unfold determinant123  exact finiteRingSum.closed with ring, permutationsFinite, weights124125theorem determinant.congr (n : Nat) (N : Set)126  requires first : RingMatrix(n, R, M)127  requires second : RingMatrix(n, R, N)128  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]129  shows determinant(n, R, M) = determinant(n, R, N)130proof131  have equal := RingMatrix.ext with first, second, entries132  rw equal133  rfl134135theorem determinant.empty136  requires matrix : RingMatrix(∅, R, M)137  shows determinant(∅, R, M) = R[1]138proof139  have finite := Finite.empty140  have weights := determinantTerms.function at ∅, A, add, zero, neg, mul, one, M with *141  have singletonWeights := weights142  rw permutations.empty at singletonWeights143  have member : ∅ ∈ permutations(∅)144    rw permutations.empty145    simp146  have permutation := permutations.mem_iff.forward with member147  have entries := permutationEntries.function at ∅, A, M, ∅ with *148  have product := finiteRingProduct.empty with ring, entries149  have sign := permutationSign.empty at A, add, zero, neg, mul, one, ∅ with *150  have term := determinantTerms.value at ∅, A, add, zero, neg, mul, one, M, ∅ with *151  have sum := finiteRingSum.singleton with ring, singletonWeights152  unfold determinant153  rw [permutations.empty, sum, term, product, sign]154  ring155156end Determinants157