mathlib documentation

ring_theory.subring

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 is_subring 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)

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

def subring.to_add_subgroup {R : Type u} [ring R] :

Reinterpret a subring as an add_subgroup.

structure subring (R : Type u) [ring 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.

def subring.to_subsemiring {R : Type u} [ring R] :

Reinterpret a subring as a subsemiring.

def subring.to_submonoid {R : Type u} [ring R] :

The underlying submonoid of a subring.

Equations
@[instance]
def subring.set.has_coe {R : Type u} [ring R] :

Equations
@[instance]
def subring.has_coe_to_sort {R : Type u} [ring R] :

Equations
@[instance]
def subring.has_mem {R : Type u} [ring R] :

Equations
def subring.mk' {R : Type u} [ring R] (s : set R) (sm : submonoid R) (sa : add_subgroup R) :
sm = ssa = ssubring 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
@[simp]
theorem subring.coe_mk' {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (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 : add_subgroup R} (ha : sa = s) {x : R} :
x subring.mk' s sm sa hm ha x s

@[simp]
theorem subring.mk'_to_submonoid {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (ha : sa = s) :
(subring.mk' s sm sa hm ha).to_submonoid = sm

@[simp]
theorem subring.mk'_to_add_subgroup {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (ha : sa = s) :
(subring.mk' s sm sa hm ha).to_add_subgroup = sa

def set.to_subring {R : Type u} [ring R] (S : set R) [is_subring S] :

Construct a subring from a set satisfying is_subring.

Equations
theorem subring.exists {R : Type u} [ring R] {s : subring R} {p : s → Prop} :
(∃ (x : s), p x) ∃ (x : R) (H : x s), p x, H⟩

theorem subring.forall {R : Type u} [ring R] {s : subring R} {p : s → Prop} :
(∀ (x : s), p x) ∀ (x : R) (H : x s), p x, H⟩

def subsemiring.to_subring {R : Type u} [ring R] (s : subsemiring R) :
-1 ssubring R

A subsemiring containing -1 is a subring.

Equations
theorem subring.ext' {R : Type u} [ring R] ⦃s t : subring R⦄ :
s = ts = t

Two subrings are equal if the underlying subsets are equal.

theorem subring.ext'_iff {R : Type u} [ring R] {s t : subring R} :
s = t s = t

Two subrings are equal if and only if the underlying subsets are equal.

@[ext]
theorem subring.ext {R : Type u} [ring R] {S T : subring R} :
(∀ (x : R), x S x T)S = T

Two subrings are equal if they have the same elements.

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 sy sx * y s

A subring is closed under multiplication.

theorem subring.add_mem {R : Type u} [ring R] (s : subring R) {x y : R} :
x sy sx + 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} :
x sy sx - y s

A subring is closed under subtraction

theorem subring.list_prod_mem {R : Type u} [ring R] (s : subring R) {l : list R} :
(∀ (x : R), x lx s)l.prod s

Product of a list of elements in a subring is in the subring.

theorem subring.list_sum_mem {R : Type u} [ring R] (s : subring R) {l : list R} :
(∀ (x : R), x lx s)l.sum s

Sum of a list of elements in a subring is in the subring.

theorem subring.multiset_prod_mem {R : Type u_1} [comm_ring R] (s : subring R) (m : multiset R) :
(∀ (a : R), a ma s)m.prod s

Product of a multiset of elements in a subring of a comm_ring is in the subring.

theorem subring.multiset_sum_mem {R : Type u_1} [ring R] (s : subring R) (m : multiset R) :
(∀ (a : R), a ma s)m.sum s

Sum of a multiset of elements in an subring of a ring is in the subring.

theorem subring.prod_mem {R : Type u_1} [comm_ring R] (s : subring R) {ι : Type u_2} {t : finset ι} {f : ι → R} :
(∀ (c : ι), c tf c s)∏ (i : ι) in t, f i s

Product of elements of a subring of a comm_ring indexed by a finset is in the subring.

theorem subring.sum_mem {R : Type u_1} [ring R] (s : subring R) {ι : Type u_2} {t : finset ι} {f : ι → R} :
(∀ (c : ι), c tf c s)∑ (i : ι) in t, f i s

Sum of elements in a subring of a ring indexed by a finset is in the subring.

theorem subring.pow_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
x ^ n s

theorem subring.gsmul_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
n •ℤ x s

theorem subring.coe_int_mem {R : Type u} [ring R] (s : subring R) (n : ) :
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) :

@[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_eq_zero_iff {R : Type u} [ring R] (s : subring R) {x : s} :
x = 0 x = 0

@[instance]
def subring.to_comm_ring {R : Type u_1} [comm_ring R] (s : subring R) :

A subring of a comm_ring is a comm_ring.

Equations
def subring.subtype {R : Type u} [ring R] (s : subring R) :

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

Equations
@[simp]
theorem subring.coe_subtype {R : Type u} [ring R] (s : subring R) :

Partial order

@[instance]
def subring.partial_order {R : Type u} [ring R] :

Equations
theorem subring.le_def {R : Type u} [ring R] {s t : subring R} :
s t ∀ ⦃x : R⦄, x sx t

@[simp]
theorem subring.coe_subset_coe {R : Type u} [ring R] {s t : subring R} :
s t s t

@[simp]
theorem subring.coe_ssubset_coe {R : Type u} [ring R] {s t : subring R} :
s t s < t

@[simp]
theorem subring.mem_coe {R : Type u} [ring R] {S : subring R} {m : R} :
m S m S

@[simp]
theorem subring.coe_coe {R : Type u} [ring R] (s : subring R) :

@[simp]
theorem subring.mem_to_submonoid {R : Type u} [ring R] {s : subring R} {x : R} :

@[simp]
theorem subring.coe_to_submonoid {R : Type u} [ring R] (s : subring R) :

@[simp]
theorem subring.mem_to_add_subgroup {R : Type u} [ring R] {s : subring R} {x : R} :

@[simp]
theorem subring.coe_to_add_subgroup {R : Type u} [ring R] (s : subring R) :

top

@[instance]
def subring.has_top {R : Type u} [ring R] :

The subring R of the ring R.

Equations
@[simp]
theorem subring.mem_top {R : Type u} [ring R] (x : R) :

@[simp]
theorem subring.coe_top {R : Type u} [ring R] :

comap

def subring.comap {R : Type u} {S : Type v} [ring R] [ring S] :
(R →+* S)subring Ssubring R

The preimage of a subring along a ring homomorphism is a subring.

Equations
@[simp]
theorem subring.coe_comap {R : Type u} {S : Type v} [ring R] [ring S] (s : subring S) (f : R →+* S) :

@[simp]
theorem subring.mem_comap {R : Type u} {S : Type v} [ring R] [ring S] {s : subring S} {f : R →+* S} {x : R} :

theorem subring.comap_comap {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] (s : subring T) (g : S →+* T) (f : R →+* S) :

map

def subring.map {R : Type u} {S : Type v} [ring R] [ring S] :
(R →+* S)subring Rsubring S

The image of a subring along a ring homomorphism is a subring.

Equations
@[simp]
theorem subring.coe_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring R) :

@[simp]
theorem subring.mem_map {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {s : subring R} {y : S} :
y subring.map f s ∃ (x : R) (H : x s), f x = y

theorem subring.map_map {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] (s : subring R) (g : S →+* T) (f : R →+* S) :

theorem subring.map_le_iff_le_comap {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {s : subring R} {t : subring S} :

theorem subring.gc_map_comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

range

def ring_hom.range {R : Type u} {S : Type v} [ring R] [ring S] :
(R →+* S)subring S

The range of a ring homomorphism, as a subring of the target.

Equations
@[simp]
theorem ring_hom.coe_range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

@[simp]
theorem ring_hom.mem_range {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {y : S} :
y f.range ∃ (x : R), f x = y

theorem ring_hom.mem_range_self {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (x : R) :

theorem ring_hom.map_range {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] (g : S →+* T) (f : R →+* S) :

def ring_hom.cod_restrict' {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring S) :
(∀ (x : R), f x s)R →+* s

Restrict the codomain of a ring homomorphism to a subring that includes the range.

Equations
theorem ring_hom.surjective_onto_range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

def subring.subset_comm_ring {cR : Type u} [comm_ring cR] (S : subring cR) :

A subring of a commutative ring is a commutative ring.

Equations

bot

@[instance]
def subring.has_bot {R : Type u} [ring R] :

Equations
@[instance]
def subring.inhabited {R : Type u} [ring R] :

Equations
theorem subring.coe_bot {R : Type u} [ring R] :

theorem subring.mem_bot {R : Type u} [ring R] {x : R} :
x ∃ (n : ), n = x

inf

@[instance]
def subring.has_inf {R : Type u} [ring R] :

The inf of two subrings is their intersection.

Equations
@[simp]
theorem subring.coe_inf {R : Type u} [ring R] (p p' : subring R) :
(p p') = p p'

@[simp]
theorem subring.mem_inf {R : Type u} [ring R] {p p' : subring R} {x : R} :
x p p' x p x p'

@[instance]
def subring.has_Inf {R : Type u} [ring R] :

Equations
@[simp]
theorem subring.coe_Inf {R : Type u} [ring R] (S : set (subring R)) :
(Inf S) = ⋂ (s : subring R) (H : s S), s

theorem subring.mem_Inf {R : Type u} [ring R] {S : set (subring R)} {x : R} :
x Inf S ∀ (p : subring R), p Sx p

@[simp]
theorem subring.Inf_to_submonoid {R : Type u} [ring R] (s : set (subring R)) :
(Inf s).to_submonoid = ⨅ (t : subring R) (H : t s), t.to_submonoid

@[simp]
theorem subring.Inf_to_add_subgroup {R : Type u} [ring R] (s : set (subring R)) :
(Inf s).to_add_subgroup = ⨅ (t : subring R) (H : t s), t.to_add_subgroup

@[instance]

Subrings of a ring form a complete lattice.

Equations

subring closure of a subset

def subring.closure {R : Type u} [ring R] :
set Rsubring R

The subring generated by a set.

Equations
theorem subring.mem_closure {R : Type u} [ring R] {x : R} {s : set R} :
x subring.closure s ∀ (S : subring R), s Sx S

@[simp]
theorem subring.subset_closure {R : Type u} [ring R] {s : set R} :

The subring generated by a set includes the set.

@[simp]
theorem subring.closure_le {R : Type u} [ring R] {s : set R} {t : subring R} :

A subring t includes closure s if and only if it includes s.

theorem subring.closure_mono {R : Type u} [ring R] ⦃s t : set R⦄ :

Subring closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

theorem subring.closure_eq_of_le {R : Type u} [ring R] {s : set R} {t : subring R} :

theorem subring.closure_induction {R : Type u} [ring R] {s : set R} {p : R → Prop} {x : R} :
x subring.closure s(∀ (x : R), x sp x)p 0p 1(∀ (x y : R), p xp yp (x + y))(∀ (x : R), p xp (-x))(∀ (x y : R), p xp yp (x * y))p x

An induction principle for closure membership. If p holds for 0, 1, and all elements of s, and is preserved under addition, negation, and multiplication, then p holds for all elements of the closure of s.

theorem subring.exists_list_of_mem_closure {R : Type u} [ring R] {s : set R} {x : R} :
x subring.closure s(∃ (L : list (list R)), (∀ (t : list R), t L∀ (y : R), y ty s y = -1) (list.map list.prod L).sum = x)

closure forms a Galois insertion with the coercion to set.

Equations
theorem subring.closure_eq {R : Type u} [ring R] (s : subring R) :

Closure of a subring S equals S.

@[simp]
theorem subring.closure_empty {R : Type u} [ring R] :

@[simp]
theorem subring.closure_univ {R : Type u} [ring R] :

theorem subring.closure_union {R : Type u} [ring R] (s t : set R) :

theorem subring.closure_Union {R : Type u} [ring R] {ι : Sort u_1} (s : ι → set R) :
subring.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subring.closure (s i)

theorem subring.closure_sUnion {R : Type u} [ring R] (s : set (set R)) :
subring.closure (⋃₀s) = ⨆ (t : set R) (H : t s), subring.closure t

theorem subring.map_sup {R : Type u} {S : Type v} [ring R] [ring S] (s t : subring R) (f : R →+* S) :

theorem subring.map_supr {R : Type u} {S : Type v} [ring R] [ring S] {ι : Sort u_1} (f : R →+* S) (s : ι → subring R) :
subring.map f (supr s) = ⨆ (i : ι), subring.map f (s i)

theorem subring.comap_inf {R : Type u} {S : Type v} [ring R] [ring S] (s t : subring S) (f : R →+* S) :

theorem subring.comap_infi {R : Type u} {S : Type v} [ring R] [ring S] {ι : Sort u_1} (f : R →+* S) (s : ι → subring S) :
subring.comap f (infi s) = ⨅ (i : ι), subring.comap f (s i)

@[simp]
theorem subring.map_bot {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

@[simp]
theorem subring.comap_top {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

def subring.prod {R : Type u} {S : Type v} [ring R] [ring S] :
subring Rsubring Ssubring (R × S)

Given subrings s, t of rings R, S respectively, s.prod t is s × t as a subring of R × S.

Equations
theorem subring.coe_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :
(s.prod t) = s.prod t

theorem subring.mem_prod {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} {t : subring S} {p : R × S} :
p s.prod t p.fst s p.snd t

theorem subring.prod_mono {R : Type u} {S : Type v} [ring R] [ring S] ⦃s₁ s₂ : subring R⦄ (hs : s₁ s₂) ⦃t₁ t₂ : subring S⦄ :
t₁ t₂s₁.prod t₁ s₂.prod t₂

theorem subring.prod_mono_right {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) :
monotone (λ (t : subring S), s.prod t)

theorem subring.prod_mono_left {R : Type u} {S : Type v} [ring R] [ring S] (t : subring S) :
monotone (λ (s : subring R), s.prod t)

theorem subring.prod_top {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) :

theorem subring.top_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring S) :

@[simp]
theorem subring.top_prod_top {R : Type u} {S : Type v} [ring R] [ring S] :

def subring.prod_equiv {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :

Product of subrings is isomorphic to their product as rings.

Equations
theorem subring.mem_supr_of_directed {R : Type u} [ring R] {ι : Sort u_1} [hι : nonempty ι] {S : ι → subring R} (hS : directed has_le.le S) {x : R} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i

The underlying set of a non-empty directed Sup of subrings is just a union of the subrings. Note that this fails without the directedness assumption (the union of two subrings is typically not a subring)

theorem subring.coe_supr_of_directed {R : Type u} [ring R] {ι : Sort u_1} [hι : nonempty ι] {S : ι → subring R} :
directed has_le.le S((⨆ (i : ι), S i) = ⋃ (i : ι), (S i))

theorem subring.mem_Sup_of_directed_on {R : Type u} [ring R] {S : set (subring R)} (Sne : S.nonempty) (hS : directed_on has_le.le S) {x : R} :
x Sup S ∃ (s : subring R) (H : s S), x s

theorem subring.coe_Sup_of_directed_on {R : Type u} [ring R] {S : set (subring R)} :
S.nonemptydirected_on has_le.le S((Sup S) = ⋃ (s : subring R) (H : s S), s)

def ring_hom.restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring R) :

Restriction of a ring homomorphism to a subring of the domain.

Equations
@[simp]
theorem ring_hom.restrict_apply {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (f : R →+* S) (x : s) :
(f.restrict s) x = f x

def ring_hom.range_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

Restriction of a ring homomorphism to its range interpreted as a subsemiring.

Equations
@[simp]
theorem ring_hom.coe_range_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (x : R) :

theorem ring_hom.range_top_iff_surjective {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} :

theorem ring_hom.range_top_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

The range of a surjective ring homomorphism is the whole of the codomain.

def ring_hom.eq_locus {R : Type u} {S : Type v} [ring R] [ring S] :
(R →+* S)(R →+* S)subring R

The subring of elements x : R such that f x = g x, i.e., the equalizer of f and g as a subring of R

Equations
theorem ring_hom.eq_on_set_closure {R : Type u} {S : Type v} [ring R] [ring S] {f g : R →+* S} {s : set R} :

If two ring homomorphisms are equal on a set, then they are equal on its subring closure.

theorem ring_hom.eq_of_eq_on_set_top {R : Type u} {S : Type v} [ring R] [ring S] {f g : R →+* S} :

theorem ring_hom.eq_of_eq_on_set_dense {R : Type u} {S : Type v} [ring R] [ring S] {s : set R} (hs : subring.closure s = ) {f g : R →+* S} :
set.eq_on f g sf = g

theorem ring_hom.closure_preimage_le {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set S) :

theorem ring_hom.map_closure {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set R) :

The image under a ring homomorphism of the subring generated by a set equals the subring generated by the image of the set.

def subring.inclusion {R : Type u} [ring R] {S T : subring R} :
S TS →* T

The ring homomorphism associated to an inclusion of subrings.

Equations
@[simp]
theorem subring.range_subtype {R : Type u} [ring R] (s : subring R) :

@[simp]
theorem subring.range_fst {R : Type u} {S : Type v} [ring R] [ring S] :

@[simp]
theorem subring.range_snd {R : Type u} {S : Type v} [ring R] [ring S] :

@[simp]
theorem subring.prod_bot_sup_bot_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :

def ring_equiv.subring_congr {R : Type u} [ring R] {s t : subring R} :
s = ts ≃+* t

Makes the identity isomorphism from a proof two subrings of a multiplicative monoid are equal.

Equations
theorem subring.in_closure.rec_on {R : Type u} [ring R] {s : set R} {C : R → Prop} {x : R} :
x subring.closure sC 1C (-1)(∀ (z : R), z s∀ (n : R), C nC (z * n))(∀ {x y : R}, C xC yC (x + y))C x

theorem subring.closure_preimage_le {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set S) :

theorem add_subgroup.int_mul_mem {R : Type u} [ring R] {G : add_subgroup R} (k : ) {g : R} :
g G(k) * g G