eq_zero_of_fg_of_subtype_eq_zero — Mathlib

English

If rTensor on P.subtype t equals that on P'.subtype t', there exist Q with P ≤ Q and P' ≤ Q, Q.FG, such that rTensor on inclusions yield equality.

Русский

Если rTensor на P.subtype t равен rTensor на P'.subtype t', найдётся Q с P ≤ Q и P' ≤ Q, Q.FG, так что включения дают равенство.

LaTeX

$$$\\exists Q\\,(hPQ: P \\le Q)\\,(hP'Q: P' \\le Q), Q.FG ∧ rTensor N (inclusion hPQ) t = rTensor N (inclusion hP'Q) t'.$$$

Lean4

theorem eq_zero_of_fg_of_subtype_eq_zero (h : rTensor N P.subtype t = 0) :
    ∃ (Q : Submodule R M) (hPQ : P ≤ Q), Q.FG ∧ rTensor N (inclusion hPQ) t = 0 :=
  by
  rw [← (rTensor N P.subtype).map_zero] at h
  simpa only [map_zero] using TensorProduct.eq_of_fg_of_subtype_eq hP h

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