hom_ext — Mathlib

English

If two morphisms α, β from the extended-scalar object satisfy α(1 ⊗ m) = β(1 ⊗ m) for all m ∈ M, then α = β.

Русский

Если два морфизма α, β из расширенного скалярами объекта удовлетворяют α(1 ⊗ m) = β(1 ⊗ m) для всех m ∈ M, то α = β.

LaTeX

$$$\forall m \in M,\; α(1 \otimes m) = β(1 \otimes m) \Rightarrow α = β$$$

Lean4

@[ext]
theorem hom_ext {M : ModuleCat R} {N : ModuleCat S} {α β : (extendScalars f).obj M ⟶ N}
    (h : ∀ (m : M), α ((1 : S) ⊗ₜ m) = β ((1 : S) ⊗ₜ m)) : α = β :=
  by
  apply (restrictScalars f).map_injective
  letI := f.toAlgebra
  ext : 1
  apply TensorProduct.ext'
  intro (s : S) m
  change α (s ⊗ₜ m) = β (s ⊗ₜ m)
  have : s ⊗ₜ[R] (m : M) = s • (1 : S) ⊗ₜ[R] m := by rw [ExtendScalars.smul_tmul, mul_one]
  simp only [this, map_smul, h]

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