tensorKer_coe — Mathlib

English

There is a canonical algebra homomorphism taking T ⊗ eq(f,g) to eq(1⊗f,1⊗g), induced by tensoring with T.

Русский

Существует каноническое алгебра-отображение, отправляющее T ⊗ eq(f,g) в eq(1⊗f,1⊗g), индуцируемое тензоризацией по T.

LaTeX

$$$\text{tensorEqualizer} : T ⊗_R AlgHom.equalizer f g \to_A[S] AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g)$$$

Lean4

@[simp]
theorem tensorKer_coe (x : M ⊗[R] (LinearMap.ker f)) : (tensorKer S M f x : M ⊗[R] N) = (ker f).subtype.lTensor M x :=
  by induction x <;> simp_all

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