mathlib3 documentation

ring_theory.non_unital_subsemiring.basic

Bundled non-unital subsemirings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[class]

non_unital_subsemiring_class S R states that S is a type of subsets s ⊆ R that are both an additive submonoid and also a multiplicative subsemigroup.

Instances of this typeclass
Instances of other typeclasses for non_unital_subsemiring_class
  • non_unital_subsemiring_class.has_sizeof_inst

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

Equations

Note: currently, there are no ordered versions of non-unital rings.

A non-unital subsemiring of a non-unital semiring R is a subset s that is both an additive submonoid and a semigroup.

Instances for non_unital_subsemiring
@[ext]
theorem non_unital_subsemiring.ext {R : Type u} [non_unital_non_assoc_semiring R] {S T : non_unital_subsemiring R} (h : (x : R), x S x T) :
S = T

Two non-unital subsemirings are equal if they have the same elements.

@[protected]

Copy of a non-unital subsemiring with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem non_unital_subsemiring.coe_copy {R : Type u} [non_unital_non_assoc_semiring R] (S : non_unital_subsemiring R) (s : set R) (hs : s = S) :
(S.copy s hs) = s
theorem non_unital_subsemiring.copy_eq {R : Type u} [non_unital_non_assoc_semiring R] (S : non_unital_subsemiring R) (s : set R) (hs : s = S) :
S.copy s hs = S
@[protected]
def non_unital_subsemiring.mk' {R : Type u} [non_unital_non_assoc_semiring R] (s : set R) (sg : subsemigroup R) (hg : sg = s) (sa : add_submonoid R) (ha : sa = s) :

Construct a non_unital_subsemiring R from a set s, a subsemigroup sg, and an additive submonoid sa such that x ∈ s ↔ x ∈ sg ↔ x ∈ sa.

Equations
@[simp]
theorem non_unital_subsemiring.coe_mk' {R : Type u} [non_unital_non_assoc_semiring R] {s : set R} {sg : subsemigroup R} (hg : sg = s) {sa : add_submonoid R} (ha : sa = s) :
@[simp]
theorem non_unital_subsemiring.mem_mk' {R : Type u} [non_unital_non_assoc_semiring R] {s : set R} {sg : subsemigroup R} (hg : sg = s) {sa : add_submonoid R} (ha : sa = s) {x : R} :
@[simp]
theorem non_unital_subsemiring.mk'_to_subsemigroup {R : Type u} [non_unital_non_assoc_semiring R] {s : set R} {sg : subsemigroup R} (hg : sg = s) {sa : add_submonoid R} (ha : sa = s) :
@[simp]
theorem non_unital_subsemiring.mk'_to_add_submonoid {R : Type u} [non_unital_non_assoc_semiring R] {s : set R} {sg : subsemigroup R} (hg : sg = s) {sa : add_submonoid R} (ha : sa = s) :
@[simp, norm_cast]
@[simp, norm_cast]

Note: currently, there are no ordered versions of non-unital rings.

@[protected, instance]

The non-unital subsemiring R of the non-unital semiring R.

Equations

The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a non-unital subsemiring.

Equations

The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring.

Equations
@[simp]

A non-unital subsemiring is isomorphic to its image under an injective function

Equations

The range of a non-unital ring homomorphism is a non-unital subsemiring. See note [range copy pattern].

Equations
Instances for non_unital_ring_hom.srange
@[protected, instance]

The range of a morphism of non-unital semirings is finite if the domain is a finite.

@[protected, instance]

The inf of two non-unital subsemirings is their intersection.

Equations
@[simp]
theorem non_unital_subsemiring.mem_inf {R : Type u} [non_unital_non_assoc_semiring R] {p p' : non_unital_subsemiring R} {x : R} :
x p p' x p x p'
@[protected, instance]

Non-unital subsemirings of a non-unital semiring form a complete lattice.

Equations

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

Equations
Instances for non_unital_subsemiring.center

The centralizer of a set as non-unital subsemiring.

Equations
@[simp]

The non-unital subsemiring generated by a set includes the set.

@[simp]

A non-unital subsemiring S includes closure s if and only if it includes s.

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

The additive closure of a non-unital subsemigroup is a non-unital subsemiring.

Equations

The elements of the non-unital subsemiring closure of M are exactly the elements of the additive closure of a multiplicative subsemigroup M.

theorem non_unital_subsemiring.closure_induction {R : Type u} [non_unital_non_assoc_semiring R] {s : set R} {p : R Prop} {x : R} (h : x non_unital_subsemiring.closure s) (Hs : (x : R), x s p x) (H0 : p 0) (Hadd : (x y : R), p x p y p (x + y)) (Hmul : (x y : R), p x p y p (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 non_unital_subsemiring.closure_induction₂ {R : Type u} [non_unital_non_assoc_semiring R] {s : set R} {p : R R Prop} {x y : R} (hx : x non_unital_subsemiring.closure s) (hy : y non_unital_subsemiring.closure s) (Hs : (x : R), x s (y : R), y s p x y) (H0_left : (x : R), p 0 x) (H0_right : (x : R), p x 0) (Hadd_left : (x₁ x₂ y : R), p x₁ y p x₂ y p (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₁ y p x₂ y p (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : R), p x y₁ p x y₂ p x (y₁ * y₂)) :
p x y

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

@[protected]

closure forms a Galois insertion with the coercion to set.

Equations

Closure of a non-unital subsemiring S equals S.

Given non_unital_subsemirings s, t of semirings R, S respectively, s.prod t is s × t as a non-unital subsemiring of R × S.

Equations
theorem non_unital_subsemiring.prod_mono {R : Type u} {S : Type v} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] ⦃s₁ s₂ : non_unital_subsemiring R⦄ (hs : s₁ s₂) ⦃t₁ t₂ : non_unital_subsemiring S⦄ (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂

Product of non-unital subsemirings is isomorphic to their product as semigroups.

Equations
theorem non_unital_subsemiring.mem_supr_of_directed {R : Type u} [non_unital_non_assoc_semiring R] {ι : Sort u_1} [hι : nonempty ι] {S : ι non_unital_subsemiring R} (hS : directed has_le.le S) {x : R} :
(x (i : ι), S i) (i : ι), x S i
theorem non_unital_subsemiring.coe_supr_of_directed {R : Type u} [non_unital_non_assoc_semiring R] {ι : Sort u_1} [hι : nonempty ι] {S : ι non_unital_subsemiring R} (hS : directed has_le.le S) :
( (i : ι), S i) = (i : ι), (S i)

Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.

Equations

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

This is the bundled version of set.range_factorization.

Equations

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

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

Equations

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

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

The non-unital ring homomorphism associated to an inclusion of non-unital subsemirings.

Equations

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

Equations

Given an equivalence e : R ≃+* S of non-unital semirings and a non-unital subsemiring s of R, non_unital_subsemiring_map e s is the induced equivalence between s and s.map e

Equations