Grace/Cumulus/Algebra/Polynomial/AlgebraicDependence.g17

Open in Workbench Download source

Imports

Transfer · IndependentSubfamily · HornerRelations

Declarations

Source

1-- Relations become algebraicity over the smaller polynomial coefficient 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.Polynomial.AlgebraicDependence8import Transfer9import IndependentSubfamily10import HornerRelations1112section Rings13variable (I M A add z neg mul one B plus o minus times unit f v : Set)14notation ring R := (A, add, z, neg, mul, one)15notation ring S := (B, plus, o, minus, times, unit)16notation ring P := R[I]17notation ring Q := R[M]18hypothesis source : IsCommRing(R)19hypothesis target : IsCommRing(S)20hypothesis hom : IsRingHom(f, R, S)21hypothesis assignment : v : I → S22hypothesis subset : M ⊆ I2324theorem polynomialVariableCoefficient.supported_in (p j : Set, n : Nat)25  requires polynomial : p ∈ P26  requires variables : polynomialVariablesUsed(I, R, p) ⊆ insert(j, M)27  shows polynomialVariablesUsed(I, R, polynomialVariableCoefficient(I, R, p, j, n)) ⊆ M28proof29  have zeroIn : R[0] ∈ R by typecheck30  have bound := polynomialVariableCoefficient.variables at I, A, z, p, j, n with *31  intros i used32  have data := bound with i, used33  obtain ⟨original, absent⟩ := difference.membership.forward with data34  have included := variables with i, original35  have alternatives := insert.membership.forward with included36  cases alternatives with equal | member37  . exfalso38    have singleton := singleton.membership.backward with equal39    exact absent with singleton40  . exact member4142theorem polynomialAtOver.algebraic_of_relation (p j : Set)43  requires polynomial : p ∈ P44  requires index : j ∈ I45  requires variables : polynomialVariablesUsed(I, R, p) ⊆ insert(j, M)46  requires nonzero : p ≠ P[0]47  requires relation : polynomialAtOver(I, R, S, f, v)(p) = S[0]48  shows AlgebraicOver(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S, v(j))49proof50  have zeroIn : R[0] ∈ R by typecheck51  have oneIn : R[1] ∈ R by typecheck52  have sourceP : IsCommRing(P)53    exact polynomials.comm_ring with *54  have sourceQ : IsCommRing(Q)55    exact polynomials.comm_ring with *56  have closed : ∀ i ∈ M, v(i) ∈ S57    intros i member58    have included := subset59    have inI := included with i, member60    exact FunctionBetween.apply_closed with assignment, inI61  have restricted := restrict.function at v, I, S, M, S with *62  have evaluationI : IsRingHom(polynomialAtOver(I, R, S, f, v), P, S)63    exact polynomialAtOver.hom with *64  have evaluationM : IsRingHom(polynomialAtOver(M, R, S, f, restrict(v, M)), Q,65    S)66    exact polynomialAtOver.hom with *67  have transfer : IsRingHom(polynomialTransfer(I, M, R), P, Q)68    exact polynomialTransfer.hom with *69  have functionI := IsRingHom.function with evaluationI70  have functionM := IsRingHom.function with evaluationM71  have functionT := IsRingHom.function with transfer72  have zeroT := IsRingHom.zero with transfer73  have zeroI := IsRingHom.zero with evaluationI74  have zeroP : P[0] ∈ P by typecheck75  have variableIn := polynomialVariable.member at I, A, z, one, j with *76  have variableValue := polynomialAtOver.variable at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, j with *77  have element := FunctionBetween.apply_closed with assignment, index78  obtain ⟨cs, list, coefficients⟩ := polynomialCoefficientFamily.list_representation at I, A, z, p, j with *79  have reconstructed := polynomialFromCoefficients.reconstruct at I, A, add, z, neg, mul, one, p, j, cs with *80  have coefficientValues : ∀ n, Nat(n) → compose(polynomialAtOver(M, R, S, f, restrict(v, M)), polynomialTransfer(I, M, R), P, Q, S)(listCoefficient{P}(P[0], cs, n)) = polynomialAtOver(I, R, S, f, v)(listCoefficient{P}(P[0], cs, n))81    intros n natural82    have value := coefficients with n, natural83    have member := polynomialVariableCoefficient.member at I, A, z, p, j, n with *84    have supported := polynomialVariableCoefficient.supported_in at I, M, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, p, j, n with *85    have agreement : ∀ i ∈ polynomialVariablesUsed(I, R, polynomialVariableCoefficient(I, R, p, j, n)), v(i) = restrict(v, M)(i)86      intros i used87      have included := supported88      have inM := included with i, used89      symm90      exact restrict.apply at v, I, S, M, S, i with *91    have evaluated := polynomialTransfer.evaluate_supported at I, M, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, restrict(v, M), polynomialVariableCoefficient(I, R, p, j, n) with *92    have composed := compose.apply at polynomialAtOver(M, R, S, f, restrict(v, M)), polynomialTransfer(I, M, R), P, Q, S, polynomialVariableCoefficient(I, R, p, j, n) with *93    rw value94    cc95  have same := listMap.congr_coefficients at P, P[0], compose(polynomialAtOver(M, R, S, f, restrict(v, M)), polynomialTransfer(I, M, R), P, Q, S), polynomialAtOver(I, R, S, f, v), cs with *96  have composed := listMap.compose at P, Q, S, polynomialTransfer(I, M, R), polynomialAtOver(M, R, S, f, restrict(v, M)), cs with *97  have mapped := hornerAt.map at P, polynomialAdd(I, A, add, z, neg, mul, one), P[0], polynomialNeg(I, A, add, z, neg, mul, one), polynomialMul(I, A, add, z, neg, mul, one), polynomialConstant(I, R, one), B, plus, o, minus, times, unit, polynomialAtOver(I, R, S, f, v), P[0], polynomialVariable(I, R, j), cs with *98  rw [zeroI, variableValue] at mapped99  unfold polynomialFromCoefficients at reconstructed100  have normalized := monicValue.mapped_coefficients at Q, S, plus, times, polynomialAtOver(M, R, S, f, restrict(v, M)), o, v(j), listMap{P}(polynomialTransfer(I, M, R), cs) with *101  have vanishes : monicValue{Q}(polynomialAtOver(M, R, S, f, restrict(v, M)), plus, times, o, v(j), listMap{P}(polynomialTransfer(I, M, R), cs)) = o102    cc103  obtain ⟨n, nIn, nonzeroCoefficient⟩ := polynomialVariableCoefficient.exists_nonzero at I, A, z, p, j with *104  have natural := nat.omega.backward with nIn105  have member := polynomialVariableCoefficient.member at I, A, z, p, j, n with *106  have supported := polynomialVariableCoefficient.supported_in at I, M, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v, p, j, n with *107  have nonzeroTransfer := polynomialTransfer.nonzero_supported at I, M, A, add, z, neg, mul, one, polynomialVariableCoefficient(I, R, p, j, n) with *108  have coefficient := coefficients with n, natural109  have lookup := listCoefficient.map at P, Q, polynomialTransfer(I, M, R), P[0], cs, n with *110  rw zeroT at lookup111  have nonzeroList : ∃ k, Nat(k) ∧ listCoefficient{Q}(Q[0], listMap{P}(polynomialTransfer(I, M, R), cs), k) ≠ Q[0]112    refine ⟨n, natural, ?_⟩113    rwa [lookup, coefficient]114  exact AlgebraicOver.of_coefficient_relation with *115116theorem AlgebraicallyIndependent.maximal_algebraic (j : Set)117  requires maximal : ∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M118  requires index : j ∈ I119  requires outside : ¬(j ∈ M)120  shows AlgebraicOver(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S, v(j))121proof122  have inside : insert(j, M) ⊆ I by simp [Subset, insert.membership]123  have contains : M ⊆ insert(j, M) by simp [Subset, insert.membership]124  have closed : ∀ i ∈ insert(j, M), v(i) ∈ S125    intros i member126    have included := inside127    have inI := included with i, member128    exact FunctionBetween.apply_closed with assignment, inI129  have restricted := restrict.function with *130  have jIn := insert.self at j, M131  obtain ⟨p, polynomial, nonzero, relation⟩ := AlgebraicallyIndependent.maximal_adjoin_relation at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, I, v, M, j with *132  have variables := polynomialVariablesUsed.subset at insert(j, M), A, z, p133  have algebraic := polynomialAtOver.algebraic_of_relation with *134  have nested := restrict.nested at v, M, insert(j, M) with contains135  have value := restrict.apply with *136  rwa [nested, value] at algebraic137138end Rings139