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

Equations
Instances For
    source
    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.

    Equations
    Instances For
      source
      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 = 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] [Semiring 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] [Semiring 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] [Semiring R] [MulSemiringAction M R] (a : M) :
      a • ⊥ = ⊥
      source
      theorem Ideal.smul_sup {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring 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] [Semiring 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] [Semiring R] [MulSemiringAction M R] [MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R] :
      IsCentralScalar M (Ideal R)
      Equations
      • ⋯ = ⋯
      source
      @[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
      source
      @[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
      source
      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 = 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] [Semiring 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] [Semiring R] [MulSemiringAction M R] {a : M} {S : Ideal R} {x : R} :
      x ∈ a • S ↔ a⁻¹ • x ∈ S
      source
      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
      source
      @[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 : 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] [Semiring 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] [Semiring R] [MulSemiringAction M R] {a : M} {S : Ideal R} {T : Ideal R} :
      S ≤ a • T ↔ a⁻¹ • S ≤ T
      source
      theorem 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
      source
      @[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

      TODO: add equivSMul like we have for subgroup.