Grace/Cumulus/Algebra/Ring/DeterminantLinearity.g17

Open in Workbench Download source

Imports

Determinant · FiniteLinearity

Declarations

• determinant.row_linear theorem derivation

Source

1-- The determinant is linear in each row over any commutative ring (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.DeterminantLinearity8import Determinant9import FiniteLinearity1011section Rings12variable (A add zero neg mul one : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)1516-- The three matrices agree off row i; row i of P is a times M plus b times N.17theorem determinant.row_linear (n : Nat) (M N P i a b : Set)18  requires matrixM : RingMatrix(n, R, M)19  requires matrixN : RingMatrix(n, R, N)20  requires matrixP : RingMatrix(n, R, P)21  requires row : i ∈ n22  requires scalarA : a ∈ R23  requires scalarB : b ∈ R24  requires outsideN : ∀ k ∈ n, ¬(k = i) → ∀ j ∈ n, N[k, j] = M[k, j]25  requires outsideP : ∀ k ∈ n, ¬(k = i) → ∀ j ∈ n, P[k, j] = M[k, j]26  requires entries : ∀ j ∈ n, P[i, j] = a * M[i, j] + b * N[i, j]27  shows determinant(n, R, P) = a * determinant(n, R, M) + b * determinant(n, R, N)28proof29  have finite := Finite.natural at n with *30  have permutationsFinite := permutations.finite with finite31  have weightsM := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *32  have weightsN := determinantTerms.function at n, A, add, zero, neg, mul, one, N with *33  have weightsP := determinantTerms.function at n, A, add, zero, neg, mul, one, P with *34  have terms : ∀ p ∈ permutations(n), determinantTerms(n, R, P)(p) = a * determinantTerms(n, R, M)(p) + b * determinantTerms(n, R, N)(p)35    intros p hp36    have permutation := permutations.mem_iff.forward with hp37    have injective := Bijective.injective with permutation38    have function := Injective.function with injective39    have column := FunctionBetween.apply_closed at p, n, n, i with *40    have entriesM := permutationEntries.function at n, A, M, p with *41    have entriesN := permutationEntries.function at n, A, N, p with *42    have entriesP := permutationEntries.function at n, A, P, p with *43    have outsideNEntries : ∀ k ∈ n, ¬(k = i) → permutationEntries(n, A, N, p)(k) = permutationEntries(n, A, M, p)(k)44      intros k hk distinct45      have image := FunctionBetween.apply_closed at p, n, n, k with *46      have leftValue := permutationEntries.value at n, A, N, p, k with *47      have rightValue := permutationEntries.value at n, A, M, p, k with *48      rw [leftValue, rightValue]49      exact outsideN with k, hk, distinct, p(k), image50    have outsidePEntries : ∀ k ∈ n, ¬(k = i) → permutationEntries(n, A, P, p)(k) = permutationEntries(n, A, M, p)(k)51      intros k hk distinct52      have image := FunctionBetween.apply_closed at p, n, n, k with *53      have leftValue := permutationEntries.value at n, A, P, p, k with *54      have rightValue := permutationEntries.value at n, A, M, p, k with *55      rw [leftValue, rightValue]56      exact outsideP with k, hk, distinct, p(k), image57    have entry : permutationEntries(n, A, P, p)(i) = a * permutationEntries(n, A, M, p)(i) + b * permutationEntries(n, A, N, p)(i)58      have valueM := permutationEntries.value at n, A, M, p, i with *59      have valueN := permutationEntries.value at n, A, N, p, i with *60      have valueP := permutationEntries.value at n, A, P, p, i with *61      rw [valueP, valueM, valueN]62      exact entries with p(i), column63    have product := finiteRingProduct.linear_at at n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p), permutationEntries(n, A, N, p), permutationEntries(n, A, P, p), i, a, b with *64    have sign := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *65    have closedM := finiteRingProduct.closed at n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p) with *66    have closedN := finiteRingProduct.closed at n, A, add, zero, neg, mul, one, permutationEntries(n, A, N, p) with *67    have termM := determinantTerms.value at n, A, add, zero, neg, mul, one, M, p with *68    have termN := determinantTerms.value at n, A, add, zero, neg, mul, one, N, p with *69    have termP := determinantTerms.value at n, A, add, zero, neg, mul, one, P, p with *70    rw [termP, termM, termN, product]71    ring72  unfold determinant73  exact finiteRingSum.linear at permutations(n), A, add, zero, neg, mul, one, determinantTerms(n, R, M), determinantTerms(n, R, N), determinantTerms(n, R, P), a, b with *7475end Rings76