Grace/Cumulus/Algebra/Ring/SubringCore.g17

Open in Workbench Download source

Imports

Restriction · HomomorphismCore

Declarations

Source

1-- Unital subrings over separate pieces, with the operations restricted to2-- their domains: the engine under Subring3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Ring.SubringCore9import Restriction10import HomomorphismCore1112-- IsSubring(A, add, zero, neg, mul, one, S) is the subring over separate13-- pieces; the bundled Subring(R, S) is defined in Subring and bridged to14-- this form.15predicate IsSubring (A add zero neg mul one S : Set) :=16  S ⊆ A ∧ zero ∈ S ∧ one ∈ S ∧ ClosedUnary(S, neg) ∧17    ClosedBinary(S, add) ∧ ClosedBinary(S, mul)1819notation scoped IsSubring(R, S) => IsSubring(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, S)2021theorem IsSubring.subset_carrier (A add zero neg mul one S : Set)22  requires subring : IsSubring(A, add, zero, neg, mul, one, S)23  shows S ⊆ A24proof25  simp [IsSubring]2627theorem IsSubring.zero_closed (A add zero neg mul one S : Set)28  requires subring : IsSubring(A, add, zero, neg, mul, one, S)29  shows zero ∈ S30proof31  simp [IsSubring]3233theorem IsSubring.one_closed (A add zero neg mul one S : Set)34  requires subring : IsSubring(A, add, zero, neg, mul, one, S)35  shows one ∈ S36proof37  simp [IsSubring]3839theorem IsSubring.neg_closed (A add zero neg mul one S : Set)40  requires subring : IsSubring(A, add, zero, neg, mul, one, S)41  shows ClosedUnary(S, neg)42proof43  simp [IsSubring]4445theorem IsSubring.add_closed (A add zero neg mul one S : Set)46  requires subring : IsSubring(A, add, zero, neg, mul, one, S)47  shows ClosedBinary(S, add)48proof49  simp [IsSubring]5051theorem IsSubring.mul_closed (A add zero neg mul one S : Set)52  requires subring : IsSubring(A, add, zero, neg, mul, one, S)53  shows ClosedBinary(S, mul)54proof55  simp [IsSubring]5657theorem IsSubring.comm_ring (A add zero neg mul one S : Set)58  requires ring : IsCommRing(A, add, zero, neg, mul, one)59  requires subring : IsSubring(A, add, zero, neg, mul, one, S)60  shows IsCommRing(S, restrict(add, S × S), zero, restrict(neg, S), restrict(mul, S × S), one)61proof62  have subset := IsSubring.subset_carrier with subring63  have zeroIn := IsSubring.zero_closed with subring64  have oneIn := IsSubring.one_closed with subring65  have addClosed := IsSubring.add_closed with subring66  have mulClosed := IsSubring.mul_closed with subring67  have negClosed := IsSubring.neg_closed with subring68  have addition : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]69  have multiplication : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]70  have addAssoc : Associative(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]71  have mulAssoc : Associative(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]72  have addComm : Commutative(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]73  have mulComm : Commutative(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]74  have addUnit : Identity(A, add, zero) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]75  have mulUnit : Identity(A, mul, one) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]76  have inverse : Inverse(A, add, zero, neg) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]77  have distribute : Distributive(A, add, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]78  have negation : neg : A → A by simp [Inverse]79  have addFunction := restrictBinary.function at A, S, add with *80  have mulFunction := restrictBinary.function at A, S, mul with *81  have restrictedAdd : IsMagma(S, restrict(add, S × S)) by exact addFunction82  have restrictedMul : IsMagma(S, restrict(mul, S × S)) by exact mulFunction83  have rAddAssoc := restrictBinary.associative at A, S, add with *84  have rMulAssoc := restrictBinary.associative at A, S, mul with *85  have rAddComm := restrictBinary.commutative at A, S, add with *86  have rMulComm := restrictBinary.commutative at A, S, mul with *87  have rAddUnit := restrictBinary.identity at A, S, add, zero with *88  have rMulUnit := restrictBinary.identity at A, S, mul, one with *89  have rInverse := restrictUnary.inverse with *90  have rDistribute := restrictBinary.distributive with *91  simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]9293theorem IsSubring.inclusion_function (A add zero neg mul one S : Set)94  requires subring : IsSubring(A, add, zero, neg, mul, one, S)95  shows identity(S) : S → A96proof97  have function := identity.function at S98  have subset := IsSubring.subset_carrier with subring99  apply FunctionBetween.codomain_of_values with function100  intros x hx101  have value := identity.apply with hx102  rw value103  exact subset with x, hx104105theorem IsSubring.inclusion_hom (A add zero neg mul one S : Set)106  requires ring : IsCommRing(A, add, zero, neg, mul, one)107  requires subring : IsSubring(A, add, zero, neg, mul, one, S)108  shows IsRingHom(identity(S), S, restrict(add, S × S), zero, restrict(neg, S), restrict(mul, S × S), one, A, add, zero, neg, mul, one)109proof110  have smaller := IsSubring.comm_ring with ring, subring111  have function := IsSubring.inclusion_function with subring112  have subset := IsSubring.subset_carrier with subring113  have addClosed := IsSubring.add_closed with subring114  have mulClosed := IsSubring.mul_closed with subring115  have addition : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]116  have multiplication : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsMonoid, IsSemigroup]117  apply IsRingHom.of_add_mul_one with smaller, ring, function118  . intros x hx y hy119    have closed := ClosedBinary.mem at S, add, x, y with *120    have restricted := restrictBinary.value at A, S, add, x, y with *121    have vx := identity.apply with hx122    have vy := identity.apply with hy123    have output := identity.apply at call2(add, x, y), S with *124    cc125  . intros x hx y hy126    have closed := ClosedBinary.mem at S, mul, x, y with *127    have restricted := restrictBinary.value at A, S, mul, x, y with *128    have vx := identity.apply with hx129    have vy := identity.apply with hy130    have output := identity.apply at call2(mul, x, y), S with *131    cc132  . have oneIn := IsSubring.one_closed with subring133    exact identity.apply with oneIn134135theorem IsSubring.inclusion_injective (A add zero neg mul one S : Set)136  requires subring : IsSubring(A, add, zero, neg, mul, one, S)137  shows InjectiveBetween(identity(S), S, A)138proof139  have function := IsSubring.inclusion_function with subring140  unfold InjectiveBetween141  refine ⟨function, ?_⟩142  intros x hx y hy z hz left right143  have vx := identity.apply at x, S with *144  have vy := identity.apply at y, S with *145  have ex := FunctionBetween.apply_value at identity(S), S, A, x, z with *146  have ey := FunctionBetween.apply_value at identity(S), S, A, y, z with *147  cc148