Setting up definitions

Stream: new members

[Jakob Scholbach]

I am working my way through the Mathematics in Lean tutorial, so I want to start beginning formalize some "real" notions, for example the condition that a module over a commutative ring is flat. Is there some tutorial or cheat sheet etc, how to even write down a definition? Is that supposed to be a theorem or a def? I am skimming through the mathlib files, but I don't yet see how the syntax would work out. Thanks!

[Kevin Buzzard]

The definition of flatness will be a def of type Prop.

[Kevin Buzzard]

definitions are hard to get right :-(

[Kevin Buzzard]

The big question is: which definition will you use?

[Jakob Scholbach]

My initial idea would be to say: for all injective maps of R-modules the tensor product with the module should still be injective.

[Jakob Scholbach]

As a test case: then show that all free modules are flat.

[Kevin Buzzard]

And which universes will everything be in?

[Kevin Buzzard]

This might all be in a branch of mathlib. @Johan Commelin ?

[Jakob Scholbach]

Being a beginner (for the moment I want to just play around and see a little bit of progress for myself) I would say the ring and the modules should be in the same universe.

[Jakob Scholbach]

Or is that problematic?

[Johan Commelin]

If it's just for fun to play around, that shouldn't be a problem

[Jakob Scholbach]

Where is a good place to read about the syntax of definitions in lean?

[Johan Commelin]

Of course $\mathbb Q_l$ is in universe Type 0, but etale cohomology of a scheme in Type 0 lives in Type 1, so with your definition those vector spaces wouldn't be flat... (assuming you define etale cohomology using the general topos theoretic machine)
But it's totally fine to ignore that issue for now.

[Johan Commelin]

@Jakob Scholbach Have you seen the video recordings of "Lean for the Curious Mathematician"?

[Johan Commelin]

https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N

[Johan Commelin]

The ones on "Structures and classes" and "Building a xyz hierarchy" are probably most relevant if you want to learn about making definitions

[Jakob Scholbach]

I noticed that they are there, watched the one about category theory, but nothing else; nor did I work through the exercises. I'll check these out, thanks!

[Johan Commelin]

def flat (R M : Type) [comm_ring R] [add_comm_group M] [module R M] :=
-- some predicate goes here

[Johan Commelin]

At some point I wrote some code about tensoring linear maps with a module. In other words, give $f \colon M_1 \to M_2$ and another module $M$, the induced map $M_1 \otimes M \to M_2 \otimes M$.
But I don't know if that code ended up in mathlib.

[Johan Commelin]

I think it's still waiting for attention by me or someone else: https://github.com/leanprover-community/mathlib/pull/4773

[Eric Wieser]

Is that docs#linear_map.prod_map?

[Eric Wieser]

Ah, tmul not prod

[Adam Topaz]

Here's one possible "definition" which doesn't have universe issues:

import ring_theory.ideal.basic
import linear_algebra.tensor_product

open_locale tensor_product

variables (A M : Type*) [comm_ring A] [add_comm_group M] [module A M]

def flat_aux (𝔞 : ideal A) : 𝔞 ⊗[A] M →ₗ[A] M := tensor_product.lift $
linear_map.mk₂ A (λ a m, ((a : A) • m))
(λ a b m, by simp [add_smul]) (λ a b m, by simp [← mul_smul, mul_comm])
(λ a m n, by simp) (λ a b m, by simp [← mul_smul, mul_comm])

def flat : Prop := ∀ (𝔞 : ideal A), function.injective $ flat_aux A M 𝔞

Of course, this is a bit backwards, since it's a theorem that this is equivalent to the "usual" definition of flatness :)

[Kevin Buzzard]

Of course it doesn't matter if things are defined in a nonstandard way as long as it's mathematically equivalent to the standard way. The question is whether one can build the standard API from the definition. This now is a much easier and more fun challenge because it only involves proving theorems

[Johan Commelin]

@Jakob Scholbach So there is a branch#flat-module of mathlib, in which I've tried to set up the basic theory for flatness.

[Johan Commelin]

I got stuck for two reasons:

1. mathlib doesn't have enough basic lemmas about tensor products in all the different variants. Tensor product of modules is there, but ideally we will have base change, associativity of base change, etc... There is currently no framework that makes polynomial A a (not the) tensor product of A and polynomial int. I think we should have such a framework in order for things to work smoothly.
2. As definition I chose the minimalist assertion: for every ideal $I$, the natural map $I \otimes M \to M$ is injective. Bootstrapping from this to the "usual" definition of preserving injectivity of arbitrary maps was painful. I tried to follow https://stacks.math.columbia.edu/tag/00HD but the proof became very awkard because Lean doesn't let you smoothly move between submodules and injective maps. Recently I didn't have time to work on this, but my gut feeling is that we should first prove a general "induction principle" for the category of $R$-modules, that will say something like "if you have suitable predicate P on modules, then you only need to check it on finitely generated modules", and maybe another version that will say "if you have an even more suitable predicate Q, then you only need to check it on ideals". Once we have those results, the proof of stacks-tag 00HD should be "straightforward".

[Thomas Browning]

From my experience, proving these general induction principles is very worthwhile, particularly if it allows you to black-box a Zorn's lemma argument

[Junyan Xu]

Flat modules arose in a recent thread and I read the docs and thought about the technical problems encountered. I try to come up with a nicer characterization of the tensor product, but I don't see how we could possibly replace the universal property by something as concrete as is_localization. However, I find that instead of quantifying over all R-modules in a universe, we only need to quantify over maximal ideals of the ring R, in order to characterize the tensor product up to isomorphism. (Naively, we'd like to apply the universal property to M ⊗[R] N to obtain the isomorphism, which lies in max u v if M and N lies in universes u and v. Even though R may lie in a universe higher than max u v, the characterization using maximal ideals doesn't involve universe levels explicitly, only indirectly through the types, like the adopted definition of flatness, though I don't immediately see what problems will arise if we use the definition that quantifies over max u v.)

The idea is as follows: for a binear map M × N → P to be a tensor product, the first (intrinsic, not universal) condition is that its image spans P. By the universal property for M ⊗ N we get a surjection M ⊗ N → P, which must kill some nonzero element x in M ⊗ N if it's not an isomorphism. Take a maximal element among submodules of M ⊗ N that doesn't contain x and call it Q. Then x is nonzero in (M ⊗ N)/Q and every nonzero submodule of (M ⊗ N)/Q contains x, so Rx is an essential submodule of (M ⊗ N)/Q, and it's also simple, hence isomorphic to R/m for some maximal ideal m in R, so (M ⊗ N)/Q embeds into the injective hull E(R/m). Therefore, if for every m, every bilinear M × N → E(R/m) factors through P, then M ⊗ N -> P kills no nonzero element and must be an isomorphism.

Regarding the examples in ring_theory.flat (polynomial A vs. A ⊗ polynomial R, fin n → R, R × R (vs. (ℤ × ℤ) ⊗ R?), ℤ[i] ⊗ ℝ (vs. ℂ)): since these are all base change of free modules, they can be handled by a general theorem that says if R,A,N form a scalar tower, then a R-bilinear map f : A × M → N such that m->f(1,m) sends a R-basis of M to a A-basis of N is a tensor product. (Such bilinear maps are also in bijection with (semi)linear maps M → N.)

[Kevin Buzzard]

It's crazy how localisation had such a nice characteristic predicate but tensoring has only what looks like far nastier ones