Pointwise monoid structures on SubMulAction

This file provides SubMulAction.Monoid and weaker typeclasses, which show that SubMulActions inherit the same pointwise multiplications as sets.

To match Submodule.idemSemiring, we do not put these in the Pointwise locale.

instance SubMulAction.instOne {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] : One (SubMulAction R M)

Equations

• SubMulAction.instOne = { one := { carrier := Set.range fun (r : R) => r • 1, smul_mem' := ⋯ } }

theorem SubMulAction.coe_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] : ↑1 = Set.range fun (r : R) => r • 1

@[simp]

theorem SubMulAction.mem_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] {x : M} : x ∈ 1 ↔ ∃ (r : R), r • 1 = x

theorem SubMulAction.subset_coe_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] : 1 ⊆ ↑1

instance SubMulAction.instMul {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Mul M] [IsScalarTower R M M] : Mul (SubMulAction R M)

Equations

• SubMulAction.instMul = { mul := fun (p q : SubMulAction R M) => { carrier := Set.image2 (fun (x1 x2 : M) => x1 * x2) ↑p ↑q, smul_mem' := ⋯ } }

theorem SubMulAction.coe_mul {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Mul M] [IsScalarTower R M M] (p q : SubMulAction R M) : ↑(p * q) = ↑p * ↑q

theorem SubMulAction.mem_mul {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Mul M] [IsScalarTower R M M] {p q : SubMulAction R M} {x : M} : x ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x

instance SubMulAction.instMulOneClass {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [MulOneClass M] [IsScalarTower R M M] [SMulCommClass R M M] : MulOneClass (SubMulAction R M)

Equations

• SubMulAction.instMulOneClass = { one := 1, mul := fun (x1 x2 : SubMulAction R M) => x1 * x2, one_mul := ⋯, mul_one := ⋯ }

@[deprecated SubMulAction.instMulOneClass (since := "04-06-2025")]

def SubMulAction.mulOneClass {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [MulOneClass M] [IsScalarTower R M M] [SMulCommClass R M M] : MulOneClass (SubMulAction R M)

Alias of SubMulAction.instMulOneClass.

Equations

• @SubMulAction.mulOneClass = @SubMulAction.instMulOneClass

instance SubMulAction.instSemigroup {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Semigroup M] [IsScalarTower R M M] : Semigroup (SubMulAction R M)

Equations

• SubMulAction.instSemigroup = { mul := fun (x1 x2 : SubMulAction R M) => x1 * x2, mul_assoc := ⋯ }

@[deprecated SubMulAction.instSemigroup (since := "04-06-2025")]

def SubMulAction.semiGroup {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Semigroup M] [IsScalarTower R M M] : Semigroup (SubMulAction R M)

Alias of SubMulAction.instSemigroup.

Equations

• @SubMulAction.semiGroup = @SubMulAction.instSemigroup

instance SubMulAction.instMonoid {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Monoid M] [IsScalarTower R M M] [SMulCommClass R M M] : Monoid (SubMulAction R M)

Equations

• One or more equations did not get rendered due to their size.

theorem SubMulAction.coe_pow {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Monoid M] [IsScalarTower R M M] [SMulCommClass R M M] (p : SubMulAction R M) {n : ℕ} : n ≠ 0 → ↑(p ^ n) = ↑p ^ n

theorem SubMulAction.subset_coe_pow {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [Monoid M] [IsScalarTower R M M] [SMulCommClass R M M] (p : SubMulAction R M) {n : ℕ} : ↑p ^ n ⊆ ↑(p ^ n)