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.

@[implicit_reducible]

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.

@[implicit_reducible]

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

def Ideal.stabilizerEquiv {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {N : Type u_3} [Group N] [MulSemiringAction N R] (I : Ideal R) (e : M ≃* N) (he : ∀ (m : M) (x : R), e m • x = m • x) : ↥(MulAction.stabilizer M I) ≃* ↥(MulAction.stabilizer N I)

Assume that M and N are isomorphic and act in a compatible way on R, then for any ideal I of R, the stabilizer of I in M is isomorphic to the stabilizer of I in N.

@[simp]

theorem Ideal.stabilizerEquiv_apply_smul {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {N : Type u_3} [Group N] [MulSemiringAction N R] (I : Ideal R) (e : M ≃* N) (he : ∀ (m : M) (x : R), e m • x = m • x) (m : ↥(MulAction.stabilizer M I)) (x : R) : (I.stabilizerEquiv e he) m • x = m • x

@[simp]

theorem Ideal.stabilizerEquiv_symm_apply_smul {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {N : Type u_3} [Group N] [MulSemiringAction N R] (I : Ideal R) (e : M ≃* N) (he : ∀ (m : M) (x : R), e m • x = m • x) (n : ↥(MulAction.stabilizer N I)) (x : R) : (I.stabilizerEquiv e he).symm n • x = n • x

def Ideal.inertiaEquiv {M : Type u_1} [Group M] {N : Type u_3} [Group N] {R : Type u_4} [Ring R] [MulSemiringAction M R] [MulSemiringAction N R] (I : Ideal R) (e : M ≃* N) (he : ∀ (m : M) (x : R), e m • x = m • x) : ↥(inertia M I) ≃* ↥(inertia N I)

Assume that M and N are isomorphic and act in a compatible way on R, then for any ideal I of R, the inertia subgroup of I in M is isomorphic to the inertia subgroup of I in N.

@[simp]

theorem Ideal.inertiaEquiv_apply_smul {M : Type u_1} [Group M] {N : Type u_3} [Group N] {R : Type u_4} [Ring R] [MulSemiringAction M R] [MulSemiringAction N R] (I : Ideal R) (e : M ≃* N) (he : ∀ (m : M) (x : R), e m • x = m • x) (m : ↥(inertia M I)) (x : R) : (I.inertiaEquiv e he) m • x = m • x

@[simp]

theorem Ideal.inertiaEquiv_symm_apply_smul {M : Type u_1} [Group M] {N : Type u_3} [Group N] {R : Type u_4} [Ring R] [MulSemiringAction M R] [MulSemiringAction N R] (I : Ideal R) (e : M ≃* N) (he : ∀ (m : M) (x : R), e m • x = m • x) (n : ↥(inertia N I)) (x : R) : (I.inertiaEquiv e he).symm n • x = n • x

TODO: add equivSMul like we have for subgroup.