Pointwise instances on Submonoid
s and AddSubmonoid
s #
This file provides:
and the actions
which matches the action of Set.mulActionSet
.
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.
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 additive submonoids.
Equations
- AddSubmonoid.involutiveNeg = Function.Injective.involutiveNeg SetLike.coe ⋯ ⋯
Instances For
Inversion is involutive on submonoids.
Equations
- Submonoid.involutiveInv = Function.Injective.involutiveInv 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
Equations
- ⋯ = ⋯
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
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.