Grace/Cumulus/Algebra/Ring/DeterminantIdentity.g17

Open in Workbench Download source

Imports

CharacteristicMatrix · DeterminantZero

Declarations

Source

1-- The identity permutation has positive sign and the identity determinant is one (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.DeterminantIdentity8import CharacteristicMatrix9import DeterminantZero1011def identityMatrix (I A add zero neg mul one : Set) : Set :=12  characteristicMatrix(I, A, add, zero, neg, mul, one, constantFunction(I × I, A, zero), one)1314notation scoped identityMatrix(I, R) => identityMatrix(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)1516theorem inversions.identity (n : Nat)17  shows inversions(n, identity(n)) = ∅18proof19  have positions := natural.member with *20  ext q21  constructor22  . intro member23    obtain ⟨bound, i, hi, j, hj, shape, forward, backward⟩ := inversions.membership.forward with member24    have first := identity.apply with hi25    have second := identity.apply with hj26    rw [first, second] at backward27    have iNat := positions with i, hi28    have jNat := positions with j, hj29    have increasingRule := Less.of_membership at i, j with *30    have increasing := increasingRule with forward31    have decreasingRule := Less.of_membership at j, i with *32    have decreasing := decreasingRule with backward33    have impossible : (0 : Nat) < (0 : Nat) by arith34    exfalso35    exact Less.irreflexive with Naturals.constructor.zero, impossible36  . intro impossible37    exfalso38    exact set.empty with impossible3940section Rings41variable (A add zero neg mul one : Set)42notation ring R := (A, add, zero, neg, mul, one)43hypothesis ring : IsCommRing(R)4445theorem permutationSign.identity (n : Nat)46  shows permutationSign(n, R, identity(n)) = R[1]47proof48  have emptyCount : cardinality(∅) = (0 : Nat)49    rw ← nat.zero50    exact cardinality.natural with Naturals.constructor.zero51  unfold permutationSign52  rw [inversions.identity, emptyCount]53  exact monoidPow.zero with *5455theorem determinant.identity_entries (n : Nat) (M : Set)56  requires matrix : RingMatrix(n, R, M)57  requires diagonal : ∀ i ∈ n, M[i, i] = R[1]58  requires offDiagonal : ∀ i ∈ n, ∀ j ∈ n, i ≠ j → M[i, j] = R[0]59  shows determinant(n, R, M) = R[1]60proof61  have finite := Finite.natural at n with *62  have permutationsFinite := permutations.finite with finite63  have identityBijective := identity.bijective at n64  have identityInjective := Bijective.injective with identityBijective65  have identityFunction := Injective.function with identityInjective66  have identityMember := permutations.mem_iff.backward at n, identity(n) with *67  have ordinary := IsCommRing.ring with ring68  have zeroIn := IsRing.zero_in_carrier with ordinary69  have oneIn : R[1] ∈ R by typecheck70  have terms := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *71  have selected := coefficientSingle.function at permutations(n), A, zero, one, identity(n) with *72  have entries : ∀ p ∈ permutations(n), determinantTerms(n, R, M)(p) = coefficientSingle(permutations(n), A, zero, one, identity(n))(p)73    intros p hp74    have permutation := permutations.mem_iff.forward with hp75    have injective := Bijective.injective with permutation76    have function := Injective.function with injective77    have weights := permutationEntries.function at n, A, M, p with *78    have term := determinantTerms.value at n, A, add, zero, neg, mul, one, M, p with *79    have signIn := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *80    have alternatives : p = identity(n) ∨ p ≠ identity(n) by tauto81    cases alternatives with same | different82    . have ones : ∀ i ∈ n, permutationEntries(n, R, M, p)(i) = R[1]83        intros i hi84        have value := permutationEntries.value at n, A, M, p, i with *85        have fixed := identity.apply at i, n with *86        have entry := diagonal with i, hi87        cc88      have product := finiteRingProduct.one at n, A, add, zero, neg, mul, one, permutationEntries(n, R, M, p) with *89      have sign := permutationSign.identity at A, add, zero, neg, mul, one, n with *90      have selectedValue := coefficientSingle.same at permutations(n), A, zero, one, identity(n) with *91      rw [term, product, same, sign, selectedValue]92      ring93    . have moved : ∃ i ∈ n, p(i) ≠ i94        by_contra absent95        apply different96        apply FunctionBetween.ext with function, identityFunction97        intros i hi98        have fixed : p(i) = i99          by_contra notFixed100          apply absent101          refine ⟨i, hi, notFixed⟩102        have value := identity.apply at i, n with *103        cc104      obtain ⟨i, hi, notFixed⟩ := moved105      have column := FunctionBetween.apply_closed at p, n, n, i with *106      have distinct : i ≠ p(i)107        intro equal108        apply notFixed109        cc110      have off := offDiagonal with i, hi, p(i), column, distinct111      have value := permutationEntries.value at n, A, M, p, i with *112      have vanishes : permutationEntries(n, R, M, p)(i) = R[0] by cc113      have product := finiteRingProduct.zero_of_factor at n, A, add, zero, neg, mul, one, permutationEntries(n, R, M, p), i with *114      have selectedValue := coefficientSingle.other at permutations(n), A, zero, one, identity(n), p with *115      rw [term, product, selectedValue]116      ring117  have sum := finiteRingSum.congr at permutations(n), A, add, zero, neg, mul, one, determinantTerms(n, R, M), coefficientSingle(permutations(n), A, zero, one, identity(n)) with *118  have single := finiteRingSum.single at permutations(n), A, add, zero, neg, mul, one, one, identity(n) with *119  unfold determinant120  cc121122theorem identityMatrix.matrix (I : Set)123  shows RingMatrix(I, R, identityMatrix(I, R))124proof125  have zeroIn : R[0] ∈ R by typecheck126  have oneIn : R[1] ∈ R by typecheck127  have matrix : RingMatrix(I, R, constantFunction(I × I, A, zero))128    unfold RingMatrix129    exact constantFunction.function with *130  unfold identityMatrix131  exact characteristicMatrix.matrix with *132133theorem identityMatrix.entry (I i j : Set)134  requires row : i ∈ I135  requires column : j ∈ I136  shows identityMatrix(I, R)[i, j] = singleValue(A, zero, one, j, i)137proof138  have zeroIn : R[0] ∈ R by typecheck139  have oneIn : R[1] ∈ R by typecheck140  have matrix : RingMatrix(I, R, constantFunction(I × I, A, zero))141    unfold RingMatrix142    exact constantFunction.function with *143  have pair := product.pair at i, j, I, I with *144  have value := constantFunction.apply at I × I, A, (i, j), zero with *145  have entry := characteristicMatrix.entry at I, A, add, zero, neg, mul, one, constantFunction(I × I, A, zero), one, i, j with *146  have scalar := singleValue.closed at A, zero, one, j, i with *147  simp [identityMatrix]148  ring149150theorem determinant.identity (n : Nat)151  shows determinant(n, R, identityMatrix(n, R)) = R[1]152proof153  have matrix := identityMatrix.matrix at A, add, zero, neg, mul, one, n with *154  have zeroIn : R[0] ∈ R by typecheck155  have oneIn : R[1] ∈ R by typecheck156  have diagonal : ∀ i ∈ n, identityMatrix(n, R)[i, i] = R[1]157    intros i hi158    have same : i = i by rfl159    have entry := identityMatrix.entry at A, add, zero, neg, mul, one, n, i, i with *160    have delta := singleValue.same at A, zero, one, i, i with *161    cc162  have offDiagonal : ∀ i ∈ n, ∀ j ∈ n, i ≠ j → identityMatrix(n, R)[i, j] = R[0]163    intros i hi j hj different164    have entry := identityMatrix.entry at A, add, zero, neg, mul, one, n, i, j with *165    have delta := singleValue.other at A, zero, one, j, i with *166    cc167  exact determinant.identity_entries with *168169end Rings170