English
A Lie subalgebra H is Cartan if and only if H.toLieSubmodule is IsUcsLimit.
Русский
Ли-подалгебра H является Картановой тогда и только тогда, когда H.toLieSubmodule удовлетворяет IsUcsLimit.
LaTeX
$$$H. IsCartanSubalgebra\\; \\Leftrightarrow \\; H^{\\text{toLieSubmodule}}.IsUcsLimit$$$
Lean4
theorem isCartanSubalgebra_iff_isUcsLimit : H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit :=
by
constructor
· intro h
have h₁ : LieRing.IsNilpotent H := by infer_instance
obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁
replace hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥ :=
le_antisymm hk (LieSubmodule.ucs_le_of_normalizer_eq_self H.normalizer_eq_self_of_isCartanSubalgebra k)
refine ⟨k, fun l hl => ?_⟩
rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
· rintro ⟨k, hk⟩
exact
{ nilpotent :=
by
dsimp only [LieRing.IsNilpotent]
-- The instance for the second `H` in the goal is `lieRingSelfModule`
-- but `rw` expects it to be `H.toLieSubmodule.instLieRingModuleSubtypeMem`,
-- and these are not reducibly defeq.
erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
use k
rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
self_normalizing := by
have hk' := hk (k + 1) k.le_succ
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer, hk',
LieSubalgebra.coe_toLieSubmodule] }
