IntegralDescent

Field descent through an integral extension, without Choice

Open in Workbench View on GitHub

1-- Field descent through an integral extension, without Choice.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 IntegralDescent8import Grace.Cumulus.Algebra.Field.IntegralDescent910section 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 source : IsCommRing(R)15hypothesis field : IsField(S)16hypothesis hom : IsRingHom(f, R, S)17hypothesis embedding : InjectiveBetween(f, R, S)1819theorem field_descends20  requires integral : ∀ y ∈ S, IntegralOver(f, R, S, y)21  shows IsField(R)22proof23  exact IsField.of_integral_extension with *2425theorem a_nonfield_has_a_nonintegral_element26  requires notField : ¬IsField(R)27  shows ¬(∀ y ∈ S, IntegralOver(f, R, S, y))28proof29  intro integral30  have sourceField : IsField(R)31    exact IsField.of_integral_extension with *32  exact notField with sourceField3334end Extensions35