Quotient module as submodule

Stream: Is there code for X?

[Alena Gusakov]

I'm trying to write a helper lemma that says something like (V / p \times p) \equiv\_l[K] V. Right now there is prodEquivOfIsCompl, which requires two compl submodules. Is there a canonical way to treat V / p as a submodule of V?

[Kevin Buzzard]

Is K a field?

[Alena Gusakov]

Yeah, andModule K V so I'm working in vector spaces/subspaces

[Kevin Buzzard]

By the way there is definitely no canonical way to treat V/p as a submodule of V :-)

[Alena Gusakov]

I guess canonical is the wrong word, I more mean is there a way for V/p to be treated as a submodule of V

[Alena Gusakov]

I know there's quotientEquivOfIsCompl but that requires me to produce a submodule q such that IsCompl p q

[Adam Topaz]

there should be a lemma saying that any surjective linear map over a field splits.

[Sophie Morel]

When I needed that property, I used Module.projective_lifting_property. Normally modules over a field will have a Module.Projective instance on them so it will work.

[Alena Gusakov]

I keep getting the tactic 'cases' failed, nested error: tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
error when I try to use projective_lifting_property - is this something you usually encounter? I can post an MWE if that helps

[Adam Topaz]

What’s the goal?

[Adam Topaz]

Worst case scenario you can use choice

[Alena Gusakov]

I'm just trying to show the equivalence {W : Submodule K V | FiniteDimensional.finrank K W = k} ≃ {W : Submodule K ((V ⧸ (K ∙ a)) × (K ∙ a)) | FiniteDimensional.finrank K W = k}

[Alena Gusakov]

Which isn't quite what I need for what I'm doing but I thought it would be a useful helper lemma

[Sophie Morel]

If you're trying to construct something like your equivalence, as opposed to just proving a statement, by eliminating an existential quantifier (that means that you have a statement like ∃ x, p x and you apply a tactic like obtain or let to define a x satisfying p), then Lean will complain. The way around this is to use Classical.choose, as Adam said.
For example, in your case, you can obtain the linear equivalence between V and (V ⧸ span K {a}) × span K {a} like so:

import Mathlib.Algebra.Module.Projective

variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V]
variable {a : V} {k : ℕ}

open Submodule

noncomputable def truc : V ≃ₗ[K] (V ⧸ span K {a}) ×  span K {a} :=
  (Classical.choice (quotient_prod_linearEquiv (span K {a}))).symm

Note that Lean forced me to mark the definition as noncomputable, because it is not constructive.

Once you have the linear equivalence you can define the equivalence on submodules easily by hand, but maybe mathlib already has something like that, I am not sure.

[Alena Gusakov]

I guess what I'm confused about is, shouldn't the submodule q such that isCompl p q be unique when the ambient space is a vector space? Maybe I'm just really rusty on my linear algebra.

[Adam Topaz]

it's not unique.

[Adam Topaz]

A subspace can have many complements.

[Adam Topaz]

For example, if $(x_0,y_0)$ is any point in $k^2$ ($k$ a field) with $y_0$ is nonzero, then the span of $(x_0,y_0)$ is a complement for the span of $(1,0)$.

[Alena Gusakov]

Ah, I think I was thinking of orthogonal space

[Alena Gusakov]

I guess, stepping back, what I'm trying to prove is a recurrence relation between the number of k-dimensional subspaces of a finite-dimensional vector space V over a finite field, and k- and (k-1)-dimensional subspaces of V / p where p is some one-dimensional subspace

[Alena Gusakov]

The noncomputable definitions we have show that there is some equivalence between V / p \times p and V, but what I think I need is the specific equivalence that uses projections of V to V / p and p

[Johan Commelin]

In general there is no "projection from V to p"

[Sophie Morel]

Also, I don't understand why you need to have a specific form for the equivalence. Once you know that V and V/p x p are linearly equivalent, you also know that they have the same number of k-dimensional subspaces, so you can start counting k-dimensional subspaces of V/p x p directly.

[Alena Gusakov]

So I might be misunderstanding, but the recurrence I'm trying to prove fixes a projection f of V with nullspace p of dimension 1, and that projection is what gives us the equivalence relation

[Alena Gusakov]

I'm trying to follow the last paragraph of https://en.wikipedia.org/wiki/Gaussian_binomial_coefficient#Analogs_of_Pascal's_identity

[Alena Gusakov]

Sophie Morel said:

Also, I don't understand why you need to have a specific form for the equivalence. Once you know that V and V/p x p are linearly equivalent, you also know that they have the same number of k-dimensional subspaces, so you can start counting k-dimensional subspaces of V/p x p directly.

I think I need the specific equivalence because I'll have to break it down into the maps from V to V/p and V to p in order to prove the recurrence I want

[Alena Gusakov]

If we let ${n \choose k}_q$ denote the number of $k$-dimensional subspaces of an $n$-dimensional vector space over field of size $q$ where $q$ is a prime power, then we have ${n \choose k}_q = q^k{n - 1 \choose k}_q + {n - 1 \choose k - 1}_q$

[Alena Gusakov]

and the way I want to go about proving it, per the wikipedia article, is fixing a one-dimensional subspace $p$ of $V$ and an equivalence between $V$ and $V / p \times p$, and then considering the case where every element of a $k$-dim subspace of $V / p \times p$ is of the form $(x, 0)$ which corresponds to the first part of the term, and the other case corresponds to the second part of the term

[Sophie Morel]

What I am saying is that once you know that V and V/p x p are equivalent, you can just assume that V is equal to V/p x p (because equivalent vector spaces will have the same number of k-dimensional subspaces). For V/p x p, you know what the maps to V/p and p are, they are just the two projections.

[Alena Gusakov]

So I've been working on this and I think I'm doing it poorly - this definition that I have is really tedious to prove and I assume there's probably a better way of setting it up. Does anyone have any suggestions?

def succDimSubspaces_equivDimSubspaces (a : V) (ha : a ≠ 0) (k : ℕ) :
  {W : Submodule K ((V ⧸ (K ∙ a)) × (K ∙ a))| FiniteDimensional.finrank K W = k + 1 ∧ ⟨0, ⟨a, mem_span_singleton_self a⟩⟩ ∈ W} ≃
  {W : Submodule K ((V ⧸ (K ∙ a)) × (K ∙ a)) | FiniteDimensional.finrank K W = k ∧ ∀ x ∈ W, x.2 = 0}

[Kevin Buzzard]

This looks to me like it has nothing to do with quotients or submodules, V/<a> may as well be X and Ka may as well be Y. The dimension criterion is also artificial, you could remove it and then add it in again later. Why not prove that subspaces of X x Y containing 0 + Y biject with subspaces of X x Y having trivial intersection with Y first? The constructions each way are project onto X then inject, and project onto X and then cross with top. You can establish this bijection first and then refine it to the one you want by putting things like dimension conditions later on.

[Alena Gusakov]

Kevin Buzzard said:

This looks to me like it has nothing to do with quotients or submodules, V/<a> may as well be X and Ka may as well be Y. The dimension criterion is also artificial, you could remove it and then add it in again later. Why not prove that subspaces of X x Y containing 0 + Y biject with subspaces of X x Y having trivial intersection with Y first? The constructions each way are project onto X then inject, and project onto X and then cross with top. You can establish this bijection first and then refine it to the one you want by putting things like dimension conditions later on.

So something like

def subspacesBijection : {X : Submodule K (V × W) | Submodule.map (LinearMap.inr K V W) ⊤ ≤ X} ≃
  {X : Submodule K (V × W) | Disjoint (Submodule.map (LinearMap.inr K V W) ⊤) X } where
    toFun := _
    invFun := _
    left_inv := _
    right_inv := _

[Kevin Buzzard]

Yeah except I misspoke -- Disjoint isn't strong enough, you want "every element has W component 0"

[Alena Gusakov]

Isn't saying the top of W mapped into the vector space is disjoint from X the same thing?

[Alena Gusakov]

Like it's saying the image of all of W mapped into V \times W is disjoint from X

[Alena Gusakov]

Actually wait - changing it to ∀ x ∈ X, x.2 = 0 makes it so much easier, simp just closed the first goal instantly

[Alena Gusakov]

It's been a little while since I've worked on this but I'm trying to wrap this up - the last part I'm stuck on is the other bijection, where the submodules don't have Submodule.map (LinearMap.inr K V W) ⊤ as a submodule. In this case it's not a direct equivalence, and we have to keep track of linear maps from each submodule X to W (in order to "reconstruct" the submodules from their images). At first I thought using dependent products made the most sense, i.e. mapping into something like {(X : Submodule K (V × W), \phi)| Disjoint (Submodule.map (LinearMap.inr K V W) ⊤) X } where we have that \phi is a linear map from X to W or something, but that really doesn't work. Does anyone have any idea what type I can use for this? I'm trying to have a set of tuples like (X, \phi : X \rightarrow W).

[Alena Gusakov]

I wonder if instead of defining the linear maps as being from V \times W to W with some additional condition on the image of X would help? The problem is I don't need to count maps from V \times W to W and I can't figure out what condition I need exactly

[Alena Gusakov]

def subspacesBijection2 : {X : Submodule K (V × W) | ¬ Submodule.map (LinearMap.inr K V W) ⊤ ≤ X} ≃
  {((X, φ) : (Submodule K V × W) × (V × W →ₗ[K] W)) | ∀ x ∈ X, x.2 = 0 ∧ ∀ x ∉ X, φ x = 0}

This doesn't typecheck cause I can't figure out how I need to write it but maybe something like this

[Eric Wieser]

Just to note that Submodule.map (LinearMap.inr K V W) ⊤ is better-spelt LinearMap.range (.inr K V W)

[Eric Wieser]

Can you add imports / variables to that code snippet above so that it _almost_ typechecks?

[Alena Gusakov]

Should be

import Mathlib.Algebra.Module.Prod
import Mathlib.Algebra.Module.BigOperators
import Mathlib.Algebra.Module.Submodule.LinearMap
import Mathlib.Algebra.Module.Submodule.Map
import Mathlib.LinearAlgebra.Prod

universe u v

open Submodule

open BigOperators

variable {K : Type u} {V W : Type v}

variable [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]

def subspacesBijection2 : {X : Submodule K (V × W) | ¬ Submodule.map (LinearMap.inr K V W) ⊤ ≤ X} ≃
  {((X, φ) : (Submodule K V × W) × (V × W →ₗ[K] W)) | ∀ x ∈ X, x.2 = 0 ∧ ∀ x ∉ X, φ x = 0} where
    toFun := sorry
    invFun := sorry
    left_inv := sorry
    right_inv := sorry

[Alena Gusakov]

er sorry, missing some stuff

[Alena Gusakov]

@Eric Wieser updated

[Alena Gusakov]

Eric Wieser said:

Can you add imports / variables to that code snippet above so that it _almost_ typechecks?

Hi, the latest code snippet should be an mwe where it almost typechecks