Grace/Cumulus/Algebra/Ring/FiniteHom.g17

Open in Workbench Download source

Imports

FiniteProduct · Group.Power

Declarations

Source

1-- Ring homomorphisms preserve finite sums and products, pointwise (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.FiniteHom8import FiniteProduct9import Group.Power1011section Homomorphisms12variable (A add zero neg mul one B plus z minus times unit h : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15hypothesis source : IsCommRing(R)16hypothesis target : IsCommRing(S)17hypothesis hom : IsRingHom(h, R, S)1819theorem indexedRingSum.map (w v f : Set, n : Nat)20  shows WeightedValues(w, f, A, n) →21    (∀ i ∈ n, v(f(i)) = h(w(f(i)))) →22    h(indexedRingSum(w, f, add, zero, n)) = indexedRingSum(v, f, plus, z, n)23proof24  induction n25  | zero =>26    intros values equations27    rw [indexedRingSum, indexedRingSum]28    exact IsRingHom.zero with hom29  | succ(k) using ih =>30    intros values equations31    have prefix := WeightedValues.prefix at w, f, A, k with *32    have last := WeightedValues.last at w, f, A, k with *33    have smaller : ∀ i ∈ k, v(f(i)) = h(w(f(i)))34      intros i hi35      have next := membership.into_successor at i, k with *36      exact equations with i, next37    have lastEquation := equations with k, membership.self_successor at k with *38    have previous := ih with prefix, smaller39    have closure := indexedRingSum.closed at A, add, zero, neg, mul, one, w, f, k with *40    have prefixIn := closure with prefix41    have preserved := IsRingHom.add at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, indexedRingSum(w, f, add, zero, k), w(f(k)) with *42    rw [indexedRingSum, indexedRingSum, preserved, previous, lastEquation]43    rfl4445theorem finiteRingSum.map (V w v : Set)46  requires finite : Finite(V)47  requires weightsW : w : V → R48  requires weightsV : v : V → S49  requires entries : ∀ i ∈ V, v(i) = h(w(i))50  shows h(finiteRingSum(V, R, w)) = finiteRingSum(V, S, v)51proof52  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *53  obtain ⟨n, natural, f, enumeration, equationW⟩ := selected.right54  have injective := Bijective.injective with enumeration55  have function := Injective.function with injective56  have values := WeightedValues.of_functions with weightsW, function57  have equationV := finiteRingSum.enumeration at V, B, plus, z, minus, times, unit, v, f, n with *58  have equations : ∀ i ∈ n, v(f(i)) = h(w(f(i)))59    intros i hi60    have member := FunctionBetween.apply_closed with *61    exact entries with f(i), member62  have preserved := indexedRingSum.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, w, v, f, n with *63  rw [equationW, equationV]64  exact preserved with values, equations6566theorem indexedRingProduct.map (w v f : Set, n : Nat)67  shows WeightedValues(w, f, A, n) →68    (∀ i ∈ n, v(f(i)) = h(w(f(i)))) →69    h(indexedRingProduct(w, f, mul, one, n)) = indexedRingProduct(v, f, times, unit, n)70proof71  induction n72  | zero =>73    intros values equations74    rw [indexedRingProduct, indexedRingProduct]75    exact IsRingHom.one with hom76  | succ(k) using ih =>77    intros values equations78    have prefix := WeightedValues.prefix at w, f, A, k with *79    have last := WeightedValues.last at w, f, A, k with *80    have smaller : ∀ i ∈ k, v(f(i)) = h(w(f(i)))81      intros i hi82      have next := membership.into_successor at i, k with *83      exact equations with i, next84    have lastEquation := equations with k, membership.self_successor at k with *85    have previous := ih with prefix, smaller86    have closure := indexedRingProduct.closed at A, add, zero, neg, mul, one, w, f, k with *87    have prefixIn := closure with prefix88    have preserved := IsRingHom.mul at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, indexedRingProduct(w, f, mul, one, k), w(f(k)) with *89    rw [indexedRingProduct, indexedRingProduct, preserved, previous, lastEquation]90    rfl9192theorem finiteRingProduct.map (V w v : Set)93  requires finite : Finite(V)94  requires weightsW : w : V → R95  requires weightsV : v : V → S96  requires entries : ∀ i ∈ V, v(i) = h(w(i))97  shows h(finiteRingProduct(V, R, w)) = finiteRingProduct(V, S, v)98proof99  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *100  obtain ⟨n, natural, f, enumeration, equationW⟩ := selected.right101  have injective := Bijective.injective with enumeration102  have function := Injective.function with injective103  have values := WeightedValues.of_functions with weightsW, function104  have equationV := finiteRingProduct.enumeration at V, B, plus, z, minus, times, unit, v, f, n with *105  have equations : ∀ i ∈ n, v(f(i)) = h(w(f(i)))106    intros i hi107    have member := FunctionBetween.apply_closed with *108    exact entries with f(i), member109  have preserved := indexedRingProduct.map at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, h, w, v, f, n with *110  rw [equationW, equationV]111  exact preserved with values, equations112113theorem IsRingHom.pow (x : Set, n : Nat)114  requires element : x ∈ R115  shows h(monoidPow(R, x, n)) = monoidPow(S, h(x), n)116proof117  induction n118  | zero =>119    rw [monoidPow.zero, monoidPow.zero]120    exact IsRingHom.one with hom121  | succ(k) using ih =>122    have ordinary := IsCommRing.ring with source123    have multiplicative := IsRing.multiplicative with ordinary124    have product := IsRingHom.mul at h, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, x, monoidPow(R, x, k) with *125    rw [monoidPow.succ, monoidPow.succ, product, ih]126    rfl127128end Homomorphisms129