Grace/Cumulus/Algebra/Ring/Equalizer.g17

Open in Workbench Download source

Imports

Subring

Declarations

• ringEqualizer def
• ringEqualizer.subring theorem derivation

Source

1-- Equalizers of ring homomorphisms are subrings (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.Ring.Equalizer8import Subring910def ringEqualizer (f g A : Set) : Set := {x ∈ A | f(x) = g(x)}1112section Homomorphisms13variable (A add zero neg mul one B plus z minus times unit f g : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring S := (B, plus, z, minus, times, unit)16hypothesis ring : IsCommRing(R)17hypothesis first : IsRingHom(f, R, S)18hypothesis second : IsRingHom(g, R, S)1920theorem ringEqualizer.subring21  shows IsSubring(R, ringEqualizer(f, g, A))22proof23  have ordinary := IsCommRing.ring with ring24  have zeroIn := IsRing.zero_in_carrier with ordinary25  have multiplicative := IsRing.multiplicative with ordinary26  have oneIn := IsMonoid.unit_in_carrier with multiplicative27  have firstZero := IsRingHom.zero with first28  have secondZero := IsRingHom.zero with second29  have firstOne := IsRingHom.one with first30  have secondOne := IsRingHom.one with second31  have subset : ringEqualizer(f, g, A) ⊆ A32    intros x hx33    have data := ringEqualizer.membership.forward with hx34    exact data.left35  unfold IsSubring36  refine ⟨subset, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩37  . apply ringEqualizer.membership.backward at f, g, A, zero38    constructor39    . exact zeroIn40    . cc41  . apply ringEqualizer.membership.backward at f, g, A, one42    constructor43    . exact oneIn44    . cc45    intros x hx46    obtain ⟨member, equal⟩ := ringEqualizer.membership.forward with hx47    have closed := IsRing.neg_closed with ordinary, member48    have left := IsRingHom.neg with first, member49    have right := IsRingHom.neg with second, member50    apply ringEqualizer.membership.backward51    constructor52    . exact closed53    . cc54    intros x hx y hy55    obtain ⟨memberX, equalX⟩ := ringEqualizer.membership.forward with hx56    obtain ⟨memberY, equalY⟩ := ringEqualizer.membership.forward with hy57    have closed := IsRing.add_closed with ordinary, memberX, memberY58    have left := IsRingHom.add with first, memberX, memberY59    have right := IsRingHom.add with second, memberX, memberY60    apply ringEqualizer.membership.backward61    constructor62    . exact closed63    . cc64    intros x hx y hy65    obtain ⟨memberX, equalX⟩ := ringEqualizer.membership.forward with hx66    obtain ⟨memberY, equalY⟩ := ringEqualizer.membership.forward with hy67    have closed := IsRing.mul_closed with ordinary, memberX, memberY68    have left := IsRingHom.mul with first, memberX, memberY69    have right := IsRingHom.mul with second, memberX, memberY70    apply ringEqualizer.membership.backward71    constructor72    . exact closed73    . cc7475end Homomorphisms76