ι_eq_algebraMap_iff — Mathlib

English

For x ∈ M and r ∈ R, ι_R x = algebraMap_R r iff x = 0 and r = 0.

Русский

Для x ∈ M и r ∈ R, ι_R x = algebraMap_R r тогда и только тогда, когда x = 0 и r = 0.

LaTeX

$$$\\iota_R x = \\mathrm{algebraMap}_R (\\cdot) r \\iff x = 0 \\wedge r = 0$$$

Lean4

@[simp]
theorem ι_eq_algebraMap_iff (x : M) (r : R) : ι R x = algebraMap R _ r ↔ x = 0 ∧ r = 0 :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
    haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
    have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
    rw [h, AlgHom.commutes] at hf0
    have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
    exact this.symm.imp_left Eq.symm
  · rintro ⟨rfl, rfl⟩
    rw [LinearMap.map_zero, RingHom.map_zero]

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