FiniteModuleIntegrality

Finite-module integrality from the constructive determinant trick (ZF)

Open in Workbench View on GitHub

1-- Finite-module integrality from the constructive determinant trick (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 FiniteModuleIntegralityExample7import Grace.Cumulus.Algebra.MatrixAnnihilator89section Algebras10variable (A add zero neg mul one B plus z minus times unit f x : 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(f, R, S)16hypothesis element : x ∈ S1718theorem integral19  requires finiteModule : FiniteAlgebraModule(f, R, S)20  shows IntegralOver(f, R, S, x)21proof22  exact FiniteAlgebraModule.integral with *2324theorem annihilator (xs : List(B)) (M : Set)25  requires matrix : RingMatrix(length{B}(xs), R, M)26  requires rows : ∀ i ∈ length{B}(xs), ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧ S[x * listCoefficient{B}(z, xs, i)] = linearCombination(R, S, f, xs, cs) ∧ (∀ j ∈ length{B}(xs), M[i, j] = listCoefficient{A}(zero, cs, j))27  shows ∃ cs, List(A, cs) ∧ length{A}(cs) = length{B}(xs) ∧ (∀ g ∈ listSupport{B}(xs), S[monicValue(R, f, S, x, cs) * g] = S[0])28proof29  exact multiplicationMatrix.monic_annihilator with *3031end Algebras32