IntegralAdjoin

A quadratic relation gives a finite module after adjoining its root

Open in Workbench View on GitHub

1-- A quadratic relation gives a finite module after adjoining its root.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 IntegralAdjoin8import Grace.Cumulus.Algebra.Field.Algebraic910section Algebras11variable (A add zero neg mul one B plus z minus times unit f x a : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis source : IsCommRing(R)15hypothesis target : IsCommRing(S)16hypothesis hom : IsRingHom(f, R, S)17hypothesis element : x ∈ S18hypothesis coefficient : a ∈ R19hypothesis quadratic : S[x * x] = f(a)2021theorem quadratic_root_is_integral22  shows IntegralOver(f, R, S, x)23proof24  exact IntegralOver.of_square with *2526theorem adjoining_a_quadratic_root_is_module_finite27  shows ∃ G, Finite(G) ∧ G ⊆ algebraAdjoin(f, R, S, {x}) ∧ linearSpan(f, R, S, G) = algebraAdjoin(f, R, S, {x})28proof29  have integral := quadratic_root_is_integral at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, a with *30  exact IntegralOver.finite_adjoin with *3132end Algebras33section Fields34variable (A add zero neg mul one B plus z minus times unit f x : Set)35notation ring R := (A, add, zero, neg, mul, one)36notation ring S := (B, plus, z, minus, times, unit)37hypothesis field : IsField(R)38hypothesis target : IsCommRing(S)39hypothesis hom : IsRingHom(f, R, S)4041theorem algebraic_generator_gives_finite_module42  requires algebraic : AlgebraicOver(f, R, S, x)43  requires generates : algebraAdjoin(f, R, S, {x}) = S44  shows FiniteAlgebraModule(f, R, S)45proof46  exact AlgebraicOver.finite_module_of_generates with *4748end Fields49