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 action 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.

def Ideal.pointwiseDistribMulAction {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] : DistribMulAction 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.

def Ideal.pointwiseMulSemiringAction {M : Type u_1} [Monoid M] {R : Type u_3} [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.

theorem Ideal.pointwise_smul_def {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] {a : M} (S : Ideal R) : a • S = map (MulSemiringAction.toRingHom M R a) S

theorem Ideal.smul_mem_pointwise_smul {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (m : M) (r : R) (S : Ideal R) : r ∈ S → m • r ∈ m • S

instance Ideal.instCovariantClassHSMulLe {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] : CovariantClass M (Ideal R) HSMul.hSMul LE.le

@[simp]

theorem Ideal.smul_bot {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) : a • ⊥ = ⊥

theorem Ideal.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) (S T : Ideal R) : a • (S ⊔ T) = a • S ⊔ a • T

theorem Ideal.smul_closure {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) (s : Set R) : a • span s = span (a • s)

instance Ideal.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 (Ideal R)

@[simp]

theorem Ideal.pointwise_smul_toAddSubmonoid {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring 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} [Monoid M] {R : Type u_3} [Ring 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

theorem Ideal.pointwise_smul_eq_comap {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {a : M} (S : Ideal R) : a • S = comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

@[simp]

theorem Ideal.smul_mem_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring 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] [Semiring R] [MulSemiringAction M R] {a : M} {S : Ideal R} {x : R} : x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem Ideal.mem_inv_pointwise_smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring 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] [Semiring R] [MulSemiringAction M R] {a : M} {S 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] [Semiring R] [MulSemiringAction M R] {a : M} {S 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] [Semiring R] [MulSemiringAction M R] {a : M} {S T : Ideal R} : S ≤ a • T ↔ a⁻¹ • S ≤ T

instance Ideal.IsPrime.smul {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {I : Ideal R} [H : I.IsPrime] (g : M) : (g • I).IsPrime

@[simp]

theorem Ideal.IsPrime.smul_iff {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {I : Ideal R} (g : M) : (g • I).IsPrime ↔ I.IsPrime

theorem Ideal.inertia_le_stabilizer {M : Type u_1} [Group M] {R : Type u_3} [Ring R] (P : Ideal R) [MulSemiringAction M R] : inertia M P ≤ MulAction.stabilizer M P

instance Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia {M : Type u_1} [Group M] {R : Type u_3} [Ring R] (P : Ideal R) [MulSemiringAction M R] : ((inertia M P).subgroupOf (MulAction.stabilizer M P)).Normal

TODO: add equivSMul like we have for subgroup.