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.

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

Equations

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

theorem SubMulAction.coe_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] : Eq (SetLike.coe 1) (Set.range fun (r : R) => HSMul.hSMul r 1)

theorem SubMulAction.mem_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] {x : M} : Iff (Membership.mem 1 x) (Exists fun (r : R) => Eq (HSMul.hSMul r 1) x)

theorem SubMulAction.subset_coe_one {R : Type u_1} {M : Type u_2} [Monoid R] [MulAction R M] [One M] : HasSubset.Subset 1 (SetLike.coe 1)

def 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

• Eq SubMulAction.instMul { mul := fun (p q : SubMulAction R M) => { carrier := Set.image2 (fun (x1 x2 : M) => HMul.hMul x1 x2) (SetLike.coe p) (SetLike.coe 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) : Eq (SetLike.coe (HMul.hMul p q)) (HMul.hMul (SetLike.coe p) (SetLike.coe 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} : Iff (Membership.mem (HMul.hMul p q) x) (Exists fun (y : M) => And (Membership.mem p y) (Exists fun (z : M) => And (Membership.mem q z) (Eq (HMul.hMul y z) x)))

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)

Equations

• Eq SubMulAction.mulOneClass { one := 1, mul := fun (x1 x2 : SubMulAction R M) => HMul.hMul x1 x2, one_mul := ⋯, mul_one := ⋯ }

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)

Equations

• Eq SubMulAction.semiGroup { mul := fun (x1 x2 : SubMulAction R M) => HMul.hMul x1 x2, mul_assoc := ⋯ }

def 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

• Eq SubMulAction.instMonoid { toSemigroup := SubMulAction.semiGroup, toOne := MulOneClass.toOne, 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 : Nat} : Ne n 0 → Eq (SetLike.coe (HPow.hPow p n)) (HPow.hPow (SetLike.coe 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 : Nat} : HasSubset.Subset (HPow.hPow (SetLike.coe p) n) (SetLike.coe (HPow.hPow p n))