basis_singleton_iff — Mathlib

English

Over a nontrivial ring with NoZeroSMulDivisors, there exists a basis for M with a one-dimensional span if and only if M is a simple module of the form x·R for some nonzero x.

Русский

Существование базиса над R в M с единичной размерностью эквивалентно существованию модуля вида x·R для некоторого ненулевого x.

LaTeX

$$$\\text{basis}_\\text{singleton} \\iff \\exists x \\neq 0, \\forall y\\in M, \\exists r:\\, R, r\\cdot x = y$$$

Lean4

theorem basis_singleton_iff {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    (ι : Type*) [Unique ι] : Nonempty (Basis ι R M) ↔ ∃ x ≠ 0, ∀ y : M, ∃ r : R, r • x = y :=
  by
  constructor
  · rintro ⟨b⟩
    refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩
    simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq
  · rintro ⟨x, nz, w⟩
    refine
      ⟨ofRepr <|
          LinearEquiv.symm
            { toFun := fun f => f default • x
              invFun := fun y => Finsupp.single default (w y).choose
              left_inv := fun f => Finsupp.unique_ext ?_
              right_inv := fun y => ?_
              map_add' := fun y z => ?_
              map_smul' := fun c y => ?_ }⟩
    · simp [Finsupp.add_apply, add_smul]
    · simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
      rw [← smul_assoc]
    · refine smul_left_injective _ nz ?_
      simp only [Finsupp.single_eq_same]
      exact (w (f default • x)).choose_spec
    · simp only [Finsupp.single_eq_same]
      exact (w y).choose_spec

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