Grace/Cumulus/Algebra/Ring/DeterminantHom.g17

Open in Workbench Download source

Imports

Determinant · FiniteHom

Declarations

Source

1-- Ring homomorphisms commute with the Leibniz determinant (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.DeterminantHom8import Determinant9import FiniteHom1011-- Entrywise mapping is useful independently of ring structure.12defgraph matrixMap (I A B h M : Set) (p ∈ I × I) : B := h(M(p))13requires matrix : RingMatrix(I, A, M)14requires function : h : A → B15proof16  unfold RingMatrix at matrix17  have entry := FunctionBetween.apply_closed at M, I × I, A, p with *18  exact FunctionBetween.apply_closed at h, A, B, M(p) with *1920theorem matrixMap.matrix (I A B h M : Set)21  requires matrix : RingMatrix(I, A, M)22  requires function : h : A → B23  shows RingMatrix(I, B, matrixMap(I, A, B, h, M))24proof25  unfold RingMatrix26  exact matrixMap.function with *2728theorem matrixMap.entry (I A B h M i j : Set)29  requires matrix : RingMatrix(I, A, M)30  requires function : h : A → B31  requires row : i ∈ I32  requires column : j ∈ I33  shows matrixMap(I, A, B, h, M)[i, j] = h(M[i, j])34proof35  have pair := product.pair at i, j, I, I with *36  exact matrixMap.value with *3738section Homomorphisms39variable (A add zero neg mul one B plus z minus times unit h : Set)40notation ring R := (A, add, zero, neg, mul, one)41notation ring S := (B, plus, z, minus, times, unit)42hypothesis source : IsCommRing(R)43hypothesis target : IsCommRing(S)44hypothesis hom : IsRingHom(h, R, S)4546theorem permutationSign.map (I p : Set)47  requires finite : Finite(I)48  shows h(permutationSign(I, R, p)) = permutationSign(I, S, p)49proof50  have inversionsFinite := inversions.finite at I, p with *51  have count := cardinality.correct with inversionsFinite52  have natural := count.left53  have ordinary := IsCommRing.ring with source54  have multiplicative := IsRing.multiplicative with ordinary55  have oneIn := IsMonoid.unit_in_carrier with multiplicative56  have negative := IsRing.neg_closed with ordinary, oneIn57  have mapsOne := IsRingHom.one with hom58  have mapsNegative := IsRingHom.neg at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, one with *59  have power := IsRingHom.pow at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, R[-1], cardinality(inversions(I, p)) with *60  simp [permutationSign]6162theorem determinant.map (n : Nat) (M N : Set)63  requires matrixM : RingMatrix(n, R, M)64  requires matrixN : RingMatrix(n, S, N)65  requires entries : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = h(M[i, j])66  shows h(determinant(n, R, M)) = determinant(n, S, N)67proof68  have finite := Finite.natural at n with *69  have permutationsFinite := permutations.finite with finite70  have weightsM := determinantTerms.function at n, A, add, zero, neg, mul, one, M with *71  have weightsN := determinantTerms.function at n, B, plus, z, minus, times, unit, N with *72  have terms : ∀ p ∈ permutations(n), determinantTerms(n, S, N)(p) = h(determinantTerms(n, R, M)(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 entriesM := permutationEntries.function at n, A, M, p with *78    have entriesN := permutationEntries.function at n, B, N, p with *79    have pointwise : ∀ i ∈ n, permutationEntries(n, B, N, p)(i) = h(permutationEntries(n, A, M, p)(i))80      intros i hi81      have column := FunctionBetween.apply_closed at p, n, n, i with *82      have left := permutationEntries.value at n, B, N, p, i with *83      have right := permutationEntries.value at n, A, M, p, i with *84      rw [left, right]85      exact entries with i, hi, p(i), column86    have product := finiteRingProduct.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, n, permutationEntries(n, A, M, p), permutationEntries(n, B, N, p) with *87    have sign := permutationSign.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, n, p with *88    have multiply := IsRingHom.mul at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, permutationSign(n, R, p), finiteRingProduct(n, R, permutationEntries(n, A, M, p)) with *89    have termM := determinantTerms.value at n, A, add, zero, neg, mul, one, M, p with *90    have termN := determinantTerms.value at n, B, plus, z, minus, times, unit, N, p with *91    rw [termM, termN, multiply, sign, product]92    rfl93  unfold determinant94  exact finiteRingSum.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, permutations(n), determinantTerms(n, R, M), determinantTerms(n, S, N) with *9596theorem determinant.map_matrix (n : Nat) (M : Set)97  requires matrix : RingMatrix(n, R, M)98  shows h(determinant(n, R, M)) = determinant(n, S, matrixMap(n, R, S, h, M))99proof100  have function := IsRingHom.function with hom101  have mapped := matrixMap.matrix with *102  have entries : ∀ i ∈ n, ∀ j ∈ n, matrixMap(n, R, S, h, M)[i, j] = h(M[i, j])103    intros i hi j hj104    exact matrixMap.entry with *105  exact determinant.map with *106107end Homomorphisms108