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_reducible]

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_reducible]

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_reducible]

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 = { toOne := SubMulAction.instOne, toMul := SubMulAction.instMul, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

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 = { toMul := SubMulAction.instMul, mul_assoc := ⋯ }

@[instance_reducible]

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

• SubMulAction.instMonoid = { toOne := SubMulAction.instOne, toMul := SubMulAction.instMul, mul_assoc := ⋯, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

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)