mathlib documentation

ring_theory.subring.basic

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

@[class]
structure subring_class (S : Type u_1) (R : out_param (Type u)) [ring R] [set_like S R] :
Type

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

Instances
@[protected, instance]
def subring_class.add_subgroup_class (S : Type u_1) (R : out_param (Type u)) [set_like S R] [ring R] [h : subring_class S R] :
Equations
theorem coe_int_mem {R : Type u} {S : Type v} [ring R] [set_like S R] [hSR : subring_class S R] (s : S) (n : ) :
n s
@[protected, instance]
def subring_class.to_comm_ring {S : Type v} (s : S) {R : Type u_1} [comm_ring R] [set_like S R] [subring_class S R] :

A subring of a comm_ring is a comm_ring.

Equations
@[protected, instance]
def subring_class.is_domain {S : Type v} (s : S) {R : Type u_1} [ring R] [is_domain R] [set_like S R] [subring_class S R] :

A subring of a domain is a domain.

@[protected, instance]
def subring_class.to_ordered_ring {S : Type v} (s : S) {R : Type u_1} [ordered_ring R] [set_like S R] [subring_class S R] :

A subring of an ordered_ring is an ordered_ring.

Equations
@[protected, instance]
def subring_class.to_ordered_comm_ring {S : Type v} (s : S) {R : Type u_1} [ordered_comm_ring R] [set_like S R] [subring_class S R] :

A subring of an ordered_comm_ring is an ordered_comm_ring.

Equations
@[protected, instance]
def subring_class.to_linear_ordered_ring {S : Type v} (s : S) {R : Type u_1} [linear_ordered_ring R] [set_like S R] [subring_class S R] :

A subring of a linear_ordered_ring is a linear_ordered_ring.

Equations
def subring_class.subtype {R : Type u} {S : Type v} [ring R] [set_like S R] [hSR : subring_class S R] (s : S) :

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

Equations
@[simp]
theorem subring_class.coe_subtype {R : Type u} {S : Type v} [ring R] [set_like S R] [hSR : subring_class S R] (s : S) :
@[simp, norm_cast]
theorem subring_class.coe_nat_cast {R : Type u} {S : Type v} [ring R] [set_like S R] [hSR : subring_class S R] (s : S) (n : ) :
@[simp, norm_cast]
theorem subring_class.coe_int_cast {R : Type u} {S : Type v} [ring R] [set_like S R] [hSR : subring_class S R] (s : S) (n : ) :
def subring.to_add_subgroup {R : Type u} [ring R] (self : subring 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] (self : subring R) :

Reinterpret a subring as a subsemiring.

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

The underlying submonoid of a subring.

Equations
@[protected, instance]
def subring.set_like {R : Type u} [ring R] :
Equations
@[protected, instance]
def subring.subring_class {R : Type u} [ring R] :
Equations
@[simp]
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 : set R} {x : R} (h₁ : ∀ {a b : R}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : R}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : R}, x S-x S) :
x {carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅} x S
@[simp]
theorem subring.coe_set_mk {R : Type u} [ring R] (S : set R) (h₁ : ∀ {a b : R}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : R}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : R}, x S-x S) :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅} = S
@[simp]
theorem subring.mk_le_mk {R : Type u} [ring R] {S S' : set R} (h₁ : ∀ {a b : R}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : R}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : R}, x S-x S) (h₁' : ∀ {a b : R}, a S'b S'a * b S') (h₂' : 1 S') (h₃' : ∀ {a b : R}, a S'b S'a + b S') (h₄' : 0 S') (h₅' : ∀ {x : R}, x S'-x S') :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅} {carrier := S', mul_mem' := h₁', one_mem' := h₂', add_mem' := h₃', zero_mem' := h₄', neg_mem' := h₅'} S S'
@[ext]
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.

@[protected]
def subring.copy {R : Type u} [ring R] (S : subring R) (s : set R) (hs : s = S) :

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

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

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 subsemiring.to_subring {R : Type u} [ring R] (s : subsemiring R) (hneg : -1 s) :

A subsemiring containing -1 is a subring.

Equations
@[protected]
theorem subring.one_mem {R : Type u} [ring R] (s : subring R) :
1 s

A subring contains the ring's 1.

@[protected]
theorem subring.zero_mem {R : Type u} [ring R] (s : subring R) :
0 s

A subring contains the ring's 0.

@[protected]
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.

@[protected]
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.

@[protected]
theorem subring.neg_mem {R : Type u} [ring R] (s : subring R) {x : R} :
x s-x s

A subring is closed under negation.

@[protected]
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

@[protected]
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.

@[protected]
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.

@[protected]
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.

@[protected]
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.

@[protected]
theorem subring.prod_mem {R : Type u_1} [comm_ring R] (s : subring R) {ι : Type u_2} {t : finset ι} {f : ι → R} (h : ∀ (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.

@[protected]
theorem subring.sum_mem {R : Type u_1} [ring R] (s : subring R) {ι : Type u_2} {t : finset ι} {f : ι → R} (h : ∀ (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.

@[protected]
theorem subring.zsmul_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
n x s
@[protected]
theorem subring.pow_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
x ^ n s
@[simp, norm_cast]
theorem subring.coe_add {R : Type u} [ring R] (s : subring R) (x y : s) :
(x + y) = x + y
@[simp, norm_cast]
theorem subring.coe_neg {R : Type u} [ring R] (s : subring R) (x : s) :
@[simp, norm_cast]
theorem subring.coe_mul {R : Type u} [ring R] (s : subring R) (x y : s) :
x * y = (x) * y
@[simp, norm_cast]
theorem subring.coe_zero {R : Type u} [ring R] (s : subring R) :
0 = 0
@[simp, norm_cast]
theorem subring.coe_one {R : Type u} [ring R] (s : subring R) :
1 = 1
@[simp, norm_cast]
theorem subring.coe_pow {R : Type u} [ring R] (s : subring R) (x : s) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem subring.coe_eq_zero_iff {R : Type u} [ring R] (s : subring R) {x : s} :
x = 0 x = 0
@[protected, 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
@[protected, instance]
def subring.nontrivial {R : Type u_1} [ring R] [nontrivial R] (s : subring R) :

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

@[protected, instance]

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

@[protected, instance]
def subring.is_domain {R : Type u_1} [ring R] [is_domain R] (s : subring R) :

A subring of a domain is a domain.

@[protected, instance]
def subring.to_ordered_ring {R : Type u_1} [ordered_ring R] (s : subring R) :

A subring of an ordered_ring is an ordered_ring.

Equations
@[protected, instance]

A subring of an ordered_comm_ring is an ordered_comm_ring.

Equations
@[protected, instance]

A subring of a linear_ordered_ring is a linear_ordered_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) :
@[simp, norm_cast]
theorem subring.coe_nat_cast {R : Type u} [ring R] (s : subring R) (n : ) :
@[simp, norm_cast]
theorem subring.coe_int_cast {R : Type u} [ring R] (s : subring R) (n : ) :

Partial order #

@[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 #

@[protected, 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] (f : R →+* S) (s : subring S) :

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] (f : R →+* S) (s : subring R) :

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
@[simp]
theorem subring.map_id {R : Type u} [ring R] (s : subring R) :
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) :
noncomputable def subring.equiv_map_of_injective {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (f : R →+* S) (hf : function.injective f) :

A subring is isomorphic to its image under an injective function

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

range #

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

The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern].

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.range_eq_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
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) (h : ∀ (x : R), f x s) :

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

Equations
@[protected, instance]
def ring_hom.fintype_range {R : Type u} {S : Type v} [ring R] [ring S] [fintype R] [decidable_eq S] (f : R →+* S) :

The range of a ring homomorphism is a fintype, if the domain is a fintype. Note: this instance can form a diamond with subtype.fintype in the presence of fintype S.

Equations

bot #

@[protected, instance]
def subring.has_bot {R : Type u} [ring R] :
Equations
@[protected, 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 #

@[protected, 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'
@[protected, instance]
def subring.has_Inf {R : Type u} [ring R] :
Equations
@[simp, norm_cast]
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
@[protected, instance]

Subrings of a ring form a complete lattice.

Equations
theorem subring.eq_top_iff' {R : Type u} [ring R] (A : subring R) :
A = ∀ (x : R), x A

Center of a ring #

def subring.center (R : Type u) [ring R] :

The center of a ring R is the set of elements that commute with everything in R

Equations
theorem subring.coe_center (R : Type u) [ring R] :
theorem subring.mem_center_iff {R : Type u} [ring R] {z : R} :
z subring.center R ∀ (g : R), g * z = z * g
@[protected, instance]
def subring.decidable_mem_center {R : Type u} [ring R] [decidable_eq R] [fintype R] :
decidable_pred (λ (_x : R), _x subring.center R)
Equations
@[simp]
theorem subring.center_eq_top (R : Type u_1) [comm_ring R] :
@[protected, instance]
Equations
@[simp]
theorem subring.center.coe_inv {K : Type u} [division_ring K] (a : (subring.center K)) :
@[simp]
theorem subring.center.coe_div {K : Type u} [division_ring K] (a b : (subring.center K)) :
(a / b) = a / b

subring closure of a subset #

def subring.closure {R : Type u} [ring R] (s : set 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.

theorem subring.not_mem_of_not_mem_closure {R : Type u} [ring R] {s : set R} {P : R} (hP : P subring.closure s) :
P s
@[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⦄ (h : s t) :

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} (h₁ : s t) (h₂ : t subring.closure s) :
theorem subring.closure_induction {R : Type u} [ring R] {s : set R} {p : R → Prop} {x : R} (h : x subring.closure s) (Hs : ∀ (x : R), x sp x) (H0 : p 0) (H1 : p 1) (Hadd : ∀ (x y : R), p xp yp (x + y)) (Hneg : ∀ (x : R), p xp (-x)) (Hmul : ∀ (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.closure_induction₂ {R : Type u} [ring R] {s : set R} {p : R → R → Prop} {a b : R} (ha : a subring.closure s) (hb : b subring.closure s) (Hs : ∀ (x : R), x s∀ (y : R), y sp x y) (H0_left : ∀ (x : R), p 0 x) (H0_right : ∀ (x : R), p x 0) (H1_left : ∀ (x : R), p 1 x) (H1_right : ∀ (x : R), p x 1) (Hneg_left : ∀ (x y : R), p x yp (-x) y) (Hneg_right : ∀ (x y : R), p x yp x (-y)) (Hadd_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ * y₂)) :
p a b

An induction principle for closure membership, for predicates with two arguments.

def subring.closure_comm_ring_of_comm {R : Type u} [ring R] {s : set R} (hcomm : ∀ (a : R), a s∀ (b : R), b sa * b = b * a) :

If all elements of s : set A commute pairwise, then closure s is a commutative ring.

Equations
theorem subring.exists_list_of_mem_closure {R : Type u} [ring R] {s : set R} {x : R} (h : 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
@[protected]

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] (s : subring R) (t : subring S) :
subring (R × S)

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

Equations
@[norm_cast]
theorem subring.coe_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :
(s.prod t) = s ×ˢ 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⦄ (ht : 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} (hS : 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)} (Sne : S.nonempty) (hS : directed_on has_le.le S) :
(Sup S) = ⋃ (s : subring R) (H : s S), s
theorem subring.mem_map_equiv {R : Type u} {S : Type v} [ring R] [ring S] {f : R ≃+* S} {K : subring R} {x : S} :
theorem subring.map_equiv_eq_comap_symm {R : Type u} {S : Type v} [ring R] [ring S] (f : R ≃+* S) (K : subring R) :
theorem subring.comap_equiv_eq_map_symm {R : Type u} {S : Type v} [ring R] [ring S] (f : R ≃+* S) (K : subring 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.

This is the bundled version of set.range_factorization.

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_restrict_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
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) (hf : function.surjective f) :

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] (f g : R →+* S) :

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} (h : set.eq_on f g s) :

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} (h : set.eq_on f g ) :
f = g
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} (h : set.eq_on f g s) :
f = 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} (h : S 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} (h : s = t) :

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

Equations
def ring_equiv.of_left_inverse {R : Type u} {S : Type v} [ring R] [ring S] {g : S → R} {f : R →+* S} (h : function.left_inverse g f) :

Restrict a ring homomorphism with a left inverse to a ring isomorphism to its ring_hom.range.

Equations
@[simp]
theorem ring_equiv.of_left_inverse_apply {R : Type u} {S : Type v} [ring R] [ring S] {g : S → R} {f : R →+* S} (h : function.left_inverse g f) (x : R) :
@[simp]
theorem ring_equiv.of_left_inverse_symm_apply {R : Type u} {S : Type v} [ring R] [ring S] {g : S → R} {f : R →+* S} (h : function.left_inverse g f) (x : (f.range)) :
@[simp]
@[simp]
theorem ring_equiv.subring_map_apply_coe {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (e : R ≃+* S) (ᾰ : (s.to_subsemiring.to_add_submonoid)) :
((e.subring_map) ᾰ) = e
def ring_equiv.subring_map {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (e : R ≃+* S) :

Given an equivalence e : R ≃+* S of rings and a subring s of R, subring_equiv_map e s is the induced equivalence between s and s.map e

Equations
@[protected]
theorem subring.in_closure.rec_on {R : Type u} [ring R] {s : set R} {C : R → Prop} {x : R} (hx : x subring.closure s) (h1 : C 1) (hneg1 : C (-1)) (hs : ∀ (z : R), z s∀ (n : R), C nC (z * n)) (ha : ∀ {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} (h : g G) :
(k) * g G

Actions by subrings #

These are just copies of the definitions about subsemiring starting from subsemiring.mul_action.

When R is commutative, algebra.of_subring provides a stronger result than those found in this file, which uses the same scalar action.

@[protected, instance]
def subring.has_scalar {R : Type u} [ring R] {α : Type u_1} [has_scalar R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
theorem subring.smul_def {R : Type u} [ring R] {α : Type u_1} [has_scalar R α] {S : subring R} (g : S) (m : α) :
g m = g m
@[protected, instance]
def subring.smul_comm_class_left {R : Type u} [ring R] {α : Type u_1} {β : Type u_2} [has_scalar R β] [has_scalar α β] [smul_comm_class R α β] (S : subring R) :
@[protected, instance]
def subring.smul_comm_class_right {R : Type u} [ring R] {α : Type u_1} {β : Type u_2} [has_scalar α β] [has_scalar R β] [smul_comm_class α R β] (S : subring R) :
@[protected, instance]
def subring.is_scalar_tower {R : Type u} [ring R] {α : Type u_1} {β : Type u_2} [has_scalar α β] [has_scalar R α] [has_scalar R β] [is_scalar_tower R α β] (S : subring R) :

Note that this provides is_scalar_tower S R R which is needed by smul_mul_assoc.

@[protected, instance]
def subring.has_faithful_scalar {R : Type u} [ring R] {α : Type u_1} [has_scalar R α] [has_faithful_scalar R α] (S : subring R) :
@[protected, instance]
def subring.mul_action {R : Type u} [ring R] {α : Type u_1} [mul_action R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.distrib_mul_action {R : Type u} [ring R] {α : Type u_1} [add_monoid α] [distrib_mul_action R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.mul_distrib_mul_action {R : Type u} [ring R] {α : Type u_1} [monoid α] [mul_distrib_mul_action R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.smul_with_zero {R : Type u} [ring R] {α : Type u_1} [has_zero α] [smul_with_zero R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.mul_action_with_zero {R : Type u} [ring R] {α : Type u_1} [has_zero α] [mul_action_with_zero R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.module {R : Type u} [ring R] {α : Type u_1} [add_comm_monoid α] [module R α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations

The subgroup of positive units of a linear ordered semiring.

Equations
@[simp]
theorem units.mem_pos_subgroup {R : Type u_1} [linear_ordered_semiring R] (u : Rˣ) :