exists_of_fg — Mathlib

English

Any tensor u ∈ M ⊗_R N can be realized as coming from some FG submodule P ⊆ M via rTensor with P.subtype.

Русский

Любый тензор u ∈ M ⊗_R N получается как элемент rTensor от FG-подмодуля P ⊆ M.

LaTeX

$$$\\exists P\\subseteq M\\, (P.FG) \\land u \\in \\operatorname{range}(\\, rTensor\\; N\\; P\\,\\.subtype).$$$

Lean4

theorem exists_of_fg : ∃ (P : Submodule R M), P.FG ∧ u ∈ range (rTensor N P.subtype) := by
  classical
  let ⟨P, t, ht⟩ := Module.DirectLimit.exists_of ((Submodule.FG.rTensor.directLimit R M N).symm u)
  use P.val, P.property, t
  rw [← Submodule.FG.rTensor.directLimit_apply, ht, LinearEquiv.apply_symm_apply]

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