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]
structure
non_unital_subsemiring_class
(S : Type u_1)
(R : Type u)
[non_unital_non_assoc_semiring R]
[set_like S R] :
- to_add_submonoid_class : add_submonoid_class S R
- mul_mem : ∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a * b ∈ s
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
@[protected, instance]
def
non_unital_subsemiring_class.mul_mem_class
(S : Type u_1)
(R : Type u)
[non_unital_non_assoc_semiring R]
[set_like S R]
[h : non_unital_subsemiring_class S R] :
mul_mem_class S R
@[protected, instance]
def
non_unital_subsemiring_class.to_non_unital_non_assoc_semiring
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[set_like S R]
[non_unital_subsemiring_class S R]
(s : S) :
A non-unital subsemiring of a non_unital_non_assoc_semiring inherits a
non_unital_non_assoc_semiring structure
@[protected, instance]
def
non_unital_subsemiring_class.no_zero_divisors
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[set_like S R]
[non_unital_subsemiring_class S R]
(s : S)
[no_zero_divisors R] :
def
non_unital_subsemiring_class.subtype
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[set_like S R]
[non_unital_subsemiring_class S R]
(s : S) :
The natural non-unital ring hom from a non-unital subsemiring of a non-unital semiring R to
R.
Equations
- non_unital_subsemiring_class.subtype s = {to_fun := coe coe_to_lift, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
non_unital_subsemiring_class.coe_subtype
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[set_like S R]
[non_unital_subsemiring_class S R]
(s : S) :
@[protected, instance]
def
non_unital_subsemiring_class.to_non_unital_semiring
{S : Type v}
(s : S)
{R : Type u_1}
[non_unital_semiring R]
[set_like S R]
[non_unital_subsemiring_class S R] :
A non-unital subsemiring of a non_unital_semiring is a non_unital_semiring.
Equations
@[protected, instance]
def
non_unital_subsemiring_class.to_non_unital_comm_semiring
{S : Type v}
(s : S)
{R : Type u_1}
[non_unital_comm_semiring R]
[set_like S R]
[non_unital_subsemiring_class S R] :
A non-unital subsemiring of a non_unital_comm_semiring is a non_unital_comm_semiring.
Note: currently, there are no ordered versions of non-unital rings.
def
non_unital_subsemiring.to_add_submonoid
{R : Type u}
[non_unital_non_assoc_semiring R]
(self : non_unital_subsemiring R) :
Reinterpret a non_unital_subsemiring as an add_submonoid.
- carrier : set R
- add_mem' : ∀ {a b : R}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- mul_mem' : ∀ {a b : R}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
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
- non_unital_subsemiring.has_sizeof_inst
- non_unital_subsemiring.set_like
- non_unital_subsemiring.non_unital_subsemiring_class
- non_unital_subsemiring.has_top
- non_unital_subsemiring.has_bot
- non_unital_subsemiring.inhabited
- non_unital_subsemiring.has_inf
- non_unital_subsemiring.has_Inf
- non_unital_subsemiring.complete_lattice
def
non_unital_subsemiring.to_subsemigroup
{R : Type u}
[non_unital_non_assoc_semiring R]
(self : non_unital_subsemiring R) :
Reinterpret a non_unital_subsemiring as a subsemigroup.
@[protected, instance]
Equations
- non_unital_subsemiring.set_like = {coe := non_unital_subsemiring.carrier _inst_1, coe_injective' := _}
@[protected, instance]
def
non_unital_subsemiring.non_unital_subsemiring_class
{R : Type u}
[non_unital_non_assoc_semiring R] :
Equations
@[simp]
theorem
non_unital_subsemiring.mem_carrier
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : non_unital_subsemiring R}
{x : R} :
@[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]
def
non_unital_subsemiring.copy
{R : Type u}
[non_unital_non_assoc_semiring R]
(S : non_unital_subsemiring R)
(s : set R)
(hs : s = ↑S) :
Copy of a non-unital subsemiring with a new carrier equal to the old one. Useful to fix
definitional equalities.
@[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) :
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) :
@[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.
@[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) :
↑(non_unital_subsemiring.mk' s sg hg sa ha) = 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} :
x ∈ non_unital_subsemiring.mk' s sg hg sa ha ↔ x ∈ s
@[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) :
(non_unital_subsemiring.mk' s sg hg sa ha).to_subsemigroup = sg
@[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) :
(non_unital_subsemiring.mk' s sg hg sa ha).to_add_submonoid = sa
@[simp, norm_cast]
theorem
non_unital_subsemiring.coe_zero
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R) :
@[simp, norm_cast]
theorem
non_unital_subsemiring.coe_add
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R)
(x y : ↥s) :
@[simp, norm_cast]
theorem
non_unital_subsemiring.coe_mul
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R)
(x y : ↥s) :
Note: currently, there are no ordered versions of non-unital rings.
@[simp]
theorem
non_unital_subsemiring.mem_to_subsemigroup
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : non_unital_subsemiring R}
{x : R} :
x ∈ s.to_subsemigroup ↔ x ∈ s
@[simp]
theorem
non_unital_subsemiring.coe_to_subsemigroup
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R) :
↑(s.to_subsemigroup) = ↑s
@[simp]
theorem
non_unital_subsemiring.mem_to_add_submonoid
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : non_unital_subsemiring R}
{x : R} :
x ∈ s.to_add_submonoid ↔ x ∈ s
@[simp]
theorem
non_unital_subsemiring.coe_to_add_submonoid
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R) :
↑(s.to_add_submonoid) = ↑s
@[protected, instance]
The non-unital subsemiring R of the non-unital semiring R.
@[simp]
@[simp]
def
non_unital_subsemiring.comap
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(s : non_unital_subsemiring S) :
The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a non-unital subsemiring.
@[simp]
theorem
non_unital_subsemiring.coe_comap
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(s : non_unital_subsemiring S)
(f : F) :
@[simp]
theorem
non_unital_subsemiring.mem_comap
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{s : non_unital_subsemiring S}
{f : F}
{x : R} :
x ∈ non_unital_subsemiring.comap f s ↔ ⇑f x ∈ s
theorem
non_unital_subsemiring.comap_comap
{R : Type u}
{S : Type v}
{T : Type w}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
[non_unital_non_assoc_semiring T]
{F : Type u_1}
{G : Type u_2}
[non_unital_ring_hom_class F R S]
[non_unital_ring_hom_class G S T]
(s : non_unital_subsemiring T)
(g : G)
(f : F) :
def
non_unital_subsemiring.map
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(s : non_unital_subsemiring R) :
The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring.
@[simp]
theorem
non_unital_subsemiring.coe_map
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(s : non_unital_subsemiring R) :
@[simp]
theorem
non_unital_subsemiring.mem_map
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{f : F}
{s : non_unital_subsemiring R}
{y : S} :
@[simp]
theorem
non_unital_subsemiring.map_id
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R) :
theorem
non_unital_subsemiring.map_map
{R : Type u}
{S : Type v}
{T : Type w}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
[non_unital_non_assoc_semiring T]
{F : Type u_1}
{G : Type u_2}
[non_unital_ring_hom_class F R S]
[non_unital_ring_hom_class G S T]
(s : non_unital_subsemiring R)
(g : G)
(f : F) :
theorem
non_unital_subsemiring.map_le_iff_le_comap
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{f : F}
{s : non_unital_subsemiring R}
{t : non_unital_subsemiring S} :
non_unital_subsemiring.map f s ≤ t ↔ s ≤ non_unital_subsemiring.comap f t
theorem
non_unital_subsemiring.gc_map_comap
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
noncomputable
def
non_unital_subsemiring.equiv_map_of_injective
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(s : non_unital_subsemiring R)
(f : F)
(hf : function.injective ⇑f) :
↥s ≃+* ↥(non_unital_subsemiring.map f s)
A non-unital subsemiring is isomorphic to its image under an injective function
@[simp]
theorem
non_unital_subsemiring.coe_equiv_map_of_injective_apply
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(s : non_unital_subsemiring R)
(f : F)
(hf : function.injective ⇑f)
(x : ↥s) :
def
non_unital_ring_hom.srange
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
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
@[simp]
theorem
non_unital_ring_hom.coe_srange
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
@[simp]
theorem
non_unital_ring_hom.mem_srange
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{f : F}
{y : S} :
theorem
non_unital_ring_hom.srange_eq_map
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
theorem
non_unital_ring_hom.mem_srange_self
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(x : R) :
⇑f x ∈ non_unital_ring_hom.srange f
theorem
non_unital_ring_hom.map_srange
{R : Type u}
{S : Type v}
{T : Type w}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
[non_unital_non_assoc_semiring T]
(g : S →ₙ+* T)
(f : R →ₙ+* S) :
@[protected, instance]
def
non_unital_ring_hom.finite_srange
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
[finite R]
(f : F) :
The range of a morphism of non-unital semirings is finite if the domain is a finite.
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
The inf of two non-unital subsemirings is their intersection.
@[simp]
theorem
non_unital_subsemiring.coe_inf
{R : Type u}
[non_unital_non_assoc_semiring R]
(p p' : non_unital_subsemiring R) :
@[simp]
theorem
non_unital_subsemiring.mem_inf
{R : Type u}
[non_unital_non_assoc_semiring R]
{p p' : non_unital_subsemiring R}
{x : R} :
@[protected, instance]
Equations
- non_unital_subsemiring.has_Inf = {Inf := λ (s : set (non_unital_subsemiring R)), non_unital_subsemiring.mk' (⋂ (t : non_unital_subsemiring R) (H : t ∈ s), ↑t) (⨅ (t : non_unital_subsemiring R) (H : t ∈ s), t.to_subsemigroup) _ (⨅ (t : non_unital_subsemiring R) (H : t ∈ s), t.to_add_submonoid) _}
@[simp, norm_cast]
theorem
non_unital_subsemiring.coe_Inf
{R : Type u}
[non_unital_non_assoc_semiring R]
(S : set (non_unital_subsemiring R)) :
↑(has_Inf.Inf S) = ⋂ (s : non_unital_subsemiring R) (H : s ∈ S), ↑s
theorem
non_unital_subsemiring.mem_Inf
{R : Type u}
[non_unital_non_assoc_semiring R]
{S : set (non_unital_subsemiring R)}
{x : R} :
x ∈ has_Inf.Inf S ↔ ∀ (p : non_unital_subsemiring R), p ∈ S → x ∈ p
@[simp]
theorem
non_unital_subsemiring.Inf_to_subsemigroup
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : set (non_unital_subsemiring R)) :
(has_Inf.Inf s).to_subsemigroup = ⨅ (t : non_unital_subsemiring R) (H : t ∈ s), t.to_subsemigroup
@[simp]
theorem
non_unital_subsemiring.Inf_to_add_submonoid
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : set (non_unital_subsemiring R)) :
(has_Inf.Inf s).to_add_submonoid = ⨅ (t : non_unital_subsemiring R) (H : t ∈ s), t.to_add_submonoid
@[protected, instance]
Non-unital subsemirings of a non-unital semiring form a complete lattice.
Equations
- non_unital_subsemiring.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (non_unital_subsemiring R) non_unital_subsemiring.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (non_unital_subsemiring R) non_unital_subsemiring.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (non_unital_subsemiring R) non_unital_subsemiring.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf non_unital_subsemiring.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (non_unital_subsemiring R) non_unital_subsemiring.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (non_unital_subsemiring R) non_unital_subsemiring.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
theorem
non_unital_subsemiring.eq_top_iff'
{R : Type u}
[non_unital_non_assoc_semiring R]
(A : non_unital_subsemiring R) :
The center of a semiring R is the set of elements that commute with everything in R
Equations
- non_unital_subsemiring.center R = {carrier := set.center R (distrib.to_has_mul R), add_mem' := _, zero_mem' := _, mul_mem' := _}
Instances for ↥non_unital_subsemiring.center
@[simp]
@[protected, instance]
def
non_unital_subsemiring.decidable_mem_center
{R : Type u_1}
[non_unital_semiring R]
[decidable_eq R]
[fintype R] :
decidable_pred (λ (_x : R), _x ∈ non_unital_subsemiring.center R)
Equations
- non_unital_subsemiring.decidable_mem_center = λ (_x : R), decidable_of_iff' (∀ (g : R), g * _x = _x * g) non_unital_subsemiring.mem_center_iff
@[simp]
@[protected, instance]
The center is commutative.
Equations
- non_unital_subsemiring.center.non_unital_comm_semiring = {add := non_unital_semiring.add (non_unital_subsemiring_class.to_non_unital_semiring (non_unital_subsemiring.center R)), add_assoc := _, zero := non_unital_semiring.zero (non_unital_subsemiring_class.to_non_unital_semiring (non_unital_subsemiring.center R)), zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul (non_unital_subsemiring_class.to_non_unital_semiring (non_unital_subsemiring.center R)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semigroup.mul subsemigroup.center.comm_semigroup, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
The centralizer of a set as non-unital subsemiring.
Equations
- non_unital_subsemiring.centralizer s = {carrier := s.centralizer (distrib.to_has_mul R), add_mem' := _, zero_mem' := _, mul_mem' := _}
@[simp, norm_cast]
theorem
non_unital_subsemiring.centralizer_to_subsemigroup
{R : Type u_1}
[non_unital_semiring R]
(s : set R) :
theorem
non_unital_subsemiring.mem_centralizer_iff
{R : Type u_1}
[non_unital_semiring R]
{s : set R}
{z : R} :
theorem
non_unital_subsemiring.center_le_centralizer
{R : Type u_1}
[non_unital_semiring R]
(s : set R) :
theorem
non_unital_subsemiring.centralizer_le
{R : Type u_1}
[non_unital_semiring R]
(s t : set R)
(h : s ⊆ t) :
@[simp]
theorem
non_unital_subsemiring.centralizer_eq_top_iff_subset
{R : Type u_1}
[non_unital_semiring R]
{s : set R} :
@[simp]
The non_unital_subsemiring generated by a set.
Equations
- non_unital_subsemiring.closure s = has_Inf.Inf {S : non_unital_subsemiring R | s ⊆ ↑S}
theorem
non_unital_subsemiring.mem_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
{x : R}
{s : set R} :
x ∈ non_unital_subsemiring.closure s ↔ ∀ (S : non_unital_subsemiring R), s ⊆ ↑S → x ∈ S
@[simp]
theorem
non_unital_subsemiring.subset_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : set R} :
The non-unital subsemiring generated by a set includes the set.
theorem
non_unital_subsemiring.not_mem_of_not_mem_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : set R}
{P : R}
(hP : P ∉ non_unital_subsemiring.closure s) :
P ∉ s
@[simp]
theorem
non_unital_subsemiring.closure_le
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : set R}
{t : non_unital_subsemiring R} :
non_unital_subsemiring.closure s ≤ t ↔ s ⊆ ↑t
A non-unital subsemiring S includes closure s if and only if it includes s.
theorem
non_unital_subsemiring.closure_mono
{R : Type u}
[non_unital_non_assoc_semiring R]
⦃s t : set R⦄
(h : s ⊆ t) :
Subsemiring closure of a set is monotone in its argument: if s ⊆ t,
then closure s ≤ closure t.
theorem
non_unital_subsemiring.closure_eq_of_le
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : set R}
{t : non_unital_subsemiring R}
(h₁ : s ⊆ ↑t)
(h₂ : t ≤ non_unital_subsemiring.closure s) :
theorem
non_unital_subsemiring.mem_map_equiv
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{f : R ≃+* S}
{K : non_unital_subsemiring R}
{x : S} :
theorem
non_unital_subsemiring.map_equiv_eq_comap_symm
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(f : R ≃+* S)
(K : non_unital_subsemiring R) :
theorem
non_unital_subsemiring.comap_equiv_eq_map_symm
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(f : R ≃+* S)
(K : non_unital_subsemiring S) :
def
subsemigroup.non_unital_subsemiring_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
(M : subsemigroup R) :
The additive closure of a non-unital subsemigroup is a non-unital subsemiring.
Equations
- M.non_unital_subsemiring_closure = {carrier := (add_submonoid.closure ↑M).carrier, add_mem' := _, zero_mem' := _, mul_mem' := _}
theorem
subsemigroup.non_unital_subsemiring_closure_coe
{R : Type u}
[non_unital_non_assoc_semiring R]
(M : subsemigroup R) :
theorem
subsemigroup.non_unital_subsemiring_closure_eq_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
(M : subsemigroup R) :
The non_unital_subsemiring generated by a multiplicative subsemigroup coincides with the
non_unital_subsemiring.closure of the subsemigroup itself .
@[simp]
theorem
non_unital_subsemiring.closure_subsemigroup_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : set R) :
theorem
non_unital_subsemiring.coe_closure_eq
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : set R) :
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.mem_closure_iff
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : set R}
{x : R} :
@[simp]
theorem
non_unital_subsemiring.closure_add_submonoid_closure
{R : Type u}
[non_unital_non_assoc_semiring R]
{s : set R} :
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
- non_unital_subsemiring.gi R = {choice := λ (s : set R) (_x : ↑(non_unital_subsemiring.closure s) ≤ s), non_unital_subsemiring.closure s, gc := _, le_l_u := _, choice_eq := _}
theorem
non_unital_subsemiring.closure_eq
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R) :
Closure of a non-unital subsemiring S equals S.
@[simp]
@[simp]
theorem
non_unital_subsemiring.closure_union
{R : Type u}
[non_unital_non_assoc_semiring R]
(s t : set R) :
theorem
non_unital_subsemiring.closure_Union
{R : Type u}
[non_unital_non_assoc_semiring R]
{ι : Sort u_1}
(s : ι → set R) :
non_unital_subsemiring.closure (⋃ (i : ι), s i) = ⨆ (i : ι), non_unital_subsemiring.closure (s i)
theorem
non_unital_subsemiring.closure_sUnion
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : set (set R)) :
non_unital_subsemiring.closure (⋃₀ s) = ⨆ (t : set R) (H : t ∈ s), non_unital_subsemiring.closure t
theorem
non_unital_subsemiring.map_sup
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(s t : non_unital_subsemiring R)
(f : F) :
non_unital_subsemiring.map f (s ⊔ t) = non_unital_subsemiring.map f s ⊔ non_unital_subsemiring.map f t
theorem
non_unital_subsemiring.map_supr
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{ι : Sort u_2}
(f : F)
(s : ι → non_unital_subsemiring R) :
non_unital_subsemiring.map f (supr s) = ⨆ (i : ι), non_unital_subsemiring.map f (s i)
theorem
non_unital_subsemiring.comap_inf
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(s t : non_unital_subsemiring S)
(f : F) :
theorem
non_unital_subsemiring.comap_infi
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{ι : Sort u_2}
(f : F)
(s : ι → non_unital_subsemiring S) :
non_unital_subsemiring.comap f (infi s) = ⨅ (i : ι), non_unital_subsemiring.comap f (s i)
@[simp]
theorem
non_unital_subsemiring.map_bot
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
@[simp]
theorem
non_unital_subsemiring.comap_top
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
def
non_unital_subsemiring.prod
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(s : non_unital_subsemiring R)
(t : non_unital_subsemiring S) :
non_unital_subsemiring (R × 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.
@[norm_cast]
theorem
non_unital_subsemiring.coe_prod
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(s : non_unital_subsemiring R)
(t : non_unital_subsemiring S) :
theorem
non_unital_subsemiring.mem_prod
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{s : non_unital_subsemiring R}
{t : non_unital_subsemiring S}
{p : R × S} :
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₂) :
theorem
non_unital_subsemiring.prod_mono_right
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(s : non_unital_subsemiring R) :
monotone (λ (t : non_unital_subsemiring S), s.prod t)
theorem
non_unital_subsemiring.prod_mono_left
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(t : non_unital_subsemiring S) :
monotone (λ (s : non_unital_subsemiring R), s.prod t)
theorem
non_unital_subsemiring.prod_top
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(s : non_unital_subsemiring R) :
theorem
non_unital_subsemiring.top_prod
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(s : non_unital_subsemiring S) :
@[simp]
theorem
non_unital_subsemiring.top_prod_top
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S] :
def
non_unital_subsemiring.prod_equiv
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(s : non_unital_subsemiring R)
(t : non_unital_subsemiring S) :
Product of non-unital subsemirings is isomorphic to their product as semigroups.
theorem
non_unital_subsemiring.mem_Sup_of_directed_on
{R : Type u}
[non_unital_non_assoc_semiring R]
{S : set (non_unital_subsemiring R)}
(Sne : S.nonempty)
(hS : directed_on has_le.le S)
{x : R} :
x ∈ has_Sup.Sup S ↔ ∃ (s : non_unital_subsemiring R) (H : s ∈ S), x ∈ s
theorem
non_unital_subsemiring.coe_Sup_of_directed_on
{R : Type u}
[non_unital_non_assoc_semiring R]
{S : set (non_unital_subsemiring R)}
(Sne : S.nonempty)
(hS : directed_on has_le.le S) :
↑(has_Sup.Sup S) = ⋃ (s : non_unital_subsemiring R) (H : s ∈ S), ↑s
def
non_unital_ring_hom.cod_restrict
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(s : non_unital_subsemiring S)
(h : ∀ (x : R), ⇑f x ∈ s) :
Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.
def
non_unital_ring_hom.srange_restrict
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
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.
@[simp]
theorem
non_unital_ring_hom.coe_srange_restrict
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(x : R) :
↑(⇑(non_unital_ring_hom.srange_restrict f) x) = ⇑f x
theorem
non_unital_ring_hom.srange_restrict_surjective
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F) :
theorem
non_unital_ring_hom.srange_top_iff_surjective
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{f : F} :
theorem
non_unital_ring_hom.srange_top_of_surjective
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(hf : function.surjective ⇑f) :
The range of a surjective non-unital ring homomorphism is the whole of the codomain.
def
non_unital_ring_hom.eq_slocus
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f g : F) :
The non-unital subsemiring of elements x : R such that f x = g x
theorem
non_unital_ring_hom.eq_on_sclosure
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{f g : F}
{s : set R}
(h : set.eq_on ⇑f ⇑g s) :
If two non-unital ring homomorphisms are equal on a set, then they are equal on its non-unital subsemiring closure.
theorem
non_unital_ring_hom.eq_of_eq_on_stop
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{f g : F}
(h : set.eq_on ⇑f ⇑g ↑⊤) :
f = g
theorem
non_unital_ring_hom.eq_of_eq_on_sdense
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{s : set R}
(hs : non_unital_subsemiring.closure s = ⊤)
{f g : F}
(h : set.eq_on ⇑f ⇑g s) :
f = g
theorem
non_unital_ring_hom.sclosure_preimage_le
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(s : set S) :
theorem
non_unital_ring_hom.map_sclosure
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
(f : F)
(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
non_unital_subsemiring.inclusion
{R : Type u}
[non_unital_non_assoc_semiring R]
{S T : non_unital_subsemiring R}
(h : S ≤ T) :
The non-unital ring homomorphism associated to an inclusion of non-unital subsemirings.
@[simp]
theorem
non_unital_subsemiring.srange_subtype
{R : Type u}
[non_unital_non_assoc_semiring R]
(s : non_unital_subsemiring R) :
@[simp]
theorem
non_unital_subsemiring.range_fst
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S] :
@[simp]
theorem
non_unital_subsemiring.range_snd
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S] :
def
ring_equiv.non_unital_subsemiring_congr
{R : Type u}
[non_unital_non_assoc_semiring R]
{s t : non_unital_subsemiring R}
(h : s = t) :
Makes the identity isomorphism from a proof two non-unital subsemirings of a multiplicative monoid are equal.
Equations
- ring_equiv.non_unital_subsemiring_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
def
ring_equiv.sof_left_inverse'
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{g : S → R}
{f : F}
(h : function.left_inverse g ⇑f) :
Restrict a non-unital ring homomorphism with a left inverse to a ring isomorphism to its
non_unital_ring_hom.srange.
Equations
- ring_equiv.sof_left_inverse' h = {to_fun := ⇑(non_unital_ring_hom.srange_restrict f), inv_fun := λ (x : ↥(non_unital_ring_hom.srange f)), g (⇑(non_unital_subsemiring_class.subtype (non_unital_ring_hom.srange f)) x), left_inv := h, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
ring_equiv.sof_left_inverse'_apply
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{g : S → R}
{f : F}
(h : function.left_inverse g ⇑f)
(x : R) :
↑(⇑(ring_equiv.sof_left_inverse' h) x) = ⇑f x
@[simp]
theorem
ring_equiv.sof_left_inverse'_symm_apply
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
{F : Type u_1}
[non_unital_ring_hom_class F R S]
{g : S → R}
{f : F}
(h : function.left_inverse g ⇑f)
(x : ↥(non_unital_ring_hom.srange f)) :
⇑((ring_equiv.sof_left_inverse' h).symm) x = g ↑x
@[simp]
theorem
ring_equiv.non_unital_subsemiring_map_symm_apply
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(e : R ≃+* S)
(s : non_unital_subsemiring R)
(ᾰ : ↥(add_submonoid.map e.to_add_equiv.to_add_monoid_hom s.to_add_submonoid)) :
⇑((e.non_unital_subsemiring_map s).symm) ᾰ = (e.to_add_equiv.add_submonoid_map s.to_add_submonoid).inv_fun ᾰ
@[simp]
theorem
ring_equiv.non_unital_subsemiring_map_apply
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(e : R ≃+* S)
(s : non_unital_subsemiring R)
(ᾰ : ↥(s.to_add_submonoid)) :
⇑(e.non_unital_subsemiring_map s) ᾰ = (e.to_add_equiv.add_submonoid_map s.to_add_submonoid).to_fun ᾰ
def
ring_equiv.non_unital_subsemiring_map
{R : Type u}
{S : Type v}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(e : R ≃+* S)
(s : non_unital_subsemiring R) :
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
- e.non_unital_subsemiring_map s = {to_fun := (e.to_add_equiv.add_submonoid_map s.to_add_submonoid).to_fun, inv_fun := (e.to_add_equiv.add_submonoid_map s.to_add_submonoid).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}