mathlib3 documentation

ring_theory.subring.pointwise

Pointwise instances on subrings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the action subring.pointwise_mul_action which matches the action of mul_action_set.

This actions is available in the pointwise locale.

Implementation notes #

This file is almost identical to ring_theory/subsemiring/pointwise.lean. Where possible, try to keep them in sync.

source
@[protected]
def subring.pointwise_mul_action {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] :
mul_action M (subring R)

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

This is available as an instance in the pointwise locale.

Equations
source
theorem subring.pointwise_smul_def {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] {a : M} (S : subring R) :
a • S = subring.map (mul_semiring_action.to_ring_hom M R a) S
source
@[simp]
theorem subring.coe_pointwise_smul {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (m : M) (S : subring R) :
↑(m • S) = m • ↑S
source
@[simp]
theorem subring.pointwise_smul_to_add_subgroup {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (m : M) (S : subring R) :
(m • S).to_add_subgroup = m • S.to_add_subgroup
source
@[simp]
theorem subring.pointwise_smul_to_subsemiring {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (m : M) (S : subring R) :
(m • S).to_subsemiring = m • S.to_subsemiring
source
theorem subring.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (m : M) (r : R) (S : subring R) :
r ∈ S → m • r ∈ m • S
source
theorem subring.mem_smul_pointwise_iff_exists {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (m : M) (r : R) (S : subring R) :
r ∈ m • S ↔ ∃ (s : R), s ∈ S ∧ m • s = r
source
@[simp]
theorem subring.smul_bot {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (a : M) :
a • ⊥ = ⊥
source
theorem subring.smul_sup {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (a : M) (S T : subring R) :
a • (S ⊔ T) = a • S ⊔ a • T
source
theorem subring.smul_closure {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] (a : M) (s : set R) :
a • subring.closure s = subring.closure (a • s)
source
@[protected, instance]
def subring.pointwise_central_scalar {M : Type u_1} {R : Type u_2} [monoid M] [ring R] [mul_semiring_action M R] [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
is_central_scalar M (subring R)
source
@[simp]
theorem subring.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [ring R] [mul_semiring_action M R] {a : M} {S : subring R} {x : R} :
a • x ∈ a • S ↔ x ∈ S
source
theorem subring.mem_pointwise_smul_iff_inv_smul_mem {M : Type u_1} {R : Type u_2} [group M] [ring R] [mul_semiring_action M R] {a : M} {S : subring R} {x : R} :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem subring.mem_inv_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [ring R] [mul_semiring_action M R] {a : M} {S : subring R} {x : R} :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem subring.pointwise_smul_le_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [ring R] [mul_semiring_action M R] {a : M} {S T : subring R} :
a • S ≤ a • T ↔ S ≤ T
source
theorem subring.pointwise_smul_subset_iff {M : Type u_1} {R : Type u_2} [group M] [ring R] [mul_semiring_action M R] {a : M} {S T : subring R} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem subring.subset_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [group M] [ring R] [mul_semiring_action M R] {a : M} {S T : subring R} :
S ≤ a • T ↔ a⁻¹ • S ≤ T

TODO: add equiv_smul like we have for subgroup.

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