ι_range_disjoint_one — Mathlib

English

The submodule generated by the images of M under ι_R is disjoint from the scalars 1 in ExteriorAlgebra R M.

Русский

Подмодуль, порождаемый образами M под ι_R, распрямлен (дисjoint) с модулями скалярами, единицей в ExteriorAlgebra.

LaTeX

$$$\mathrm{Disjoint}\big(\mathrm{range}(\iota_R), 1\big) \subseteq \mathrm{ExteriorAlgebra} R M$$$

Lean4

/-- The generators of the exterior algebra are disjoint from its scalars. -/
theorem ι_range_disjoint_one :
    Disjoint (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M)) (1 : Submodule R (ExteriorAlgebra R M)) :=
  by
  rw [Submodule.disjoint_def]
  rintro _ ⟨x, hx⟩ h
  obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h
  rw [ι_eq_algebraMap_iff x] at hx
  rw [hx.2, RingHom.map_zero]

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