eq_bot_of_rank_le_one — Mathlib

English

If the F-rank of a subalgebra S of E over F is at most 1 and S is free as an F-module, then S is the bottom subalgebra.

Русский

Если ранг F-S подалгебры S в E над F не превышает 1 и S свободно как F-модуль, то S равно нижнему подалгебре.

LaTeX

$$$(\operatorname{rank} F S \le 1) \implies S = \bot$$$

Lean4

theorem eq_bot_of_rank_le_one (h : Module.rank F S ≤ 1) [Module.Free F S] : S = ⊥ :=
  by
  nontriviality E
  obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := S)
  by_cases h1 : Module.rank F S = 1
  · refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_
    rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1
    obtain ⟨h1⟩ := h1
    obtain ⟨y, hy⟩ :=
      (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ Finsupp.LinearEquiv.finsuppUnique _ _ _).symm).surjective ⟨x, hx⟩
    exact ⟨y, congr(Subtype.val $(hy))⟩
  haveI := mk_eq_zero_iff.1 (b.mk_eq_rank''.symm ▸ lt_one_iff_zero.1 (h.lt_of_ne h1))
  haveI := b.repr.toEquiv.subsingleton
  exact False.elim <| one_ne_zero congr(S.val $(Subsingleton.elim 1 0))

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