Grace/Cumulus/Algebra/Field/Embedding.g17

Open in Workbench Download source

Imports

Homomorphism

Declarations

Source

1-- Unital homomorphisms from a field into a nontrivial ring are injective (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.Embedding8import Homomorphism910section Fields11variable (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 field : IsField(R)15hypothesis target : IsCommRing(S)16hypothesis nontrivial : Nontrivial(S)17hypothesis hom : IsRingHom(f, R, S)1819theorem IsRingHom.field_reflects_zero (x : Set)20  requires member : x ∈ R21  requires vanishes : f(x) = S[0]22  shows x = R[0]23proof24  by_contra nonzero25  obtain ⟨y, inverse⟩ := IsField.inverse_exists at A, add, zero, neg, mul, one, x with *26  unfold IsInverse at inverse27  have yIn := inverse.right.left28  have product := inverse.right.right.left29  have mapped := IsRingHom.mul with hom, member, yIn30  have oneValue := IsRingHom.one with hom31  have imageY := IsRingHom.closed with hom, yIn32  have annihilate : S[0 * f(y)] = S[0] by ring33  have impossible : S[0] = S[1] by cc34  have distinct := Nontrivial.distinct with nontrivial35  exact distinct with impossible3637theorem IsRingHom.field_injective38  shows InjectiveBetween(f, R, S)39proof40  have source := IsField.comm_ring with field41  have ordinary := IsCommRing.ring with source42  have function := IsRingHom.function with hom43  constructor44  . exact function45  . intros x hx y hy b hb first second46    have valueX := FunctionBetween.apply_value with function, hx, first47    have valueY := FunctionBetween.apply_value with function, hy, second48    have negative := IsRing.neg_closed with ordinary, hy49    have difference := IsRing.add_closed with ordinary, hx, negative50    have mapped := IsRingHom.sub with source, hom, hx, hy51    have zero : S[f(x) - f(y)] = S[0]52      rw [valueX, valueY]53      ring54    have vanishes : f(R[x - y]) = S[0] by cc55    have equal := IsRingHom.field_reflects_zero with *56    have recover : R[(x - y) + y] = x by ring57    have remove : R[0 + y] = y by ring58    cc5960theorem IsRingHom.field_iso_of_surjective61  requires onto : SurjectiveBetween(f, R, S)62  shows IsRingIso(f, R, S)63proof64  have injective := IsRingHom.field_injective with *65  have bijective : BijectiveBetween(f, R, S)66    unfold BijectiveBetween67    refine ⟨injective, onto⟩68  unfold IsRingIso69  refine ⟨hom, bijective⟩7071end Fields72