Pointwise monoid structures on sub_mul_action #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides sub_mul_action.monoid and weaker typeclasses, which show that sub_mul_actions inherit the same pointwise multiplications as sets.

To match submodule.idem_semiring, we do not put these in the pointwise locale.

source

@[protected, instance]

def sub_mul_action.has_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] :

has_one (sub_mul_action R M)

Equations

sub_mul_action.has_one = {one := {carrier := set.range (λ (r : R), r • 1), smul_mem' := _}}

source

theorem sub_mul_action.coe_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] :

↑1 = set.range (λ (r : R), r • 1)

source

@[simp]

theorem sub_mul_action.mem_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] {x : M} :

x ∈ 1 ↔ ∃ (r : R), r • 1 = x

source

theorem sub_mul_action.subset_coe_one {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_one M] :

1 ⊆ ↑1

source

@[protected, instance]

def sub_mul_action.has_mul {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_mul M] [is_scalar_tower R M M] :

has_mul (sub_mul_action R M)

Equations

sub_mul_action.has_mul = {mul := λ (p q : sub_mul_action R M), {carrier := set.image2 has_mul.mul ↑p ↑q, smul_mem' := _}}

source

@[norm_cast]

theorem sub_mul_action.coe_mul {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_mul M] [is_scalar_tower R M M] (p q : sub_mul_action R M) :

↑(p * q) = ↑p * ↑q

source

theorem sub_mul_action.mem_mul {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [has_mul M] [is_scalar_tower R M M] {p q : sub_mul_action R M} {x : M} :

x ∈ p * q ↔ ∃ (y z : M), y ∈ p ∧ z ∈ q ∧ y * z = x

source

@[protected, instance]

def sub_mul_action.mul_one_class {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [mul_one_class M] [is_scalar_tower R M M] [smul_comm_class R M M] :

mul_one_class (sub_mul_action R M)

Equations

sub_mul_action.mul_one_class = {one := 1, mul := has_mul.mul sub_mul_action.has_mul, one_mul := _, mul_one := _}

source

@[protected, instance]

def sub_mul_action.semigroup {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [semigroup M] [is_scalar_tower R M M] :

semigroup (sub_mul_action R M)

Equations

sub_mul_action.semigroup = {mul := has_mul.mul sub_mul_action.has_mul, mul_assoc := _}

source

@[protected, instance]

def sub_mul_action.monoid {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [monoid M] [is_scalar_tower R M M] [smul_comm_class R M M] :

monoid (sub_mul_action R M)

Equations

sub_mul_action.monoid = {mul := has_mul.mul sub_mul_action.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (sub_mul_action R M)), npow_zero' := _, npow_succ' := _}

source

theorem sub_mul_action.coe_pow {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [monoid M] [is_scalar_tower R M M] [smul_comm_class R M M] (p : sub_mul_action R M) {n : ℕ} (hn : n ≠ 0) :

↑(p ^ n) = ↑p ^ n

source

theorem sub_mul_action.subset_coe_pow {R : Type u_1} {M : Type u_2} [monoid R] [mul_action R M] [monoid M] [is_scalar_tower R M M] [smul_comm_class R M M] (p : sub_mul_action R M) {n : ℕ} :

↑p ^ n ⊆ ↑(p ^ n)