ofTensorProduct_bijective_of_pi_of_fintype

English

If M is the Pi-indexed free module R^ι with ι finite, then the canonical map AdicCompletion I R ⊗_R (ι → R) → AdicCompletion I (ι → R) is bijective.

Русский

Если M ≅ R^ι для конечного множества индексов ι, то каноническое отображение AdicCompletion I R ⊗_R (ι → R) → AdicCompletion I (ι → R) биективно.

LaTeX

$$$ \mathrm{ofTensorProduct}\ I\ (\iota \to R) : \mathrm{AdicCompletion}_I(R) \otimes_R (\iota \to R) \to \mathrm{AdicCompletion}_I(\iota \to R) \text{ is bijective }$$$

Lean4

/-- If `M = R^ι`, `ofTensorProduct` is bijective. -/
theorem ofTensorProduct_bijective_of_pi_of_fintype [Finite ι] : Function.Bijective (ofTensorProduct I (ι → R)) := by
  classical
  cases nonempty_fintype ι
  exact EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)

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