basisOfFiniteTypeTorsionFree — Mathlib

English

A finite type torsion-free module over a PID admits a basis; there exists a finite index set and a basis for the module.

Русский

Конечный ранговый тензор-тривиальный модуль над PID допускает базис; существует конечный индекс и база модуля.

LaTeX

$$$\\exists n, Basis (Fin n) R M$ under NoZeroSMulDivisors and span-top condition$$

Lean4

/-- A finite type torsion free module over a PID admits a basis. -/
noncomputable def basisOfFiniteTypeTorsionFree [Fintype ι] {s : ι → M} (hs : span R (range s) = ⊤)
    [NoZeroSMulDivisors R M] : Σ n : ℕ, Basis (Fin n) R M := by
  classical
    -- We define `N` as the submodule spanned by a maximal linear independent subfamily of `s`

  have := exists_maximal_linearIndepOn R s
  let I : Set ι := this.choose
  obtain
    ⟨indepI : LinearIndependent R (s ∘ (fun x => x) : I → M), hI :
      ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
    this.choose_spec
  let N :=
    span R
      (range <| (s ∘ (fun x => x) : I → M))
        -- same as `span R (s '' I)` but more convenient

  let _sI : I → N := fun i ↦
    ⟨s i.1, subset_span (mem_range_self i)⟩
      -- `s` restricted to `I` is a basis of `N`

  let sI_basis : Basis I R N := Basis.span indepI
  have exists_a : ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N :=
    by
    intro i
    by_cases hi : i ∈ I
    · use 1, zero_ne_one.symm
      rw [one_smul]
      exact subset_span (mem_range_self (⟨i, hi⟩ : I))
    · simpa [image_eq_range s I] using hI i hi
  choose a ha ha' using exists_a
  let A := ∏ i, a i
  have hA : A ≠ 0 := by
    rw [Finset.prod_ne_zero_iff]
    simpa using ha
  let φ : M →ₗ[R] M := LinearMap.lsmul R M A
  have : LinearMap.ker φ = ⊥ := @LinearMap.ker_lsmul R M _ _ _ _ _ hA
  let ψ := LinearEquiv.ofInjective φ (LinearMap.ker_eq_bot.mp this)
  have : LinearMap.range φ ≤ N := by
    -- as announced, `A • M ⊆ N`

    suffices ∀ i, φ (s i) ∈ N by
      rw [LinearMap.range_eq_map, ← hs, map_span_le]
      rintro _ ⟨i, rfl⟩
      apply this
    intro i
    calc
      (∏ j ∈ { i }ᶜ, a j) • a i • s i ∈ N := N.smul_mem _ (ha' i)
      _ = (∏ j, a j) • s i := by
        rw [Fintype.prod_eq_prod_compl_mul i, mul_smul]
          -- Since a submodule of a free `R`-module is free, we get that `A • M` is free

  obtain ⟨n, b : Basis (Fin n) R (LinearMap.range φ)⟩ := Submodule.basisOfPidOfLE this sI_basis
  exact ⟨n, b.map ψ.symm⟩

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