# Pointwise instances on `Subsemiring`s #

This file provides the action `Subsemiring.PointwiseMulAction` which matches the action of `MulActionSet`.

This actions is available in the `Pointwise` locale.

## Implementation notes #

This file is almost identical to the files `Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean` and `Mathlib/Algebra/Ring/Submonoid/Pointwise.lean`. Where possible, try to keep them in sync.

source
def Subsemiring.pointwiseMulAction {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] :
MulAction M (Subsemiring R)

The action on a subsemiring corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.

Equations

- Subsemiring.pointwiseMulAction = { smul := fun (a : M) (S : Subsemiring R) => Subsemiring.map (MulSemiringAction.toRingHom M R a) S, one_smul := ⋯, mul_smul := ⋯ }

Instances For

source
theorem Subsemiring.pointwise_smul_def {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] {a : M} (S : Subsemiring R) :
a • S = map (MulSemiringAction.toRingHom M R a) S
source
@[simp]
theorem Subsemiring.coe_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (S : Subsemiring R) :
↑(m • S) = m • ↑S
source
@[simp]
theorem Subsemiring.pointwise_smul_toAddSubmonoid {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (S : Subsemiring R) :
(m • S).toAddSubmonoid = m • S.toAddSubmonoid
source
theorem Subsemiring.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subsemiring R) :
r ∈ S → m • r ∈ m • S
source
instance Subsemiring.instCovariantClassHSMulLe {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] :
CovariantClass M (Subsemiring R) HSMul.hSMul LE.le
source
theorem Subsemiring.mem_smul_pointwise_iff_exists {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subsemiring R) :
r ∈ m • S ↔ ∃ s ∈ S, m • s = r
source
@[simp]
theorem Subsemiring.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) :
a • ⊥ = ⊥
source
theorem Subsemiring.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) (S T : Subsemiring R) :
a • (S ⊔ T) = a • S ⊔ a • T
source
theorem Subsemiring.smul_closure {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) (s : Set R) :
a • closure s = closure (a • s)
source
instance Subsemiring.pointwise_central_scalar {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] [MulSemiringAction M ᵐᵒᵖ R] [IsCentralScalar M R] :
IsCentralScalar M (Subsemiring R)
source
@[simp]
theorem Subsemiring.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} {S : Subsemiring R} {x : R} :
a • x ∈ a • S ↔ x ∈ S
source
theorem Subsemiring.mem_pointwise_smul_iff_inv_smul_mem {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} {S : Subsemiring R} {x : R} :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem Subsemiring.mem_inv_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} {S : Subsemiring R} {x : R} :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem Subsemiring.pointwise_smul_le_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} {S T : Subsemiring R} :
a • S ≤ a • T ↔ S ≤ T
source
theorem Subsemiring.pointwise_smul_subset_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} {S T : Subsemiring R} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem Subsemiring.subset_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} {S T : Subsemiring R} :
S ≤ a • T ↔ a⁻¹ • S ≤ T

TODO: add `equiv_smul` like we have for subgroup.

source
@[simp]
theorem Subsemiring.smul_mem_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) (S : Subsemiring R) (x : R) :
a • x ∈ a • S ↔ x ∈ S
source
theorem Subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) (S : Subsemiring R) (x : R) :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem Subsemiring.mem_inv_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) (S : Subsemiring R) (x : R) :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem Subsemiring.pointwise_smul_le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) {S T : Subsemiring R} :
a • S ≤ a • T ↔ S ≤ T
source
theorem Subsemiring.pointwise_smul_le_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) {S T : Subsemiring R} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem Subsemiring.le_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Semiring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) {S T : Subsemiring R} :
S ≤ a • T ↔ a⁻¹ • S ≤ T