Grace/Cumulus/Algebra/Polynomial/IndependentSubfamily.g17

Open in Workbench Download source

Imports

EvaluationOver · Nonvanishing · Cardinal.FiniteSubsets

Declarations

Source

1-- Empty and maximal finite algebraically independent subfamilies (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.IndependentSubfamily8import EvaluationOver9import Nonvanishing10import Cardinal.FiniteSubsets1112def independentSubfamilies (I A add z neg mul one B plus o minus times unit f v : Set) : Set :=13  {J ∈ 𝒫(I) | AlgebraicallyIndependent(J, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, restrict(v, J))}1415section Rings16variable (A add z neg mul one B plus o minus times unit f : Set)17notation ring R := (A, add, z, neg, mul, one)18notation ring S := (B, plus, o, minus, times, unit)19hypothesis source : IsCommRing(R)20hypothesis target : IsCommRing(S)21hypothesis hom : IsRingHom(f, R, S)2223theorem AlgebraicallyIndependent.empty (v : Set)24  requires injective : InjectiveBetween(f, R, S)25  requires assignment : v : ∅ → S26  shows AlgebraicallyIndependent(∅, R, S, f, v)27proof28  have zeroIn : R[0] ∈ R by typecheck29  have zero := IsRingHom.zero with hom30  apply AlgebraicallyIndependent.of_no_relation with source, target, hom, assignment31  intros p polynomial vanishes32  have used := polynomialVariablesUsed.subset at ∅, A, z, p33  have constant := polynomialVariablesUsed.empty_constant with *34  have monomial := monomialOne.member at ∅35  have coefficient := polynomials.coefficient with *36  have evaluated := polynomialAtOver.constant with coefficient37  have same : f(p(monomialOne(∅))) = f(R[0])38    rw constant at vanishes39    cc40  have coefficientZero := Injective.apply_cancel with injective, coefficient, same41  rw [constant, coefficientZero]42  exact polynomialConstant.zero with *4344theorem AlgebraicallyIndependent.maximal_extension (I v J : Set)45  requires finite : Finite(I)46  requires subset : J ⊆ I47  requires independent : AlgebraicallyIndependent(J, R, S, f, restrict(v, J))48  shows ∃ M, M ⊆ I ∧ J ⊆ M ∧ AlgebraicallyIndependent(M, R, S, f, restrict(v, M)) ∧49    (∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M)50proof51  have powerFinite := Finite.powerset with finite52  have bounded : independentSubfamilies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v) ⊆ 𝒫(I)53    simp [Subset, independentSubfamilies.membership]54  have familyFinite := Finite.subset with powerFinite, bounded55  have inPower := powerset.membership_iff.backward with subset56  have seed : J ∈ independentSubfamilies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v)57    simp [independentSubfamilies.membership]58  obtain ⟨M, member, extends, maximal⟩ := Finite.maximal_extension with familyFinite, seed59  have data : M ∈ 𝒫(I) ∧ AlgebraicallyIndependent(M, R, S, f, restrict(v, M))60    simp [independentSubfamilies.membership]61  have included := powerset.membership_iff.forward with data.left62  refine ⟨M, included, extends, data.right, ?_⟩63  intros T inside contains independentT64  have power := powerset.membership_iff.backward with inside65  have memberT : T ∈ independentSubfamilies(I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v)66    simp [independentSubfamilies.membership]67  exact maximal with T, memberT, contains6869theorem AlgebraicallyIndependent.exists_maximal (I v : Set)70  requires finite : Finite(I)71  requires injective : InjectiveBetween(f, R, S)72  requires assignment : v : I → S73  shows ∃ M, M ⊆ I ∧ AlgebraicallyIndependent(M, R, S, f, restrict(v, M)) ∧74    (∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M)75proof76  have subset := empty.subset at I77  have closed : ∀ x ∈ ∅, v(x) ∈ S by simp [set.empty]78  have restricted := restrict.function with *79  have empty := AlgebraicallyIndependent.empty with *80  obtain ⟨M, included, extends, independent, maximal⟩ := AlgebraicallyIndependent.maximal_extension at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, I, v, ∅ with *81  refine ⟨M, included, independent, maximal⟩8283section Relations84variable (I v : Set)85notation ring P := R[I]8687theorem AlgebraicallyIndependent.relation_of_dependent88  requires assignment : v : I → S89  requires dependent : ¬AlgebraicallyIndependent(I, R, S, f, v)90  shows ∃ p ∈ P, p ≠ P[0] ∧ polynomialAtOver(I, R, S, f, v)(p) = S[0]91proof92  by_contra absent93  have relations : ∀ p ∈ P, polynomialAtOver(I, R, S, f, v)(p) = S[0] → p = P[0]94    intros p polynomial vanishes95    by_contra nonzero96    apply absent97    refine ⟨p, polynomial, nonzero, vanishes⟩98  have independent := AlgebraicallyIndependent.of_no_relation with *99  exact dependent with independent100101end Relations102section Adjoin103variable (I v M j : Set)104notation ring Q := R[insert(j, M)]105106theorem AlgebraicallyIndependent.maximal_adjoin_relation107  requires assignment : v : I → S108  requires subset : M ⊆ I109  requires maximal : ∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M110  requires index : j ∈ I111  requires outside : ¬(j ∈ M)112  shows ∃ p ∈ Q, p ≠ Q[0] ∧113    polynomialAtOver(insert(j, M), R, S, f, restrict(v, insert(j, M)))(p) = S[0]114proof115  have inside : insert(j, M) ⊆ I116    settle with Subset, insert.membership117  have contains : M ⊆ insert(j, M) by simp [Subset, insert.membership]118  have closed : ∀ x ∈ insert(j, M), v(x) ∈ S119    intros x member120    have included := inside121    have inI := included with x, member122    exact FunctionBetween.apply_closed with assignment, inI123  have restricted := restrict.function at v, I, S, insert(j, M), S with *124  have dependent : ¬AlgebraicallyIndependent(insert(j, M), R, S, f, restrict(v, insert(j, M)))125    intro independent126    have equal := maximal with insert(j, M), inside, contains, independent127    have member := insert.self at j, M128    rw equal at member129    exact outside with member130  exact AlgebraicallyIndependent.relation_of_dependent with *131132end Adjoin133end Rings134