Grace/Cumulus/Algebra/Ring/FiniteProduct.g17

Open in Workbench Download source

Imports

SumSupport

Declarations

Source

1-- Finite products in commutative rings, independent of enumeration (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.FiniteProduct8import SumSupport910def indexedRingProduct (w f mul u1 : Set, n : Nat) → Set11  | w, f, mul, u1, zero => u112  | w, f, mul, u1, succ(k) => call2(mul, indexedRingProduct(w, f, mul, u1, k), w(f(k)))1314def matchingProductRow (A u1 mul w f x : Set, n : Nat) → Set15  | A, u1, mul, w, f, x, zero => u116  | A, u1, mul, w, f, x, succ(k) => call2(mul, matchingProductRow(A, u1, mul, w, f, x, k), singleValue(A, u1, w(x), x, f(k)))1718def matchingProductTotal (A u1 mul w f g : Set, n m : Nat) → Set19  | A, u1, mul, w, f, g, n, zero => u120  | A, u1, mul, w, f, g, n, succ(k) => call2(mul, matchingProductTotal(A, u1, mul, w, f, g, n, k), matchingProductRow(A, u1, mul, w, f, g(k), n))21  descends m2223section Rings24variable (A add zero neg mul one w : Set)25hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)26notation ring R := (A, add, zero, neg, mul, one)2728theorem indexedRingProduct.closed (f : Set, n : Nat)29  shows WeightedValues(w, f, A, n) → indexedRingProduct(w, f, mul, one, n) ∈ A30proof31  induction n32  | zero =>33    have ordinary := IsCommRing.ring with ring34    have multiplicative := IsRing.multiplicative with ordinary35    intro values36    rw indexedRingProduct37    exact IsMonoid.unit_in_carrier with multiplicative38  | succ(k) using ih =>39    have ordinary := IsCommRing.ring with ring40    have multiplicative := IsRing.multiplicative with ordinary41    intro values42    have prefix := WeightedValues.prefix at w, f, A, k with *43    have last := WeightedValues.last at w, f, A, k with *44    have previous := ih with prefix45    rw indexedRingProduct46    exact IsRing.mul_closed with ordinary, previous, last4748theorem matchingProductRow.closed (f x : Set, n : Nat)49  requires value : w(x) ∈ A50  shows matchingProductRow(A, one, mul, w, f, x, n) ∈ A51proof52  induction n53  | zero =>54    have ordinary := IsCommRing.ring with ring55    have multiplicative := IsRing.multiplicative with ordinary56    have oneIn := IsMonoid.unit_in_carrier with multiplicative57    rwa matchingProductRow58  | succ(k) using ih =>59    have ordinary := IsCommRing.ring with ring60    have multiplicative := IsRing.multiplicative with ordinary61    have oneIn := IsMonoid.unit_in_carrier with multiplicative62    have last := singleValue.closed at A, one, w(x), x, f(k) with *63    rw matchingProductRow64    exact IsRing.mul_closed with ordinary, ih, last6566theorem matchingProductTotal.closed (f g : Set, n m : Nat)67  shows WeightedValues(w, g, A, m) → matchingProductTotal(A, one, mul, w, f, g, n, m) ∈ A68proof69  induction m70  | zero =>71    have ordinary := IsCommRing.ring with ring72    have multiplicative := IsRing.multiplicative with ordinary73    intro values74    rw matchingProductTotal75    exact IsMonoid.unit_in_carrier with multiplicative76  | succ(k) using ih =>77    have ordinary := IsCommRing.ring with ring78    have multiplicative := IsRing.multiplicative with ordinary79    intro values80    have prefix := WeightedValues.prefix at w, g, A, k with *81    have last := WeightedValues.last at w, g, A, k with *82    have previous := ih with prefix83    have row := matchingProductRow.closed at A, add, zero, neg, mul, one, w, f, g(k), n with *84    rw matchingProductTotal85    exact IsRing.mul_closed with ordinary, previous, row8687theorem matchingProductRow.absent (f x : Set, n : Nat)88  requires value : w(x) ∈ A89  shows (∀ i ∈ n, f(i) ≠ x) → matchingProductRow(A, one, mul, w, f, x, n) = one90proof91  induction n92  | zero =>93    have ordinary := IsCommRing.ring with ring94    have multiplicative := IsRing.multiplicative with ordinary95    have oneIn := IsMonoid.unit_in_carrier with multiplicative96    intro absent97    rw matchingProductRow98    rfl99  | succ(k) using ih =>100    have ordinary := IsCommRing.ring with ring101    have multiplicative := IsRing.multiplicative with ordinary102    have oneIn := IsMonoid.unit_in_carrier with multiplicative103    intro absent104    have prefix : ∀ i ∈ k, f(i) ≠ x105      intros i before106      have included := membership.into_successor at i, k with *107      exact absent with i, included108    have last := absent with k, membership.self_successor at k with *109    have previous := ih with prefix110    have entry := singleValue.other at A, one, w(x), x, f(k) with *111    rw [matchingProductRow, previous, entry]112    ring113114theorem matchingProductRow.unique (f x : Set, n : Nat)115  requires value : w(x) ∈ A116  shows DistinctValues(f, n) → Occurs(f, n, x) → matchingProductRow(A, one, mul, w, f, x, n) = w(x)117proof118  induction n119  | zero =>120    have ordinary := IsCommRing.ring with ring121    have multiplicative := IsRing.multiplicative with ordinary122    have oneIn := IsMonoid.unit_in_carrier with multiplicative123    intros distinct occurs124    rcases occurs with ⟨i, impossible, same⟩125    exfalso126    simp [nat.zero, set.empty]127  | succ(k) using ih =>128    have ordinary := IsCommRing.ring with ring129    have multiplicative := IsRing.multiplicative with ordinary130    have oneIn := IsMonoid.unit_in_carrier with multiplicative131    intros distinct occurs132    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto133    cases alternatives with last | other134    . have fresh := DistinctValues.last_fresh at f, k with *135      have absent : ∀ i ∈ k, f(i) ≠ x136        intros i before equal137        have different := fresh with i, before138        rw ← last at equal139        exact different with equal140      have previous := matchingProductRow.absent at A, add, zero, neg, mul, one, w, f, x, k with *141      have entry := singleValue.same at A, one, w(x), x, f(k) with *142      rw [matchingProductRow, previous, entry]143      ring144    . obtain ⟨position, before, equal⟩ := Occurs.forward at f, succ(k), x with occurs145      have shape := membership.successor_forward{n := k} with before146      have earlier : position ∈ k147        cases shape with inside | atLast148        . exact inside149        . exfalso150          rw atLast at equal151          exact other with equal152      have prefix := DistinctValues.prefix at f, k with *153      have occurrence : Occurs(f, k, x)154        unfold Occurs155        refine ⟨position, earlier, equal⟩156      have previous := ih with prefix, occurrence157      have entry := singleValue.other at A, one, w(x), x, f(k) with *158      rw [matchingProductRow, previous, entry]159      ring160161theorem matchingProductWeight.symmetric (x y : Set)162  requires xValue : w(x) ∈ A163  requires yValue : w(y) ∈ A164  shows singleValue(A, one, w(x), x, y) = singleValue(A, one, w(y), y, x)165proof166  have ordinary := IsCommRing.ring with ring167  have multiplicative := IsRing.multiplicative with ordinary168  have oneIn := IsMonoid.unit_in_carrier with multiplicative169  have alternatives : x = y ∨ x ≠ y by tauto170  cases alternatives with same | different171  . rw same172    rfl173  . have reverse : y ≠ x174      intro equal175      have impossible : x = y by cc176      exact different with impossible177    have left := singleValue.other at A, one, w(x), x, y with *178    have right := singleValue.other at A, one, w(y), y, x with *179    cc180181theorem matchingProductTotal.empty_left (f g : Set, m : Nat)182  shows matchingProductTotal(A, one, mul, w, f, g, (0:Nat), m) = one183proof184  induction m185  | zero =>186    rw matchingProductTotal187    rfl188  | succ(k) using ih =>189    rw [matchingProductTotal, matchingProductRow, ih]190    ring191192theorem matchingProductTotal.extend_left (f g : Set, n m : Nat)193  requires value : w(f(n)) ∈ A194  shows WeightedValues(w, g, A, m) →195    matchingProductTotal(A, one, mul, w, f, g, succ(n), m) =196    matchingProductTotal(A, one, mul, w, f, g, n, m) * matchingProductRow(A, one, mul, w, g, f(n), m)197proof198  induction m199  | zero =>200    have ordinary := IsCommRing.ring with ring201    have multiplicative := IsRing.multiplicative with ordinary202    have oneIn := IsMonoid.unit_in_carrier with multiplicative203    intro values204    simp [matchingProductTotal, matchingProductRow]205    ring206  | succ(k) using ih =>207    have ordinary := IsCommRing.ring with ring208    have multiplicative := IsRing.multiplicative with ordinary209    have oneIn := IsMonoid.unit_in_carrier with multiplicative210    intro values211    have prefix := WeightedValues.prefix at w, g, A, k with *212    have last := WeightedValues.last at w, g, A, k with *213    have previous := ih with prefix214    have symmetric := matchingProductWeight.symmetric at A, add, zero, neg, mul, one, w, g(k), f(n) with *215    have totalBound := matchingProductTotal.closed at A, add, zero, neg, mul, one, w, f, g, n, k with *216    have totalIn := totalBound with prefix217    have rowLeftIn := matchingProductRow.closed at A, add, zero, neg, mul, one, w, g, f(n), k with *218    have rowRightIn := matchingProductRow.closed at A, add, zero, neg, mul, one, w, f, g(k), n with *219    have entryIn := singleValue.closed at A, one, w(f(n)), f(n), g(k) with *220    rw [matchingProductTotal, matchingProductTotal, matchingProductRow, matchingProductRow, previous, symmetric]221    ring222223theorem matchingProductTotal.transpose (f g : Set, m n : Nat)224  requires valuesG : WeightedValues(w, g, A, m)225  shows WeightedValues(w, f, A, n) →226    matchingProductTotal(A, one, mul, w, f, g, n, m) = matchingProductTotal(A, one, mul, w, g, f, m, n)227proof228  induction n229  | zero =>230    intro valuesF231    have empty := matchingProductTotal.empty_left at A, add, zero, neg, mul, one, w, f, g, m with *232    rw [empty, matchingProductTotal]233    rfl234  | succ(k) using ih =>235    intro valuesF236    have prefix := WeightedValues.prefix at w, f, A, k with *237    have last := WeightedValues.last at w, f, A, k with *238    have previous := ih with prefix239    have extended := matchingProductTotal.extend_left at A, add, zero, neg, mul, one, w, f, g, k, m with *240    rw [extended, matchingProductTotal, previous]241    rfl242243theorem matchingProductTotal.product (f g : Set, n m : Nat)244  requires distinct : DistinctValues(f, n)245  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j))) →246    matchingProductTotal(A, one, mul, w, f, g, n, m) = indexedRingProduct(w, g, mul, one, m)247proof248  induction m249  | zero =>250    intros values covered251    simp [matchingProductTotal, indexedRingProduct]252  | succ(k) using ih =>253    intros values covered254    have prefix : ∀ j ∈ k, Occurs(f, n, g(j))255      intros j before256      have included := membership.into_successor at j, k with *257      exact covered with j, included258    have last := covered with k, membership.self_successor at k with *259    have valuePrefix := WeightedValues.prefix at w, g, A, k with *260    have valueLast := WeightedValues.last at w, g, A, k with *261    have row := matchingProductRow.unique at A, add, zero, neg, mul, one, w, f, g(k), n with *262    have previous := ih with valuePrefix, prefix263    rw [matchingProductTotal, indexedRingProduct, previous, row]264    rfl265266theorem indexedRingProduct.same_entries (f g : Set, n m : Nat)267  requires valuesF : WeightedValues(w, f, A, n)268  requires valuesG : WeightedValues(w, g, A, m)269  requires distinctF : DistinctValues(f, n)270  requires distinctG : DistinctValues(g, m)271  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i))272  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j))273  shows indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(w, g, mul, one, m)274proof275  have left := matchingProductTotal.product at A, add, zero, neg, mul, one, w, g, f, m, n with *276  have right := matchingProductTotal.product at A, add, zero, neg, mul, one, w, f, g, n, m with *277  have transpose := matchingProductTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *278  rw [← left, ← right]279  symm280  exact transpose with valuesF281282theorem indexedRingProduct.reindex (V f g : Set, n m : Nat)283  requires weights : w : V → A284  requires enumerationF : BijectiveBetween(f, n, V)285  requires enumerationG : BijectiveBetween(g, m, V)286  shows indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(w, g, mul, one, m)287proof288  have injF := Bijective.injective with enumerationF289  have injG := Bijective.injective with enumerationG290  have surjF := Bijective.surjective with enumerationF291  have surjG := Bijective.surjective with enumerationG292  have fnF := Injective.function with injF293  have fnG := Injective.function with injG294  have distinctF := Injective.distinct_values with injF295  have distinctG := Injective.distinct_values with injG296  have valuesF : WeightedValues(w, f, A, n)297    intros i hi298    have member := FunctionBetween.apply_closed with *299    exact FunctionBetween.apply_closed with *300  have valuesG : WeightedValues(w, g, A, m)301    intros j hj302    have member := FunctionBetween.apply_closed with *303    exact FunctionBetween.apply_closed with *304  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i))305    intros i hi306    have member := FunctionBetween.apply_closed with *307    exact Surjective.occurs with *308  have coveredG : ∀ j ∈ m, Occurs(f, n, g(j))309    intros j hj310    have member := FunctionBetween.apply_closed with *311    exact Surjective.occurs with *312  exact indexedRingProduct.same_entries with *313314theorem indexedRingProduct.mul (v h f : Set, n : Nat)315  shows WeightedValues(w, f, A, n) → WeightedValues(v, f, A, n) →316    (∀ i ∈ n, h(f(i)) = w(f(i)) * v(f(i))) →317    indexedRingProduct(h, f, mul, one, n) = indexedRingProduct(w, f, mul, one, n) * indexedRingProduct(v, f, mul, one, n)318proof319  induction n320  | zero =>321    intros valuesW valuesV equations322    simp [indexedRingProduct]323    ring324  | succ(k) using ih =>325    intros valuesW valuesV equations326    have prefixW := WeightedValues.prefix at w, f, A, k with *327    have prefixV := WeightedValues.prefix at v, f, A, k with *328    have lastW := WeightedValues.last at w, f, A, k with *329    have lastV := WeightedValues.last at v, f, A, k with *330    have prefix : ∀ i ∈ k, h(f(i)) = w(f(i)) * v(f(i))331      intros i hi332      have next := membership.into_successor at i, k with *333      exact equations with i, next334    have last := equations with k, membership.self_successor at k with *335    have previous := ih with prefixW, prefixV, prefix336    have closureW := indexedRingProduct.closed at A, add, zero, neg, mul, one, w, f, k with *337    have productW := closureW with prefixW338    have closureV := indexedRingProduct.closed at A, add, zero, neg, mul, one, v, f, k with *339    have productV := closureV with prefixV340    rw [indexedRingProduct, indexedRingProduct, indexedRingProduct, previous, last]341    ring342343end Rings344345defunique finiteRingProduct (V A add zero neg mul one w : Set) (product ∈ A) :=346  ∃ n, Nat(n) ∧ ∃ f, BijectiveBetween(f, n, V) ∧ product = indexedRingProduct(w, f, mul, one, n)347requires ring : IsCommRing(A, add, zero, neg, mul, one)348requires finite : Finite(V)349requires weights : w : V → A350proof351  obtain ⟨n, natural, equivalent⟩ := finite352  obtain ⟨f, bijective⟩ := equivalent353  have enumeration := converse.bijective at f, V, n with bijective354  have function := converse.function_of_bijective at f, V, n with bijective355  have values := WeightedValues.of_functions with weights, function356  have closure := indexedRingProduct.closed at A, add, zero, neg, mul, one, w, converse(f, V, n), n with *357  have productIn := closure with values358  witness indexedRingProduct(w, converse(f, V, n), mul, one, n)359  refine ⟨productIn, n, natural, converse(f, V, n), enumeration, rfl⟩360uniqueness361  intros u uIn first v vIn second362  obtain ⟨n, naturalN, f, enumerationF, valueF⟩ := first363  obtain ⟨m, naturalM, g, enumerationG, valueG⟩ := second364  have same := indexedRingProduct.reindex at A, add, zero, neg, mul, one, w, V, f, g, n, m with *365  cc366367notation scoped finiteRingProduct(V, R, w) => finiteRingProduct(V, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, w)368369theorem finiteRingProduct.closed (V A add zero neg mul one w : Set)370  requires ring : IsCommRing(A, add, zero, neg, mul, one)371  requires finite : Finite(V)372  requires weights : w : V → A373  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) ∈ A374proof375  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *376  exact selected.left377378theorem finiteRingProduct.enumeration (V A add zero neg mul one w f : Set, n : Nat)379  requires ring : IsCommRing(A, add, zero, neg, mul, one)380  requires weights : w : V → A381  requires enumeration : BijectiveBetween(f, n, V)382  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = indexedRingProduct(w, f, mul, one, n)383proof384  have reverse := converse.bijective with enumeration385  have cardinality : HasCardinality(V, n)386    unfold HasCardinality387    refine ⟨assumption, ?_⟩388    unfold Equipotent389    refine ⟨converse(f, n, V), reverse⟩390  have finite := Finite.from_cardinality with cardinality391  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *392  obtain ⟨m, naturalM, g, enumerationG, value⟩ := selected.right393  have same := indexedRingProduct.reindex at A, add, zero, neg, mul, one, w, V, g, f, m, n with *394  cc395396theorem indexedRingProduct.congr (w v f g mul one : Set, n : Nat)397  shows (∀ i ∈ n, w(f(i)) = v(g(i))) → indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(v, g, mul, one, n)398proof399  induction n400  | zero =>401    intro values402    simp [indexedRingProduct]403  | succ(k) using ih =>404    intro values405    have prefix : ∀ i ∈ k, w(f(i)) = v(g(i))406      intros i before407      have included := membership.into_successor at i, k with *408      exact values with i, included409    have last := values with k, membership.self_successor at k with *410    have previous := ih with prefix411    rw [indexedRingProduct, indexedRingProduct, previous, last]412    rfl413414theorem finiteRingProduct.congr (V A add zero neg mul one w v : Set)415  requires ring : IsCommRing(A, add, zero, neg, mul, one)416  requires finite : Finite(V)417  requires weightsW : w : V → A418  requires weightsV : v : V → A419  requires values : ∀ x ∈ V, w(x) = v(x)420  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = finiteRingProduct(V, A, add, zero, neg, mul, one, v)421proof422  have equal := FunctionBetween.ext with weightsW, weightsV, values423  rw equal424  rfl425426theorem indexedRingProduct.one (A add zero neg mul one w f : Set, n : Nat)427  requires ring : IsCommRing(A, add, zero, neg, mul, one)428  shows (∀ i ∈ n, w(f(i)) = one) → indexedRingProduct(w, f, mul, one, n) = one429proof430  induction n431  | zero =>432    intro values433    rw indexedRingProduct434    rfl435  | succ(k) using ih =>436    intro values437    have prefix : ∀ i ∈ k, w(f(i)) = one438      intros i before439      have included := membership.into_successor at i, k with *440      exact values with i, included441    have last := values with k, membership.self_successor at k with *442    have previous := ih with prefix443    rw [indexedRingProduct, previous, last]444    ring445446theorem finiteRingProduct.one (V A add zero neg mul one w : Set)447  requires ring : IsCommRing(A, add, zero, neg, mul, one)448  requires finite : Finite(V)449  requires weights : w : V → A450  requires values : ∀ x ∈ V, w(x) = one451  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) = one452proof453  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *454  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right455  have injective := Bijective.injective with enumeration456  have function := Injective.function with injective457  have unitValues : ∀ i ∈ n, w(f(i)) = one458    intros i hi459    have member := FunctionBetween.apply_closed with *460    exact values with f(i), member461  have unitProduct := indexedRingProduct.one at A, add, zero, neg, mul, one, w, f, n with *462  rw equation463  exact unitProduct with unitValues464465section Rings466variable (A add zero neg mul one w : Set)467hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)468notation ring R := (A, add, zero, neg, mul, one)469470theorem matchingProductRow.one (f x : Set, n : Nat)471  requires neutral : w(x) = one472  shows matchingProductRow(A, one, mul, w, f, x, n) = one473proof474  induction n475  | zero =>476    rw matchingProductRow477    rfl478  | succ(k) using ih =>479    have ordinary := IsCommRing.ring with ring480    have multiplicative := IsRing.multiplicative with ordinary481    have oneIn := IsMonoid.unit_in_carrier with multiplicative482    have value : w(x) ∈ A by rwa neutral483    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto484    have entry : singleValue(A, one, w(x), x, f(k)) = one485      cases alternatives with same | different486      . have selected := singleValue.same at A, one, w(x), x, f(k) with *487        cc488      . exact singleValue.other at A, one, w(x), x, f(k) with *489    rw [matchingProductRow, ih, entry]490    ring491492theorem matchingProductRow.covered_or_one (f x : Set, n : Nat)493  requires value : w(x) ∈ A494  requires distinct : DistinctValues(f, n)495  requires covered : Occurs(f, n, x) ∨ w(x) = one496  shows matchingProductRow(A, one, mul, w, f, x, n) = w(x)497proof498  cases covered with occurs | neutral499  . have unique := matchingProductRow.unique at A, add, zero, neg, mul, one, w, f, x, n with *500    exact unique with distinct, occurs501  . have empty := matchingProductRow.one at A, add, zero, neg, mul, one, w, f, x, n with *502    cc503504theorem matchingProductTotal.support_product (f g : Set, n m : Nat)505  requires distinct : DistinctValues(f, n)506  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = one) →507    matchingProductTotal(A, one, mul, w, f, g, n, m) = indexedRingProduct(w, g, mul, one, m)508proof509  induction m510  | zero =>511    intros values covered512    simp [matchingProductTotal, indexedRingProduct]513  | succ(k) using ih =>514    intros values covered515    have prefix : ∀ j ∈ k, Occurs(f, n, g(j)) ∨ w(g(j)) = one516      intros j before517      have included := membership.into_successor at j, k with *518      exact covered with j, included519    have last := covered with k, membership.self_successor at k with *520    have valuePrefix := WeightedValues.prefix at w, g, A, k with *521    have valueLast := WeightedValues.last at w, g, A, k with *522    have row := matchingProductRow.covered_or_one at A, add, zero, neg, mul, one, w, f, g(k), n with *523    have previous := ih with valuePrefix, prefix524    rw [matchingProductTotal, indexedRingProduct, previous, row]525    rfl526527theorem indexedRingProduct.same_nonunit_entries (f g : Set, n m : Nat)528  requires valuesF : WeightedValues(w, f, A, n)529  requires valuesG : WeightedValues(w, g, A, m)530  requires distinctF : DistinctValues(f, n)531  requires distinctG : DistinctValues(g, m)532  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = one533  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = one534  shows indexedRingProduct(w, f, mul, one, n) = indexedRingProduct(w, g, mul, one, m)535proof536  have left := matchingProductTotal.support_product at A, add, zero, neg, mul, one, w, g, f, m, n with *, valuesF, coveredF537  have right := matchingProductTotal.support_product at A, add, zero, neg, mul, one, w, f, g, n, m with *, valuesG, coveredG538  have transpose := matchingProductTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *539  rw [← left, ← right]540  symm541  exact transpose with valuesF542543end Rings544545theorem finiteRingProduct.restrict (V S A add zero neg mul one w : Set)546  requires ring : IsCommRing(A, add, zero, neg, mul, one)547  requires finite : Finite(V)548  requires weights : w : V → A549  requires subset : S ⊆ V550  requires neutral : ∀ x ∈ V, ¬(x ∈ S) → w(x) = one551  shows finiteRingProduct(V, A, add, zero, neg, mul, one, w) =552    finiteRingProduct(S, A, add, zero, neg, mul, one, restrict(w, S))553proof554  have finiteS := Finite.subset with finite, subset555  have closed : ∀ x ∈ S, w(x) ∈ A556    intros x hx557    have included := subset558    have member := included with x, hx559    exact FunctionBetween.apply_closed with *560  have restricted := restrict.function with *561  have selectedV := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, w with *562  have selectedS := finiteRingProduct.selected at S, A, add, zero, neg, mul, one, restrict(w, S) with *563  obtain ⟨n, naturalN, f, enumerationF, equationV⟩ := selectedV.right564  obtain ⟨m, naturalM, g, enumerationG, equationS⟩ := selectedS.right565  have injF := Bijective.injective with enumerationF566  have injG := Bijective.injective with enumerationG567  have surjF := Bijective.surjective with enumerationF568  have surjG := Bijective.surjective with enumerationG569  have functionF := Injective.function with injF570  have functionG := Injective.function with injG571  have distinctF := Injective.distinct_values with injF572  have distinctG := Injective.distinct_values with injG573  have valuesF := WeightedValues.of_functions with weights, functionF574  have valuesG : WeightedValues(w, g, A, m)575    intros i hi576    have member := FunctionBetween.apply_closed with *577    exact closed with g(i), member578  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = one579    intros i hi580    have member := FunctionBetween.apply_closed with *581    have alternatives : f(i) ∈ S ∨ ¬(f(i) ∈ S) by tauto582    cases alternatives with inside | outside583    . left584      exact Surjective.occurs with *585    . right586      exact neutral with f(i), member, outside587  have coveredG : ∀ i ∈ m, Occurs(f, n, g(i)) ∨ w(g(i)) = one588    intros i hi589    have inS := FunctionBetween.apply_closed with *590    have included := subset591    have inV := included with g(i), inS592    left593    exact Surjective.occurs with *594  have same := indexedRingProduct.same_nonunit_entries with valuesF, valuesG, distinctF, distinctG, coveredF, coveredG595  have pointwise : ∀ i ∈ m, w(g(i)) = restrict(w, S)(g(i))596    intros i hi597    have inS := FunctionBetween.apply_closed with *598    symm599    exact restrict.apply with *600  have congr := indexedRingProduct.congr at w, restrict(w, S), g, g, mul, one, m with naturalM601  have equal := congr with pointwise602  cc603604theorem finiteRingProduct.reindex (D E A add zero neg mul one w v f : Set)605  requires ring : IsCommRing(A, add, zero, neg, mul, one)606  requires finite : Finite(D)607  requires weightsW : w : D → A608  requires weightsV : v : E → A609  requires bijective : BijectiveBetween(f, D, E)610  requires values : ∀ d ∈ D, w(d) = v(f(d))611  shows finiteRingProduct(D, A, add, zero, neg, mul, one, w) = finiteRingProduct(E, A, add, zero, neg, mul, one, v)612proof613  have selected := finiteRingProduct.selected at D, A, add, zero, neg, mul, one, w with *614  obtain ⟨n, natural, g, enumeration, equation⟩ := selected.right615  have composed := compose.bijective at f, g, n, D, E with *616  have injF := Bijective.injective with bijective617  have injG := Bijective.injective with enumeration618  have functionF := Injective.function with injF619  have functionG := Injective.function with injG620  have equationV := finiteRingProduct.enumeration at E, A, add, zero, neg, mul, one, v, compose(f, g, n, D, E), n with *621  have pointwise : ∀ i ∈ n, w(g(i)) = v(compose(f, g, n, D, E)(i))622    intros i hi623    have member := FunctionBetween.apply_closed at g, n, D, i with *624    have value := values with g(i), member625    have composite := compose.apply at f, g, n, D, E, i with *626    cc627  have congr := indexedRingProduct.congr at w, v, g, compose(f, g, n, D, E), mul, one, n with natural628  have same := congr with pointwise629  cc630631-- The smaller-domain weights may be represented by any agreeing graph.632theorem finiteRingProduct.unit_extension (D S A add zero neg mul one w v : Set)633  requires ring : IsCommRing(A, add, zero, neg, mul, one)634  requires finite : Finite(D)635  requires weightsW : w : D → A636  requires weightsV : v : S → A637  requires subset : S ⊆ D638  requires agreement : ∀ s ∈ S, w(s) = v(s)639  requires neutral : ∀ d ∈ D, ¬(d ∈ S) → w(d) = one640  shows finiteRingProduct(D, A, add, zero, neg, mul, one, w) = finiteRingProduct(S, A, add, zero, neg, mul, one, v)641proof642  have closed : ∀ s ∈ S, w(s) ∈ A643    intros s hs644    have value := FunctionBetween.apply_closed with *645    have equal := agreement with s, hs646    rwa equal647  have restricted := restrict.function with *648  have same : restrict(w, S) = v649    apply FunctionBetween.ext with restricted, weightsV650    intros s hs651    have value := restrict.apply with *652    have equal := agreement with s, hs653    cc654  have product := finiteRingProduct.restrict with *655  rwa same at product656657658theorem finiteRingProduct.empty (A add zero neg mul one w : Set)659  requires ring : IsCommRing(A, add, zero, neg, mul, one)660  requires weights : w : ∅ → A661  shows finiteRingProduct(∅, A, add, zero, neg, mul, one, w) = one662proof663  have finite := Finite.empty664  have values : ∀ x ∈ ∅, w(x) = one665    intros x impossible666    exfalso667    exact set.empty with impossible668  exact finiteRingProduct.one with ring, finite, weights, values669670theorem finiteRingProduct.insert (V A add zero neg mul one w a : Set)671  requires ring : IsCommRing(A, add, zero, neg, mul, one)672  requires finite : Finite(V)673  requires weights : w : insert(a, V) → A674  requires fresh : ¬(a ∈ V)675  shows finiteRingProduct(insert(a, V), A, add, zero, neg, mul, one, w) =676    call2(mul, finiteRingProduct(V, A, add, zero, neg, mul, one, restrict(w, V)), w(a))677proof678  have subset : V ⊆ insert(a, V)679    intros x hx680    exact insert.contains with hx681  have closed : ∀ x ∈ V, w(x) ∈ A682    intros x hx683    have member := insert.contains at x, a, V with hx684    exact FunctionBetween.apply_closed at w, insert(a, V), A, x with *685  have restricted := restrict.function at w, insert(a, V), A, V, A with *686  have selected := finiteRingProduct.selected at V, A, add, zero, neg, mul, one, restrict(w, V) with *687  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right688  have injective := Bijective.injective with enumeration689  have function := Injective.function with injective690  have nFresh := membership.irreflexive at n691  have extended := adjoinMap.bijective with enumeration, nFresh, fresh692  have successor := natural.successor_as_insert with natural693  rw ← successor at extended694  have extendedInjective := Bijective.injective with extended695  have extendedFunction := Injective.function with extendedInjective696  have extendedProduct := finiteRingProduct.enumeration at insert(a, V), A, add, zero, neg, mul, one, w, adjoinMap(f, n, a), succ(n) with *697  have oldValues : ∀ i ∈ n, w(adjoinMap(f, n, a)(i)) = restrict(w, V)(f(i))698    intros i hi699    have oldMember := FunctionBetween.apply_closed at f, n, V, i with *700    have oldEdge := FunctionBetween.relates_apply at f, n, V, i with *701    have edge := adjoinMap.relates_old at f, n, a, i, f(i) with oldEdge702    have next := membership.into_successor at i, n with *703    have value := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), i, f(i) with *704    have restrictedValue := restrict.apply at w, insert(a, V), A, V, A, f(i) with *705    cc706  have congr := indexedRingProduct.congr at w, restrict(w, V), adjoinMap(f, n, a), f, mul, one, n with natural707  have prefix := congr with oldValues708  have newIndex := membership.self_successor with natural709  have newEdge := adjoinMap.relates_new at f, n, a710  have newValue := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), n, a with *711  rw [extendedProduct, indexedRingProduct, prefix, newValue, equation]712  rfl713714theorem finiteRingProduct.singleton (A add zero neg mul one w x : Set)715  requires ring : IsCommRing(A, add, zero, neg, mul, one)716  requires weights : w : {x} → A717  shows finiteRingProduct({x}, A, add, zero, neg, mul, one, w) = w(x)718proof719  have same : insert(x, ∅) = {x}720    ext y721    simp722  have empty := Finite.empty723  have fresh : ¬(x ∈ ∅) by exact set.empty at x724  have extended : w : insert(x, ∅) → A by rwa same725  have subset : ∅ ⊆ insert(x, ∅) by simp [Subset, set.empty]726  have closed : ∀ y ∈ ∅, w(y) ∈ A727    intros y hy728    exfalso729    exact set.empty with hy730  have restricted := restrict.function with *731  have emptyProduct := finiteRingProduct.empty with *732  have inserted := finiteRingProduct.insert with *733  have member : x ∈ {x} by simp [singleton.membership]734  have value := FunctionBetween.apply_closed with *735  rw same at inserted736  rw [inserted, emptyProduct]737  ring738739theorem finiteRingProduct.mul (D A add zero neg mul one w v h : Set)740  requires ring : IsCommRing(A, add, zero, neg, mul, one)741  requires finite : Finite(D)742  requires weightsW : w : D → A743  requires weightsV : v : D → A744  requires weightsH : h : D → A745  requires equations : ∀ x ∈ D, h(x) = call2(mul, w(x), v(x))746  shows finiteRingProduct(D, A, add, zero, neg, mul, one, h) = call2(mul, finiteRingProduct(D, A, add, zero, neg, mul, one, w), finiteRingProduct(D, A, add, zero, neg, mul, one, v))747proof748  have selected := finiteRingProduct.selected at D, A, add, zero, neg, mul, one, w with *749  obtain ⟨n, natural, f, enumeration, valueW⟩ := selected.right750  have injective := Bijective.injective with enumeration751  have function := Injective.function with injective752  have valuesW := WeightedValues.of_functions with weightsW, function753  have valuesV := WeightedValues.of_functions with weightsV, function754  have valueV := finiteRingProduct.enumeration at D, A, add, zero, neg, mul, one, v, f, n with *755  have valueH := finiteRingProduct.enumeration at D, A, add, zero, neg, mul, one, h, f, n with *756  have pointwise : ∀ i ∈ n, h(f(i)) = call2(mul, w(f(i)), v(f(i)))757    intros i hi758    have member := FunctionBetween.apply_closed with *759    exact equations with f(i), member760  have multiply := indexedRingProduct.mul with *, valuesW, valuesV, pointwise761  cc762