Subrings

Let R be a ring. This file defines the "bundled" subring type Subring R, a type whose terms correspond to subrings of R. This is the preferred way to talk about subrings in mathlib. Unbundled subrings (s : Set R and IsSubring s) are not in this file, and they will ultimately be deprecated.

We prove that subrings are a complete lattice, and that you can map (pushforward) and comap (pull back) them along ring homomorphisms.

We define the closure construction from Set R to Subring R, sending a subset of R to the subring it generates, and prove that it is a Galois insertion.

Main definitions

Notation used here:

(R : Type u) [Ring R] (S : Type u) [Ring S] (f g : R →+* S) (A : Subring R) (B : Subring S) (s : Set R)

• Subring R : the type of subrings of a ring R.

• instance : CompleteLattice (Subring R) : the complete lattice structure on the subrings.

• Subring.center : the center of a ring R.

• Subring.closure : subring closure of a set, i.e., the smallest subring that includes the set.

• Subring.gi : closure : Set M → Subring M and coercion (↑) : Subring M → et M form a GaloisInsertion.

• comap f B : Subring A : the preimage of a subring B along the ring homomorphism f

• map f A : Subring B : the image of a subring A along the ring homomorphism f.

• prod A B : Subring (R × S) : the product of subrings

• f.range : Subring B : the range of the ring homomorphism f.

• eqLocus f g : Subring R : given ring homomorphisms f g : R →+* S, the subring of R where f x = g x

Implementation notes

A subring is implemented as a subsemiring which is also an additive subgroup. The initial PR was as a submonoid which is also an additive subgroup.

Lattice inclusion (e.g. ≤ and ⊓) is used rather than set notation (⊆ and ∩), although ∈ is defined as membership of a subring's underlying set.

Tags

subring, subrings

class SubringClass (S : Type u_1) (R : outParam (Type u)) [Ring R] [SetLike S R] extends SubsemiringClass S R, NegMemClass S R : Prop

SubringClass S R states that S is a type of subsets s ⊆ R that are both a multiplicative submonoid and an additive subgroup.

• mul_mem {s : S} {a b : R} : a ∈ s → b ∈ s → a * b ∈ s
• one_mem (s : S) : 1 ∈ s
• add_mem {s : S} {a b : R} : a ∈ s → b ∈ s → a + b ∈ s
• zero_mem (s : S) : 0 ∈ s
• neg_mem {s : S} {x : R} : x ∈ s → -x ∈ s

@[instance 100]

instance SubringClass.addSubgroupClass (S : Type u_1) (R : Type u) [SetLike S R] [Ring R] [h : SubringClass S R] : AddSubgroupClass S R

@[instance 100]

instance SubringClass.nonUnitalSubringClass (S : Type u_1) (R : Type u) [SetLike S R] [Ring R] [SubringClass S R] : NonUnitalSubringClass S R

@[simp]

theorem intCast_mem {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ) : ↑n ∈ s

@[instance 75]

instance SubringClass.toHasIntCast {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) : IntCast ↥s

Equations

• SubringClass.toHasIntCast s = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }

@[instance 75]

instance SubringClass.toRing {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) : Ring ↥s

A subring of a ring inherits a ring structure

Equations

• One or more equations did not get rendered due to their size.

@[instance 75]

instance SubringClass.toCommRing {S : Type v} (s : S) {R : Type u_1} [CommRing R] [SetLike S R] [SubringClass S R] : CommRing ↥s

A subring of a CommRing is a CommRing.

Equations

• SubringClass.toCommRing s = { toRing := SubringClass.toRing s, mul_comm := ⋯ }

@[instance 75]

instance SubringClass.instIsDomainSubtypeMem {S : Type v} (s : S) {R : Type u_1} [Ring R] [IsDomain R] [SetLike S R] [SubringClass S R] : IsDomain ↥s

A subring of a domain is a domain.

def SubringClass.subtype {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) : ↥s →+* R

The natural ring hom from a subring of ring R to R.

Equations

• SubringClass.subtype s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SubringClass.subtype_apply {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] {s : S} (x : ↥s) : (subtype s) x = ↑x

theorem SubringClass.subtype_injective {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) : Function.Injective ⇑(subtype s)

@[simp]

theorem SubringClass.coe_subtype {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) : ⇑(subtype s) = Subtype.val

@[simp]

theorem SubringClass.coe_natCast {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem SubringClass.coe_intCast {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ) : ↑↑n = ↑n

structure Subring (R : Type u) [Ring R] extends Subsemiring R, AddSubgroup R : Type u

Subring R is the type of subrings of R. A subring of R is a subset s that is a multiplicative submonoid and an additive subgroup. Note in particular that it shares the same 0 and 1 as R.

• carrier : Set R
• mul_mem' {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• neg_mem' {x : R} : x ∈ self.carrier → -x ∈ self.carrier

instance Subring.instSetLike {R : Type u} [Ring R] : SetLike (Subring R) R

Equations

• Subring.instSetLike = { coe := fun (s : Subring R) => s.carrier, coe_injective' := ⋯ }

def Subring.ofClass {S : Type u_1} {R : Type u_2} [Ring R] [SetLike S R] [SubringClass S R] (s : S) : Subring R

The actual Subring obtained from an element of a SubringClass.

Equations

• Subring.ofClass s = { carrier := ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subring.coe_ofClass {S : Type u_1} {R : Type u_2} [Ring R] [SetLike S R] [SubringClass S R] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg {R : Type u} [Ring R] : CanLift (Set R) (Subring R) SetLike.coe fun (s : Set R) => 0 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → -x ∈ s

instance Subring.instSubringClass {R : Type u} [Ring R] : SubringClass (Subring R) R

def Subring.toNonUnitalSubring {R : Type u} [Ring R] (S : Subring R) : NonUnitalSubring R

Turn a Subring into a NonUnitalSubring by forgetting that it contains 1.

Equations

• S.toNonUnitalSubring = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subring.mem_toSubsemiring {R : Type u} [Ring R] {s : Subring R} {x : R} : x ∈ s.toSubsemiring ↔ x ∈ s

theorem Subring.mem_carrier {R : Type u} [Ring R] {s : Subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem Subring.mem_mk {R : Type u} [Ring R] {S : Subsemiring R} {x : R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : x ∈ { toSubsemiring := S, neg_mem' := h } ↔ x ∈ S

@[simp]

theorem Subring.coe_set_mk {R : Type u} [Ring R] (S : Subsemiring R) (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : ↑{ toSubsemiring := S, neg_mem' := h } = ↑S

@[simp]

theorem Subring.mk_le_mk {R : Type u} [Ring R] {S S' : Subsemiring R} (h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) (h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier) : { toSubsemiring := S, neg_mem' := h₁ } ≤ { toSubsemiring := S', neg_mem' := h₂ } ↔ S ≤ S'

theorem Subring.one_mem_toNonUnitalSubring {R : Type u} [Ring R] (S : Subring R) : 1 ∈ S.toNonUnitalSubring

theorem Subring.ext {R : Type u} [Ring R] {S T : Subring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) : S = T

Two subrings are equal if they have the same elements.

theorem Subring.ext_iff {R : Type u} [Ring R] {S T : Subring R} : S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T

def Subring.copy {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = ↑S) : Subring R

Copy of a subring with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subring.copy_toSubsemiring {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subring.coe_copy {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem Subring.copy_eq {R : Type u} [Ring R] (S : Subring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S

theorem Subring.toSubsemiring_injective {R : Type u} [Ring R] : Function.Injective toSubsemiring

theorem Subring.toAddSubgroup_injective {R : Type u} [Ring R] : Function.Injective toAddSubgroup

theorem Subring.toSubmonoid_injective {R : Type u} [Ring R] : Function.Injective fun (s : Subring R) => s.toSubmonoid

def Subring.mk' {R : Type u} [Ring R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : Subring R

Construct a Subring R from a set s, a submonoid sm, and an additive subgroup sa such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa.

Equations

• Subring.mk' s sm sa hm ha = { toSubmonoid := sm.copy s ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subring.coe_mk' {R : Type u} [Ring R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : ↑(Subring.mk' s sm sa hm ha) = s

@[simp]

theorem Subring.mem_mk' {R : Type u} [Ring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} : x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s

@[simp]

theorem Subring.mk'_toSubmonoid {R : Type u} [Ring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (Subring.mk' s sm sa hm ha).toSubmonoid = sm

@[simp]

theorem Subring.mk'_toAddSubgroup {R : Type u} [Ring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (Subring.mk' s sm sa hm ha).toAddSubgroup = sa

def Subsemiring.toSubring {R : Type u} [Ring R] (s : Subsemiring R) (hneg : -1 ∈ s) : Subring R

A Subsemiring containing -1 is a Subring.

Equations

• s.toSubring hneg = { toSubsemiring := s, neg_mem' := ⋯ }

@[simp]

theorem Subsemiring.toSubring_toSubsemiring {R : Type u} [Ring R] (s : Subsemiring R) (hneg : -1 ∈ s) : (s.toSubring hneg).toSubsemiring = s

theorem Subring.one_mem {R : Type u} [Ring R] (s : Subring R) : 1 ∈ s

A subring contains the ring's 1.

theorem Subring.zero_mem {R : Type u} [Ring R] (s : Subring R) : 0 ∈ s

A subring contains the ring's 0.

theorem Subring.mul_mem {R : Type u} [Ring R] (s : Subring R) {x y : R} : x ∈ s → y ∈ s → x * y ∈ s

A subring is closed under multiplication.

theorem Subring.add_mem {R : Type u} [Ring R] (s : Subring R) {x y : R} : x ∈ s → y ∈ s → x + y ∈ s

A subring is closed under addition.

theorem Subring.neg_mem {R : Type u} [Ring R] (s : Subring R) {x : R} : x ∈ s → -x ∈ s

A subring is closed under negation.

theorem Subring.sub_mem {R : Type u} [Ring R] (s : Subring R) {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s

A subring is closed under subtraction

instance Subring.toRing {R : Type u} [Ring R] (s : Subring R) : Ring ↥s

A subring of a ring inherits a ring structure

Equations

• s.toRing = SubringClass.toRing s

theorem Subring.zsmul_mem {R : Type u} [Ring R] (s : Subring R) {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s

theorem Subring.pow_mem {R : Type u} [Ring R] (s : Subring R) {x : R} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s

@[simp]

theorem Subring.coe_add {R : Type u} [Ring R] (s : Subring R) (x y : ↥s) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Subring.coe_neg {R : Type u} [Ring R] (s : Subring R) (x : ↥s) : ↑(-x) = -↑x

@[simp]

theorem Subring.coe_mul {R : Type u} [Ring R] (s : Subring R) (x y : ↥s) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Subring.coe_zero {R : Type u} [Ring R] (s : Subring R) : ↑0 = 0

@[simp]

theorem Subring.coe_one {R : Type u} [Ring R] (s : Subring R) : ↑1 = 1

@[simp]

theorem Subring.coe_pow {R : Type u} [Ring R] (s : Subring R) (x : ↥s) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem Subring.coe_eq_zero_iff {R : Type u} [Ring R] (s : Subring R) {x : ↥s} : ↑x = 0 ↔ x = 0

instance Subring.toCommRing {R : Type u_1} [CommRing R] (s : Subring R) : CommRing ↥s

A subring of a CommRing is a CommRing.

Equations

• s.toCommRing = SubringClass.toCommRing s

instance Subring.instNontrivialSubtypeMem {R : Type u_1} [Ring R] [Nontrivial R] (s : Subring R) : Nontrivial ↥s

A subring of a non-trivial ring is non-trivial.

instance Subring.instNoZeroDivisorsSubtypeMem {R : Type u_1} [Ring R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors ↥s

A subring of a ring with no zero divisors has no zero divisors.

instance Subring.instIsDomainSubtypeMem {R : Type u_1} [Ring R] [IsDomain R] (s : Subring R) : IsDomain ↥s

A subring of a domain is a domain.

def Subring.subtype {R : Type u} [Ring R] (s : Subring R) : ↥s →+* R

The natural ring hom from a subring of ring R to R.

Equations

• s.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Subring.subtype_apply {R : Type u} [Ring R] {s : Subring R} (x : ↥s) : s.subtype x = ↑x

theorem Subring.subtype_injective {R : Type u} [Ring R] (s : Subring R) : Function.Injective ⇑s.subtype

@[simp]

theorem Subring.coe_subtype {R : Type u} [Ring R] (s : Subring R) : ⇑s.subtype = Subtype.val

theorem Subring.coe_natCast {R : Type u} [Ring R] (s : Subring R) (n : ℕ) : ↑↑n = ↑n

theorem Subring.coe_intCast {R : Type u} [Ring R] (s : Subring R) (n : ℤ) : ↑↑n = ↑n

Partial order

@[simp]

theorem Subring.coe_toSubsemiring {R : Type u} [Ring R] (s : Subring R) : ↑s.toSubsemiring = ↑s

theorem Subring.mem_toSubmonoid {R : Type u} [Ring R] {s : Subring R} {x : R} : x ∈ s.toSubmonoid ↔ x ∈ s

@[simp]

theorem Subring.coe_toSubmonoid {R : Type u} [Ring R] (s : Subring R) : ↑s.toSubmonoid = ↑s

theorem Subring.mem_toAddSubgroup {R : Type u} [Ring R] {s : Subring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s

@[simp]

theorem Subring.coe_toAddSubgroup {R : Type u} [Ring R] (s : Subring R) : ↑s.toAddSubgroup = ↑s

def NonUnitalSubring.toSubring {R : Type u} [Ring R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : Subring R

Turn a non-unital subring containing 1 into a subring.

Equations

• S.toSubring h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Subring.toNonUnitalSubring_toSubring {R : Type u} [Ring R] (S : Subring R) : S.toNonUnitalSubring.toSubring ⋯ = S

theorem NonUnitalSubring.toSubring_toNonUnitalSubring {R : Type u} [Ring R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : (S.toSubring h1).toNonUnitalSubring = S