Documentation

Mathlib.Algebra.Ring.Subring.Pointwise

Pointwise instances on Subrings #

This file provides the action Subring.pointwiseMulAction which matches the action of mulActionSet.

This actions is available in the Pointwise locale.

Implementation notes #

This file is almost identical to the file Mathlib/Algebra/Ring/Subsemiring/Pointwise.lean. Where possible, try to keep them in sync.

source
theorem Subring.coe_iSup_eq_iUnion_finset_coe_biSup {R : Type u_2} [NonAssocRing R] {ι : Type u_3} (S : ι → Subring R) :
↑(⨆ (i : ι), S i) = ⋃ (s : Finset ι), ↑(⨆ i ∈ s, S i)
source
@[instance_reducible]
def Subring.pointwiseMulAction {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] :
MulAction 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
Instances For
    source
    theorem Subring.pointwise_smul_def {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] {a : M} (S : Subring R) :
    a • S = map (MulSemiringAction.toRingHom M R a) S
    source
    @[simp]
    theorem Subring.coe_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (S : Subring R) :
    ↑(m • S) = m • ↑S
    source
    @[simp]
    theorem Subring.pointwise_smul_toAddSubgroup {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (S : Subring R) :
    (m • S).toAddSubgroup = m • S.toAddSubgroup
    source
    @[simp]
    theorem Subring.pointwise_smul_toSubsemiring {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (S : Subring R) :
    (m • S).toSubsemiring = m • S.toSubsemiring
    source
    theorem Subring.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subring R) :
    r ∈ S → m • r ∈ m • S
    source
    instance Subring.instCovariantClassHSMulLe {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] :
    CovariantClass M (Subring R) HSMul.hSMul LE.le
    source
    theorem Subring.mem_smul_pointwise_iff_exists {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (m : M) (r : R) (S : Subring R) :
    r ∈ m • S ↔ ∃ s ∈ S, m • s = r
    source
    @[simp]
    theorem Subring.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] (a : M) :
    a • ⊥ = ⊥
    source
    theorem Subring.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction 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] [MulSemiringAction M R] (a : M) (s : Set R) :
    a • closure s = closure (a • s)
    source
    instance Subring.pointwise_central_scalar {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] [MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R] :
    IsCentralScalar M (Subring R)
    source
    @[simp]
    theorem Subring.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Ring R] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction 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] [MulSemiringAction M R] {a : M} {S T : Subring R} :
    S ≤ a • T ↔ a⁻¹ • S ≤ T

    TODO: add equivSMul like we have for subgroup.

    source
    @[simp]
    theorem Subring.smul_mem_pointwise_smul_iff₀ {M : Type u_1} {R : Type u_2} [GroupWithZero M] [Ring R] [MulSemiringAction 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} [GroupWithZero M] [Ring R] [MulSemiringAction 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} [GroupWithZero M] [Ring R] [MulSemiringAction 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} [GroupWithZero M] [Ring R] [MulSemiringAction 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} [GroupWithZero M] [Ring R] [MulSemiringAction 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} [GroupWithZero M] [Ring R] [MulSemiringAction M R] {a : M} (ha : a ≠ 0) {S T : Subring R} :
    S ≤ a • T ↔ a⁻¹ • S ≤ T