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.

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
    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) :
    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 Sm r m S
    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
    • =
    @[simp]
    theorem Ideal.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] (a : M) :
    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
    theorem Ideal.smul_closure {M : Type u_1} {R : Type u_2} [Monoid M] [CommRing R] [MulSemiringAction M R] (a : M) (s : Set R) :
    @[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
    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
    @[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
    @[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) :
    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
    @[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
    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
    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.