Standard inclusion R^n → R^{n+1}

Stream: Is there code for X?

[Riccardo Brasca]

What is the best way of defining the standard inclusion of $R^n$ inside $R^{n+1}$ (meaning adding $0$ as the last component) as a linear map? Thank you!

[Eric Wieser]

is the unbundled version docs#fin.snoc (fin.snoc v 0)?

[Filippo A. E. Nuccio]

Stupid related question (on your answer): why "unbundled"?

[Eric Wieser]

"unbundled" meaning "without any proof that it is linear"

[Yaël Dillies]

because fin.snoc isn't (defined as) a linear map.

[Filippo A. E. Nuccio]

Crystal clear, thanks.

[Riccardo Brasca]

To be precise what I'm looking for is

import linear_algebra.basic

example (n : ℕ) (R : Type u) [semiring R] : (fin n → R) →ₗ[R] (fin (n + 1) → R) := sorry

[Riccardo Brasca]

And to be honest I am having troubles in understand what fin.snoc does...

[Ruben Van de Velde]

Adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.

[Eric Wieser]

I would hope you can build it from (fin n → R) →ₗ[R] (fin n → R) × (fin 1 → R) (which is just docs#linear_map.inl), and then maybe docs#linear_map.coprod

[Kevin Buzzard]

I'd be tempted to just build it by hand!

[Riccardo Brasca]

Yes, with basis it should be easy, using fin.cast_succ. I am surprised that nobody needed it, but maybe it is too specific for mathlib :)

[Eric Wieser]

The version that inserts zero at the start instead of the end might be more likely to exist

[Eric Wieser]

Kevin Buzzard said:

I'd be tempted to just build it by hand!

Yes, I agree - we should probably have fin.snoc_zero_zero and fin.snoc_zero_add lemmas that say fin.snoc 0 0 = 0 and fin.snoc (v + w) 0 = fin.snoc v 0 + fin.snoc w 0

[Eric Wieser]

Then the final step of bundling the map becomes easy

[Shing Tak Lam]

Eric Wieser said:

Then the final step of bundling the map becomes easy

it's not very hard anyways

example (n : ℕ) (R : Type u) [semiring R] : (fin n → R) →ₗ[R] (fin (n + 1) → R) :=
{ to_fun := λ v, fin.snoc v 0,
  map_add' := λ x y, by ext t; refine fin.last_cases _ _ t; simp,
  map_smul' := λ x y, by ext t; refine fin.last_cases _ _ t; simp }

[Riccardo Brasca]

I think it is

import linear_algebra.std_basis

noncomputable example (n : ℕ) (R : Type u) [semiring R] : (fin n → R) →ₗ[R] (fin (n + 1) → R) :=
basis.constr (pi.basis_fun R (fin n)) ℕ (λ i, pi.basis_fun R (fin (n + 1)) i)

[Eric Rodriguez]

I will warn that when I was using snoc I hated the stupid thing

[Eric Rodriguez]

cons is much better behaved

[Eric Rodriguez]

obviously it's mathematically weird to insert at the start but it's a much more pleasant lean experience

[Eric Wieser]

Using noncomputable seems a bit extreme for something so trivial!

[Riccardo Brasca]

It's always interesting to see how math people and CS people think differently. Of course adding 0 at the end (or at the beginning) is totally trivial, but if I want a linear map my brain immediately say "of course you can do it, it is a free module, so just say where the standard basis should go". And somehow I feel it's better to check that this really just a 0 somewhere rather than checking that adding a 0 is linear :)

[Sebastien Gouezel]

By the way, are you sure it's really what you need? I'm asking because in #8898 I am doing a Gauss pivot-like argument, with an induction on the dimension to reduce a matrix. At first, I tried precisely with an embedding of fin n in fin (n+1) like you're doing, but in the end it was much nicer when using a sum type fin n ⊕ unit (because it avoids all casts, all nat inequalities, and things on the two components are distinguished definitionally by the kernel), and doing a reindexing at the very end of the argument.

[Reid Barton]

fin.snoc and fin.cons are both really awkward to use because they handle the case of a dependent function. I should finish that finvec PR some day...

[Riccardo Brasca]

Sebastien Gouezel said:

By the way, are you sure it's really what you need? I'm asking because in #8898 I am doing a Gauss pivot-like argument, with an induction on the dimension to reduce a matrix. At first, I tried precisely with an embedding of fin n in fin (n+1) like you're doing, but in the end it was much nicer when using a sum type fin n ⊕ unit (because it avoids all casts, all nat inequalities, and things on the two components are distinguished definitionally by the kernel), and doing a reindexing at the very end of the argument.

I am not sure. I want to prove that a commutative ring satisfies docs#strong_rank_condition. In practice it is enough to show that $R^{n+1}$ does not embed in $R^n$, and the first step of the proof I want to formalize is to consider the composition of $R^{n+1} \to R^n$ with the inclusion.

[Riccardo Brasca]

Maybe I can just prove that the strong rank condition is equivalent to the nonexistence of an injective morphism ((fin n ⊕ unit )→ R) → (fin n → R)

[Yakov Pechersky]

Probably as easily provable for any sum type where the other side isn't trivial

[Riccardo Brasca]

Shing Tak Lam said:

Eric Wieser said:

Then the final step of bundling the map becomes easy

it's not very hard anyways

example (n : ℕ) (R : Type u) [semiring R] : (fin n → R) →ₗ[R] (fin (n + 1) → R) :=
{ to_fun := λ v, fin.snoc v 0,
  map_add' := λ x y, by ext t; refine fin.last_cases _ _ t; simp,
  map_smul' := λ x y, by ext t; refine fin.last_cases _ _ t; simp }

Do you see an easy way to generalize this to the inclusion $R^n \to R^m$ where $n < m$?

[Adam Topaz]

@Riccardo Brasca you can use docs#fin_sum_fin_equiv to obtain $R^a \to R^{a+b}$.

[Kevin Buzzard]

How about defining an R-alg hom R^S -> R^T for every injection S -> T?

[Riccardo Brasca]

Indeed my question is rather how to do this correctly in mathlib. I see a lot of ways of doing it by hand with different degree of generality. What I need is that the map is injective, linear and the last component of any element of the image is $0$ (the last component or more generally any component whose index is not in the (image of) the first set).

[Riccardo Brasca]

I ended up doing it with in some generality in #9128. Not sure it's the best way...