MaximalIndependentFamily

Finite maximal independent families and polynomial relations, without Choice

Open in Workbench View on GitHub

1-- Finite maximal independent families and polynomial relations, without Choice.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module MaximalIndependentFamily8import Grace.Cumulus.Algebra.Polynomial.IndependentSubfamily910theorem finite_subsets (I : Set)11  requires finite : Finite(I)12  shows Finite(𝒫(I))13proof14  exact Finite.powerset with *1516theorem maximal_member (F J : Set)17  requires finite : Finite(F)18  requires seed : J ∈ F19  shows ∃ M ∈ F, J ⊆ M ∧ (∀ T ∈ F, M ⊆ T → T = M)20proof21  exact Finite.maximal_extension with *2223section Rings24variable (I A add z neg mul one B plus o minus times unit f v : Set)25notation ring R := (A, add, z, neg, mul, one)26notation ring S := (B, plus, o, minus, times, unit)27hypothesis source : IsCommRing(R)28hypothesis target : IsCommRing(S)29hypothesis hom : IsRingHom(f, R, S)3031theorem empty_family32  requires injective : InjectiveBetween(f, R, S)33  requires emptyAssignment : v : ∅ → S34  shows AlgebraicallyIndependent(∅, R, S, f, v)35proof36  exact AlgebraicallyIndependent.empty with *3738theorem maximal_independent_family39  requires finite : Finite(I)40  requires injective : InjectiveBetween(f, R, S)41  requires assignment : v : I → S42  shows ∃ M, M ⊆ I ∧ AlgebraicallyIndependent(M, R, S, f, restrict(v, M)) ∧43    (∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M)44proof45  exact AlgebraicallyIndependent.exists_maximal with *4647theorem extend_independent_family (J : Set)48  requires finite : Finite(I)49  requires subset : J ⊆ I50  requires independent : AlgebraicallyIndependent(J, R, S, f, restrict(v, J))51  shows ∃ M, M ⊆ I ∧ J ⊆ M ∧ AlgebraicallyIndependent(M, R, S, f, restrict(v, M)) ∧52    (∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M)53proof54  exact AlgebraicallyIndependent.maximal_extension with *5556section Adjoin57variable (M j : Set)58notation ring Q := R[insert(j, M)]5960theorem excluded_generator_has_relation61  requires assignment : v : I → S62  requires subset : M ⊆ I63  requires maximal : ∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M64  requires index : j ∈ I65  requires outside : ¬(j ∈ M)66  shows ∃ p ∈ Q, p ≠ Q[0] ∧67    polynomialAtOver(insert(j, M), R, S, f, restrict(v, insert(j, M)))(p) = S[0]68proof69  exact AlgebraicallyIndependent.maximal_adjoin_relation with *7071end Adjoin72end Rings73