Elementwise monoid structure of additive submonoids

These definitions are a cut-down versions of the ones around Submodule.mul, as that API is usually more useful.

SMul (AddSubmonoid R) (AddSubmonoid A) is also provided given DistribSMul R A, and when R = A it is definitionally equal to the multiplication on AddSubmonoid R.

These are all available in the Pointwise locale.

Additionally, it provides various degrees of monoid structure:

• AddSubmonoid.one
• AddSubmonoid.mul
• AddSubmonoid.mulOneClass
• AddSubmonoid.semigroup
• AddSubmonoid.monoid

which is available globally to match the monoid structure implied by Submodule.idemSemiring.

Implementation notes

Many results about multiplication are derived from the corresponding results about scalar multiplication, but results requiring right distributivity do not have SMul versions, due to the lack of a suitable typeclass (unless one goes all the way to Module).

def AddSubmonoid.one {R : Type u_2} [AddMonoidWithOne R] : One (AddSubmonoid R)

If R is an additive monoid with one (e.g., a semiring), then 1 : AddSubmonoid R is the range of Nat.cast : ℕ → R.

Equations

• AddSubmonoid.one = { one := AddMonoidHom.mrange (Nat.castAddMonoidHom R) }

theorem AddSubmonoid.one_eq_mrange {R : Type u_2} [AddMonoidWithOne R] : 1 = AddMonoidHom.mrange (Nat.castAddMonoidHom R)

theorem AddSubmonoid.natCast_mem_one {R : Type u_2} [AddMonoidWithOne R] (n : ℕ) : ↑n ∈ 1

@[simp]

theorem AddSubmonoid.mem_one {R : Type u_2} [AddMonoidWithOne R] {x : R} : x ∈ 1 ↔ ∃ (n : ℕ), ↑n = x

theorem AddSubmonoid.one_eq_closure {R : Type u_2} [AddMonoidWithOne R] : 1 = closure {1}

theorem AddSubmonoid.one_eq_closure_one_set {R : Type u_2} [AddMonoidWithOne R] : 1 = closure 1

def AddSubmonoid.smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] : SMul (AddSubmonoid R) (AddSubmonoid A)

For M : Submonoid R and N : AddSubmonoid A, M • N is the additive submonoid generated by all m • n where m ∈ M and n ∈ N.

Equations

• AddSubmonoid.smul = { smul := fun (M : AddSubmonoid R) (N : AddSubmonoid A) => ⨆ (s : ↥M), AddSubmonoid.map (DistribSMul.toAddMonoidHom A ↑s) N }

theorem AddSubmonoid.smul_mem_smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} {m : R} {n : A} (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N

theorem AddSubmonoid.smul_le {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P

theorem AddSubmonoid.smul_induction_on {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} {C : A → Prop} {a : A} (ha : a ∈ M • N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ (x y : A), C x → C y → C (x + y)) : C a

@[simp]

theorem AddSubmonoid.addSubmonoid_smul_bot {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] (S : AddSubmonoid R) : S • ⊥ = ⊥

theorem AddSubmonoid.smul_le_smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M M' : AddSubmonoid R} {N P : AddSubmonoid A} (h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P

theorem AddSubmonoid.smul_le_smul_left {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M M' : AddSubmonoid R} {P : AddSubmonoid A} (h : M ≤ M') : M • P ≤ M' • P

theorem AddSubmonoid.smul_le_smul_right {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} (h : N ≤ P) : M • N ≤ M • P

theorem AddSubmonoid.smul_subset_smul {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N : AddSubmonoid A} : ↑M • ↑N ⊆ ↑(M • N)

theorem AddSubmonoid.addSubmonoid_smul_sup {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {M : AddSubmonoid R} {N P : AddSubmonoid A} : M • (N ⊔ P) = M • N ⊔ M • P

theorem AddSubmonoid.smul_iSup {R : Type u_2} {A : Type u_3} [AddMonoid R] [AddMonoid A] [DistribSMul R A] {ι : Sort u_4} (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : T • ⨆ (i : ι), S i = ⨆ (i : ι), T • S i

def AddSubmonoid.mul {R : Type u_2} [NonUnitalNonAssocSemiring R] : Mul (AddSubmonoid R)

Multiplication of additive submonoids of a semiring R. The additive submonoid S * T is the smallest R-submodule of R containing the elements s * t for s ∈ S and t ∈ T.

Equations

• AddSubmonoid.mul = { mul := fun (M N : AddSubmonoid R) => ⨆ (s : ↥M), AddSubmonoid.map (AddMonoidHom.mul ↑s) N }

theorem AddSubmonoid.mul_mem_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N

theorem AddSubmonoid.mul_le {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

theorem AddSubmonoid.mul_induction_on {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {C : R → Prop} {r : R} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ (x y : R), C x → C y → C (x + y)) : C r

theorem AddSubmonoid.closure_mul_closure {R : Type u_2} [NonUnitalNonAssocSemiring R] (S T : Set R) : closure S * closure T = closure (S * T)

theorem AddSubmonoid.mul_eq_closure_mul_set {R : Type u_2} [NonUnitalNonAssocSemiring R] (M N : AddSubmonoid R) : M * N = closure (↑M * ↑N)

@[simp]

theorem AddSubmonoid.mul_bot {R : Type u_2} [NonUnitalNonAssocSemiring R] (S : AddSubmonoid R) : S * ⊥ = ⊥

@[simp]

theorem AddSubmonoid.bot_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] (S : AddSubmonoid R) : ⊥ * S = ⊥

theorem AddSubmonoid.mul_le_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P Q : AddSubmonoid R} (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q

theorem AddSubmonoid.mul_le_mul_left {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} (h : M ≤ N) : M * P ≤ N * P

theorem AddSubmonoid.mul_le_mul_right {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} (h : N ≤ P) : M * N ≤ M * P

theorem AddSubmonoid.mul_subset_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} : ↑M * ↑N ⊆ ↑(M * N)

theorem AddSubmonoid.mul_sup {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} : M * (N ⊔ P) = M * N ⊔ M * P

theorem AddSubmonoid.sup_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R} : (M ⊔ N) * P = M * P ⊔ N * P

theorem AddSubmonoid.iSup_mul {R : Type u_2} [NonUnitalNonAssocSemiring R] {ι : Sort u_4} (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ (i : ι), S i) * T = ⨆ (i : ι), S i * T

theorem AddSubmonoid.mul_iSup {R : Type u_2} [NonUnitalNonAssocSemiring R] {ι : Sort u_4} (T : AddSubmonoid R) (S : ι → AddSubmonoid R) : T * ⨆ (i : ι), S i = ⨆ (i : ι), T * S i

theorem AddSubmonoid.mul_comm_of_commute {R : Type u_2} [NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M

def AddSubmonoid.hasDistribNeg {R : Type u_2} [NonUnitalNonAssocRing R] : HasDistribNeg (AddSubmonoid R)

AddSubmonoid.neg distributes over multiplication.

This is available as an instance in the Pointwise locale.

Equations

• AddSubmonoid.hasDistribNeg = { toInvolutiveNeg := AddSubmonoid.involutiveNeg, neg_mul := ⋯, mul_neg := ⋯ }

def AddSubmonoid.mulOneClass {R : Type u_2} [NonAssocSemiring R] : MulOneClass (AddSubmonoid R)

A MulOneClass structure on additive submonoids of a (possibly, non-associative) semiring.

Equations

• AddSubmonoid.mulOneClass = { toOne := AddSubmonoid.one, toMul := AddSubmonoid.mul, one_mul := ⋯, mul_one := ⋯ }

def AddSubmonoid.semigroup {R : Type u_2} [NonUnitalSemiring R] : Semigroup (AddSubmonoid R)

Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.

Equations

• AddSubmonoid.semigroup = { toMul := AddSubmonoid.mul, mul_assoc := ⋯ }

def AddSubmonoid.monoid {R : Type u_2} [Semiring R] : Monoid (AddSubmonoid R)

Monoid structure on additive submonoids of a semiring.

Equations

• AddSubmonoid.monoid = { toSemigroup := AddSubmonoid.semigroup, toOne := AddSubmonoid.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

theorem AddSubmonoid.closure_pow {R : Type u_2} [Semiring R] (s : Set R) (n : ℕ) : closure s ^ n = closure (s ^ n)

theorem AddSubmonoid.pow_eq_closure_pow_set {R : Type u_2} [Semiring R] (s : AddSubmonoid R) (n : ℕ) : s ^ n = closure (↑s ^ n)

theorem AddSubmonoid.pow_subset_pow {R : Type u_2} [Semiring R] {s : AddSubmonoid R} {n : ℕ} : ↑s ^ n ⊆ ↑(s ^ n)