FiniteExtensions
Finite adjoining and towers of algebraic extensions
1-- Finite adjoining and towers of algebraic extensions.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 FiniteExtensions8import Grace.Cumulus.Algebra.IntegralFinite9import Grace.Cumulus.Algebra.FiniteModuleTower1011section QuadraticRoots12variable (A add zero neg mul one B plus z minus times unit f x y a b : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15hypothesis source : IsCommRing(R)16hypothesis target : IsCommRing(S)17hypothesis hom : IsRingHom(f, R, S)18hypothesis xIn : x ∈ S19hypothesis yIn : y ∈ S20hypothesis aIn : a ∈ R21hypothesis bIn : b ∈ R22hypothesis squareX : S[x * x] = f(a)23hypothesis squareY : S[y * y] = f(b)2425theorem two_quadratic_roots26 shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, insert(x, {y})))27proof28 have integralX := IntegralOver.of_square with source, target, hom, xIn, aIn, squareX29 have integralY := IntegralOver.of_square with source, target, hom, yIn, bIn, squareY30 have single := Finite.singleton at y31 have finite := Finite.insert at {y}, x with single32 have bounded : insert(x, {y}) ⊆ S33 unfold Subset34 intros u hu35 simp [insert.membership, singleton.membership]36 have integral : ∀ u ∈ insert(x, {y}), IntegralOver(f, R, S, u)37 intros u hu38 have casesU := insert.membership.forward with hu39 cases casesU with equal | member40 . rw equal41 exact integralX42 . have equal := singleton.membership.forward at u, y with member43 rw equal44 exact integralY45 exact integralGenerators.finite_adjoin with source, target, hom, finite, bounded, integral4647end QuadraticRoots4849section Towers50variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e f g : Set)51notation ring R := (A, add, zero, neg, mul, one)52notation ring S := (B, plus, z, minus, times, unit)53notation ring U := (C, sum, o, inverse, product, e)54hypothesis fieldR : IsField(R)55hypothesis fieldS : IsField(S)56hypothesis target : IsCommRing(U)57hypothesis mapRS : IsRingHom(f, R, S)58hypothesis mapSU : IsRingHom(g, S, U)5960theorem algebraic_tower_is_finite61 requires generatedS : FinitelyGeneratedAlgebra(f, R, S)62 requires algebraicS : ∀ x ∈ S, AlgebraicOver(f, R, S, x)63 requires generatedU : FinitelyGeneratedAlgebra(g, S, U)64 requires algebraicU : ∀ x ∈ U, AlgebraicOver(g, S, U, x)65 shows FiniteAlgebraModule(compose(g, f, R, S, U), R, U)66proof67 have ringR := IsField.comm_ring with fieldR68 have ringS := IsField.comm_ring with fieldS69 have finiteS := FinitelyGeneratedAlgebra.finite_module_of_algebraic with fieldR, ringS, mapRS, generatedS, algebraicS70 have finiteU := FinitelyGeneratedAlgebra.finite_module_of_algebraic with fieldS, target, mapSU, generatedU, algebraicU71 exact FiniteAlgebraModule.tower with ringR, ringS, target, mapRS, mapSU, finiteS, finiteU7273end Towers74