English
Given an additive submonoid p of M and two closure properties hA and hB describing A- and B-compatibility, one may construct a Submodule of M with respect to the tensor product A ⊗R B, consisting of elements closed under the two scalar actions a ∈ A and b ∈ B.
Русский
Пусть p — подмножество M, обладающее аддитивной структурой, и заданы замкнутости hA и hB по действиям A и B; тогда можно построить подмодуль M над тензорным произведением A ⊗R B, состоящий из элементов, замкнутых двумя скалярами.
LaTeX
$$$$ Mk(p,h_A,h_B) = \\{ m \\in M \\\\mid m \\in p \\\\land (\\forall a \\in A)\\ a \\cdot m \\in p \\\\land (\\forall b \\in B)\\ b \\cdot m \\in p \\} \\,.$$$$
Lean4
/-- A constructor for a subbimodule which demands closure under the two sets of scalars
individually, rather than jointly via their tensor product.
Note that `R` plays no role but it is convenient to make this generalisation to support the cases
`R = ℕ` and `R = ℤ` which both show up naturally. See also `Subbimodule.baseChange`. -/
@[simps]
def mk (p : AddSubmonoid M) (hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p) (hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) :
Submodule (A ⊗[R] B) M :=
{ p with
carrier := p
smul_mem' := fun ab m =>
TensorProduct.induction_on ab (fun _ => by simp only [zero_smul, SetLike.mem_coe, zero_mem])
(fun a b hm => by simpa only [TensorProduct.Algebra.smul_def] using hA a (hB b hm)) fun z w hz hw hm => by
simpa only [add_smul] using p.add_mem (hz hm) (hw hm) }
