directLimitRight — Mathlib

English

There is a canonical isomorphism between M ⊗ DirectLimit G f and DirectLimit (M ⊗ G) (M ◁ f).

Русский

Существует канонический изоморфизм между M ⊗ DirectLimit G f и DirectLimit (M ⊗ G) (M ◁ f).

LaTeX

$$$\text{directLimitRight}:\ M \otimes_R DirectLimit G f \cong_\ell DirectLimit (M \otimes_R G) (M \triangleleft f)$$$

Lean4

/-- `M ⊗ (limᵢ Gᵢ)` and `limᵢ (M ⊗ Gᵢ)` are isomorphic as modules
-/
noncomputable def directLimitRight : M ⊗[R] DirectLimit G f ≃ₗ[R] DirectLimit (M ⊗[R] G ·) (M ◁ f) :=
  TensorProduct.comm _ _ _ ≪≫ₗ directLimitLeft f M ≪≫ₗ
    Module.DirectLimit.congr (fun _ ↦ TensorProduct.comm _ _ _)
      (fun i j h ↦ TensorProduct.ext <| DFunLike.ext _ _ <| by aesop)

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