tmul — Mathlib

English

If y ∈ B is integral over R, then for any x ∈ A, the tensor x ⊗ y is integral over A in A ⊗_R B.

Русский

Если y ∈ B интегрален над R, то для любого x ∈ A элемент x ⊗ y ∈ A ⊗_R B интегрален над A.

LaTeX

$$$\IsIntegral(R,y) \Rightarrow \IsIntegral(A, x \otimes_R y)$$$

Lean4

theorem tmul [Ring B] [Algebra R A] [Algebra R B] (x : A) {y : B} (h : IsIntegral R y) : IsIntegral A (x ⊗ₜ[R] y) :=
  by
  rw [← mul_one x, ← smul_eq_mul, ← smul_tmul']
  exact
    smul _
      (h.map_of_comp_eq (algebraMap R A) (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
        Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap)

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