Grace/Cumulus/Algebra/Field/Homomorphism.g17

Open in Workbench Download source

Imports

Quotient · Ring.FirstIsomorphism

Declarations

• IsRingHom.kernel_maximal theorem derivation

Source

1-- Kernels of surjective homomorphisms to fields are maximal (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.Homomorphism8import Quotient9import Ring.FirstIsomorphism1011theorem IsRingHom.kernel_maximal (f A add zero neg mul one B plus z minus times unit : Set)12  requires source : IsCommRing(A, add, zero, neg, mul, one)13  requires field : IsField(B, plus, z, minus, times, unit)14  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)15  requires onto : SurjectiveBetween(f, A, B)16  shows IsMaximalIdeal(A, add, zero, neg, mul, one, ringKernel(f, A, z))17proof18  have target := IsField.comm_ring with field19  have nontrivial := IsField.nontrivial with field20  have distinct := Nontrivial.distinct with nontrivial21  have ideal := IsRingHom.kernel_ideal with source, target, hom22  have function := IsRingHom.function with hom23  have ordinary := IsCommRing.ring with source24  have multiplicative := IsRing.multiplicative with ordinary25  have oneIn := IsMonoid.unit_in_carrier with multiplicative26  have unitValue := IsRingHom.one with hom27  have proper : IsProperIdeal(A, add, zero, neg, mul, one, ringKernel(f, A, z))28    constructor29    . exact ideal30    . intro member31      have data := ringKernel.membership.forward with member32      have impossible : z = unit by cc33      exact distinct with impossible34  unfold IsMaximalIdeal35  refine ⟨proper, ?_⟩36  intros J properJ contains37  have idealJ : IsIdeal(A, add, zero, neg, mul, J) by simp [IsProperIdeal]38  have bounded := IsIdeal.subset_carrier with idealJ39  apply Subset.antisymmetric40    intros x hx41    have xIn := bounded with x, hx42    by_contra outside43    have image := IsRingHom.closed with hom, xIn44    have nonzero : f(x) ≠ z45      intro equal46      have member : x ∈ ringKernel(f, A, z) := ringKernel.membership.backward with ⟨xIn, equal⟩47      exact outside with member48    obtain ⟨y, inverse⟩ := IsField.inverse_exists at B, plus, z, minus, times, unit, f(x) with *49    unfold IsInverse at inverse50    have yIn := inverse.right.left51    have surjection := onto52    obtain ⟨a, aIn, edge⟩ := surjection.right with y, yIn53    have imageA := FunctionBetween.apply_value with *54    have productIn := IsRing.mul_closed with ordinary, aIn, xIn55    have mapped := IsRingHom.mul with hom, aIn, xIn56    have equal : f(call2(mul, a, x)) = f(one) by cc57    have congruent := IsRingHom.kernel_congruent.backward with *58    have differenceInJ : call2(add, call2(mul, a, x), neg(one)) ∈ J59      exact contains with call2(add, call2(mul, a, x), neg(one)), congruent60    have productInJ := IsIdeal.mul_left_closed with idealJ, aIn, hx61    have negative := IsIdeal.neg_closed with idealJ, differenceInJ62    have sum := IsIdeal.add_closed with idealJ, productInJ, negative63    have oneInJ : one ∈ J64      ring_nf at sum65      exact sum66    exact properJ.right with oneInJ67  . exact contains68