DeterminantMaps

Determinants commute with ring maps and polynomial evaluation (ZF)

Open in Workbench View on GitHub

1-- Determinants commute with ring maps and polynomial evaluation (ZF).2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module DeterminantMaps7import Grace.Cumulus.Algebra.Polynomial.Determinant89section Maps10variable (A add zero neg mul one B plus z minus times unit h : Set)11notation ring R := (A, add, zero, neg, mul, one)12notation ring S := (B, plus, z, minus, times, unit)13hypothesis source : IsCommRing(R)14hypothesis target : IsCommRing(S)15hypothesis hom : IsRingHom(h, R, S)1617theorem transport (n : Nat) (M N : Set)18  requires matrixM : RingMatrix(n, R, M)19  requires matrixN : RingMatrix(n, S, N)20  requires entries : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = h(M[i, j])21  shows h(determinant(n, R, M)) = determinant(n, S, N)22proof23  exact determinant.map with *2425end Maps2627section Polynomials28variable (I A add zero neg mul one v : Set)29notation ring R := (A, add, zero, neg, mul, one)30notation ring P := R[I]31hypothesis ring : IsCommRing(R)32hypothesis assignment : v : I → R3334theorem evaluate (n : Nat) (M N : Set)35  requires matrixM : RingMatrix(n, P, M)36  requires matrixN : RingMatrix(n, R, N)37  requires entries : ∀ i ∈ n, ∀ j ∈ n, N[i, j] = polynomialAt(I, R, v)(M[i, j])38  shows polynomialAt(I, R, v)(determinant(n, P, M)) = determinant(n, R, N)39proof40  exact determinant.evaluate with *4142theorem evaluate_without_auxiliary_matrix (n : Nat) (M : Set)43  requires matrix : RingMatrix(n, P, M)44  shows polynomialAt(I, R, v)(determinant(n, P, M)) =45    determinant(n, R, matrixMap(n, P, R, polynomialAt(I, R, v), M))46proof47  exact determinant.evaluate_matrix with *4849end Polynomials50