hasTrivialRadical_of_isIrreducible_of_isFaithful

English

If a representation is irreducible and faithful, the radical equals the center.

Русский

Если представление неразложимо и верно, радикал равен центру.

LaTeX

$$hasTrivialRadical_of_isIrreducible_of_isFaithful (h) : HasTrivialRadical k L$$

Lean4

theorem hasTrivialRadical_of_isIrreducible_of_isFaithful (h : ∀ x, LinearMap.trace k _ (toEnd k L M x) = 0) :
    HasTrivialRadical k L :=
  by
  have : finrank k M ≠ 0 := ((finrank_pos_iff).mpr <| nontrivial_of_isIrreducible k L M).ne'
  obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M
  rw [hasTrivialRadical_iff, (hasCentralRadical_iff k L).mp inferInstance, LieSubmodule.eq_bot_iff]
  intro x hx
  specialize h x
  rw [h' x] at hx
  obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx
  suffices t = 0 by simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), ← ht, this]
  simpa [this, ← ht] using h

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