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
.
Reinterpret a subsemiring
as a submonoid
.
- carrier : set R
- one_mem' : 1 ∈ c.carrier
- mul_mem' : ∀ {a b : R}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
- zero_mem' : 0 ∈ c.carrier
- add_mem' : ∀ {a b : R}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
A subsemiring of a semiring R
is a subset s
that is both a multiplicative and an additive
submonoid.
Equations
- subsemiring.set_like = {coe := subsemiring.carrier _inst_1, coe_injective' := _}
Two subsemirings are equal if they have the same elements.
Copy of a subsemiring with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Construct a subsemiring R
from a set s
, a submonoid sm
, and an additive
submonoid sa
such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa
.
A subsemiring contains the semiring's 1.
A subsemiring contains the semiring's 0.
A subsemiring is closed under multiplication.
A subsemiring is closed under addition.
Product of a list of elements in a subsemiring
is in the subsemiring
.
Sum of a list of elements in a subsemiring
is in the subsemiring
.
Product of a multiset of elements in a subsemiring
of a comm_semiring
is in the subsemiring
.
Sum of a multiset of elements in a subsemiring
of a semiring
is
in the add_subsemiring
.
Product of elements of a subsemiring of a comm_semiring
indexed by a finset
is in the
subsemiring.
Sum of elements in an subsemiring
of an semiring
indexed by a finset
is in the add_subsemiring
.
A subsemiring of a semiring inherits a semiring structure
Equations
- s.to_semiring = {add := add_comm_monoid.add s.to_add_submonoid.to_add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero s.to_add_submonoid.to_add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul s.to_add_submonoid.to_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul s.to_submonoid.to_monoid, mul_assoc := _, one := monoid.one s.to_submonoid.to_monoid, one_mul := _, mul_one := _, npow := npow s.to_submonoid.to_monoid, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
A subsemiring of a comm_semiring
is a comm_semiring
.
Equations
- s.to_comm_semiring = {add := semiring.add s.to_semiring, add_assoc := _, zero := semiring.zero s.to_semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul s.to_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul s.to_semiring, mul_assoc := _, one := semiring.one s.to_semiring, one_mul := _, mul_one := _, npow := semiring.npow s.to_semiring, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
A subsemiring of an ordered_semiring
is an ordered_semiring
.
Equations
- s.to_ordered_semiring = function.injective.ordered_semiring coe _ _ _ _ _
A subsemiring of an ordered_comm_semiring
is an ordered_comm_semiring
.
Equations
A subsemiring of a linear_ordered_semiring
is a linear_ordered_semiring
.
Equations
Note: currently, there is no linear_ordered_comm_semiring
.
The preimage of a subsemiring along a ring homomorphism is a subsemiring.
The image of a subsemiring along a ring homomorphism is a subsemiring.
The range of a ring homomorphism is a subsemiring. See Note [range copy pattern].
Equations
- subsemiring.has_bot = {bot := (nat.cast_ring_hom R).srange}
Equations
The inf of two subsemirings is their intersection.
Equations
- subsemiring.has_Inf = {Inf := λ (s : set (subsemiring R)), subsemiring.mk' (⋂ (t : subsemiring R) (H : t ∈ s), ↑t) (⨅ (t : subsemiring R) (H : t ∈ s), t.to_submonoid) _ (⨅ (t : subsemiring R) (H : t ∈ s), t.to_add_submonoid) _}
Subsemirings of a semiring form a complete lattice.
Equations
- subsemiring.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (subsemiring R) 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 subsemiring.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (subsemiring R) subsemiring.complete_lattice._proof_1), Inf_le := _, le_Inf := _}
The subsemiring
generated by a set.
Equations
- subsemiring.closure s = Inf {S : subsemiring R | s ⊆ ↑S}
The subsemiring generated by a set includes the set.
A subsemiring S
includes closure s
if and only if it includes s
.
The additive closure of a submonoid is a subsemiring.
The subsemiring
generated by a multiplicative submonoid coincides with the
subsemiring.closure
of the submonoid itself .
The elements of the subsemiring closure of M
are exactly the elements of the additive closure
of a multiplicative submonoid M
.
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
.
closure
forms a Galois insertion with the coercion to set.
Equations
- subsemiring.gi R = {choice := λ (s : set R) (_x : ↑(subsemiring.closure s) ≤ s), subsemiring.closure s, gc := _, le_l_u := _, choice_eq := _}
Closure of a subsemiring S
equals S
.
Given subsemiring
s s
, t
of semirings R
, S
respectively, s.prod t
is s × t
as a subsemiring of R × S
.
Product of subsemirings is isomorphic to their product as monoids.
Restriction of a ring homomorphism to a subsemiring of the codomain.
Restriction of a ring homomorphism to its range interpreted as a subsemiring.
This is the bundled version of set.range_factorization
.
Equations
- f.srange_restrict = f.cod_srestrict f.srange _
The range of a surjective ring homomorphism is the whole of the codomain.
The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.
The ring homomorphism associated to an inclusion of subsemirings.
Equations
- subsemiring.inclusion h = ↑(S.subtype.cod_srestrict T _)
Makes the identity isomorphism from a proof two subsemirings of a multiplicative monoid are equal.
Equations
- ring_equiv.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' := _}
Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
ring_hom.srange
.