Grace/Cumulus/Algebra/Field/IntegralDescent.g17
Imports
IntegralInverse · Construction · Set.OrderTransport
Declarations
Source
1-- Fieldness descends through an injective integral ring homomorphism (ZF).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.IntegralDescent8import IntegralInverse9import Construction10import Set.OrderTransport1112section Maps13variable (A add zero neg mul one B plus z minus times unit f : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring S := (B, plus, z, minus, times, unit)16hypothesis source : IsCommRing(R)17hypothesis target : IsCommRing(S)18hypothesis hom : IsRingHom(f, R, S)19hypothesis injective : InjectiveBetween(f, R, S)2021theorem IsRingHom.reflects_inverse (a b : Set)22 requires memberA : a ∈ R23 requires memberB : b ∈ R24 requires inverse : IsInverse(B, times, unit, f(a), f(b))25 shows IsInverse(A, mul, one, a, b)26proof27 have ordinary := IsCommRing.ring with source28 have monoid := IsRing.multiplicative with ordinary29 have oneIn := IsMonoid.unit_in_carrier with monoid30 have leftIn := IsRing.mul_closed with ordinary, memberB, memberA31 have rightIn := IsRing.mul_closed with ordinary, memberA, memberB32 have leftMap := IsRingHom.mul with hom, memberB, memberA33 have rightMap := IsRingHom.mul with hom, memberA, memberB34 have oneMap := IsRingHom.one with hom35 unfold IsInverse at inverse36 have leftValue : f(R[b * a]) = f(R[1]) by cc37 have rightValue : f(R[a * b]) = f(R[1]) by cc38 have left := Injective.apply_cancel with injective, leftIn, oneIn, leftValue39 have right := Injective.apply_cancel with injective, rightIn, oneIn, rightValue40 unfold IsInverse41 refine ⟨memberA, memberB, left, right⟩4243end Maps4445section Descent46variable (A add zero neg mul one B plus z minus times unit f : Set)47notation ring R := (A, add, zero, neg, mul, one)48notation ring S := (B, plus, z, minus, times, unit)49hypothesis source : IsCommRing(R)50hypothesis field : IsField(S)51hypothesis hom : IsRingHom(f, R, S)52hypothesis injective : InjectiveBetween(f, R, S)5354theorem IsField.of_integral_extension55 requires integral : ∀ y ∈ S, IntegralOver(f, R, S, y)56 shows IsField(R)57proof58 have target := IsField.comm_ring with field59 have distinct := IsField.nontrivial with field60 have ordinary := IsCommRing.ring with source61 have monoid := IsRing.multiplicative with ordinary62 have zeroIn := IsRing.zero_in_carrier with ordinary63 have oneIn := IsMonoid.unit_in_carrier with monoid64 have zeroValue := IsRingHom.zero with hom65 have oneValue := IsRingHom.one with hom66 have distinctTarget := Nontrivial.distinct with distinct67 have distinctSource : R[0] ≠ R[1]68 intro equal69 have impossible : S[0] = S[1] by cc70 exact distinctTarget with impossible71 have nontrivial : Nontrivial(R)72 unfold Nontrivial73 refine ⟨zeroIn, oneIn, distinctSource⟩74 unfold IsField75 refine ⟨source, nontrivial, ?_⟩76 intros a ha nonzero77 have imageA := IsRingHom.closed with hom, ha78 have imageNonzero : f(a) ≠ S[0]79 intro vanishes80 have equal : f(a) = f(R[0]) by cc81 have impossible := Injective.apply_cancel with injective, ha, zeroIn, equal82 exact nonzero with impossible83 obtain ⟨y, inverse⟩ := IsField.inverse_exists with field, imageNonzero84 have data := inverse85 have element := data.right.left86 have cancels := data.right.right.right87 have algebraic := integral with y, element88 obtain ⟨b, hb, value⟩ := IntegralOver.inverse_in_image with source, target, hom, ha, element, cancels, algebraic89 rw value at inverse90 have reflected := IsRingHom.reflects_inverse with source, target, hom, injective, ha, hb, inverse91 refine ⟨b, reflected⟩9293end Descent94