Bundled subsemirings #
We define bundled subsemirings and some standard constructions: CompleteLattice
structure,
Subtype
and inclusion
ring homomorphisms, subsemiring map
, comap
and range (rangeS
) of
a RingHom
etc.
AddSubmonoidWithOneClass S R
says S
is a type of subsets s ≤ R
that contain 0
, 1
,
and are closed under (+)
Instances
SubsemiringClass S R
states that S
is a type of subsets s ⊆ R
that
are both a multiplicative and an additive submonoid.
Instances
A subsemiring of a NonAssocSemiring
inherits a NonAssocSemiring
structure
The natural ring hom from a subsemiring of semiring R
to R
.
Instances For
A subsemiring of a CommSemiring
is a CommSemiring
.
A subsemiring of an OrderedSemiring
is an OrderedSemiring
.
A subsemiring of a StrictOrderedSemiring
is a StrictOrderedSemiring
.
A subsemiring of an OrderedCommSemiring
is an OrderedCommSemiring
.
A subsemiring of a StrictOrderedCommSemiring
is a StrictOrderedCommSemiring
.
A subsemiring of a LinearOrderedSemiring
is a LinearOrderedSemiring
.
A subsemiring of a LinearOrderedCommSemiring
is a LinearOrderedCommSemiring
.
Reinterpret a Subsemiring
as an AddSubmonoid
.
Instances For
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.
Instances For
Construct a Subsemiring R
from a set s
, a submonoid sm
, and an additive
submonoid sa
such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa
.
Instances For
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 CommSemiring
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 CommSemiring
indexed by a Finset
is in the
subsemiring.
Sum of elements in a Subsemiring
of a Semiring
indexed by a Finset
is in the add_subsemiring
.
A subsemiring of a NonAssocSemiring
inherits a NonAssocSemiring
structure
A subsemiring of a CommSemiring
is a CommSemiring
.
The natural ring hom from a subsemiring of semiring R
to R
.
Instances For
A subsemiring of an OrderedSemiring
is an OrderedSemiring
.
A subsemiring of a StrictOrderedSemiring
is a StrictOrderedSemiring
.
A subsemiring of an OrderedCommSemiring
is an OrderedCommSemiring
.
A subsemiring of a StrictOrderedCommSemiring
is a StrictOrderedCommSemiring
.
A subsemiring of a LinearOrderedSemiring
is a LinearOrderedSemiring
.
A subsemiring of a LinearOrderedCommSemiring
is a LinearOrderedCommSemiring
.
The subsemiring R
of the semiring R
.
The ring equiv between the top element of Subsemiring R
and R
.
Instances For
The preimage of a subsemiring along a ring homomorphism is a subsemiring.
Instances For
The image of a subsemiring along a ring homomorphism is a subsemiring.
Instances For
A subsemiring is isomorphic to its image under an injective function
Instances For
The range of a ring homomorphism is a subsemiring. See Note [range copy pattern].
Instances For
The range of a morphism of semirings is a fintype, if the domain is a fintype.
Note: this instance can form a diamond with Subtype.fintype
in the
presence of Fintype S
.
The inf of two subsemirings is their intersection.
Subsemirings of a 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 subsemiring.
Instances For
The Subsemiring
generated by a set.
Instances For
The subsemiring generated by a set includes the set.
A 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 submonoid is a subsemiring.
Instances For
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
.
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 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
.
Instances For
Product of subsemirings is isomorphic to their product as monoids.
Instances For
Restriction of a ring homomorphism to a subsemiring of the domain.
Instances For
Restriction of a ring homomorphism to a subsemiring of the codomain.
Instances For
The ring homomorphism from the preimage of s
to s
.
Instances For
Restriction of a ring homomorphism to its range interpreted as a subsemiring.
This is the bundled version of Set.rangeFactorization
.
Instances For
The range of a surjective ring homomorphism is the whole of the codomain.
The subsemiring of elements x : R
such that f x = g x
Instances For
If two ring homomorphisms are equal on a set, then they are equal on its 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 ring homomorphism associated to an inclusion of subsemirings.
Instances For
Makes the identity isomorphism from a proof two subsemirings of a multiplicative monoid are equal.
Instances For
Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
RingHom.rangeS
.
Instances For
Given an equivalence e : R ≃+* S
of semirings and a subsemiring s
of R
,
subsemiring_map e s
is the induced equivalence between s
and s.map e
Instances For
Actions by Subsemiring
s #
These are just copies of the definitions about Submonoid
starting from submonoid.mul_action
.
The only new result is subsemiring.module
.
When R
is commutative, Algebra.ofSubsemiring
provides a stronger result than those found in
this file, which uses the same scalar action.
The action by a subsemiring is the action by the underlying semiring.
Note that this provides IsScalarTower S R R
which is needed by smul_mul_assoc
.
The action by a subsemiring is the action by the underlying semiring.
The action by a subsemiring is the action by the underlying semiring.
The action by a subsemiring is the action by the underlying semiring.
The action by a subsemiring is the action by the underlying semiring.
The action by a subsemiring is the action by the underlying semiring.
The action by a subsemiring is the action by the underlying semiring.
The action by a subsemiring is the action by the underlying semiring.
The center of a semiring acts commutatively on that semiring.
The center of a semiring acts commutatively on that semiring.
If all the elements of a set s
commute, then closure s
is a commutative monoid.
Instances For
Submonoid of positive elements of an ordered semiring.