English
Characterizes when ι_R x equals an algebra map from R to ExteriorAlgebra; specifically, ι_R x = algebraMap r iff x = 0 and r = 0.
Русский
Характеризуется, когда ι_R x равен алгебраMap(r); то есть ι_R x = algebraMap r ↔ x = 0 ∧ r = 0.
LaTeX
$$$\iota_R x = \mathrm{algebraMap}_R(\mathrm{ExteriorAlgebra} R M)\, r \iff x = 0 \land 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) := toTrivSqZeroExt_ι _
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]
