field extensions and linear independence

Stream: maths

[Jakob von Raumer]

I'm considering formalising the following theorem: 235.png

[Jakob von Raumer]

It looks like it's quite painful to formalise and I wondered if one of you recognize the core argument from some other proof?

[Kevin Buzzard]

If you have a non-trivial finite linear combination $\sum_i \lambda_i x_i=0$ in $L^I$ then for every $K$-linear map $\phi:L\to K$ you can push the relation forward and deduce $\sum_i\phi(\lambda_i)x_i=0$ in $K^I$, which means that all the $\lambda_i$ are zero in every $L$-linear map $L\to K$, so by general vector space nonsense they're all 0.

Another way to think about this approach: choose a $K$-basis for $L$, say $e_j$. Then for $\sum_i \lambda_i x_i=0$ write each $\lambda_i$ as a $K$-linear combination of the $e_j$ and now look at $e_j$ components and use $K$-lin-ind to prove that all the components of each $\lambda_i$ are zero.

[Jakob von Raumer]

Kevin Buzzard said:

If you have a non-trivial finite linear combination $\sum_i \lambda_i x_i=0$ in $L^I$ then for every $K$-linear map $\phi:L\to K$ you can push the relation forward and deduce $\sum_i\phi(\lambda_i)x_i=0$ in $K^I$, which means that all the $\lambda_i$ are zero in every $L$-linear map $L\to K$, so by general vector space nonsense they're all 0.

Ah yes, so that implication might be in linear_algebra somewhere.

[Jakob von Raumer]

As for the second approach: Is $L$ guaranteed to have a $K$-basis if it's an arbitrary algebra over $K$?

[Kevin Buzzard]

Every vector space has a basis (this is probably equivalent to AC)

[Kevin Buzzard]

(so it does in my head but I can't speak for anyone else's head :-) )

[Jakob von Raumer]

I keep on forgetting that that is the head I should be using for this formalisation, and not the constructivist one ;)

[Jakob von Raumer]

Kevin Buzzard said:

which means that all the $\lambda_i$ are zero in every $L$-linear map $L\to K$, so by general vector space nonsense they're all 0.

This had in fact not been added to mathlib yet...

theorem eq_zero_of_linear_maps_to_zero
  {K L : Type*} [field K] [add_comm_group L] [module K L]
  (x : L) (hφs : ∀ (φ : L →ₗ[K] K), φ x = 0) : x = 0 :=
begin
  by_cases ha : x = 0,
  { assumption },
  { exfalso, apply @zero_ne_one K,
    let s : set L := {x},
    have xind : linear_independent K (@coe s L _) := linear_independent_singleton ha,
    let b := extend xind,
    rw [ ←hφs (b.to_dual x),
      show x = b ⟨x, linear_independent.subset_extend _ _ (set.mem_singleton x)⟩,
        by rw [coe_extend, subtype.coe_mk],
      coe_to_dual_self, coord_apply, repr_self, finsupp.single_eq_same] }
end

[Damiano Testa]

You can probably replace the first three lines by

by_contradiction ha,
apply @zero_ne_one K,

and get rid of some indenting.

[Jakob von Raumer]

Ah, thanks, yes :)