Existence of a suitable basis

Stream: Is there code for X?

[Antoine Chambert-Loir]

In #31138, I prove the result that if $f$ is a nonzero linear form of a $K$-vector space $V$ and $v\in V$ is a nonzero vector such that $f(v)=0$, then there exists a basis of $V$ containing $v$ and such that $f$ is one of the coordinate functions (for another vector basis).

This is at exists_basis_of_pairing_eq_zero
Presumably, these 150 lines can be shortened.

[Aaron Liu]

my attempt

import Mathlib

namespace LinearMap

open Polynomial LinearMap

universe u v

variable {K : Type u} {V : Type v} [Field K] [AddCommGroup V]
  [Module K V] [FiniteDimensional K V] {f : Module.Dual K V} {v : V}

omit [FiniteDimensional K V] in
/-- In a vector space, given a nonzero linear form `f`,
a nonzero vector `v` such that `f v = 0`,
there exists a basis `b` with two distinct indices `i`, `j`
such that `v = b i` and `f = b.coord j`. -/
theorem exists_basis_of_pairing_eq_zero
    (hfv : f v = 0) (hf : f ≠ 0) (hv : v ≠ 0) :
    ∃ (n : Set V) (b : Module.Basis n K V) (i j : n),
      i ≠ j ∧ v = b i ∧ f = b.coord j := by
  obtain ⟨u, hfu⟩ : ∃ u : V, f u = 1 := by
    contrapose! hf
    ext x
    by_contra! hx
    simpa [inv_mul_cancel₀ hx] using hf ((f x)⁻¹ • x)
  let w : LinearMap.ker f := ⟨v, hfv⟩
  have hw : LinearIndepOn K _root_.id {w} := by
    simp [Subtype.ext_iff, w, hv]
  let bKer := Module.Basis.extend hw
  let s := insert u (Set.range ((LinearMap.ker f).subtype ∘ bKer))
  have hr : Submodule.span K (Set.range ((LinearMap.ker f).subtype ∘ bKer)) =
      LinearMap.ker f := by
    unfold bKer
    rw [Set.range_comp, Submodule.span_image, Module.Basis.coe_extend, Subtype.range_coe,
      LinearIndepOn.span_extend_eq_span, Submodule.span_univ, Submodule.map_top,
      Submodule.range_subtype]
  have hu : LinearIndepOn K _root_.id s := by
    unfold s
    apply LinearIndepOn.id_insert
    · unfold bKer
      rw [Module.Basis.coe_extend]
      apply LinearIndependent.linearIndepOn_id
      rw [LinearMap.linearIndependent_iff_of_injOn _ (Submodule.subtype_injective _).injOn]
      apply LinearIndependent.of_linearIndepOn_id_range Subtype.val_injective
      rw [Subtype.range_coe]
      apply LinearIndepOn.linearIndepOn_extend
    · rw [hr, LinearMap.mem_ker, hfu]
      exact one_ne_zero
  have hs : ⊤ ≤ Submodule.span K (Set.range fun x : s => (x : V)) := by
    intro x _
    unfold s
    rw [Subtype.range_coe, Submodule.span_insert, hr]
    rw [← add_sub_cancel (f x • u) x]
    apply add_mem
    · apply Submodule.smul_mem
      apply Submodule.mem_sup_left
      apply Submodule.mem_span_of_mem
      simp
    · apply Submodule.mem_sup_right
      rw [LinearMap.mem_ker]
      simp [hfu]
  let b := Module.Basis.mk hu.linearIndependent hs
  refine ⟨_, b, ⟨v, ?_⟩, ⟨u, ?_⟩, ?_, by simp [b], ?_⟩
  · right
    refine ⟨⟨w, ?_⟩, by simp [bKer, w]⟩
    apply LinearIndepOn.subset_extend
    simp
  · exact Set.mem_insert u _
  · intro hvu
    apply zero_ne_one' K
    rw [← hfu, ← hfv]
    exact congrArg (f ∘ Subtype.val) hvu
  · ext x
    conv_rhs =>
      rw [← add_sub_cancel (f x • u) x, map_add, map_smul]
      enter [1, 2]
      apply Module.Basis.mk_coord_apply_eq
    rw [smul_eq_mul, mul_one, eq_comm, add_eq_left, Module.Basis.coord_apply]
    have hss := congrArg f (b.repr.symm_apply_apply (x - f x • u))
    rw [Module.Basis.repr_symm_apply, Finsupp.apply_linearCombination,
      map_sub f, map_smul f, hfu, smul_eq_mul, mul_one, sub_self] at hss
    classical
    suffices hfb : f ∘ b = Pi.single (⟨u, Set.mem_insert u _⟩ : s) 1 by
      rw [← hss, hfb, Finsupp.linearCombination_single_index, smul_eq_mul, mul_one]
    ext ⟨i, hi⟩
    obtain rfl | hi := hi
    · simp [b, hfu]
    · have hfi : f i = 0 := by
        rw [← LinearMap.mem_ker, ← hr]
        exact Submodule.mem_span_of_mem hi
      have hiu : i ≠ u := ne_of_apply_ne f (by simp [hfi, hfu])
      simp [b, hfi, hiu]

[Yury G. Kudryashov]

Almost same:

theorem exists_basis_of_pairing_eq_zero
    (hfv : f v = 0) (hf : f ≠ 0) (hv : v ≠ 0) :
    ∃ (n : Set V) (b : Module.Basis n K V) (i j : n),
      i ≠ j ∧ v = b i ∧ f = b.coord j := by
  lift v to LinearMap.ker f using hfv
  have : LinearIndepOn K _root_.id {v} := by simpa using hv
  set b₁ : Module.Basis _ K (LinearMap.ker f) := .extend this
  obtain ⟨w, hw⟩ : ∃ w, f w = 1 := by
    simp only [ne_eq, DFunLike.ext_iff, not_forall] at hf
    rcases hf with ⟨w, hw⟩
    use (f w)⁻¹ • w
    simp_all
  set s : Set V := (LinearMap.ker f).subtype '' Set.range b₁
  have hs : Submodule.span K s = LinearMap.ker f := by
    simp only [s, Submodule.span_image]
    simp
  have hvs : v.1 ∈ s := by
    refine ⟨v, ?_, by simp⟩
    simp [b₁, this.subset_extend _ _]
  set n := insert w s
  have H₁ : LinearIndepOn K _root_.id n := by
    apply LinearIndepOn.id_insert
    · apply LinearIndepOn.image
      · exact b₁.linearIndependent.linearIndepOn_id
      · simp
    · simp [hs, hw]
  have H₂ : ⊤ ≤ Submodule.span K n := by
    rintro x -
    simp only [n, Submodule.mem_span_insert']
    use -f x
    simp [hs, hw]
  set b := Module.Basis.mk H₁ (by simpa using H₂)
  refine ⟨n, b, ⟨v, by simp [n, hvs]⟩, ⟨w, by simp [n]⟩, ?_, by simp [b], ?_⟩
  · apply_fun (f ∘ (↑))
    simp [hw]
  · apply b.ext
    intro i
    rw [Module.Basis.coord_apply, Module.Basis.repr_self]
    simp only [b, Module.Basis.mk_apply]
    rcases i with ⟨x, rfl | ⟨x, hx, rfl⟩⟩
    · simp [hw]
    · suffices x ≠ w by simp [this]
      apply_fun f
      simp [hw]

[Antoine Chambert-Loir]

Thanks!!!