AlgebraicRigidity

No new algebraic elements over an algebraically closed field

Open in Workbench View on GitHub

1-- No new algebraic elements over an algebraically closed field.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 AlgebraicRigidity8import Grace.Cumulus.Algebra.Field.Rigidity910section Extensions11variable (A add zero neg mul one B plus z minus times unit f : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis closed : IsAlgebraicallyClosed(R)15hypothesis field : IsField(S)16hypothesis hom : IsRingHom(f, R, S)1718theorem algebraic_element (x : Set)19  requires algebraic : AlgebraicOver(f, R, S, x)20  shows ∃ a ∈ R, f(a) = x21proof22  exact IsAlgebraicallyClosed.algebraic_in_image with *2324theorem no_proper_algebraic_extension25  requires algebraic : ∀ x ∈ S, AlgebraicOver(f, R, S, x)26  shows SurjectiveBetween(f, R, S)27proof28  exact IsAlgebraicallyClosed.algebraic_extension_surjective with *2930end Extensions31