Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

SubMulAction.instOne instance

: One (SubMulAction R M)

Full source

instance : One (SubMulAction R M) where
  one :=
    { carrier := Set.range fun r : R => r • (1 : M)
      smul_mem' := fun r _ ⟨r', hr'⟩ => hr' ▸ ⟨r * r', mul_smul _ _ _⟩ }

One Element in Submodule of Scalar Action

Informal description

For a scalar action of a monoid $R$ on a monoid $M$, the submodule $\text{SubMulAction}\, R\, M$ has a canonical one element given by the set of all scalar multiples $r \cdot 1_M$ for $r \in R$, where $1_M$ is the identity element of $M$.

SubMulAction.coe_one theorem

: ↑(1 : SubMulAction R M) = Set.range fun r : R => r • (1 : M)

Full source

theorem coe_one : ↑(1 : SubMulAction R M) = Set.range fun r : R => r • (1 : M) :=
  rfl

Image of Submodule Identity Equals Scalar Multiples of Monoid Identity

Informal description

The image of the multiplicative identity element $1$ in the submodule $\text{SubMulAction}\, R\, M$ under the canonical embedding is equal to the range of the function $r \mapsto r \cdot 1_M$, where $1_M$ is the identity element of $M$ and $r$ ranges over $R$.

SubMulAction.mem_one theorem

{x : M} : x ∈ (1 : SubMulAction R M) ↔ ∃ r : R, r • (1 : M) = x

Full source

@[simp]
theorem mem_one {x : M} : x ∈ (1 : SubMulAction R M)x ∈ (1 : SubMulAction R M) ↔ ∃ r : R, r • (1 : M) = x :=
  Iff.rfl

Characterization of Elements in the Identity Submodule

Informal description

An element $x \in M$ belongs to the multiplicative identity submodule $1 \subseteq \text{SubMulAction}(R, M)$ if and only if there exists an element $r \in R$ such that $x = r \cdot 1_M$, where $1_M$ is the multiplicative identity of $M$.

SubMulAction.subset_coe_one theorem

: (1 : Set M) ⊆ (1 : SubMulAction R M)

Full source

theorem subset_coe_one : (1 : Set M) ⊆ (1 : SubMulAction R M) := fun _ hx =>
  ⟨1, (one_smul _ _).trans hx.symm⟩

Inclusion of Monoid Identity in Submodule Identity

Informal description

The singleton set $\{1_M\}$ in $M$ is contained in the multiplicative identity submodule of $\text{SubMulAction}(R, M)$, where $1_M$ is the identity element of $M$.

SubMulAction.instMul instance

: Mul (SubMulAction R M)

Full source

instance : Mul (SubMulAction R M) where
  mul p q :=
    { carrier := Set.image2 (· * ·) p q
      smul_mem' := fun r _ ⟨m₁, hm₁, m₂, hm₂, h⟩ =>
        h ▸ smul_mul_assoc r m₁ m₂ ▸ Set.mul_mem_mul (p.smul_mem _ hm₁) hm₂ }

Pointwise Multiplication on Submodules of a Monoid Action

Informal description

For any scalar action of a semiring $R$ on a monoid $M$, the type of submodules $\text{SubMulAction}(R, M)$ inherits a multiplication operation defined pointwise from $M$.

SubMulAction.coe_mul theorem

(p q : SubMulAction R M) : ↑(p * q) = (p * q : Set M)

Full source

@[norm_cast]
theorem coe_mul (p q : SubMulAction R M) : ↑(p * q) = (p * q : Set M) :=
  rfl

Pointwise Multiplication of Submodules Corresponds to Set Multiplication

Informal description

For any submodules $p$ and $q$ of a monoid $M$ under a scalar action of a semiring $R$, the underlying set of their pointwise product $p * q$ is equal to the pointwise product of their underlying sets, i.e., $(p * q) = p * q$ as subsets of $M$.

SubMulAction.mem_mul theorem

{p q : SubMulAction R M} {x : M} : x ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x

Full source

theorem mem_mul {p q : SubMulAction R M} {x : M} : x ∈ p * qx ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x :=
  Set.mem_mul

Membership in Pointwise Product of Submodules

Informal description

For any submodules $p, q$ of a monoid action $\text{SubMulAction}(R, M)$ and any element $x \in M$, we have $x \in p \cdot q$ if and only if there exist elements $y \in p$ and $z \in q$ such that $y \cdot z = x$.

SubMulAction.mulOneClass instance

: MulOneClass (SubMulAction R M)

Full source

instance mulOneClass : MulOneClass (SubMulAction R M) where
  mul := (· * ·)
  one := 1
  mul_one a := by
    ext x
    simp only [mem_mul, mem_one, mul_smul_comm, exists_exists_eq_and, mul_one]
    constructor
    · rintro ⟨y, hy, r, rfl⟩
      exact smul_mem _ _ hy
    · intro hx
      exact ⟨x, hx, 1, one_smul _ _⟩
  one_mul a := by
    ext x
    simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]
    refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
    rintro ⟨r, y, hy, rfl⟩
    exact smul_mem _ _ hy

Submodules of a Monoid Action Form a Mul-One Class

Informal description

For a scalar action of a monoid $R$ on a monoid $M$, the submodules $\text{SubMulAction}(R, M)$ form a mul-one class under pointwise multiplication. This means they have an associative multiplication operation and a multiplicative identity element inherited from $M$.

SubMulAction.semiGroup instance

: Semigroup (SubMulAction R M)

Full source

instance semiGroup : Semigroup (SubMulAction R M) where
  mul := (· * ·)
  mul_assoc _ _ _ := SetLike.coe_injective (mul_assoc (_ : Set _) _ _)

Submodules of a Semigroup Action Form a Semigroup

Informal description

For any scalar action of a semiring $R$ on a semigroup $M$, the submodules $\text{SubMulAction}(R, M)$ form a semigroup under pointwise multiplication inherited from $M$.

SubMulAction.instMonoid instance

: Monoid (SubMulAction R M)

Full source

instance : Monoid (SubMulAction R M) :=
  { SubMulAction.semiGroup,
    SubMulAction.mulOneClass with }

Submodules of a Monoid Action Form a Monoid

Informal description

For any scalar action of a monoid $R$ on a monoid $M$, the submodules $\text{SubMulAction}(R, M)$ form a monoid under pointwise multiplication inherited from $M$.

SubMulAction.coe_pow theorem

(p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = (p : Set M) ^ n

Full source

theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = (p : Set M) ^ n
  | 0, hn => (hn rfl).elim
  | 1, _ => by rw [pow_one, pow_one]
  | n + 2, _ => by
    rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]

Power of Submodule Equals Power of Underlying Set

Informal description

For any submodule $p$ of a monoid $M$ under a scalar action of a semiring $R$, and for any nonzero natural number $n$, the underlying set of $p^n$ is equal to the $n$-th power of the underlying set of $p$, i.e., $(p^n) = p^n$ as subsets of $M$.

SubMulAction.subset_coe_pow theorem

(p : SubMulAction R M) : ∀ {n : ℕ}, (p : Set M) ^ n ⊆ ↑(p ^ n)

Full source

theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, (p : Set M) ^ n ⊆ ↑(p ^ n)
  | 0 => by
    rw [pow_zero, pow_zero]
    exact subset_coe_one
  | n + 1 => by rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]

Inclusion of Set Powers in Submodule Powers

Informal description

For any submodule $p$ of a monoid $M$ under a scalar action of a semiring $R$, and for any natural number $n$, the $n$-th power of the underlying set of $p$ is contained in the underlying set of $p^n$, i.e., $p^n \subseteq p^n$ as subsets of $M$.