notation for weird dependent type

Stream: mathlib4

[Alena Gusakov]

I'm having trouble figuring out the correct way to write this dependent type - I'm trying to prove an equivalence between the set of submodules that don't contain Submodule.map (LinearMap.inr K V W) ⊤ as a submodule, and the set of products of submodules with linear maps that behave the way I want them to when taken for the given submodule. Here's my attempt, I don't know how to make it typecheck. Thanks!

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.1, x.2 = 0 ∧ ∀ x ∉ X.1, X.2 x = 0} where
    toFun := sorry
    invFun := sorry
    left_inv := sorry
    right_inv := sorry

[Eric Wieser]

Is it possible you want

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 : V × W, (x.1 ∈ X.1.1 → x.2 = 0) ∧ (x.1 ∉ X.1.1 → X.2 x = 0)} where
    toFun := sorry
    invFun := sorry
    left_inv := sorry
    right_inv := sorry

[Eric Wieser]

Though that doesn't make much sense, because x.2 = 0 forces W to be trivial

[Eric Wieser]

Are you confusing Submodule K V × W with Submodule K (V × W)

[Eric Wieser]

If you make that change, your version works as written (though you should parenthesize the foralls)

[Alena Gusakov]

Eric Wieser said:

Are you confusing Submodule K V × W with Submodule K (V × W)

This was part of it.

[Alena Gusakov]

What I'm trying to do with the second condition comes from
Screenshot-2024-05-10-at-1.35.19PM.png
where I'm trying to keep track of the linear function $\phi : V' \rightarrow E_1$. I thought having a map from $(V \times W)$ to $W$ made the most sense type theoretically, and then tried restricting it by requiring that the linear map takes everything outside the submodule to 0.