Grace/Cumulus/Algebra/Ring/Subring.g17

Open in Workbench Download source

Imports

SubringCore · Homomorphism

Declarations

Source

1-- Subrings of a bundled ring: Subring(R, S) under a ring hypothesis, the2-- bridges to the form over separate pieces, the closure instances, the3-- ring on a subring, and its inclusion homomorphism; everything here is ZF4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Ring.Subring10import SubringCore11import Homomorphism1213-- Under a hypothesis Ring(R), a subring is a subset containing zero and14-- one and closed under negation, addition, and multiplication. IsSubring(A,15-- add, zero, neg, mul, one, S) remains the form over separate pieces,16-- bridged below.17section Definitions18variable (R : Set)19hypothesis ring : Ring(R)2021predicate Subring (S : Set) :=22  S ⊆ R ∧ R[0] ∈ S ∧ R[1] ∈ S ∧ (∀ x ∈ S, -x ∈ S) ∧23  (∀ x y ∈ S, x + y ∈ S) ∧ (∀ x y ∈ S, x * y ∈ S)2425end Definitions2627notation infixl 60 "+" => call2(R.add, _, _) via hypothesis Subring(R, S) for S28notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis Subring(R, S) for S29notation prefix 75 "-" => apply(R.neg, _) via hypothesis Subring(R, S) for S30notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis Subring(R, S) for S3132instance Subring.parts (R S : Set)33  requires subring : Subring(R, S)34  shows IsSubring(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S)35proof36  obtain ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩ := subring37  unfold IsSubring38  refine ⟨bounded, zeroIn, oneIn, ?_, ?_, ?_⟩39  . unfold ClosedUnary40    exact negatives41  . unfold ClosedBinary42    exact sums43  . unfold ClosedBinary44    exact products4546theorem Subring.of_projections (R S : Set)47  requires subring : IsSubring(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S)48  shows Subring(R, S)49proof50  obtain ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩ := subring51  unfold ClosedUnary at negatives52  unfold ClosedBinary at sums53  unfold ClosedBinary at products54  unfold Subring.Subring55  exact ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩5657theorem Subring.of_parts (A add zero neg mul one S : Set)58  requires subring : IsSubring(A, add, zero, neg, mul, one, S)59  shows Subring(Ring.mk(A, add, zero, neg, mul, one), S)60proof61  have shifted : IsSubring(Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),62      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),63      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),64      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),65      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)),66      Ring.one(Ring.mk(A, add, zero, neg, mul, one)), S)67    ring_projections68  exact Subring.of_projections with shifted6970section SubringLaws71variable (R S : Set)72hypothesis subring : Subring(R, S)7374theorem Subring.subset75  shows S ⊆ R.carrier76proof77  obtain ⟨bounded, rest⟩ := subring78  exact bounded7980-- Closure: the carrier membership of an element is a typing rule, and the81-- memberships of the constants and of compound terms are instances.82theorem Subring.mem_carrier (x : S)83  shows x ∈ R.carrier84proof85  have bounded := Subring.subset with subring86  have xIn : x ∈ S by assumption87  exact bounded with x, xIn8889instance Subring.zero_mem90  shows R[0] ∈ S91proof92  obtain ⟨bounded, zeroIn, rest⟩ := subring93  exact zeroIn9495instance Subring.one_mem96  shows R[1] ∈ S97proof98  obtain ⟨bounded, zeroIn, oneIn, rest⟩ := subring99  exact oneIn100101instance Subring.neg_mem (x : S)102  shows -x ∈ S103proof104  obtain ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩ := subring105  have xIn : x ∈ S by assumption106  exact negatives with x, xIn107108instance Subring.add_mem (x y : S)109  shows x + y ∈ S110proof111  obtain ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩ := subring112  have xIn : x ∈ S by assumption113  have yIn : y ∈ S by assumption114  exact sums with x, xIn, y, yIn115116instance Subring.mul_mem (x y : S)117  shows x * y ∈ S118proof119  obtain ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩ := subring120  have xIn : x ∈ S by assumption121  have yIn : y ∈ S by assumption122  exact products with x, xIn, y, yIn123124end SubringLaws125126section SubringSubtraction127variable (R S : Set)128hypothesis ring : Ring(R)129hypothesis subring : Subring(R, S)130131instance Subring.sub_mem (x y : S)132  shows x - y ∈ S133proof134  have xIn : x ∈ R := Subring.mem_carrier with *135  have yIn : y ∈ R := Subring.mem_carrier with *136  have negIn : -y ∈ S := Subring.neg_mem with *137  rw Ring.sub.value138  exact Subring.add_mem with *139140end SubringSubtraction141142section SubringConstructions143variable (R : Set)144hypothesis ring : Ring(R)145146-- The constructor, and the whole ring as a subring of itself.147theorem Subring.mk (S : Set)148  requires bounded : S ⊆ R149  requires zeroIn : R[0] ∈ S150  requires oneIn : R[1] ∈ S151  requires negatives : ∀ x ∈ S, -x ∈ S152  requires sums : ∀ x y ∈ S, x + y ∈ S153  requires products : ∀ x y ∈ S, x * y ∈ S154  shows Subring(R, S)155proof156  unfold Subring.Subring157  exact ⟨bounded, zeroIn, oneIn, negatives, sums, products⟩158159theorem Subring.whole160  shows Subring(R, R.carrier)161proof162  have reflexive := Subset.reflexive at R.carrier163  have zeroIn : R[0] ∈ R := Ring.zero_mem with *164  have oneIn : R[1] ∈ R := Ring.one_mem with *165  apply Subring.mk with ring, reflexive, zeroIn, oneIn166  . intros x hx167    exact Ring.neg_mem with *168  . intros x hx y hy169    exact Ring.add_mem with *170  . intros x hx y hy171    exact Ring.mul_mem with *172173end SubringConstructions174175-- The ring on a subring: the operations of R restricted to S, with the176-- same zero and one.177def subringRing (R S : Set) : Set :=178  Ring.mk(S, restrict(R.add, S × S), R.zero, restrict(R.neg, S),179    restrict(R.mul, S × S), R.one)180181theorem subringRing.carrierOf (R S : Set)182  shows Ring.carrier(subringRing(R, S)) = S183proof184  simp [subringRing, Ring.mk.carrier]185186section SubringRings187variable (R S : Set)188hypothesis comm : CommRing(R)189hypothesis subring : Subring(R, S)190191theorem subringRing.comm_ring192  shows CommRing(subringRing(R, S))193proof194  have parts := CommRing.parts with comm195  have subParts := Subring.parts with subring196  have engine := IsSubring.comm_ring with parts, subParts197  unfold subringRing198  exact CommRing.of_parts with engine199200-- The inclusion is an injective homomorphism.201theorem Subring.inclusion202  shows identity(S) : subringRing(R, S) →+* R203proof204  have parts := CommRing.parts with comm205  have subParts := Subring.parts with subring206  have engine := IsSubring.inclusion_hom with parts, subParts207  have smaller := subringRing.comm_ring with comm, subring208  have shifted : IsRingHom(identity(S), Ring.carrier(subringRing(R, S)),209      Ring.add(subringRing(R, S)), Ring.zero(subringRing(R, S)),210      Ring.neg(subringRing(R, S)), Ring.mul(subringRing(R, S)),211      Ring.one(subringRing(R, S)), R.carrier, R.add, R.zero, R.neg, R.mul,212      R.one)213    unfold subringRing214    ring_projections215  exact RingHom.of_projections with (CommRing.to_ring with smaller),216    (CommRing.to_ring with comm), shifted217218end SubringRings219