tensor_ext₃ — Mathlib

English

Let f,g: M1 ⊗ (M2 ⊗ M3) ⟶ M4 be morphisms with f(m1 ⊗ (m2 ⊗ m3)) = g(m1 ⊗ (m2 ⊗ m3)) for all m1,m2,m3; then f = g.

Русский

Пусть f,g: M1 ⊗ (M2 ⊗ M3) ⟶ M4 — гомоморфизмы с равенством на всех m1 ⊗ (m2 ⊗ m3); тогда f = g.

LaTeX

$$$\\forall m_1,m_2,m_3:\\; f(m_1 \\otimes (m_2 \\otimes m_3)) = g(m_1 \\otimes (m_2 \\otimes m_3)) \\Rightarrow f = g$$$

Lean4

/-- Extensionality lemma for morphisms from a module of the form `M₁ ⊗ (M₂ ⊗ M₃)`. -/
theorem tensor_ext₃ {f g : M₁ ⊗ (M₂ ⊗ M₃) ⟶ M₄} (h : ∀ m₁ m₂ m₃, f (m₁ ⊗ₜ (m₂ ⊗ₜ m₃)) = g (m₁ ⊗ₜ (m₂ ⊗ₜ m₃))) : f = g :=
  by
  rw [← cancel_epi (α_ _ _ _).hom]
  exact tensor_ext₃' h

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