Grace/Cumulus/Algebra/Field/Infinite.g17
Imports
AlgebraicClosure · Polynomial.MonicVanishing
Declarations
Source
1-- Algebraically closed fields are infinite, by an explicit root-free polynomial.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.Field.Infinite8import AlgebraicClosure9import Polynomial.MonicVanishing1011section Fields12variable (A add zero neg mul one : Set)13notation ring R := (A, add, zero, neg, mul, one)1415-- A monic polynomial vanishing on a finite cover cannot take the value -1.16-- Adding 1 to its constant coefficient contradicts algebraic closedness.17theorem IsAlgebraicallyClosed.infinite18 requires closed : IsAlgebraicallyClosed(R)19 shows ¬Finite(R)20proof21 have field := IsAlgebraicallyClosed.field with closed22 have ring := IsField.comm_ring with field23 have ordinary := IsCommRing.ring with ring24 have multiplicative := IsRing.multiplicative with ordinary25 have unitIn := IsMonoid.unit_in_carrier with multiplicative26 have nontrivial := IsField.nontrivial with field27 have distinct := Nontrivial.distinct with nontrivial28 intro finite29 obtain ⟨xs, list, cover⟩ := Finite.list_cover with finite30 obtain ⟨c, coefficient, cs, coefficients, vanishes⟩ := hornerAt.monic_vanishing_on_list at A, add, zero, neg, mul, one, xs with *31 have shifted := IsRing.add_closed with ordinary, coefficient, unitIn32 have nonconstant : R[c + 1] :: cs ≠ []33 intro same34 have lengths : length{A}(R[c + 1] :: cs) = length{A}([])35 rw same36 rfl37 rw [length.cons, length.nil] at lengths38 have reversed : (0 : Nat) = succ(length{A}(cs)) by cc39 exact Naturals.disjoint.zero.succ at length{A}(cs) with reversed40 obtain ⟨x, element, root⟩ := IsAlgebraicallyClosed.root at A, add, zero, neg, mul, one, R[c + 1] :: cs with *41 have rootValue : hornerAt{A}(add, mul, one, x, R[c + 1] :: cs) = R[0]42 simp [hornerAt]43 have member := cover with x, element44 have old := vanishes with x, element, member45 have tailValue := hornerAt.closed at A, add, zero, neg, mul, one, one, x, cs with *46 rw hornerAt.cons at rootValue47 rw hornerAt.cons at old48 have rearrange : R[(c + 1) + x * hornerAt{A}(add, mul, one, x, cs)] = R[(c + x * hornerAt{A}(add, mul, one, x, cs)) + 1]49 ring50 rw [rootValue, old] at rearrange51 have unit : R[0 + 1] = R[1] by ring52 rw unit at rearrange53 exact distinct with rearrange5455end Fields56