Task 239 help

Stream: FLT

[Madison Crim]

For task 239, I'm able to prove in general that I can commute a direct product with a tensor product when I have a finite free module M. The issue I'm running into is it's difficult to show then that this sends pure tensors to what'd we expect.

import Mathlib.Algebra.DirectSum.Module
import Mathlib.LinearAlgebra.FreeModule.Finite.Basic

section
variable {ι' : Type*} {R ι: Type*} {M N : ι → ι' → Type*} [CommRing R] [∀i i', AddCommGroup (M i i')]
[∀i i', AddCommGroup (N i i')] [∀i i', Module R (M i i')] [∀i i', Module R (N i i')] [Fintype ι'][DecidableEq ι']

open DirectSum

def proddirectsum' : (⨁ (i' : ι'), (∀ i, N i i')) ≃ₗ[R] (∀ i, (⨁ i', N i i')) where
  toFun nm i := ∑i', DirectSum.of (fun i' ↦ N i i') i' (nm i' i)
  map_add' x y := sorry --proved
  map_smul' := sorry --proved
  invFun nm :=  ∑i', DirectSum.of (fun j ↦ ∀ i, N i j) i' (fun i ↦ nm i i')
  left_inv nm := sorry --proved
  right_inv nm := sorry --proved

end

open TensorProduct

variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] {ι : Type*}
(N : ι → Type*) [∀ i, AddCommGroup (N i)] [∀ i, Module R (N i)]

noncomputable def moduleTensorProdEquiv [Module.Free R M] [Module.Finite R M] :
    M ⊗[R] (∀ i, N i) ≃ₗ[R] (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (∀i, N i) :=
  TensorProduct.congr (Module.Free.repr R M) (LinearEquiv.refl R ((i : ι) → N i))

noncomputable def TensorProdEquivProdTensor [Module.Free R M] [Module.Finite R M] :
    (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (∀i, N i) ≃ₗ[R]
      ∀i, ( Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (N i) :=
  finsuppScalarLeft R (∀i, N i) (Module.Free.ChooseBasisIndex R M) ≪≫ₗ
    (finsuppLEquivDirectSum R (∀i, N i) (Module.Free.ChooseBasisIndex R M)) ≪≫ₗ
    proddirectsum' ≪≫ₗ
    LinearEquiv.piCongrRight (fun i ↦(finsuppLEquivDirectSum R (N i)
    (Module.Free.ChooseBasisIndex R M)).symm)
    ≪≫ₗ LinearEquiv.piCongrRight (fun i ↦
      (finsuppScalarLeft R (N i) (Module.Free.ChooseBasisIndex R M)).symm)

noncomputable def prodTensorEquiv [Module.Free R M] [Module.Finite R M] :
  (∀i, (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] N i) ≃ₗ[R] ∀i, (M ⊗[R] N i) :=
  LinearEquiv.piCongrRight (fun i ↦ (LinearEquiv.rTensor (N i) (Module.Free.repr R M).symm))

noncomputable def tensorProdbilinear_map [Module.Free R M] [Module.Finite R M]  :
  M ⊗[R] (∀ i, N i) ≃ₗ[R] ∀ i, (M ⊗[R] N i) :=
  (moduleTensorProdEquiv R M N) ≪≫ₗ (TensorProdEquivProdTensor R M N) ≪≫ₗ (prodTensorEquiv R M N)

noncomputable def tensorProdbilinear_map_apply [Module.Free R M] [Module.Finite R M]
  (m : M) (n : ∀ i, N i) :
  tensorProdbilinear_map R M N (m ⊗ₜ n) =
  fun i ↦ (m ⊗ₜ n i) := sorry

This is where I'm struggling to show the map is the same as if I constructed the map tensorProdbilinear_map using TensorProduct.lift which wouldn't have given me the desired bijection.

[Kevin Buzzard]

Nice question! I agree that this needs some thought. This is FLT-free so you could even ask in #mathlib ;-)

[Madison Crim]

I can certainly ask there. I do plan to use these ideas for the FLT task. This is the generalization of the task I'm working on.

[Kevin Buzzard]

I've got no idea whether I'm going the right way, somehow the goal feels simpler but that doesn't mean I'm for sure going in the right direction (I made no attempt to tidy up but I need to sleep)

noncomputable def tensorProdbilinear_map_apply [Module.Free R M] [Module.Finite R M]
    (m : M) (n : ∀ i, N i) :
    tensorProdbilinear_map R M N (m ⊗ₜ n) =
    fun i ↦ (m ⊗ₜ n i) := by
  -- unfold some of your definitions (but not all)
  unfold tensorProdbilinear_map
  simp [moduleTensorProdEquiv]
  -- the goal now mentions `(Module.Free.repr R M) m` which has type `(some set) →₀ R`
  -- i.e. `Finsupp`, so we can (rather inelegantly) change the goal so that it
  -- doesn't mention m at all and only mentions `m'`, this finitely-supported function.
  let m' := (Module.Free.repr R M) m
  have hm' : (Module.Free.repr R M).symm m' = m := by simp [m']
  rw [← hm']
  simp
  -- Now the goal only has m' not m so we can apply an induction principle
  induction m' using Finsupp.induction_linear
  · -- goal true for zero function
    ext
    simp
  · -- goal preserved under addition
    ext i
    simp_all [add_tmul]
  · -- what's left: goal is true for functions supported at one place
    rename_i j r
    -- STP for m' the function sending j to r and everything else to 0
    -- randomly move an equiv to the other side out of hope more
    -- than anything else
    rw [← LinearEquiv.eq_symm_apply]
    simp [prodTensorEquiv]
    ext i
    simp
    -- we are surely close!
    -- ⊢ (TensorProdEquivProdTensor R M N) (Finsupp.single j r ⊗ₜ[R] n) i = Finsupp.single j r ⊗ₜ[R] n i
    sorry

[Aaron Liu]

I don't know much about linear algebra, but building off what @Kevin Buzzard has I was able to prove the goal.

import Mathlib.Algebra.DirectSum.Module
import Mathlib.LinearAlgebra.FreeModule.Finite.Basic

section
variable {ι' : Type*} {R ι: Type*} {M N : ι → ι' → Type*} [CommRing R] [∀i i', AddCommGroup (M i i')]
[∀i i', AddCommGroup (N i i')] [∀i i', Module R (M i i')] [∀i i', Module R (N i i')] [Fintype ι'][DecidableEq ι']

open DirectSum

def proddirectsum' : (⨁ (i' : ι'), (∀ i, N i i')) ≃ₗ[R] (∀ i, (⨁ i', N i i')) where
  toFun nm i := ∑i', DirectSum.of (fun i' ↦ N i i') i' (nm i' i)
  map_add' x y := sorry --proved
  map_smul' := sorry --proved
  invFun nm :=  ∑i', DirectSum.of (fun j ↦ ∀ i, N i j) i' (fun i ↦ nm i i')
  left_inv nm := sorry --proved
  right_inv nm := sorry --proved

end

open TensorProduct

variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] {ι : Type*}
(N : ι → Type*) [∀ i, AddCommGroup (N i)] [∀ i, Module R (N i)]

noncomputable def moduleTensorProdEquiv [Module.Free R M] [Module.Finite R M] :
    M ⊗[R] (∀ i, N i) ≃ₗ[R] (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (∀i, N i) :=
  TensorProduct.congr (Module.Free.repr R M) (LinearEquiv.refl R ((i : ι) → N i))

noncomputable def TensorProdEquivProdTensor [Module.Free R M] [Module.Finite R M] :
    (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (∀i, N i) ≃ₗ[R]
      ∀i, ( Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (N i) :=
  finsuppScalarLeft R (∀i, N i) (Module.Free.ChooseBasisIndex R M) ≪≫ₗ
    (finsuppLEquivDirectSum R (∀i, N i) (Module.Free.ChooseBasisIndex R M)) ≪≫ₗ
    proddirectsum' ≪≫ₗ
    LinearEquiv.piCongrRight (fun i ↦(finsuppLEquivDirectSum R (N i)
    (Module.Free.ChooseBasisIndex R M)).symm)
    ≪≫ₗ LinearEquiv.piCongrRight (fun i ↦
      (finsuppScalarLeft R (N i) (Module.Free.ChooseBasisIndex R M)).symm)

noncomputable def prodTensorEquiv [Module.Free R M] [Module.Finite R M] :
  (∀i, (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] N i) ≃ₗ[R] ∀i, (M ⊗[R] N i) :=
  LinearEquiv.piCongrRight (fun i ↦ (LinearEquiv.rTensor (N i) (Module.Free.repr R M).symm))

noncomputable def tensorProdbilinear_map [Module.Free R M] [Module.Finite R M]  :
  M ⊗[R] (∀ i, N i) ≃ₗ[R] ∀ i, (M ⊗[R] N i) :=
  (moduleTensorProdEquiv R M N) ≪≫ₗ (TensorProdEquivProdTensor R M N) ≪≫ₗ (prodTensorEquiv R M N)

noncomputable def tensorProdbilinear_map_apply [Module.Free R M] [Module.Finite R M]
    (m : M) (n : ∀ i, N i) :
    tensorProdbilinear_map R M N (m ⊗ₜ n) =
    fun i ↦ (m ⊗ₜ n i) := by
  -- unfold some of your definitions (but not all)
  unfold tensorProdbilinear_map
  simp [moduleTensorProdEquiv]
  -- the goal now mentions `(Module.Free.repr R M) m` which has type `(some set) →₀ R`
  -- i.e. `Finsupp`, so we can (rather inelegantly) change the goal so that it
  -- doesn't mention m at all and only mentions `m'`, this finitely-supported function.
  let m' := (Module.Free.repr R M) m
  have hm' : (Module.Free.repr R M).symm m' = m := by simp [m']
  rw [← hm']
  simp
  -- Now the goal only has m' not m so we can apply an induction principle
  induction m' using Finsupp.induction_linear
  · -- goal true for zero function
    ext
    simp
  · -- goal preserved under addition
    ext i
    simp_all [add_tmul]
  · -- what's left: goal is true for functions supported at one place
    rename_i j r
    -- STP for m' the function sending j to r and everything else to 0
    -- randomly move an equiv to the other side out of hope more
    -- than anything else
    rw [← LinearEquiv.eq_symm_apply]
    simp [prodTensorEquiv]
    ext i
    simp
    -- we are surely close!
    -- ⊢ (TensorProdEquivProdTensor R M N) (Finsupp.single j r ⊗ₜ[R] n) i = Finsupp.single j r ⊗ₜ[R] n i
    -- Kevin got here
    rw [TensorProdEquivProdTensor]
    simp only [LinearEquiv.trans_apply, LinearEquiv.piCongrRight_apply]
    rw [LinearEquiv.symm_apply_eq]
    ext k
    rw [finsuppScalarLeft_apply, LinearMap.rTensor_tmul, Finsupp.lapply_apply, TensorProduct.lid_tmul]
    rw [Finsupp.single_apply, ite_smul, zero_smul, ← Finsupp.single_apply]
    apply congrFun
    apply congrArg
    clear k hm' m' m
    rw [LinearEquiv.symm_apply_eq]
    rw [finsuppLEquivDirectSum_single]
    rw [finsuppScalarLeft_apply_tmul, Finsupp.sum_single_index (by simp)]
    rw [finsuppLEquivDirectSum_single]
    rw [DirectSum.lof_eq_of, DirectSum.lof_eq_of]
    rw [proddirectsum']
    simp_rw [← LinearEquiv.toFun_eq_coe]
    conv_lhs =>
      enter [2, x]
      rw [DirectSum.of_apply]
      simp only [Eq.recOn.eq_def, eq_rec_constant, dif_eq_if]
      rw [ite_apply, Pi.zero_apply, Pi.smul_apply, apply_ite (DFunLike.coe _), AddMonoidHom.map_zero]
    apply Fintype.sum_dite_eq
    done

[Madison Crim]

Thank you both so much! Using this I was able to prove my task. My issue now is I have this additional file containing the work above including the proofs of the sorries. To create my PR for this task, should I include this file, or should I try to PR these results to mathlib before creating a PR for FLT?

[Ruben Van de Velde]

Perhaps submit it to flt first

[Kevin Buzzard]

I guess there might be better ways to define those maps, that's probably the first thing to think about