Bundled non-unital subsemirings #
We define bundled non-unital subsemirings and some standard constructions:
CompleteLattice
structure, subtype
and inclusion
ring homomorphisms, non-unital subsemiring
map
, comap
and range (srange
) of a NonUnitalRingHom
etc.
- zero_mem : ∀ (s : S), 0 ∈ s
NonUnitalSubsemiringClass S R
states that S
is a type of subsets s ⊆ R
that
are both an additive submonoid and also a multiplicative subsemigroup.
Instances
A non-unital subsemiring of a NonUnitalNonAssocSemiring
inherits a
NonUnitalNonAssocSemiring
structure
The natural non-unital ring hom from a non-unital subsemiring of a non-unital semiring R
to
R
.
Instances For
A non-unital subsemiring of a NonUnitalSemiring
is a NonUnitalSemiring
.
A non-unital subsemiring of a NonUnitalCommSemiring
is a NonUnitalCommSemiring
.
Note: currently, there are no ordered versions of non-unital rings.
- carrier : Set R
- zero_mem' : 0 ∈ s.carrier
The product of two elements of a subsemigroup belongs to the subsemigroup.
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
Reinterpret a NonUnitalSubsemiring
as a Subsemigroup
.
Instances For
Two non-unital subsemirings are equal if they have the same elements.
Copy of a non-unital subsemiring with a new carrier
equal to the old one. Useful to fix
definitional equalities.
Instances For
Construct a NonUnitalSubsemiring R
from a set s
, a subsemigroup sg
, and an additive
submonoid sa
such that x ∈ s ↔ x ∈ sg ↔ x ∈ sa
.
Instances For
Note: currently, there are no ordered versions of non-unital rings.
The non-unital subsemiring R
of the non-unital semiring R
.
The ring equiv between the top element of NonUnitalSubsemiring R
and R
.
Instances For
The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a non-unital subsemiring.
Instances For
The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring.
Instances For
A non-unital subsemiring is isomorphic to its image under an injective function
Instances For
The range of a non-unital ring homomorphism is a non-unital subsemiring. See note [range copy pattern].
Instances For
The range of a morphism of non-unital semirings is finite if the domain is a finite.
The inf of two non-unital subsemirings is their intersection.
Non-unital subsemirings of a non-unital semiring form a complete lattice.
The center of a semiring R
is the set of elements that commute with everything in R
Instances For
The center is commutative.
The centralizer of a set as non-unital subsemiring.
Instances For
The NonUnitalSubsemiring
generated by a set.
Instances For
The non-unital subsemiring generated by a set includes the set.
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.
Instances For
The NonUnitalSubsemiring
generated by a multiplicative subsemigroup coincides with the
NonUnitalSubsemiring.closure
of the subsemigroup itself .
The elements of the non-unital subsemiring closure of M
are exactly the elements of the
additive closure of a multiplicative subsemigroup 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
.
An induction principle for closure membership for predicates with two arguments.
closure
forms a Galois insertion with the coercion to set.
Instances For
Closure of a non-unital subsemiring S
equals S
.
Given NonUnitalSubsemiring
s s
, t
of semirings R
, S
respectively, s.prod t
is
s × t
as a non-unital subsemiring of R × S
.
Instances For
Product of non-unital subsemirings is isomorphic to their product as semigroups.
Instances For
Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.
Instances For
Restriction of a non-unital ring homomorphism to its range interpreted as a non-unital subsemiring.
This is the bundled version of Set.rangeFactorization
.
Instances For
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
Instances For
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.
Instances For
Makes the identity isomorphism from a proof two non-unital subsemirings of a multiplicative monoid are equal.
Instances For
Restrict a non-unital ring homomorphism with a left inverse to a ring isomorphism to its
NonUnitalRingHom.srange
.
Instances For
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