Zulip Chat Archive

Stream: maths

Topic: flat modules


Andrew Yang (Jul 19 2022 at 10:16):

Are there people currently developing some API around flat modules? For the first step, having I ⊗ M →ₗ M injective for all I(the definition in mathlib) iff - ⊗ M is exact would be nice.

Tagging @Matej Penciak since you seem to have asked some related questions before.
Also @Markus Himmel since you are working on cogenerators in abelian categories; this result follows from Baer's criterion if we know that Hom(M,X)\operatorname{Hom}(M, X) is injective iff MM is flat for X being a (injective?) cogenerator (if I am not mistaken). I'm not sure if this is in your plan.
And also @Jujian Zhang since Baer's criterion is your work.

Johan Commelin (Jul 19 2022 at 10:20):

This has been a major todo ever since I added the definition of flat modules. It would be awesome to close it.

Markus Himmel (Jul 19 2022 at 10:29):

This is not on my roadmap.

Andrew Yang (Jul 19 2022 at 10:34):

Will your work imply that Module R has an injective cogenerator?

Markus Himmel (Jul 19 2022 at 10:36):

Yes, when combined with Jujian's proof that Module R has enough injectives

Matej Penciak (Jul 19 2022 at 12:01):

Andrew Yang said:

Are there people currently developing some API around flat modules? For the first step, having I ⊗ M →ₗ M injective for all I(the definition in mathlib) iff - ⊗ M is exact would be nice.

I have this project on flat modules working towards that: https://github.com/mpenciak/flat_modules

It's funny you should bring it up because I hadn't touched the project in months, but I just dusted it off last night (bumped mathlib) and intended on trying to make some more progress.

Andrew Yang (Jul 19 2022 at 12:05):

What a coincidence!
Have you ever considered the approach I mentioned? I think it might be easier than the proof in stacks since we already have Baer's criterion.

Matej Penciak (Jul 19 2022 at 12:05):

So far I've managed to prove a couple technical things that are used in the Stacks project proof:

1) Any module is a direct limit of its f.g. submodules.
2) Tensor product commutes with direct limit (turns out I did more work than needed for this, because it's easy to deduce from some lemmas already in mathlib)

I got stuck on the next part of the proof because at the time I found the API around short exact sequences in mathlib wasn't quite there to state/prove things like 0 → R¹ → Rⁿ⁺¹ → Rⁿ → 0is short exact

Matej Penciak (Jul 19 2022 at 12:06):

Andrew Yang said:

What a coincidence!
Have you ever considered the approach I mentioned? I think it might be easier than the proof in stacks since we already have Baer's criterion.

I'd have to look at the proof using Baer's criterion, but it sounds like it should be more do-able!

Andrew Yang (Jul 19 2022 at 12:18):

The proof goes like:
Let M* denote Hom(M, X), then by the tensor-hom adjunction, Hom(- , M*) is naturally isomorphic to (_ ⊗ M)*.
Since -* = Hom(-, X) preserves mono, and reflects mono when it is faithful (X is a cogenerator), M* is injective iff Hom(- , M*) preserves mono iff _ ⊗ M preserves mono iff M is flat.
But Baer's criterion tells you that it suffices to check if Hom(- , M*) preserves mono of the form I → R, so we only need to check such morphisms when checking flatness.

Junyan Xu (Jul 19 2022 at 14:51):

I would say -* = Hom(-, X) sends epi to mono, and Hom(- , M*) sends mono to epi, but maybe you are implicitly working in the opposite category ...

Andrew Yang (Jul 19 2022 at 14:53):

Yeah that's what I meant. -* is contravariant.

Junyan Xu (Jul 19 2022 at 15:20):

I am confused, as the argument seems to require -* reflects epi to mono, instead of reflecting mono to epi ...

Andrew Yang (Jul 19 2022 at 15:29):

Sorry, I should have made things clearer. I meant -* (and Hom(-, M*)) as the contravariant functor taking R-Mod to R-Mod^op.

Junyan Xu (Jul 19 2022 at 15:48):

Yes but I don't see how -* reflects mono.

Andrew Yang (Jul 19 2022 at 15:51):

Since X is a cogenerator, Hom(-, X) is faithful, and thus reflects mono (and also epi).

Jujian Zhang (Jan 26 2023 at 13:29):

At here, there is a proof that if IMRMI \otimes M \to R \otimes M is injective for all ideals, then MM is flat in the sense that NMNMN \otimes M \to N' \otimes M is injective whenever NNN\to N' is injective, i.e. 00HD (3) implies (2)

def flat' : Prop :=  N N' : Module.{u} R (L : N  N'),
  function.injective L 
  function.injective (tensor_product.map L (linear_map.id : M →ₗ[R] M))

/--
`tensor_embedding M I` is the canonical map `I ⊗ M ⟶ R ⊗ M`
-/
lemma flat'_of_ideal (hIs :  (I : ideal R), function.injective (tensor_embedding M I)) :
  flat' R M := sorry

The only sorry in this repo is Q/Z\mathbb Q / \mathbb Z is injective as a group which is proved elsewhere

It basically follows the approach suggested by @Andrew Yang with everything de-categorified.

Jujian Zhang (Feb 01 2023 at 23:42):

Update: this contains a full proof of 00HD: flat iff tensoring is exact iff tensoring preserves injective functions iff IMRMI \otimes M \to R \otimes M is injective for all ideals iff IMRMI \otimes M \to R \otimes M is injective for all finitely generated ideals.

Kevin Buzzard (Feb 01 2023 at 23:46):

Oh nice! So now we actually have a working definition of flatness!

A cool thing to do next would be to show flat iff the relevant Tor_1 vanishes a la stacks 00M5

Julian Külshammer (Feb 02 2023 at 10:30):

Another todo would be to remove the unnecessary comm_ring assumptions :-)

Jujian Zhang (Mar 31 2023 at 11:12):

Kevin Buzzard said:

Oh nice! So now we actually have a working definition of flatness!

A cool thing to do next would be to show flat iff the relevant Tor_1 vanishes a la stacks 00M5

By copying enough from liquid tensor experiment's snake lemma and short exact sequences turning into long exact sequences, a formalisation stakcs 00M5 can be found here,

lemma equiv_defs : tfae
  [ module.flat.ses R M
  , module.flat.inj R M
  , module.flat.ideal R M
  , module.flat.fg_ideal R M
  , module.flat.exact R M
  ,  (N : Module.{u} R), nonempty (((Tor' (Module.{u} R) 1).obj N).obj M  0)
  ,  (I : ideal R), nonempty (((Tor' (Module.{u} R) 1).obj (Module.of R (R  I))).obj M  0)
  ,   (I : ideal R) (hI : I.fg),
    nonempty (((Tor' (Module.{u} R) 1).obj (Module.of R (R  I))).obj M  0)
  ,  (n : ) (hn : 0 < n) (N : Module.{u} R),
    nonempty (((Tor' (Module.{u} R) n).obj N).obj M  0)] := sorry

Richard Copley (Nov 18 2023 at 12:46):

(4) → (3) (short version):

import Mathlib.LinearAlgebra.TensorProduct.RightExactness
import Mathlib.RingTheory.Flat
import Mathlib.Tactic.RewriteSearch

-- Remove the `FG` condition from `Module.Flat.iff_rTensor_injective`

noncomputable section
suppress_compilation
open TensorProduct

variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]

-- Every `x : I ⊗ M` is the image of some `y : J ⊗ M` where `J ≤ I` is finitely generated,
-- under the tensor product of the inclusion `J.subtype.codRestrict .. : J → I`
-- and the identity `M → M`.
open Submodule TensorProduct LinearMap in
theorem exists_fg_le_tensor_eq_rTensor_subtype_codRestrict_tensor {I : Submodule R N} (x : I  M) :
     (J : Submodule R N) (_ : J.FG) (hle : J  I) (y : J  M),
      x = LinearMap.rTensor M (J.subtype.codRestrict I (fun c => hle.subset c.property)) y := by
  induction x using TensorProduct.induction_on with
  | zero => refine , fg_bot, zero_le _, 0, rfl
  | tmul i m =>
    refine R  i.val, ?_, ?_, i.val, mem_span_singleton_self _ ⊗ₜ[R] m, rfl
    . exact fg_span_singleton i.val
    . rw [span_le, Set.singleton_subset_iff] ; exact Subtype.mem i
  | add x₁ x₂ ihx₁ ihx₂ =>
    have J₁, hfg₁, hle₁, y₁, hy₁ := ihx₁
    have J₂, hfg₂, hle₂, y₂, hy₂ := ihx₂
    have h₁ (c : J₁) := (le_sup_left : J₁  J₁  J₂).subset c.property
    have h₂ (c : J₂) := (le_sup_right : J₂  J₁  J₂).subset c.property
    let z₁ :=
      rTensor M (J₁.subtype.codRestrict (J₁  J₂) h₁) y₁ +
      rTensor M (J₂.subtype.codRestrict (J₁  J₂) h₂) y₂
    refine J₁  J₂, FG.sup hfg₁ hfg₂, sup_le hle₁ hle₂, z₁, ?_
    rewrite [map_add,
       comp_apply,  rTensor_comp, comp_codRestrict,
       comp_apply,  rTensor_comp, comp_codRestrict]
    simp_rw [subtype_comp_codRestrict]
    rw [hy₁, hy₂]

-- Remove the `FG` condition from `Module.Flat.iff_rTensor_injective`
open LinearMap in
theorem iff_rTensor_injective' :
    Module.Flat R M  ( (I : Ideal R), Function.Injective (LinearMap.rTensor M I.subtype)) := by
  rewrite [Module.Flat.iff_rTensor_injective]
  refine fun h I => ?_, fun h I _ => h I
  letI : AddCommGroup (I [R] M) := inferInstance -- injective_iff_map_eq_zero cannot find this
  rewrite [injective_iff_map_eq_zero]
  intro x hx₀
  have J, hfg, hle, y, hy := exists_fg_le_tensor_eq_rTensor_subtype_codRestrict_tensor x
  apply (fun hy₀ => by rw [hy, hy₀, map_zero] : y = 0  x = 0)
  rewrite [hy,  comp_apply,  rTensor_comp, subtype_comp_codRestrict] at hx₀
  letI : AddCommGroup (J [R] M) := inferInstance -- injective_iff_map_eq_zero cannot find this
  exact (injective_iff_map_eq_zero _).mp (h hfg) y hx₀

Is this any use? Would you prefer to keep the gnarly colimits argument?

Kevin Buzzard (Nov 18 2023 at 12:59):

I would rather see this material in mathlib, however it gets there. It's a little frustrating having code kicking around "in the wild" which people can't use; I will need finite flat group schemes for FLT and so the sooner there are more lemmas characteristing flatness in mathlib, the better :-)

Richard Copley (Nov 18 2023 at 13:09):

I should presumably commit this in #7225, if anywhere

Richard Copley (Nov 18 2023 at 13:19):

There is no gnarly colimits argument, sorry. The argument uses Baer's criterion, and it's a little beyond me.
exists_fg_le_tensor_eq_rTensor_subtype_codRestrict_tensor might be nice to have anyway. I'm just not sure the name is ugly enough yet.

Joël Riou (Nov 18 2023 at 13:24):

Kevin Buzzard said:

I would rather see this material in mathlib, however it gets there. It's a little frustrating having code kicking around "in the wild" which people can't use; I will need finite flat group schemes for FLT and so the sooner there are more lemmas characteristing flatness in mathlib, the better :-)

It would be great if @Jujian Zhang 's work on flat modules could be ported to Lean4!

Jujian Zhang (Nov 18 2023 at 13:26):

I have started porting dependencies already for example ![here](https://github.com/leanprover-community/mathlib4/pull/8473) is direct limit and tensor products commutes which is used in finitely generated ideals are already sufficient for checking flatness

Richard Copley (Nov 18 2023 at 13:33):

"finitely generated ideals are already sufficient for checking flatness" is what my thing above shows, too.

Richard Copley (Nov 18 2023 at 13:37):

Kind of. The existing Mathlib4 definition of Flat makes that a tautology. I show it implies a stronger version, but still only "all ideals", not the full-strength "all submodules" definition.

Jujian Zhang (Nov 18 2023 at 13:40):

Your version is actually shorter than mine. The other blocking dependency I need is the tensor-hom adjunction from https://en.m.wikipedia.org/wiki/Tensor-hom_adjunction. This is almost what we have in the TensorProduct.Tower file but not really because of the algebra instances in the said file.

Kevin Buzzard (Nov 18 2023 at 13:43):

@Jujian Zhang I know you explained this to me verbally the other day, but can you write down exactly what is blocking you here? I would really like to get flatness back on the move.

Jujian Zhang (Nov 18 2023 at 13:48):

I will open another pr writing down the adjunction I need and inside the pr explain why I could not use the existing file this afternoon.

Richard Copley (Nov 18 2023 at 13:50):

Jujian Zhang said:

Your version is actually shorter than mine. The other blocking dependency I need is the tensor-hom adjunction from https://en.m.wikipedia.org/wiki/Tensor-hom_adjunction. This is almost what we have in the TensorProduct.Tower file but not really because of the algebra instances in the said file.

Want me to do anything about it? Say, should I make a new PR for my version, in Mathlib.RingTheory.Flat, mentioning #8473?

Jujian Zhang (Nov 18 2023 at 13:56):

Yes please! But #8473 is really just to show an ideal is isomorphic to direct limit of its finitely generated subideals so that ideal tensoring with another module is also related to fg ideals tensoring with another module. Since your code doesn’t need it, you don’t have to mention it. #8473 is probably useful on its own. But ideal is isomorphic to direct limit of its finitely generated subideals is probably less useful.

Richard Copley (Nov 18 2023 at 14:50):

#8494

Jujian Zhang (Nov 18 2023 at 15:54):

#8495
set up: RR commutative ring, SS ring, XX an R,SR, S-bimodule, YY an RR-module and ZZ an SS-module, we want HomS(XRY,Z)HomR(Y,HomS(X,Z))\operatorname{Hom}_S(X⊗_R Y, Z) \cong \operatorname{Hom}_R(Y, \operatorname{Hom}_S(X, Z)). so to use the Tower file, we need SS to be an RR-algebra which is a luxury we do not have here.
But note that in Tower file, curry and uncurry are both tri-linear maps. So Tower file
allows interplay of 3 rings which is not allowed in this PR.

definition in question: docs#TensorProduct.AlgebraTensorModule.uncurry docs#TensorProduct.AlgebraTensorModule.lcurry


another issue is that we can't have HomS(YRX,Z)HomR(Y,HomS(X,Z))\operatorname{Hom}_S(Y⊗_R X, Z) \cong \operatorname{Hom}_R(Y, \operatorname{Hom}_S(X, Z)) (the order of argument is flipped) because in mathlib4 we know XRYX\otimes_R Y is SS-module but we don't know that YRXY\otimes_R X is SS-module as well. (At least I think this is the case)

Scott Morrison (Nov 19 2023 at 03:06):

Aside about reviewing: when there are multiple people working on similar topics in Mathlib, it is super useful if they can write reviews of each others PRs. If a review has already taken place, responses made, and there is an "approval" tick, it is then much easier and faster for a maintainer or "official" reviewer to put it on the queue. Reviews can be done by everyone, not just "official" reviewers, and indeed Mathlib can only scale if we get good at this.

Moreover, if you've reviewed someone's PR, and would like to see it merged soon, writing on the #PR reviews stream something like "I've reviewed #NNN and it now looks good to me. Could a maintainer please take a look?" is very welcome.

I wrote this message specifically because it would be great to see @Jujian Zhang's green tick on #8494, and @Richard Copley's green tick on #8495! :-)

Eric Wieser (Nov 19 2023 at 17:57):

Reiterating my comment on #8495; I would rather we work out how to generalize the existing curry/uncurry rather than add a third copy of the API.

Eric Wieser (Nov 19 2023 at 17:58):

Jujian Zhang said:

another issue is that we can't have $\operatorname{Hom}_S(Y⊗_R X, Z) \cong \operatorname{Hom}_R(Y, \operatorname{Hom}_S(X, Z))$ (the order of argument is flipped) because in mathlib4 we know $X\otimes_R Y$ is $S$-module but we don't know that $Y\otimes_R X$ is $S$-module as well. (At least I think this is the case)

It's not that mathlib doesn't know this, it that it can't know it without issues for instance diamonds in the case when R = S

Richard Copley (Nov 19 2023 at 22:37):

#8494 is merged (to staging). Thanks all!

Eric Wieser (Nov 19 2023 at 23:07):

Nice job finding inclusion just after I renamed it; that's good evidence that ofLe was a lousy name.

Richard Copley (Nov 19 2023 at 23:32):

inclusion is easier to get a handle on, yeah. I reckon I had seen ofLe and forgotten all about it.

Richard Copley (Dec 11 2023 at 21:03):

Free modules are flat: branch#richard-copley/free-modules-are-flat

I'm not sure if this is needed. I just thought it would be fun!

Thanks to @Joël Riou for the advice.

Riccardo Brasca (Dec 11 2023 at 21:12):

We surely want this! How long is it?

Ruben Van de Velde (Dec 11 2023 at 21:14):

+934+934

Adam Topaz (Dec 11 2023 at 21:15):

I'm confused. Can't we deduce this easily from docs#Module.Flat.self docs#Module.Flat.directSum the fact that tensoring commutes with direct sums (I don't remember the name, but it's there), and some lemma about transferring flatness across isomorphisms (i.e. docs#Module.Flat.of_linearEquiv )?

Riccardo Brasca (Dec 11 2023 at 21:16):

934 lines seems indeed a lot

Richard Copley (Dec 11 2023 at 21:17):

Riccardo Brasca said:

We surely want this! How long is it?

Really long :)

Richard Copley (Dec 11 2023 at 21:19):

Adam Topaz said:

I'm confused. Can't we deduce this easily from docs#Module.Flat.self docs#Module.Flat.directSum the fact that tensoring commutes with direct sums (I don't remember the name, but it's there), and some lemma about transferring flatness across isomorphisms (i.e. docs#Module.Flat.of_linearEquiv )?

Sounds plausible. I just plodded through the argument in Dummit and Foote.

Richard Copley (Dec 11 2023 at 21:20):

Does that only work for finite and free modules?

Eric Wieser (Dec 11 2023 at 21:21):

the fact that tensoring commutes with direct sums (

docs#TensorProduct.directSum

Adam Topaz (Dec 11 2023 at 21:21):

import Mathlib

variable (A M : Type*) [CommRing A] [AddCommGroup M] [Module A M] [Module.Free A M]

example : Module.Flat A M := by
  obtain I,⟨𝓑⟩⟩ : Module.Free A M := inferInstance
  apply Module.Flat.of_linearEquiv (e := 𝓑)

It was much easier.

Eric Wieser (Dec 11 2023 at 21:21):

It is very unfortunate that neither TensorProduct nor DirectSum notation appears in the docs

Junyan Xu (Dec 11 2023 at 21:22):

docs#Module.Flat.of_free
(the PR #7567 was 133 lines)

Richard Copley (Dec 11 2023 at 21:23):

Oh sure, but this is because our definition of flat is wrong, isn't it?

Richard Copley (Dec 11 2023 at 21:23):

The result is

theorem lTensor_free_injective_of_injective [DecidableEq M] [DecidableEq P]
    [DecidableEq (M × N →₀ )] [Module.Free R M]
    (ψ : N →ₗ[R] P) ( : Injective ψ) : Injective (lTensor M ψ) := by

Adam Topaz (Dec 11 2023 at 21:24):

Richard Copley said:

Oh sure, but this is because our definition of flat is wrong, isn't it?

No, our definition of flatness is correct. But it's a theorem that it's equivalent to the definition of flatness that you see in books.

Adam Topaz (Dec 11 2023 at 21:24):

I thought we had that theorem in mathlib, but maybe we dont?

Richard Copley (Dec 11 2023 at 21:24):

Not last time I looked.

Richard Copley (Dec 11 2023 at 21:25):

But it's a short step from this result (the short step is the next part of the Dummit and Foote exercise)

Riccardo Brasca (Dec 11 2023 at 21:26):

The doc says "This is equivalent to the claim that for all injective R-linear maps f : M₁ → M₂ the induced map M₁ ⊗ M → M₂ ⊗ M is injective. See . This result is not yet formalised."

Riccardo Brasca (Dec 11 2023 at 21:27):

Note that there is literally "See ." I don't know why

Richard Copley (Dec 11 2023 at 21:27):

Yes, sorry for the unclarity. This is towards that result.

Adam Topaz (Dec 11 2023 at 21:27):

Perhaps a porting error?

Riccardo Brasca (Dec 11 2023 at 21:28):

Who wants to fix the doc? It should take like 30 seconds, but here it's late

Richard Copley (Dec 11 2023 at 21:28):

It says See <https://stacks.math.columbia.edu/tag/00HD>.

Adam Topaz (Dec 11 2023 at 21:28):

Oh, that's a bug in docgen then!

Adam Topaz (Dec 11 2023 at 21:29):

I assume Riccardo was looking at https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Flat.html

Riccardo Brasca (Dec 11 2023 at 21:30):

Yes, with Firefox on Debian I see "See ."

Adam Topaz (Dec 11 2023 at 21:30):

I assume the link doesn't show up because it's not a markdown link.

Riccardo Brasca (Dec 11 2023 at 21:31):

@Jujian Zhang how far are we from this result?

Richard Copley (Dec 11 2023 at 21:33):

## TODO

* Show that tensoring with a flat module preserves injective morphisms.
  Show that this is equivalent to be flat.

One can do this TODO item using the result I proved (lTensor_free_injective_of_injective) and a diagram chasing argument.

Like I said, this was for my own edification. I won't be at all offended if someone else does it better.

Riccardo Brasca (Dec 11 2023 at 21:34):

#8473 just got a maintainer merge by @Junyan Xu , so we are at least moving towards the result

Adam Topaz (Dec 11 2023 at 21:36):

Another question: Why does Module.DirectLimit even exist?

Junyan Xu (Dec 11 2023 at 21:36):

I thought we had that theorem in mathlib, but maybe we dont?

00HD is done in #7225 by @Jujian Zhang and he's opening PRs to move it into mathlib piece by piece. #8906 and #8559 are currently pending PRs.

Adam Topaz (Dec 11 2023 at 21:37):

Pinging @Coleton Kotch since he is interested in applying this.

Junyan Xu (Dec 11 2023 at 21:39):

Another question: Why does Module.DirectLimit even exist?

Why should it not exist? If what you have in mind is to apply the category theory library, I outlined some difficulties here.

Riccardo Brasca (Dec 11 2023 at 21:41):

Can someone who really understand UnivLE.{u, v} have a look at #8905?

Richard Copley (Dec 11 2023 at 21:41):

Junyan Xu said:

I thought we had that theorem in mathlib, but maybe we dont?

00HD is done in #7225 by Jujian Zhang and he's opening PRs to move it into mathlib piece by piece. #8906 and #8559 are currently pending PRs.

OK, no need for a PR from me

Adam Topaz (Dec 11 2023 at 21:44):

Junyan Xu said:

Another question: Why does Module.DirectLimit even exist?

Why should it not exist? If what you have in mind is to apply the category theory library, I outlined some difficulties here.

Yes, I was thinking precisely of just using the category theory colimits. Is there anything you get by having an explicit description of the colimit that you can't get by using (or appropriately extending) the API for (co)limits in concrete categories?

Eric Wieser (Dec 11 2023 at 21:46):

Adam Topaz said:

I assume the link doesn't show up because it's not a markdown link.

I think <http://example.com> is valid in most markdown dialects, just not the one that doc-gen4 uses. They're in the spec.

Junyan Xu (Dec 11 2023 at 21:46):

module.direct_limit has a 4+ years history so it's not surprising that people have built a lot on it :)

Adam Topaz (Dec 11 2023 at 21:47):

ok, fair enough, but now you have to also duplicate the API every time you introduce a new algebraic gadget when you want to take a direct limit.

Eric Wieser (Dec 11 2023 at 21:49):

Presumably Module.DirectLimit is universe polymorphic and the category spelling isn't?

Adam Topaz (Dec 11 2023 at 21:49):

yes, that's true.

Eric Wieser (Dec 11 2023 at 21:50):

Which almost certainly is irrelevant here, but in general is a curse of doing things through CategoryTheory first

Richard Copley (Dec 11 2023 at 21:50):

What would have been the natural spelling in Mathlib of my first few auxiliary results? [Edit: imports fixed]

import Mathlib.Algebra.DirectSum.Module
import Mathlib.LinearAlgebra.TensorProduct

open Submodule TensorProduct Function

variable (R : Type*) [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]

open DirectSum in
/-- The natural linear map `⨁̂ⁿ M → ⨁̂ⁿ N` induced on direct sums by a linear map `M → N`. -/
def DirectSum.induced (ι : Type*) [DecidableEq ι] (f : M →ₗ[R] N) :
    ( _ : ι, M) →ₗ[R] ( _ : ι, N) :=
  (DirectSum.toModule R ι ( _i : ι, N) fun i : ι => ((lof R ι (fun _ => N) i) ∘ₗ f))

open DirectSum in
/-- The natural linear map `F : ⨁̂ⁿ M → ⨁̂ⁿ N` induced on direct sums by a linear map `f : M → N`
satisfies `(F x) i = f (x i)`, for all `x` in `⨁̂ⁿ M`, for each index `i`. -/
theorem DirectSum.induced_apply (ι : Type*) [DecidableEq ι] (f : M →ₗ[R] N)
    (x :  _ : ι, M) (i : ι) :
      induced R ι f x i = f (x i) := by
  sorry

/-- The linear map on direct sums induced by an injective linear map is injective. -/
theorem DirectSum.induced_injective (ι : Type*) [DecidableEq ι] {ψ : M →ₗ[R] N}
    (hinjective : Function.Injective ψ) : Function.Injective (DirectSum.induced R ι ψ) := by
  sorry

Adam Topaz (Dec 11 2023 at 21:51):

the first one is probably called docs#DirectSum.map ?

Junyan Xu (Dec 11 2023 at 21:51):

Yeah, working with categories usually means sacrificing universe polymorphism (for example here the direct limit lies in the max universe of the indexing type's and the modules'), so sometimes you need to use ULifts. Maybe the solution is to add a ULift instance for every algebraic gadget, and maybe UnivLE could help a bit.

Eric Wieser (Dec 11 2023 at 21:52):

I think induced is docs#DFinsupp.mapRange.linearMap

Eric Wieser (Dec 11 2023 at 21:52):

That is, DirectSum is missing a lot of API because copying the dfinsupp API by hand is a massive waste of time

Adam Topaz (Dec 11 2023 at 21:54):

Eric Wieser said:

Which almost certainly is irrelevant here, but in general is a curse of doing things through CategoryTheory first

I think we need to seriously think about this as a community. I hope this "issue" can be solved with some metaprogramming.

Eric Wieser (Dec 11 2023 at 21:54):

(to recap: DFinsupp and DirectSum are defeq, and they used to be identically treated. I hijacked the meaning of the latter to mean "has convolutional multiplication", leaving the former with (the potential for) pointwise multiplication)

Kevin Buzzard (Dec 11 2023 at 22:00):

Do we really care about making mathlib be as universe polymorphic as the underlying type theory allows us to be? Before 2017 I had never heard of any universes beyond Type, I only put universes in because that seems to be the current fashion. When I'm teaching I only ever use Type.

Eric Wieser (Dec 11 2023 at 22:51):

I think the problem is we're forced to pick between:

  • Use Type everywhere. This breaks people working with Cardinal
  • Use Type* everywhere we can. This rules out going via category theory without losing generality
  • Use X Y : Type u as much as possible. This means people writing Type* get more confusing universe error messages, and forces us to use ULift more often

Junyan Xu (Dec 11 2023 at 22:58):

Universes got more annoying in Lean 4 mainly because of lean4#2297

(UnivLE was designed to bypass the issue, but universe inequalities have been of independent interest.)

Eric Wieser (Dec 11 2023 at 22:58):

(and note that if we use Type u everywhere, then we're not even allowed to state things like docs#ULift.moduleEquiv, which makes ULift even harder to use)

Richard Copley (Dec 13 2023 at 18:10):

Eric Wieser said:

I think induced is docs#DFinsupp.mapRange.linearMap

I cleaned up the branch a little using this. It didn't save a huge number of lines.

DFinsupp.mapRange is a real pain to use! :smile: Is there a short proof of TensorProduct.rid_DirectSum_tmul (below), or do we already have it? If not, do we want it?

Eric Wieser (Dec 14 2023 at 00:40):

I recommend writing the suffices explicitly if you can

Junyan Xu (Dec 14 2023 at 00:51):

I guess looking at the proof of docs#Module.Flat.directSum should help? Indeed the proof is longer than I'd expect ...

Richard Copley (Dec 14 2023 at 03:04):

Junyan Xu said:

I guess looking at the proof of docs#Module.Flat.directSum should help? Indeed the proof is longer than I'd expect ...

It helps a little! The proof in Flat.directSum doesn't contain the whole of this lemma. That proof's diagram has (IM)nI(Mn)R(Mn)Mn(I⊗M)ⁿ → I⊗(Mⁿ) → R⊗(Mⁿ) → Mⁿ plus some projections and maps between components, but nowhere does it need (Rn)M(Rⁿ)⊗M. Still, part of it is very similar to my proof, and the details might be applicable. I'll give it some thought.

Junyan Xu (Dec 14 2023 at 03:10):

It was a fairly recent PR #7567 and the author is @Robin Carlier

Richard Copley (Dec 16 2023 at 15:27):

Eric Wieser said:

I recommend writing the suffices explicitly if you can

I can, and it allows more of the rewriting to be done in the "complicated → simple" direction, which is easier to understand. I take it that's one of the motivations for your recommendation? Unfortunately, it so happens that when I do that, I also need to add more workarounds for the fact that the defeq between DirectProduct and DFinsupp is not reducible. That makes the proofs quite slow to elaborate.

Junyan Xu said:

I guess looking at the proof of docs#Module.Flat.directSum should help? Indeed the proof is longer than I'd expect ...

Part of it was unnecessarily long (the split ifs was not needed) and I have golfed it.
My lemma is mostly about DFinsupp.mapRange which is not used in @Robin Carlier's proof, so while the proofs are already have a strong family resemblance, the details of the one aren't really applicable to the other.

Here are three more versions to illustrate.

Richard Copley (Dec 20 2023 at 02:23):

Richard Copley said:

But it's a short step from this result (the short step is the next part of the Dummit and Foote exercise)

The statement of the exercise is short, but I've finally given up trying to solve it and looked for others' solutions online. The answers to this question on Math StackExchange use a certain amount of technology that's a liitle beyond me. I don't think I'll be posting a 3000-line elementary proof any time soon :sad:

Kevin Buzzard (Dec 20 2023 at 10:57):

All of this is done but not PRed by @Jujian Zhang or possibly @Jujian Zhang


Last updated: Dec 20 2023 at 11:08 UTC