mathlib documentation

ring_theory.subsemiring

Bundled subsemirings

We define bundled subsemirings and some standard constructions: complete_lattice structure, subtype and inclusion ring homomorphisms, subsemiring map, comap and range (srange) of a ring_hom etc.

Reinterpret a subsemiring as an add_submonoid.

def subsemiring.to_submonoid {R : Type u} [semiring R] :

Reinterpret a subsemiring as a submonoid.

structure subsemiring (R : Type u) [semiring R] :
Type u

A subsemiring of a semiring R is a subset s that is both a multiplicative and an additive submonoid.

@[instance]
def subsemiring.has_coe {R : Type u} [semiring R] :

Equations
@[instance]

Equations
@[instance]
def subsemiring.has_mem {R : Type u} [semiring R] :

Equations
def subsemiring.mk' {R : Type u} [semiring R] (s : set R) (sm : submonoid R) (hm : sm = s) (sa : add_submonoid R) :
sa = ssubsemiring R

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

Equations
@[simp]
theorem subsemiring.coe_mk' {R : Type u} [semiring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_submonoid R} (ha : sa = s) :
(subsemiring.mk' s sm hm sa ha) = s

@[simp]
theorem subsemiring.mem_mk' {R : Type u} [semiring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_submonoid R} (ha : sa = s) {x : R} :
x subsemiring.mk' s sm hm sa ha x s

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

@[simp]
theorem subsemiring.mk'_to_add_submonoid {R : Type u} [semiring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_submonoid R} (ha : sa = s) :

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

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

theorem subsemiring.ext' {R : Type u} [semiring R] ⦃s t : subsemiring R⦄ :
s = ts = t

Two subsemirings are equal if the underlying subsets are equal.

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

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

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

Two subsemirings are equal if they have the same elements.

theorem subsemiring.one_mem {R : Type u} [semiring R] (s : subsemiring R) :
1 s

A subsemiring contains the semiring's 1.

theorem subsemiring.zero_mem {R : Type u} [semiring R] (s : subsemiring R) :
0 s

A subsemiring contains the semiring's 0.

theorem subsemiring.mul_mem {R : Type u} [semiring R] (s : subsemiring R) {x y : R} :
x sy sx * y s

A subsemiring is closed under multiplication.

theorem subsemiring.add_mem {R : Type u} [semiring R] (s : subsemiring R) {x y : R} :
x sy sx + y s

A subsemiring is closed under addition.

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

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

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

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

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

Product of a multiset of elements in a subsemiring of a comm_semiring is in the subsemiring.

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

Sum of a multiset of elements in a subsemiring of a semiring is in the add_subsemiring.

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

Product of elements of a subsemiring of a comm_semiring indexed by a finset is in the subsemiring.

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

Sum of elements in an subsemiring of an semiring indexed by a finset is in the add_subsemiring.

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

theorem subsemiring.nsmul_mem {R : Type u} [semiring R] (s : subsemiring R) {x : R} (hx : x s) (n : ) :
n •ℕ x s

theorem subsemiring.coe_nat_mem {R : Type u} [semiring R] (s : subsemiring R) (n : ) :
n s

@[instance]
def subsemiring.to_semiring {R : Type u} [semiring R] (s : subsemiring R) :

A subsemiring of a semiring inherits a semiring structure

Equations
@[instance]
def subsemiring.nontrivial {R : Type u} [semiring R] (s : subsemiring R) [nontrivial R] :

@[simp]
theorem subsemiring.coe_mul {R : Type u} [semiring R] (s : subsemiring R) (x y : s) :
x * y = (x) * y

@[simp]
theorem subsemiring.coe_one {R : Type u} [semiring R] (s : subsemiring R) :
1 = 1

def subsemiring.subtype {R : Type u} [semiring R] (s : subsemiring R) :

The natural ring hom from a subsemiring of semiring R to R.

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

@[instance]

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

@[simp]
theorem subsemiring.coe_subset_coe {R : Type u} [semiring R] {s t : subsemiring R} :
s t s t

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

@[simp]
theorem subsemiring.mem_coe {R : Type u} [semiring R] {S : subsemiring R} {m : R} :
m S m S

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

@[simp]
theorem subsemiring.mem_to_submonoid {R : Type u} [semiring R] {s : subsemiring R} {x : R} :

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

@[simp]
theorem subsemiring.mem_to_add_submonoid {R : Type u} [semiring R] {s : subsemiring R} {x : R} :

@[simp]

@[instance]
def subsemiring.has_top {R : Type u} [semiring R] :

The subsemiring R of the semiring R.

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

@[simp]
theorem subsemiring.coe_top {R : Type u} [semiring R] :

def subsemiring.comap {R : Type u} {S : Type v} [semiring R] [semiring S] :
(R →+* S)subsemiring Ssubsemiring R

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

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

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

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

def subsemiring.map {R : Type u} {S : Type v} [semiring R] [semiring S] :
(R →+* S)subsemiring Rsubsemiring S

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

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

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

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

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

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

def ring_hom.srange {R : Type u} {S : Type v} [semiring R] [semiring S] :
(R →+* S)subsemiring S

The range of a ring homomorphism is a subsemiring.

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

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

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

@[instance]
def subsemiring.has_bot {R : Type u} [semiring R] :

Equations
@[instance]
def subsemiring.inhabited {R : Type u} [semiring R] :

Equations
theorem subsemiring.coe_bot {R : Type u} [semiring R] :

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

@[instance]
def subsemiring.has_inf {R : Type u} [semiring R] :

The inf of two subsemirings is their intersection.

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

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

@[instance]
def subsemiring.has_Inf {R : Type u} [semiring R] :

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

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

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

@[simp]
theorem subsemiring.Inf_to_add_submonoid {R : Type u} [semiring R] (s : set (subsemiring R)) :
(Inf s).to_add_submonoid = ⨅ (t : subsemiring R) (H : t s), t.to_add_submonoid

@[instance]

Subsemirings of a semiring form a complete lattice.

Equations
def subsemiring.closure {R : Type u} [semiring R] :

The subsemiring generated by a set.

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

@[simp]
theorem subsemiring.subset_closure {R : Type u} [semiring R] {s : set R} :

The subsemiring generated by a set includes the set.

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

A subsemiring S includes closure s if and only if it includes s.

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

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

theorem subsemiring.closure_eq_of_le {R : Type u} [semiring R] {s : set R} {t : subsemiring R} :

theorem subsemiring.closure_induction {R : Type u} [semiring R] {s : set R} {p : R → Prop} {x : R} :
x subsemiring.closure s(∀ (x : R), x sp x)p 0p 1(∀ (x y : R), p xp yp (x + y))(∀ (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 and multiplication, then p holds for all elements of the closure of s.

theorem subsemiring.mem_closure_iff_exists_list {R : Type u} [semiring R] {s : set R} {x : R} :
x subsemiring.closure s ∃ (L : list (list R)), (∀ (t : list R), t L∀ (y : R), y ty s) (list.map list.prod L).sum = x

closure forms a Galois insertion with the coercion to set.

Equations
theorem subsemiring.closure_eq {R : Type u} [semiring R] (s : subsemiring R) :

Closure of a subsemiring S equals S.

@[simp]

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

theorem subsemiring.closure_sUnion {R : Type u} [semiring R] (s : set (set R)) :

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

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

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

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

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

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

def subsemiring.prod {R : Type u} {S : Type v} [semiring R] [semiring S] :

Given subsemirings s, t of semirings R, S respectively, s.prod t is s × t as a subsemiring of R × S.

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

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

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

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

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

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

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

@[simp]
theorem subsemiring.top_prod_top {R : Type u} {S : Type v} [semiring R] [semiring S] :

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

Product of subsemirings is isomorphic to their product as monoids.

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

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

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

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

def ring_hom.srestrict {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (s : subsemiring R) :

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

Equations
@[simp]
theorem ring_hom.srestrict_apply {R : Type u} {S : Type v} [semiring R] [semiring S] {s : subsemiring R} (f : R →+* S) (x : s) :
(f.srestrict s) x = f x

def ring_hom.cod_srestrict {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (s : subsemiring S) :
(∀ (x : R), f x s)R →+* s

Restriction of a ring homomorphism to a subsemiring of the codomain.

Equations
def ring_hom.srange_restrict {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :

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

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

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

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

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

def ring_hom.eq_slocus {R : Type u} {S : Type v} [semiring R] [semiring S] :
(R →+* S)(R →+* S)subsemiring R

The subsemiring of elements x : R such that f x = g x

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

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

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

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

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

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

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

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

The ring homomorphism associated to an inclusion of subsemirings.

Equations
@[simp]
theorem subsemiring.srange_subtype {R : Type u} [semiring R] (s : subsemiring R) :

@[simp]
theorem subsemiring.range_fst {R : Type u} {S : Type v} [semiring R] [semiring S] :

@[simp]
theorem subsemiring.range_snd {R : Type u} {S : Type v} [semiring R] [semiring S] :

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

def ring_equiv.subsemiring_congr {R : Type u} [semiring R] {s t : subsemiring R} :
s = ts ≃+* t

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

Equations