isFaithful_iff' — Mathlib

English

A reformulation states that a LieModule is faithful iff the bracket with x being zero on all m implies x = 0.

Русский

Переформулировка: LieModule.IsFaithful эквивалентно тому, что для любого x, если ⁅x,m⁆=0 для всех m, то x=0.

LaTeX

$$$$ \text{IsFaithful } R L M \iff \forall x\in L, (\forall m\in M, \,[x,m]=0) \Rightarrow x=0.$$$$

Lean4

theorem isFaithful_iff' : IsFaithful R L M ↔ ∀ x : L, (∀ m : M, ⁅x, m⁆ = 0) → x = 0 :=
  by
  refine ⟨fun h x hx ↦ ?_, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
  · replace hx : toEnd R L M x = 0 := by ext m; simpa using hx m
    simpa using hx
  · rw [← sub_eq_zero]
    refine h _ fun m ↦ ?_
    rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]

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