Grace/Cumulus/Algebra/Ring/GeneratedSubring.g17

Open in Workbench Download source

Imports

Subring

Declarations

Source

1-- Generated subrings and their closure principles (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.GeneratedSubring8import Subring910def generatedSubring (A add zero neg mul one G : Set) : Set :=11  {x ∈ A | ∀ S, IsSubring(A, add, zero, neg, mul, one, S) → G ⊆ S → x ∈ S}1213notation scoped generatedSubring(R, G) => generatedSubring(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, G)1415section Generation16variable (A add zero neg mul one : Set)17notation ring R := (A, add, zero, neg, mul, one)18hypothesis ring : IsCommRing(R)1920theorem generatedSubring.mem_iff (G x : Set)21  shows x ∈ generatedSubring(A, add, zero, neg, mul, one, G) ↔ x ∈ R ∧ (∀ S, IsSubring(R, S) → G ⊆ S → x ∈ S)22proof23  simp2425theorem generatedSubring.subset (G : Set)26  shows generatedSubring(A, add, zero, neg, mul, one, G) ⊆ R27proof28  simp2930theorem generatedSubring.contains (G : Set)31  requires bounded : G ⊆ R32  shows G ⊆ generatedSubring(A, add, zero, neg, mul, one, G)33proof34  intros x hx35  apply generatedSubring.mem_iff.backward with ring36  constructor37  . exact bounded with x, hx38  . intros S subring included39    exact included with x, hx4041theorem generatedSubring.least (G S : Set)42  requires subring : IsSubring(R, S)43  requires included : G ⊆ S44  shows generatedSubring(A, add, zero, neg, mul, one, G) ⊆ S45proof46  intros x hx47  have data := generatedSubring.mem_iff.forward with *48  exact data.right with S, subring, included4950theorem generatedSubring.subring (G : Set)51  shows IsSubring(R, generatedSubring(A, add, zero, neg, mul, one, G))52proof53  have ordinary := IsCommRing.ring with ring54  have multiplicative := IsRing.multiplicative with ordinary55  have zeroIn := IsRing.zero_in_carrier with ordinary56  have oneIn := IsMonoid.unit_in_carrier with multiplicative57  have bounded := generatedSubring.subset at A, add, zero, neg, mul, one, G with *58  have zeroMember : zero ∈ generatedSubring(A, add, zero, neg, mul, one, G)59    apply generatedSubring.mem_iff.backward with ring60    refine ⟨zeroIn, ?_⟩61    intros S subring included62    exact IsSubring.zero_closed with subring63  have oneMember : one ∈ generatedSubring(A, add, zero, neg, mul, one, G)64    apply generatedSubring.mem_iff.backward with ring65    refine ⟨oneIn, ?_⟩66    intros S subring included67    exact IsSubring.one_closed with subring68  have negative : ClosedUnary(generatedSubring(A, add, zero, neg, mul, one, G), neg)69    intros x hx70    have data := generatedSubring.mem_iff.forward with hx71    have closed := IsRing.neg_closed with ordinary, data.left72    apply generatedSubring.mem_iff.backward with ring73    refine ⟨closed, ?_⟩74    intros S subring included75    have member := data.right with S, subring, included76    have closure := IsSubring.neg_closed with subring77    exact ClosedUnary.mem with closure, member78  have addition : ClosedBinary(generatedSubring(A, add, zero, neg, mul, one, G), add)79    intros x hx y hy80    have first := generatedSubring.mem_iff.forward with hx81    have second := generatedSubring.mem_iff.forward with hy82    have closed := IsRing.add_closed with ordinary, first.left, second.left83    apply generatedSubring.mem_iff.backward with ring84    refine ⟨closed, ?_⟩85    intros S subring included86    have xIn := first.right with S, subring, included87    have yIn := second.right with S, subring, included88    have closure := IsSubring.add_closed with subring89    exact ClosedBinary.mem with closure, xIn, yIn90  have multiplication : ClosedBinary(generatedSubring(A, add, zero, neg, mul, one, G), mul)91    intros x hx y hy92    have first := generatedSubring.mem_iff.forward with hx93    have second := generatedSubring.mem_iff.forward with hy94    have closed := IsRing.mul_closed with ordinary, first.left, second.left95    apply generatedSubring.mem_iff.backward with ring96    refine ⟨closed, ?_⟩97    intros S subring included98    have xIn := first.right with S, subring, included99    have yIn := second.right with S, subring, included100    have closure := IsSubring.mul_closed with subring101    exact ClosedBinary.mem with closure, xIn, yIn102  unfold IsSubring103  refine ⟨bounded, zeroMember, oneMember, negative, addition, multiplication⟩104105theorem generatedSubring.mono (G H : Set)106  requires included : G ⊆ H107  shows generatedSubring(A, add, zero, neg, mul, one, G) ⊆ generatedSubring(A, add, zero, neg, mul, one, H)108proof109  intros x hx110  have data := generatedSubring.mem_iff.forward with *111  apply generatedSubring.mem_iff.backward with ring112  refine ⟨data.left, ?_⟩113  intros S subring containsH114  have containsG : G ⊆ S115    intros y hy116    have inH := included with y, hy117    exact containsH with y, inH118  exact data.right with S, subring, containsG119120theorem generatedSubring.eq_of_subring (S : Set)121  requires subring : IsSubring(R, S)122  shows generatedSubring(A, add, zero, neg, mul, one, S) = S123proof124  have bounded := IsSubring.subset_carrier with subring125  have includes := generatedSubring.contains with *126  have reflexive : S ⊆ S by simp [Subset]127  have least := generatedSubring.least with *128  exact Subset.antisymmetric with least, includes129130theorem generatedSubring.idempotent (G : Set)131  shows generatedSubring(A, add, zero, neg, mul, one, generatedSubring(A, add, zero, neg, mul, one, G)) = generatedSubring(A, add, zero, neg, mul, one, G)132proof133  have subring := generatedSubring.subring at A, add, zero, neg, mul, one, G with *134  exact generatedSubring.eq_of_subring with *135136end Generation137