Constructing linear maps

Stream: Is there code for X?

[Daniel Weber]

I want to do a projective transformation, so I need to construct a linear map f : V →ₗ[K] V such that $f(p_1) = e_1$, $f(p_2) = e_2$ (for two linearly independent $p_1, p_2$), and I don't care about the rest of its values as long as it's linear and injective. What would be the nicest way to construct it?

[Kevin Buzzard]

Can you ask your question as an explicit sorry in a #mwe ? That's the best way to ask questions such as this.

[Daniel Weber]

Sure (my earlier spelling of this was bit awkward, so I didn't want to send it):

import Mathlib

open Finset Classical

variable {α V : Type*} [DivisionRing α] [Fintype α] [AddCommMonoid V] [Module α V]

theorem construct_map
  (p₁ p₂ v₁ v₂ : V) (h : LinearIndependent α ((↑) : ({p₁, p₂} : Set V) → V)) (h₂ : LinearIndependent α ((↑) : ({v₁, v₂} : Set V) → V))
  : ∃ l : V →ₗ[α] V, l p₁ = v₁ ∧ l p₂ = v₂ ∧ Function.Injective l := sorry

[Sophie Morel]

(deleted)

[Sophie Morel]

Denote by $W_1$ the span of $p_1, p_2$ and by $W_2$ the span of $v_1,v_2$. If V is finite-dimensional, what you want to do is easy: choose a complement $W'_i$ of $W_i$ (Submodule.exists_isCompl), you have a linear equivalence eᵢ : Wᵢ × W'ᵢ ≃ₗ V (Submodule.prodEquivOfIsCompl). You also have a linear equivalence f from $W_1$ to $W_2$ sending the obvious basis of $W_1$ to the obvious basis of $W_2$, and a linear equivalence f' from $W'_1$ to $W'_2$ given by the fact that these vector spaces have the same dimension, which is dim(V)-2 (LinearEquiv.ofFinrankEq). Now you just compose e, e.symm, and LinearEquiv.prod f f' in the right order to get a linear equivalence from V to V that sends $p_i$ to $v_i$.

[Sophie Morel]

If V is not finite-dimensional, the easiest way I see is to first work in the finite-dimensional subspace V' spanned by the $p_i$ and $v_i$. You can define a linear auto-equivalence e'of V' extending your f as before. Then choose a complement V'' of V', and use the linear equivalence between $V$ and $V' \times V''$, as well as the product of e' and of the identity of V'', to get a linear auto-equivalence of V extending your f.

[Sophie Morel]

I can give you code that does all that, but it's written very quickly and absolutely not optimized.

[Daniel Weber]

Sophie Morel said:

Denote by $W_1$ the span of $p_1, p_2$ and by $W_2$ the span of $v_1,v_2$. If V is finite-dimensional, what you want to do is easy: choose a complement $W'_i$ of $W_i$ (Submodule.exists_isCompl), you have a linear equivalence eᵢ : Wᵢ × W'ᵢ ≃ₗ V (Submodule.prodEquivOfIsCompl). You also have a linear equivalence f from $W_1$ to $W_2$ sending the obvious basis of $W_1$ to the obvious basis of $W_2$, and a linear equivalence f' from $W'_1$ to $W'_2$ given by the fact that these vector spaces have the same dimension, which is dim(V)-2 (LinearEquiv.ofFinrankEq). Now you just compose e, e.symm, and LinearEquiv.prod f f' in the right order to get a lineare quivalence from V to V that sends $p_i$ to $v_i$.

Thanks! How can this f be constructed?

[Sophie Morel]

If $b_i$ is a basis of $W_i$ for $i=1,2$, and if $b_1$ and $b_2$ are indexed by the same type, then you take b₁.repr.trans b₂.repr.symm.

[Sophie Morel]

The idea is that, in Lean, a basis b of W indexed by a type u is literally a linear equivalence from V to the free module on the basis u, i.e. u →₀ α (finitely supported functions from u to your base field). This equivalence is called b.repr.

[Daniel Weber]

Ok, thanks! I want to show independence using docs#linearIndependent_pair , so I should just use docs#Basis.reindex to make them indexed by the same type?

[Sophie Morel]

Here it would be easier to represent your pairs of vectors as p, v : Fin 2 → V . Then the linear independence condition becomes hp : LinearIndependent α p, you can set W₁ := Submodule.span α (Set.range p) and then b₁ := Basis.span hp.

[Sophie Morel]

And the same for v. Then both your bases will be indexed by Fin 2.

[Daniel Weber]

What would be a nice way to show independence, then? docs#linearIndependent_pair uses a different indexing

[Daniel Weber]

Also, is there a nice way to construct such a function, given two elements of V?

[Sophie Morel]

I don't understand the question. Show independence of what ? In your question, the linear independence of p and v was a hypothesis.

[Sophie Morel]

Daniel Weber said:

Also, is there a nice way to construct such a function, given two elements of V?

example (a b : V) : Fin 2 → V := fun i ↦ if i = 0 then a else b

[Sophie Morel]

I think I understand the question about linear independence now. Use linearIndependent_fin2.

[Daniel Weber]

Ok, thanks!

[Notification Bot]

Daniel Weber has marked this topic as resolved.

[Notification Bot]

Daniel Weber has marked this topic as unresolved.

[Daniel Weber]

To prove I have a basis one of the things I need to prove is:

import Mathlib

variable {α : Type*} {v : Type*} [DivisionRing α] [Fintype α] [AddCommMonoid V] [Module α V]

lemma mem_span (S : Set V) (x : S) : ↑x ∈ Submodule.span α S := by
  have : S ⊆ Submodule.span α S := Submodule.subset_span ..
  aesop

example (S : Set V) : (Submodule.span α (Set.range (fun (x : S) => ⟨x, mem_span S x⟩)) : Submodule α (Submodule.span α S)) = ⊤ := by
  sorry

how can I do that? Is it proven somewhere in mathlib?

[Kevin Buzzard]

Are you sure that this is a good path to whatever you're trying to do? You have (S : Set V) (x : S) in mem_span so you have a term S and immediately you're treating it as a type with (x : S). This introduces a coercion ↑ and as you're finding, up-arrows make things complicated. The conclusion we might want to draw is that perhaps it's best not to introduce a coercion unless we absolutely have to. mem_span will definitely not be in mathlib because it's as ugly as sin. Why not have x : X and hx : x \in S instead of x : \u S (because that's what x : S expands to)? There are no up-arrows in the x \in S version, and that version of mem_span will be in mathlib.

[Kevin Buzzard]

Similarly, if at some point you took a submodule of a submodule which you coerced to a module (which you seem to have done, the type Submodule α ↥(span α S) is buried in your lemma) -- could it have been easier to have just taken a submodule of the big module and added a hypothesis that it was <= the first submodule? No coercion is then involved and you have access to all the lattice theory API.

[Daniel Weber]

I'm definitely not sure about it, although this is just how I spelled it for the #mwe. What I actually need is:

import Mathlib

variable {α : Type*} [DivisionRing α] [Fintype α]

instance instMem : Membership (α × α) (Submodule α (α × α × α)) where
  mem x l := ⟨x.1, x.2, 1⟩ ∈ l

def Submodule.pair (i j : α × α) := Submodule.span α (M := α × α × α) {⟨i.1, i.2, 1⟩, ⟨j.1, j.2, 1⟩}

lemma mem_span1 (i j : α × α) : i ∈ Submodule.pair i j := by
  have : ({⟨i.1, i.2, 1⟩, ⟨j.1, j.2, 1⟩} : Set (α × α × α)) ⊆ Submodule.pair i j := by apply Submodule.subset_span
  aesop

lemma mem_span2 (i j : α × α) : j ∈ Submodule.pair i j := by
  have : ({⟨i.1, i.2, 1⟩, ⟨j.1, j.2, 1⟩} : Set (α × α × α)) ⊆ Submodule.pair i j := by apply Submodule.subset_span
  aesop

noncomputable def Submodule.pair_basis (i j : α × α) (h : i ≠ j) : Basis (Fin 2) α (Submodule.pair i j) := Basis.mk (ι := Fin 2)
  (v := fun x => if x = 0 then ⟨⟨i.1,i.2,1⟩, mem_span1 i j⟩ else ⟨⟨j.1,j.2,1⟩, mem_span2 i j⟩) (by
  rw [linearIndependent_fin2]
  aesop
  ) (by
  simp [Submodule.pair]
  rw [←Submodule.span_span_coe_preimage]
  congr
  ext x
  aesop
  exists 0
  intro a
  simp at a
  exists 1
  intro a
  simp at a
  )

I managed to prove it, but it's quite ugly, so I'd love suggestions for a nicer way to write this.

[Kevin Buzzard]

Here's some tidy-up but I'm sure that more can be golfed off this:

import Mathlib
set_option autoImplicit true

variable {α : Type*} [DivisionRing α] [Fintype α]

instance instMem : Membership (α × α) (Submodule α (α × α × α)) where
  mem x l := ⟨x.1, x.2, 1⟩ ∈ l

def Submodule.pair (i j : α × α) :=
  Submodule.span α (M := α × α × α) {⟨i.1, i.2, 1⟩, ⟨j.1, j.2, 1⟩}

lemma mem_span1 (i j : α × α) : i ∈ Submodule.pair i j :=
  Submodule.subset_span <| Or.inl rfl

lemma mem_span2 (i j : α × α) : j ∈ Submodule.pair i j :=
  Submodule.subset_span <| Or.inr rfl

noncomputable def Submodule.pair_basis (i j : α × α) (h : i ≠ j) :
    Basis (Fin 2) α (Submodule.pair i j) :=
  Basis.mk
    (ι := Fin 2)
    (v := ![⟨⟨i.1,i.2,1⟩, mem_span1 i j⟩,⟨⟨j.1,j.2,1⟩, mem_span2 i j⟩])
    (by rw [linearIndependent_fin2]
        aesop)
    (by simp [Submodule.pair]
        rw [←Submodule.span_span_coe_preimage]
        congr
        ext x
        aesop
        )

[Sophie Morel]

I am so confused, what are you trying to do, in words ?

[Daniel Weber]

Sophie Morel said:

I am so confused, what are you trying to do, in words ?

I'm trying to do a projective transformation, moving a line defined by two points to the line at infinity. I define the line as the span of ⟨i.1, i.2, 1⟩ and ⟨j.1, j.2, 1⟩, and I want to show that this is a basis (so I could do what you outlined earlier)

[Sophie Morel]

To construct a basis of the span of a linearly independent family, the easiest way is Basis.span. That will require you to put an AddCommGroup instance on V and not just an AddCommMonoid instance, which you should probably do anyway, as your base Semiring is a ring.

[Kevin Buzzard]

Finite division rings are fields so there'd be no harm in assuming that too :-)

[Sophie Morel]

Also, since your base ring α is finite, I don't understand why you make it a DivisionRinginstead of a Field. (A finite division ring is automatically a field.) That probably won't change anything.

[Sophie Morel]

Haha, we have one brain cell, Kevin!

[Sophie Morel]

The DivisionRing is probably unimportant, but the AddCommMonoid would keep you from using some results, and since the base ring has a -1, I think that V will automatically be a group.

[Daniel Weber]

Thanks, I managed to simplify this to:

import Mathlib

variable {α : Type*} [DivisionRing α] [Fintype α]

instance instMem : Membership (α × α) (Submodule α (α × α × α)) where
  mem x l := ⟨x.1, x.2, 1⟩ ∈ l

def Submodule.pair (i j : α × α) := Submodule.span α (M := α × α × α) {⟨i.1, i.2, 1⟩, ⟨j.1, j.2, 1⟩}

lemma mem_span1 (i j : α × α) : i ∈ Submodule.pair i j := Submodule.subset_span <| Or.inl rfl

lemma mem_span2 (i j : α × α) : j ∈ Submodule.pair i j := Submodule.subset_span <| Or.inr rfl

lemma rangevec : Set.range ![a, b] = {a, b} := by aesop

noncomputable def Submodule.pair_basis (i j : α × α) (h : i ≠ j) : Basis (Fin 2) α (Submodule.pair i j) := by
  have := Basis.span
    (R := α)
    (M := α × α × α)
    (v := ![⟨i.1,i.2,1⟩, ⟨j.1,j.2,1⟩]) (by
      rw [linearIndependent_fin2]
      aesop
    )
  rw [rangevec] at this
  exact this

Any more suggestions?

[Daniel Weber]

By the way, what does autoImplicit do?

[Johan Commelin]

It means that if you mention foo as a variable in the statement of your theorem, and Lean has never seen foo before, then it will not complain, but just guess that it should be a new fresh variable.

[Kevin Buzzard]

I cut and pasted your code into a scratch file in mathlib but that has autoImplicits off so I had to turn them on in your file to get it to work for me, I had an error on a V or something in the file you posted