le_comap_range_rTensor — Mathlib

English

Tensor product with a surjective map preserves surjectivity on the left; i.e., lTensor(Q,g) is surjective if g is surjective.

Русский

Тензорное произведение с сюръективной картой сохраняет сюръективность слева; i.e., lTensor(Q,g) сюрьективно при сюрьективности g.

LaTeX

$$$$ \text{If } g: N \to P \text{ is surjective, then } l_{Q} g: M \otimes_R N \to M \otimes_R P \text{ is surjective}. $$$$

Lean4

theorem le_comap_range_rTensor (q : Q) :
    LinearMap.range g ≤ (LinearMap.range (rTensor Q g)).comap ((TensorProduct.mk R P Q).flip q) :=
  by
  rintro x ⟨n, rfl⟩
  exact ⟨n ⊗ₜ[R] q, rfl⟩

Похожие утверждения