flat modules

Stream: maths

[Andrew Yang]

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 $\operatorname{Hom}(M, X)$ is injective iff $M$ 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]

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

[Markus Himmel]

This is not on my roadmap.

[Andrew Yang]

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

[Markus Himmel]

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

[Matej Penciak]

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]

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]

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]

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]

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]

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]

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

[Junyan Xu]

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

[Andrew Yang]

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]

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

[Andrew Yang]

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

[Jujian Zhang]

At here, there is a proof that if $I \otimes M \to R \otimes M$ is injective for all ideals, then $M$ is flat in the sense that $N \otimes M \to N' \otimes M$ is injective whenever $N\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 $\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]

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

[Kevin Buzzard]

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]

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

[Jujian Zhang]

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]

(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]

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]

I should presumably commit this in #7225, if anywhere

[Richard Copley]

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]

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]

I have started porting dependencies already for example  is direct limit and tensor products commutes which is used in finitely generated ideals are already sufficient for checking flatness

[Richard Copley]

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

[Richard Copley]

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]

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]

@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]

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]

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]

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]

#8494

[Jujian Zhang]

#8495
set up: $R$ commutative ring, $S$ ring, $X$ an $R, S$-bimodule, $Y$ an $R$-module and $Z$ an $S$-module, we want $\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 $S$ to be an $R$-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 $\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)

[Scott Morrison]

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]

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]

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]

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

[Eric Wieser]

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

[Richard Copley]

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

[Richard Copley]

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]

We surely want this! How long is it?

[Ruben Van de Velde]

$+934$

[Adam Topaz]

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]

934 lines seems indeed a lot

[Richard Copley]

Riccardo Brasca said:

We surely want this! How long is it?

Really long :)

[Richard Copley]

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]

Does that only work for finite and free modules?

[Eric Wieser]

the fact that tensoring commutes with direct sums (

docs#TensorProduct.directSum

[Adam Topaz]

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]

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

[Junyan Xu]

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

[Richard Copley]

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

[Richard Copley]

The result is

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

[Adam Topaz]

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]

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

[Richard Copley]

Not last time I looked.

[Richard Copley]

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

[Riccardo Brasca]

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]

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

[Richard Copley]

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

[Adam Topaz]

Perhaps a porting error?

[Riccardo Brasca]

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

[Richard Copley]

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

[Adam Topaz]

Oh, that's a bug in docgen then!

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

@Jujian Zhang how far are we from this result?

[Richard Copley]

## 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]

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

[Adam Topaz]

Another question: Why does Module.DirectLimit even exist?

[Junyan Xu]

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]

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

[Junyan Xu]

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]

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

[Richard Copley]

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]

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]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

yes, that's true.

[Eric Wieser]

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

[Richard Copley]

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]

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

[Junyan Xu]

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]

I think induced is docs#DFinsupp.mapRange.linearMap

[Eric Wieser]

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

[Adam Topaz]

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]

(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]

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]

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]

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]

(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]

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?

import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.LinearAlgebra.DFinsupp
import Mathlib.LinearAlgebra.DirectSum.TensorProduct

noncomputable section

variable (R : Type*) [CommRing R]
variable (N : Type*) [AddCommGroup N] [Module R N]
variable (ι : Type*) [DecidableEq ι]
open DirectSum TensorProduct

/-- If `N` is an `R`-module then `Rⁿ ⊗ N ≃ Nⁿ`. -/
@[simps! apply]
def TensorProduct.rid_DirectSum (ι : Type*) [DecidableEq ι] :
    (N ⊗[R] ⨁ _ : ι, R) ≃ₗ[R] (⨁ _ : ι, N) :=
  TensorProduct.directSumRight R N (fun _ : ι => R) ≪≫ₗ
    DFinsupp.mapRange.linearEquiv (fun _ : ι => TensorProduct.rid R N)

/-- Applying the linear equivalence `rid_DirectSum` to a simple element `x ⊗ r` of `N ⊗ Rⁿ`. -/
theorem TensorProduct.rid_DirectSum_tmul [DecidableEq R]
    (x : N) (r : ⨁ _ : ι, R) (i : ι) :
      rid_DirectSum R N ι (x ⊗ₜ[R] r) i = r i • x := by
  -- It suffices to show the equality holds when `r` is a Kronecker delta.
  -- To show this we recast as an equality of linear maps ...
  rewrite [show r i • x =
        DFinsupp.mapRange.linearMap (fun _ => LinearMap.flip (LinearMap.lsmul R N) x) r i by
      erw [DFinsupp.mapRange.linearMap_apply]
      rewrite [DFinsupp.mapRange_def, DFinsupp.mk_apply]
      split_ifs with h
      . rw [LinearMap.flip_apply, LinearMap.lsmul_apply, Subtype.coe_mk]
      . rw [DFinsupp.not_mem_support_iff.mp h, zero_smul],
    ← mk_apply, ← LinearEquiv.coe_coe, ← LinearMap.comp_apply]
  congr 2
  -- ... and apply the default extensionality theorems (explicit here for clarity).
  refine DirectSum.linearMap_ext R fun i : ι => LinearMap.ext_ring ?_
  rewrite [LinearMap.comp_apply, LinearMap.comp_apply, LinearMap.comp_apply,
    LinearEquiv.coe_coe, rid_DirectSum_apply, mk_apply, directSumRight_tmul_lof]
  erw [DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange.linearMap_apply]
  rw [← single_eq_lof, ← single_eq_lof, DFinsupp.mapRange_single, DFinsupp.mapRange_single,
    LinearEquiv.coe_coe, rid_tmul, LinearMap.flip_apply, LinearMap.lsmul_apply]

end

[Eric Wieser]

I recommend writing the suffices explicitly if you can

[Junyan Xu]

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

[Richard Copley]

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 $(I⊗M)ⁿ → I⊗(Mⁿ) → R⊗(Mⁿ) → Mⁿ$ plus some projections and maps between components, but nowhere does it need $(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]

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

[Richard Copley]

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.

import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.LinearAlgebra.DFinsupp
import Mathlib.LinearAlgebra.DirectSum.TensorProduct

noncomputable section

variable (R : Type*) [CommRing R]
variable (N : Type*) [AddCommGroup N] [Module R N]
variable (ι : Type*) [DecidableEq ι]
open DirectSum TensorProduct LinearMap

/-- If `N` is an `R`-module then `Rⁿ ⊗ N ≃ Nⁿ`. -/
@[simps! apply]
def TensorProduct.rid_DirectSum : (N ⊗[R] ⨁ _ : ι, R) ≃ₗ[R] (⨁ _ : ι, N) :=
  TensorProduct.directSumRight R N (fun _ : ι => R) ≪≫ₗ
    DFinsupp.mapRange.linearEquiv (fun _ : ι => TensorProduct.rid R N)

count_heartbeats in -- 37087
/-- Applying the linear equivalence `rid_DirectSum` to a simple element `x ⊗ r` of `N ⊗ Rⁿ`. -/
theorem TensorProduct.rid_DirectSum_tmul [DecidableEq R] (x : N) (r : ⨁ _ : ι, R) (i : ι) :
      rid_DirectSum R N ι (x ⊗ₜ[R] r) i = r i • x := by
  -- It suffices to show the equality holds when `r` is a Kronecker delta.
  -- To show this we recast as an equality of linear maps ...
  have h : r i • x = DFinsupp.mapRange.linearMap (fun _ => flip (lsmul R N) x) r i := by
    rw [DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange_apply, flip_apply, lsmul_apply]
  rw [h, ← mk_apply, ← LinearEquiv.coe_coe, ← LinearMap.comp_apply]
  congr 2
  -- ... and apply the default extensionality theorems (explicit here for clarity).
  refine DirectSum.linearMap_ext R fun i : ι => LinearMap.ext_ring ?_
  rewrite [LinearMap.comp_apply, LinearMap.comp_apply, LinearMap.comp_apply,
    LinearEquiv.coe_coe, rid_DirectSum_apply, mk_apply, directSumRight_tmul_lof]
  erw [DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange.linearMap_apply]
  rw [← single_eq_lof, ← single_eq_lof, DFinsupp.mapRange_single, DFinsupp.mapRange_single,
    LinearEquiv.coe_coe, rid_tmul, flip_apply, lsmul_apply]

count_heartbeats in -- 41817
/-- Applying the linear equivalence `rid_Finprod` to a simple element `r ⊗ x` of `Rⁿ ⊗ N`. -/
theorem TensorProduct.rid_DirectSum_tmul' [DecidableEq R] (r : ⨁ _ : ι, R) (x : N) (i : ι) :
      rid_DirectSum R N ι (x ⊗ₜ[R] r) i = r i • x := by
  -- Recast as an equality of linear maps in order to apply extensionality theorems.
  suffices h :
      ((rid_DirectSum R N ι : N ⊗[R] (⨁ _ : ι, R) →ₗ[R] ⨁ _, N) ∘ₗ (mk R N (⨁ _, R) x)) r =
        DFinsupp.mapRange.linearMap (fun _ => (lsmul R N).flip x) r from by
    rewrite [LinearMap.comp_apply, LinearEquiv.coe_coe, mk_apply] at h
    rw [h, DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange_apply, flip_apply, lsmul_apply]
  congr 1
  refine DirectSum.linearMap_ext R fun i : ι => LinearMap.ext_ring ?_
  -- We need only show the equality holds when `r` is a Kronecker delta.
  rewrite [LinearMap.comp_apply, LinearMap.comp_apply, LinearMap.comp_apply,
    LinearEquiv.coe_coe, rid_DirectSum_apply, mk_apply, directSumRight_tmul_lof]
  erw [DFinsupp.mapRange.linearEquiv_apply, DFinsupp.mapRange.linearMap_apply]
  rw [← single_eq_lof, ← single_eq_lof, DFinsupp.mapRange_single, DFinsupp.mapRange_single,
    rid_tmul, flip_apply, lsmul_apply]

count_heartbeats in -- 47069
/-- Applying the linear equivalence `rid_Finprod` to a simple element `r ⊗ x` of `Rⁿ ⊗ N`. -/
theorem TensorProduct.rid_DirectSum_tmul'' [DecidableEq R] (r : ⨁ _ : ι, R) (x : N) (i : ι) :
      rid_DirectSum R N ι (x ⊗ₜ[R] r) i = r i • x := by
  -- Recast as an equality of linear maps in order to apply extensionality theorems.
  suffices h :
      ((rid_DirectSum R N ι : N ⊗[R] (⨁ _ : ι, R) →ₗ[R] ⨁ _, N) ∘ₗ (mk R N (⨁ _, R) x)) =
        DFinsupp.mapRange.linearMap (fun _ => (lsmul R N).flip x) from by
    replace h := LinearMap.ext_iff.mp h r
    rewrite [LinearMap.comp_apply, LinearEquiv.coe_coe, mk_apply] at h
    unfold DirectSum at h ⊢
    rw [h, DFinsupp.mapRange.linearMap_apply, DFinsupp.mapRange_apply, flip_apply, lsmul_apply]
  refine DirectSum.linearMap_ext R fun i : ι => LinearMap.ext_ring ?_
  -- We need only show the equality holds when `r` is a Kronecker delta.
  rewrite [LinearMap.comp_apply, LinearMap.comp_apply, LinearMap.comp_apply,
    LinearEquiv.coe_coe, rid_DirectSum_apply, mk_apply, directSumRight_tmul_lof]
  erw [DFinsupp.mapRange.linearEquiv_apply, DFinsupp.mapRange.linearMap_apply]
  rw [← single_eq_lof, ← single_eq_lof, DFinsupp.mapRange_single, DFinsupp.mapRange_single,
    rid_tmul, flip_apply, lsmul_apply]

[Richard Copley]

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]

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