Pointwise instances on Submonoid
s and AddSubmonoid
s #
This file provides:
and the actions
which matches the action of Set.mulActionSet
.
SMul (AddSubmonoid R) (AddSubmonoid A)
is also provided given DistribSMul R A
,
and when R = A
it is definitionally equal to the multiplication on AddSubmonoid R
.
These are all available in the Pointwise
locale.
Additionally, it provides various degrees of monoid structure:
AddSubmonoid.one
AddSubmonoid.mul
AddSubmonoid.mulOneClass
AddSubmonoid.semigroup
AddSubmonoid.monoid
which is available globally to match the monoid structure implied bySubmodule.idemSemiring
.
Implementation notes #
Most of the lemmas in this file are direct copies of lemmas from Algebra/Pointwise.lean
.
While the statements of these lemmas are defeq, we repeat them here due to them not being
syntactically equal. Before adding new lemmas here, consider if they would also apply to the action
on Set
s.
Many results about multiplication is derived from the corresponding results about
scalar multiplication, but results requiring right distributivity do not have
SMul versions, due to the lack of a suitable typeclass (unless one goes all the
way to Module
).
Some lemmas about pointwise multiplication and submonoids. Ideally we put these in
GroupTheory.Submonoid.Basic
, but currently we cannot because that file is imported by this.
The additive submonoid with every element negated.
Equations
- AddSubmonoid.neg = { neg := fun (S : AddSubmonoid G) => { carrier := -↑S, add_mem' := ⋯, zero_mem' := ⋯ } }
Instances For
Inversion is involutive on submonoids.
Equations
- Submonoid.involutiveInv = Function.Injective.involutiveInv SetLike.coe ⋯ ⋯
Instances For
Inversion is involutive on additive submonoids.
Equations
- AddSubmonoid.involutiveNeg = Function.Injective.involutiveNeg SetLike.coe ⋯ ⋯
Instances For
Pointwise negation of additive submonoids as an order isomorphism
Equations
- AddSubmonoid.negOrderIso = { toEquiv := Equiv.neg (AddSubmonoid G), map_rel_iff' := ⋯ }
Instances For
The action on a submonoid corresponding to applying the action to every element.
This is available as an instance in the Pointwise
locale.
Equations
- Submonoid.pointwiseMulAction = MulAction.mk ⋯ ⋯
Instances For
The action on an additive submonoid corresponding to applying the action to every element.
This is available as an instance in the Pointwise
locale.
Equations
- AddSubmonoid.pointwiseMulAction = MulAction.mk ⋯ ⋯
Instances For
Elementwise monoid structure of additive submonoids #
These definitions are a cut-down versions of the ones around Submodule.mul
, as that API is
usually more useful.
If R
is an additive monoid with one (e.g., a semiring), then 1 : AddSubmonoid R
is the range
of Nat.cast : ℕ → R
.
Equations
- AddSubmonoid.one = { one := AddMonoidHom.mrange (Nat.castAddMonoidHom R) }
Instances For
For M : Submonoid R
and N : AddSubmonoid A
, M • N
is the additive submonoid
generated by all m • n
where m ∈ M
and n ∈ N
.
Equations
- AddSubmonoid.smul = { smul := fun (M : AddSubmonoid R) (N : AddSubmonoid A) => ⨆ (s : ↥M), AddSubmonoid.map (DistribSMul.toAddMonoidHom A ↑s) N }
Instances For
Multiplication of additive submonoids of a semiring R. The additive submonoid S * T
is the
smallest R-submodule of R
containing the elements s * t
for s ∈ S
and t ∈ T
.
Equations
- AddSubmonoid.mul = { mul := fun (M N : AddSubmonoid R) => ⨆ (s : ↥M), AddSubmonoid.map (AddMonoidHom.mul ↑s) N }
Instances For
AddSubmonoid.neg
distributes over multiplication.
This is available as an instance in the Pointwise
locale.
Equations
- AddSubmonoid.hasDistribNeg = HasDistribNeg.mk ⋯ ⋯
Instances For
A MulOneClass
structure on additive submonoids of a (possibly, non-associative) semiring.
Equations
- AddSubmonoid.mulOneClass = MulOneClass.mk ⋯ ⋯
Instances For
Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.
Equations
- AddSubmonoid.semigroup = Semigroup.mk ⋯
Instances For
Monoid structure on additive submonoids of a semiring.