Grace/Cumulus/Algebra/IntegralInverse.g17

Open in Workbench Download source

Imports

MonicRelations

Declarations

• monicValue.inverse_relation theorem derivation
• IntegralOver.inverse_in_image theorem derivation

Source

1-- An integral inverse of a coefficient is itself a coefficient (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.IntegralInverse8import MonicRelations910section Algebras11variable (A add zero neg mul one B plus z minus times unit f a y : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis source : IsCommRing(R)15hypothesis target : IsCommRing(S)16hypothesis hom : IsRingHom(f, R, S)17hypothesis coefficient : a ∈ R18hypothesis element : y ∈ S19hypothesis cancels : S[f(a) * y] = S[1]2021theorem monicValue.inverse_relation (cs : List(A))22  shows ∃ p ∈ R, ∃ q ∈ R, S[f(p) * monicValue(R, f, S, y, cs)] = S[1 + f(a) * f(q)]23proof24  induction cs25  | List.nil =>26    have ordinary := IsCommRing.ring with source27    have monoid := IsRing.multiplicative with ordinary28    have oneIn := IsMonoid.unit_in_carrier with monoid29    have zeroIn := IsRing.zero_in_carrier with ordinary30    have oneValue := IsRingHom.one with hom31    have zeroValue := IsRingHom.zero with hom32    have imageA := IsRingHom.closed with hom, coefficient33    refine ⟨one, oneIn, zero, zeroIn, ?_⟩34    rw [monicValue, oneValue, zeroValue]35    ring36  | List.cons(c, tail) using ih =>37    obtain ⟨p, hp, q, hq, identity⟩ := ih38    have ordinary := IsCommRing.ring with source39    have cIn : c ∈ R by assumption40    have nextP := IsRing.mul_closed with ordinary, coefficient, hp41    have pcIn := IsRing.mul_closed with ordinary, hp, cIn42    have nextQ := IsRing.add_closed with ordinary, pcIn, hq43    have imageA := IsRingHom.closed with hom, coefficient44    have imageP := IsRingHom.closed with hom, hp45    have imageQ := IsRingHom.closed with hom, hq46    have imageC := IsRingHom.closed with hom, cIn47    have tailIn := monicValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, y, tail with *48    have mapP := IsRingHom.mul with hom, coefficient, hp49    have mapPC := IsRingHom.mul with hom, hp, cIn50    have mapQ := IsRingHom.add with hom, pcIn, hq51    refine ⟨R[a * p], nextP, R[p * c + q], nextQ, ?_⟩52    rw [monicValue, mapP, mapQ, mapPC]53    have rearrange : S[(f(a) * f(p)) * (f(c) + y * monicValue(R, f, S, y, tail))] = S[f(a) * (f(p) * f(c)) + (f(a) * y) * (f(p) * monicValue(R, f, S, y, tail))]54      ring55    rw [rearrange, cancels, identity]56    ring5758theorem IntegralOver.inverse_in_image59  requires integral : IntegralOver(f, R, S, y)60  shows ∃ b ∈ R, y = f(b)61proof62  have ordinary := IsCommRing.ring with source63  have targetRing := IsCommRing.ring with target64  have monoid := IsRing.multiplicative with targetRing65  have imageA := IsRingHom.closed with hom, coefficient66  have data := integral67  obtain ⟨cs, list, relation⟩ := data.right68  obtain ⟨p, hp, q, hq, identity⟩ := monicValue.inverse_relation at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, a, y, cs with *69  have imageP := IsRingHom.closed with hom, hp70  have imageQ := IsRingHom.closed with hom, hq71  have negative := IsRing.neg_closed with ordinary, hq72  have imageNegative := IsRingHom.closed with hom, negative73  have mapped := IsRingHom.neg with hom, hq74  rw relation at identity75  have annihilate : S[f(p) * 0] = S[0] by ring76  have vanishes : S[1 + f(a) * f(q)] = S[0] by cc77  have inverseValue : S[f(a) * f(R[-q])] = S[1]78    rw mapped79    have rearrange : S[f(a) * (-f(q))] = S[1 - (1 + f(a) * f(q))] by ring80    rw [rearrange, vanishes]81    ring82  have equal : y = f(R[-q])83    have rearrange : S[y * (f(a) * f(R[-q]))] = S[f(R[-q]) * (f(a) * y)] by ring84    rw [inverseValue, cancels] at rearrange85    have leftUnit : S[y * 1] = y by ring86    have rightUnit : S[f(R[-q]) * 1] = f(R[-q]) by ring87    cc88  refine ⟨R[-q], negative, equal⟩8990end Algebras91