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
Alias of natCast_mem
.
Equations
SubsemiringClass S R
states that S
is a type of subsets s ⊆ R
that
are both a multiplicative and an additive submonoid.
Instances
Equations
- ⋯ = ⋯
A subsemiring of a NonAssocSemiring
inherits a NonAssocSemiring
structure
Equations
- SubsemiringClass.toNonAssocSemiring s = Function.Injective.nonAssocSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The natural ring hom from a subsemiring of semiring R
to R
.
Equations
- SubsemiringClass.subtype s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
A subsemiring of a Semiring
is a Semiring
.
Equations
- SubsemiringClass.toSemiring s = Function.Injective.semiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subsemiring of a CommSemiring
is a CommSemiring
.
Equations
- SubsemiringClass.toCommSemiring s = Function.Injective.commSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Reinterpret a Subsemiring
as an AddSubmonoid
.
Equations
- self.toAddSubmonoid = { carrier := self.carrier, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
Equations
- Subsemiring.instSetLike = { coe := fun (s : Subsemiring R) => s.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
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.
Equations
- S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
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
.
Equations
- Subsemiring.mk' s sm hm sa ha = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
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
Equations
- s.toNonAssocSemiring = SubsemiringClass.toNonAssocSemiring s
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A subsemiring of a Semiring
is a Semiring
.
Equations
- s.toSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
A subsemiring of a CommSemiring
is a CommSemiring
.
Equations
- s.toCommSemiring = CommSemiring.mk ⋯
The natural ring hom from a subsemiring of semiring R
to R
.
Equations
- s.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The subsemiring R
of the semiring R
.
The preimage of a subsemiring along a ring homomorphism is a subsemiring.
Equations
- Subsemiring.comap f s = { carrier := ⇑f ⁻¹' ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
The image of a subsemiring along a ring homomorphism is a subsemiring.
Equations
- Subsemiring.map f s = { carrier := ⇑f '' ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
A subsemiring is isomorphic to its image under an injective function
Equations
- s.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑s) hf, map_mul' := ⋯, map_add' := ⋯ }
Instances For
The range of a ring homomorphism is a subsemiring. See Note [range copy pattern].
Equations
- f.rangeS = (Subsemiring.map f ⊤).copy (Set.range ⇑f) ⋯
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
.
Equations
- f.fintypeRangeS = Set.fintypeRange ⇑f
Equations
- Subsemiring.instBot = { bot := (Nat.castRingHom R).rangeS }
The inf of two subsemirings is their intersection.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Subsemiring.instInfSet = { sInf := fun (s : Set (Subsemiring R)) => Subsemiring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, t.toSubmonoid) ⋯ (⨅ t ∈ s, t.toAddSubmonoid) ⋯ }
Subsemirings of a semiring form a complete lattice.
Equations
- Subsemiring.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The center of a non-associative semiring R
is the set of elements that commute and associate
with everything in R
Equations
- Subsemiring.center R = { carrier := (NonUnitalSubsemiring.center R).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
The center is commutative and associative.
This is not an instance as it forms a non-defeq diamond with
NonUnitalSubringClass.tNonUnitalring
in the npow
field.
Equations
Instances For
The center is commutative.
Equations
- Subsemiring.center.commSemiring = CommSemiring.mk ⋯
Equations
- Subsemiring.decidableMemCenter x = decidable_of_iff' (∀ (g : R), g * x = x * g) ⋯
The centralizer of a set as subsemiring.
Equations
- Subsemiring.centralizer s = { carrier := s.centralizer, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
The Subsemiring
generated by a set.
Equations
- Subsemiring.closure s = sInf {S : Subsemiring R | s ⊆ ↑S}
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.
Equations
- M.subsemiringClosure = { carrier := (AddSubmonoid.closure ↑M).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
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.
Equations
- Subsemiring.gi R = { choice := fun (s : Set R) (x : ↑(Subsemiring.closure s) ≤ s) => Subsemiring.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
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
.
Equations
Instances For
Product of subsemirings is isomorphic to their product as monoids.
Equations
- s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Restriction of a ring homomorphism to a subsemiring of the domain.
Equations
- f.domRestrict s = f.comp (SubsemiringClass.subtype s)
Instances For
Restriction of a ring homomorphism to a subsemiring of the codomain.
Equations
- f.codRestrict s h = { toFun := fun (n : R) => ⟨f n, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The ring homomorphism from the preimage of s
to s
.
Equations
- f.restrict s' s h = (f.domRestrict s').codRestrict s ⋯
Instances For
Restriction of a ring homomorphism to its range interpreted as a subsemiring.
This is the bundled version of Set.rangeFactorization
.
Equations
- f.rangeSRestrict = f.codRestrict f.rangeS ⋯
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
Equations
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.
Equations
- Subsemiring.inclusion h = S.subtype.codRestrict T ⋯
Instances For
Makes the identity isomorphism from a proof two subsemirings of a multiplicative monoid are equal.
Equations
- RingEquiv.subsemiringCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
RingHom.rangeS
.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- e.subsemiringMap s = { toEquiv := (e.toAddEquiv.addSubmonoidMap s.toAddSubmonoid).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
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.
Equations
- S.smul = S.smul
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Note that this provides IsScalarTower S R R
which is needed by smul_mul_assoc
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.instSMulWithZeroSubtypeMem = SMulWithZero.compHom α ↑S.subtype.toMonoidWithZeroHom
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.mulAction = S.mulAction
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.distribMulAction = S.distribMulAction
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.mulDistribMulAction = S.mulDistribMulAction
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.mulActionWithZero = MulActionWithZero.compHom α S.subtype.toMonoidWithZeroHom
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.module = Module.compHom α S.subtype
The action by a subsemiring is the action by the underlying semiring.
Equations
- S.instMulSemiringActionSubtypeMem = S.mulSemiringAction
The center of a semiring acts commutatively on that semiring.
Equations
- ⋯ = ⋯
The center of a semiring acts commutatively on that semiring.
Equations
- ⋯ = ⋯