Documentation

Mathlib.RingTheory.Ideal.Pointwise

Pointwise instances on Ideals #

This file provides the action Ideal.pointwiseMulAction which morally matches the action of mulActionSet (though here an extra Ideal.span is inserted).

This actions is available in the Pointwise locale.

Implementation notes #

This file is similar (but not identical) to Mathlib/Algebra/Ring/Subsemiring/Pointwise.lean. Where possible, try to keep them in sync.

source
def Ideal.pointwiseMulSemiringAction {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] :
MulSemiringAction M (Ideal R)

The action on an ideal corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

Equations
Instances For
    source
    theorem Ideal.pointwise_smul_def {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] {a : M} (S : Ideal R) :
    a • S = Ideal.map (MulSemiringAction.toRingHom M R a) S
    source
    theorem Ideal.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] (m : M) (r : R) (S : Ideal R) :
    r ∈ S → m • r ∈ m • S
    source
    instance Ideal.instCovariantClassHSMulLe {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] :
    CovariantClass M (Ideal R) HSMul.hSMul LE.le
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem Ideal.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] (a : M) :
    a • ⊥ = ⊥
    source
    theorem Ideal.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] (a : M) (S : Ideal R) (T : Ideal R) :
    a • (S ⊔ T) = a • S ⊔ a • T
    source
    theorem Ideal.smul_closure {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] (a : M) (s : Set R) :
    a • Ideal.span s = Ideal.span (a • s)
    source
    instance Ideal.pointwise_central_scalar {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] [MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R] :
    IsCentralScalar M (Ideal R)
    Equations
    • ⋯ = ⋯
    source
    theorem Ideal.pointwise_smul_eq_comap {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} (S : Ideal R) :
    a • S = Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S
    source
    @[simp]
    theorem Ideal.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} {S : Ideal R} {x : R} :
    a • x ∈ a • S ↔ x ∈ S
    source
    theorem Ideal.mem_pointwise_smul_iff_inv_smul_mem {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} {S : Ideal R} {x : R} :
    x ∈ a • S ↔ a⁻¹ • x ∈ S
    source
    @[simp]
    theorem Ideal.pointwise_smul_toAddSubmonoid {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] (a : M) (S : Ideal R) (ha : Function.Surjective fun (r : R) => a • r) :
    (a • S).toAddSubmonoid = a • S.toAddSubmonoid
    source
    @[simp]
    theorem Ideal.pointwise_smul_toAddSubGroup {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] (a : M) (S : Ideal R) (ha : Function.Surjective fun (r : R) => a • r) :
    Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S
    source
    theorem Ideal.mem_inv_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} {S : Ideal R} {x : R} :
    x ∈ a⁻¹ • S ↔ a • x ∈ S
    source
    @[simp]
    theorem Ideal.pointwise_smul_le_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} {S : Ideal R} {T : Ideal R} :
    a • S ≤ a • T ↔ S ≤ T
    source
    theorem Ideal.pointwise_smul_subset_iff {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} {S : Ideal R} {T : Ideal R} :
    a • S ≤ T ↔ S ≤ a⁻¹ • T
    source
    theorem Ideal.subset_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [CommRing R] [MulSemiringAction M R] {a : M} {S : Ideal R} {T : Ideal R} :
    S ≤ a • T ↔ a⁻¹ • S ≤ T

    TODO: add equivSMul like we have for subgroup.