fromDirectLimit — Mathlib

English

The left-basis sum map is injective.

Русский

Инъективна левые базисные суммирующая карта.

LaTeX

$$Function.Injective (Finsupp.lsum R fun i ⇢ (TensorProduct.mk R M N) (ℬ i))$$

Lean4

/-- the map `limᵢ (Gᵢ ⊗ M) → (limᵢ Gᵢ) ⊗ M` induced by the family of maps `Gᵢ ⊗ M → (limᵢ Gᵢ) ⊗ M`
given by `gᵢ ⊗ m ↦ [gᵢ] ⊗ m`.
-/
noncomputable def fromDirectLimit : DirectLimit (G · ⊗[R] M) (f ▷ M) →ₗ[R] DirectLimit G f ⊗[R] M :=
  Module.DirectLimit.lift _ _ _ _ (fun _ ↦ (of _ _ _ _ _).rTensor M) fun _ _ _ x ↦ by
    refine x.induction_on ?_ ?_ ?_ <;> aesop

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